theorem no_coprime_sol (p q : ℕ) (hcop : Nat.Coprime p q) (h : p ^ 2 = 2 * q ^ 2) : False := by have hp : 2 ∣ p := two_dvd_of_dvd_sq p ⟨q ^ 2, h⟩ obtain ⟨k, rfl⟩ := hp ha...

theorem n4_add_four_not_prime (n : ℕ) (hn : 2 ≤ n) : ¬ Nat.Prime (n ^ 4 + 4) := by obtain ⟨m, rfl⟩ : ∃ m, n = m + 1 := ⟨n - 1, by omega⟩ have hm : 1 ≤ m := b...

theorem dvd_norm {A B : Type*} [CommRing A] [CommRing B] [Algebra A B] [IsDomain A] [IsIntegrallyClosed A] [IsDomain B] [IsIntegrallyClosed B] [Module.Finite A B] [Module.IsTorsionFree A B] (b : B) (hb : b ≠ 0) : ∃ a : A, a ≠ 0 ∧ b ∣ algebraMap A B a := ⟨Algebra.intNorm A B b, Algebra.intNorm_ne_zero.mpr hb, Algebra.dvd_algebraMa...

theorem infinitude_of_primes (n : ℕ) : ∃ p, n < p ∧ Nat.Prime p := by obtain ⟨p, hp, hpN⟩ := prime_factor_exists (Nat.factorial n + 1) (by have ...

theorem brocard_factor (n m : ℕ) (h : Nat.factorial n + 1 = (m + 1) ^ 2) : m * (m + 2) = Nat.factorial n := by have e : (m + 1) ^ 2 = m * (m + 2) + 1 := by ring omega

theorem brocard_7 : Nat.factorial 7 + 1 = 71 ^ 2 := by decide

theorem brocard_5 : Nat.factorial 5 + 1 = 11 ^ 2 := by decide

theorem brocard_4 : Nat.factorial 4 + 1 = 5 ^ 2 := by decide

theorem factorial_sum (n : ℕ) : (∑ k ∈ Finset.range (n + 1), k * Nat.factorial k) + 1 = Nat.factorial (n + 1) := by induction n with | zero => simp | succ m ih => rw [Finset.sum_range_succ] ...

theorem two_mul_le_sq_add_sq : ∀ a b : ℝ, 2 * (a * b) ≤ a ^ 2 + b ^ 2 := by intro a b; have h := sq_nonneg_real (a - b); rw [expand_sub_sq] at h; lina...