Si (∃ x, y ∈ ℝ)[z = x² + y² ∨ z = x² + y² + 1], entonces z ≥ 0

Demostrar con Lean4 que si \((∃ x, y ∈ ℝ)[z = x² + y² ∨ z = x² + y² + 1]\), entonces \(z ≥ 0\).

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

Demostración en lenguaje natural

Usaremos los siguientes lemas
\begin{align}
&(∀ x ∈ ℝ)[x² ≥ 0] \tag{L1} \\
&(∀ x, y ∈ ℝ)[x ≥ 0 → y ≥ 0 → x + y ≥ 0] \tag{L2} \\
&1 ≥ 0 \tag{L3}
\end{align}

Sean \(a\) y \(b\) tales que
\[ z = a² + b² ∨ z = a² + b² + 1 \]
Entonces, por L1, se tiene que
\begin{align}
&a² ≥ 0 \tag{1} \\
&b² ≥ 0 \tag{2}
\end{align}

En el primer caso, \(z = a² + b²\) y se tiene que \(z ≥ 0\) por el lema L2 aplicado a (1) y (2).

En el segundo caso, \(z = a² + b² + 1\) y se tiene que \(z ≥ 0\) por el lema L2 aplicado a (1), (2) y L3.

Demostraciones con Lean4

Demostraciones interactivas

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

Referencias

Demostraciones con Isabelle/HOL

Escribe un comentario