sq_eq_one_of_sq_lt_four

Mathlib.Data.Int.Order.Units

URI: https://scilib.ai/kg/mathlib#Int.sq_eq_one_of_sq_lt_four

← MathLib Explorer

English

If x^2 < 4 and x ≠ 0 in ℤ, then x^2 = 1.

Русский

Если x^2 < 4 и x ≠ 0 в ℤ, то x^2 = 1.

LaTeX

$$$\forall x \in \mathbb{Z}, x^{2} < 4 \to (x \neq 0 \to x^{2} = 1).$$$

Lean4

theorem sq_eq_one_of_sq_lt_four {x : ℤ} (h1 : x ^ 2 < 4) (h2 : x ≠ 0) : x ^ 2 = 1 :=
  sq_eq_one_iff.mpr
    ((abs_eq (zero_le_one' ℤ)).mp
      (le_antisymm (lt_add_one_iff.mp (abs_lt_of_sq_lt_sq h1 zero_le_two)) (sub_one_lt_iff.mp (abs_pos.mpr h2))))

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru