integerComplement_pow_two_ne_pow_two

English

For any x in the Gaussian-integer set ℂ_ℤ and any integer n, x^2 ≠ n^2.

Русский

Для любого x ∈ ℂ_ℤ и любого целого n верно, что x^2 ≠ n^2.

LaTeX

$$$\forall x \in \mathbb{C}_{\mathbb{Z}}, \forall n \in \mathbb{Z}, x^2 \neq n^2$$$

Lean4

theorem integerComplement_pow_two_ne_pow_two {x : ℂ} (hx : x ∈ ℂ_ℤ) (n : ℤ) : x ^ 2 ≠ n ^ 2 :=
  by
  have := not_exists.mp hx n
  have := not_exists.mp hx (-n)
  simp_all [sq_eq_sq_iff_eq_or_eq_neg, eq_comm]

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