Source indexedlemma · leanprover/lean4:v4.32.0

Erdos392.pairProd_bound

PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:3106 to 3122

Source documentation

If all elements of l are at most n, then all elements of pairProd l are at most n².

Exact Lean statement

lemma pairProd_bound (l : List ℕ) (n : ℕ) (hl : ∀ x ∈ l, x ≤ n) :
    ∀ x ∈ pairProd l, x ≤ n ^ 2

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma pairProd_bound (l : List ℕ) (n : ℕ) (hl : ∀ x ∈ l, x ≤ n) :    ∀ x ∈ pairProd l, x ≤ n ^ 2 := by  induction l using pairProd.induct with  | case1 => simp [pairProd]  | case2 a =>    simp only [pairProd, List.mem_singleton, forall_eq]    calc a ≤ n := hl a (List.mem_singleton_self a)      _ ≤ n ^ 2 := le_self_pow (by omega) n  | case3 a b rest ih =>    intro x hx    rw [pairProd, List.mem_cons] at hx    rcases hx with rfl | hx    · have ha := hl a <| by simp      have hb := hl b <| by simp      calc a * b ≤ n * n := by gcongr        _ = n ^ 2 := (sq n).symm    · exact ih (fun x hx' ↦ hl x <| by grind) x hx