La semana en Calculemus (20 de enero de 2024)

Esta semana he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades:

A continuación se muestran las soluciones.

1. En ℝ, |x + y| ≤ |x| + |y|

Demostrar con Lean4 que en \(ℝ\),
\[ |x + y| ≤ |x| + |y|\]

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

Demostración en lenguaje natural

Se usarán los siguientes lemas
\begin{align}
&(∀ x ∈ ℝ)[0 ≤ x → |x| = x) \tag{L1} \\
&(∀ a, b, c, d ∈ ℝ)[a ≤ b ∧ c ≤ d → a + c ≤ b + d] \tag{L2} \\
&(∀ x ∈ ℝ)[x ≤ |x|] \tag{L3} \\
&(∀ x ∈ ℝ)[x < 0 → |x| = -x] \tag{L4} \\
&(∀ x, y ∈ ℝ)[-(x + y) = -x + -y] \tag{L5} \\
&(∀ x ∈ ℝ)[-x ≤ |x|] \tag{L6}
\end{align}

Se demostrará por casos según \(x + y ≥ 0\):

Primer caso: Supongamos que \(x + y ≥ 0\). Entonces,
\begin{align}
|x + y| &= x + y &&\text{[por L1]} \\
&≤ |x| + |y| &&\text{[por L2 y L3]}
\end{align}

Segundo caso: Supongamos que \(x + y < 0\). Entonces,
\begin{align}
|x + y| &= -(x + y) &&\text{[por L4]} \\
&= -x + -y &&\text{[por L5]} \\
&≤ |x| + |y| &&\text{[por L2 y L6]}
\end{align}

Demostraciones con Lean4

Demostraciones interactivas

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

Referencias

2. En ℝ, si x ≠ 0 entonces x < 0 ó x > 0

Demostrar con Lean4 que en ℝ, si \(x ≠ 0\) entonces \(x < 0\) ó \(x > 0\).

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

Demostración en lenguaje natural

Usando el siguiente lema
\[ (∀ x y ∈ ℝ)[x < y ∨ x = y ∨ y < x] \]
se demuestra distinguiendo tres casos.

Caso 1: Supongamos que \(x < 0\). Entonces, se verifica la disyunción ya
que se verifica su primera parte.

Caso 2: Supongamos que \(x = 0\). Entonces, se tiene una contradicción
con la hipótesis.

Caso 3: Supongamos que \(x > 0\). Entonces, se verifica la disyunción ya
que se verifica su segunda parte.

Demostraciones con Lean4

Demostraciones interactivas

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

Referencias

3. Si m divide a n o a k, entonces m divide a nk

Demostrar con Lean4 que si \(m\) divide a \(n\) o a \(k\), entonces \(m\) divide a \(nk\).

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

Demostración en lenguaje natural

Se demuestra por casos.

Caso 1: Supongamos que \(m ∣ n\). Entonces, existe un \(a ∈ ℕ\) tal que
\[ n = ma \]
Por tanto,
\begin{align}
nk &= (ma)k \\
&= m(ak)
\end{align}
que es divisible por \(m\).

Caso 2: Supongamos que \(m ∣ k). Entonces, existe un \(b ∈ ℕ\) tal que
\[ k = mb \]
Por tanto,
\begin{align}
nk &= n(mb) \\
&= m(nb)
\end{align}
que es divisible por \(m\).

Demostraciones con Lean4

Demostraciones interactivas

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

Referencias

Demostraciones con Isabelle/HOL

4. 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

5. 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