En ℝ, si x² = 1 entonces x = 1 ó x = -1

Demostrar con Lean4 que en \(ℝ\), si \(x² = 1\) entonces \(x = 1\) ó \(x = -1\).

Para ello, completar la siguiente teoría de Lean4:

Demostración en lenguaje natural

Usaremos los siguientes lemas
\begin{align}
&(∀ x ∈ ℝ)[x – x = 0] \tag{L1} \\
&(∀ x, y ∈ ℝ)[xy = 0 → x = 0 ∨ y = 0] \tag{L2} \\
&(∀ x, y ∈ ℝ)[x – y = 0 ↔ x = y] \tag{L3} \\
&(∀ x, y ∈ ℝ)[x + y = 0 → x = -y] \tag{L4}
\end{align}

Se tiene que
\begin{align}
(x – 1)(x + 1) &= x² – 1 \\
&= 1 – 1 &&\text{[por la hipótesis]} \\
&= 0 &&\text{[por L1]}
\end{align}
y, por el lema L2, se tiene que
\[ x – 1 = 0 ∨ x + 1 = 0 \]
Acabaremos la demostración por casos.

Primer caso:
\begin{align}
x – 1 = 0 &⟹ x = 1 &&\text{[por L3]} \\
&⟹ x = 1 ∨ x = -1
\end{align}

Segundo caso:
\begin{align}
x + 1 = 0 &⟹ x = -1 &&\text{[por L4]} \\
&⟹ x = 1 ∨ x = -1
\end{align}

Demostraciones con Lean4

Demostraciones interactivas

Se puede interactuar con las demostraciones anteriores en Lean 4 Web.

Referencias

Demostraciones con Isabelle/HOL

Escribe un comentario