Source indexedtheorem · leanprover/lean4:v4.32.0

Lcm.Criterion.r_ge

PrimeNumberTheoremAnd.IEANTN.Lcm · PrimeNumberTheoremAnd/IEANTN/Lcm.lean:405 to 421

Mathematical statement

Exact Lean statement

@[blueprint
  "div-remainder"
  (statement := /--
   There exist integers \(m \ge 0\) and \(r\) satisfying \(0 < r < 4 p_1 p_2 p_3\) and
   \[q_1 q_2 q_3 = 4 p_1 p_2 p_3 m + r \]
  -/)
  (proof := /-- This is division with remainder. -/)
  (latexEnv := "lemma")]
theorem Criterion.r_ge (c : Criterion) : 0 < c.r

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint  "div-remainder"  (statement := /--   There exist integers \(m \ge 0\) and \(r\) satisfying \(0 < r < 4 p_1 p_2 p_3\) and   \[q_1 q_2 q_3 = 4 p_1 p_2 p_3 m + r \]  -/)  (proof := /-- This is division with remainder. -/)  (latexEnv := "lemma")]theorem Criterion.r_ge (c : Criterion) : 0 < c.r := by  simp only [r, Nat.pos_iff_ne_zero, ne_eq]  intro h  have h_dvd : c.p 2 ∣ ∏ i, c.q i :=    (Finset.dvd_prod_of_mem _ (Finset.mem_univ 2)).trans <|      (Nat.dvd_mul_left _ 4).trans (Nat.dvd_of_mod_eq_zero h)  obtain ⟨i, _, hi⟩ := (c.hp 2).prime.exists_mem_finset_dvd h_dvd  have : c.p 2 = c.q i := ((c.hq i).dvd_iff_eq (c.hp 2).ne_one).mp hi |>.symm  exact absurd this (c.h_ord_2.trans_le (c.hq_mono.monotone (zero_le i))).ne