not_exists_sq — Mathlib

English

There is no t with t^2 = n when m^2 < n < (m+1)^2.

Русский

Нет такого t, чтобы t^2 = n при m^2 < n < (m+1)^2.

LaTeX

$$$ instLTNat.lt (m^2) n \\Rightarrow instLTNat.lt n ((m+1)^2) \\Rightarrow \\neg ∃ t, t^2 = n $$$

Lean4

/-- There are no perfect squares strictly between m² and (m+1)² -/
theorem not_exists_sq (hl : m * m < n) (hr : n < (m + 1) * (m + 1)) : ¬∃ t, t * t = n :=
  by
  rintro ⟨t, rfl⟩
  have h1 : m < t := Nat.mul_self_lt_mul_self_iff.1 hl
  have h2 : t < m + 1 := Nat.mul_self_lt_mul_self_iff.1 hr
  grind

Похожие утверждения