KIAS_Horizon

kias_horizon.lean

-- Use https://live.lean-lang.org/
import Mathlib

theorem imo_2001_p6
    (a b c d : Nat)
    (h0 : 0 < a ∧ 0 < b ∧ 0 < c ∧ 0 < d)
    (h1 : d < c)
    (h2 : c < b)
    (h3 : b < a)
    (h4 : a * c + b * d = (b + d + a - c) * (b + d - a + c)) :
    ¬ Nat.Prime (a * b + c * d) := by
  contrapose h4
  rw [mul_comm]
  simp [Nat.prime_def_lt, not_le_of_gt h0.1, not_forall, not_le_of_gt h3,
    Nat.mul_sub_right_distrib, Nat.add_comm]
  contrapose! h4
  contrapose! h4
  apply LT.lt.ne
  apply Nat.lt_sub_of_add_lt
  nlinarith
  
theorem infinitude_of_primes : {p : ℕ | p.Prime}.Infinite := by
  intro hfin
  obtain ⟨n, hn⟩ := hfin.bddAbove
  have hne : n.factorial + 1 ≠ 1 := by
    intro h; exact Nat.factorial_ne_zero n (by omega)
  obtain ⟨p, hp, hpdvd⟩ := Nat.exists_prime_and_dvd hne
  exact hp.not_dvd_one <| by
    have hpnfac : p ∣ n.factorial := (Nat.Prime.dvd_factorial hp).2 (hn hp)
    simpa using Nat.dvd_sub hpdvd hpnfac
    
theorem infinitude_of_primes' : {p : ℕ | p.Prime}.Infinite := by
  intro hfin
  have hne : hfin.toFinset.prod id + 1 ≠ 1 := by
    have : 0 < hfin.toFinset.prod id := Finset.prod_pos fun i hi =>
      (hfin.mem_toFinset.mp hi).pos
    omega
  obtain ⟨p, hp, hpdvd⟩ := Nat.exists_prime_and_dvd hne
  have hpS : p ∣ hfin.toFinset.prod id :=
    Finset.dvd_prod_of_mem id (hfin.mem_toFinset.mpr hp)
  exact hp.not_dvd_one (by simpa using Nat.dvd_sub hpdvd hpS)