Demostrar con Lean4 que la ra\u00edz cuadrada de 2 es irracional; es decir, que no existen \(m, n \u2208 \u2115\) tales que \(m\) y \(n\) son coprimos (es decir, que no tienen factores comunes distintos de uno) y \(m\u00b2 = 2n\u00b2\).<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\nimport Mathlib.Tactic\nimport Mathlib.Data.Nat.Prime\nimport Std.Data.Nat.Gcd\nopen Nat\nvariable {m n : \u2115}\n\nexample : \u00ac\u2203 m n, coprime m n \u2227 m ^ 2 = 2 * n ^ 2 :=\nby sorry\n<\/pre>\n<\/p>\n
1. Demostraci\u00f3n en lenguaje natural<\/h2>\n
Usaremos el lema del ejercicio anterior:
\n\[ (\u2200 n \u2208 \u2115)[2 \u2223 n\u00b2 \u2192 2 | n] \]<\/p>\n
Supongamos que existen existen \(m, n \u2208 \u2115\) tales que \(m\) y \(n\) son coprimos y \(m\u00b2 = 2n\u00b2\) y tenemos que demostrar una contradicci\u00f3n. Puesto que 2 divide a 1, para tener la contradicci\u00f3n basta demostrar que 2 divide a 1 y (ya que \(m\) y \(n\) son coprimos); para ello es suficiente demostrar que 2 divide al m\u00e1ximo com\u00fan divisor de \(m\) y \(n\). En definitiva, basta demostrar que 2 divide a \(m\) y a \(n\).<\/p>\n
La demostraci\u00f3n de que 2 divide a \(m\) es
\n\begin{align}
\n m\u00b2 = 2n\u00b2 &\u27f9 2 | m\u00b2 \\
\n &\u27f9 2 | m &&\text{[por el lema]}
\n\end{align}<\/p>\n
Para demostrar que 2 divide a \(n\), observamos que, puesto que 2 divide a \(m\), existe un \(k \u2208 \u2115\) tal que \(m = 2k\). Sustituyendo en
\n\[ m\u00b2 = 2n\u00b2 \]
\nse tiene
\n\[ (2k)\u00b2 = 2n\u00b2 \]
\nSimplificando, queda
\n\[ 2k = n\u00b2 \]
\nPor tanto, 2 divide a \(n\u00b2\) y, por el lema, 2 divide a \(n\).<\/p>\n
2. Demostraciones con Lean4<\/h2>\n\nimport Mathlib.Tactic\nimport Mathlib.Data.Nat.Prime\nimport Std.Data.Nat.Gcd\nopen Nat\nvariable {m n : \u2115}\n\nlemma par_si_cuadrado_par\n (h : 2 \u2223 n ^ 2)\n : 2 \u2223 n :=\nby\n rw [pow_two] at h\n -- h : 2 \u2223 n * n\n have h2 : 2 \u2223 n \u2228 2 \u2223 n := (Prime.dvd_mul prime_two).mp h\n tauto\n\nexample : \u00ac\u2203 m n, coprime m n \u2227 m ^ 2 = 2 * n ^ 2 :=\nby\n rintro \u27e8m, n, \u27e8h1, h2\u27e9\u27e9\n -- m n : \u2115\n -- h1 : coprime m n\n -- h2 : m ^ 2 = 2 * n ^ 2\n -- \u22a2 False\n have h3 : \u00ac(2 \u2223 1) := by norm_num\n have h4 : 2 \u2223 1 := by\n have h5 : Nat.gcd m n = 1 := h1\n rw [\u2190 h5]\n -- \u22a2 2 \u2223 Nat.gcd m n\n have h6 : 2 \u2223 m := by\n apply par_si_cuadrado_par\n -- \u22a2 2 \u2223 m ^ 2\n rw [h2]\n -- \u22a2 2 \u2223 2 * n ^ 2\n exact Nat.dvd_mul_right 2 (n ^ 2)\n have h7 : 2 \u2223 n := by\n have h8 : \u2203 k, m = 2 * k := h6\n rcases h8 with \u27e8k, h9\u27e9\n -- k : \u2115\n -- h9 : m = 2 * k\n have h10 : 2 * k ^ 2 = n ^ 2 := by\n have h10a : 2 * (2 * k ^ 2) = 2 * n ^ 2 := calc\n 2 * (2 * k ^ 2) = (2 * k) ^ 2 := by nlinarith\n _ = m ^ 2 := by rw [\u2190 h9]\n _ = 2 * n ^ 2 := h2\n show 2 * k ^ 2 = n ^ 2\n exact (mul_right_inj' (by norm_num : 2 \u2260 0)).mp h10a\n have h11 : 2 \u2223 n ^ 2 := by\n rw [\u2190 h10]\n -- \u22a2 2 \u2223 2 * k ^ 2\n exact Nat.dvd_mul_right 2 (k ^ 2)\n show 2 \u2223 n\n exact par_si_cuadrado_par h11\n show 2 \u2223 Nat.gcd m n\n exact Nat.dvd_gcd h6 h7\n show False\n exact h3 h4\n\n-- Lemas usados\n-- ============\n\n-- variable (p k : \u2115)\n-- #check (pow_two n : n ^ 2 = n * n)\n-- #check (Prime.dvd_mul : Nat.Prime p \u2192 (p \u2223 m * n \u2194 p \u2223 m \u2228 p \u2223 n))\n-- #check (prime_two : Nat.Prime 2)\n-- #check (Nat.dvd_gcd : k \u2223 m \u2192 k \u2223 n \u2192 k \u2223 Nat.gcd m n)\n-- #check (Nat.dvd_mul_right m n : m \u2223 m * n)\n-- #check (mul_right_inj' : k \u2260 0 \u2192 (k * m = k * n \u2194 m = n))\n<\/pre>\nDemostraciones interactivas<\/h3>\n