La raíz cuadrada de 2 es irracional
Demostrar con Lean4 que la raíz cuadrada de 2 es irracional; es decir, que no existen \(m, n ∈ ℕ\) tales que \(m\) y \(n\) son coprimos (es decir, que no tienen factores comunes distintos de uno) y \(m² = 2n²\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 |
import Mathlib.Tactic import Mathlib.Data.Nat.Prime import Std.Data.Nat.Gcd open Nat variable {m n : ℕ} example : ¬∃ m n, coprime m n ∧ m ^ 2 = 2 * n ^ 2 := by sorry |
1. Demostración en lenguaje natural
Usaremos el lema del ejercicio anterior:
\[ (∀ n ∈ ℕ)[2 ∣ n² → 2 | n] \]
Supongamos que existen existen \(m, n ∈ ℕ\) tales que \(m\) y \(n\) son coprimos y \(m² = 2n²\) y tenemos que demostrar una contradicción. Puesto que 2 divide a 1, para tener la contradicción 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áximo común divisor de \(m\) y \(n\). En definitiva, basta demostrar que 2 divide a \(m\) y a \(n\).
La demostración de que 2 divide a \(m\) es
\begin{align}
m² = 2n² &⟹ 2 | m² \\
&⟹ 2 | m &&\text{[por el lema]}
\end{align}
Para demostrar que 2 divide a \(n\), observamos que, puesto que 2 divide a \(m\), existe un \(k ∈ ℕ\) tal que \(m = 2k\). Sustituyendo en
\[ m² = 2n² \]
se tiene
\[ (2k)² = 2n² \]
Simplificando, queda
\[ 2k = n² \]
Por tanto, 2 divide a \(n²\) y, por el lema, 2 divide a \(n\).
2. Demostraciones con Lean4
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 |
import Mathlib.Tactic import Mathlib.Data.Nat.Prime import Std.Data.Nat.Gcd open Nat variable {m n : ℕ} lemma par_si_cuadrado_par (h : 2 ∣ n ^ 2) : 2 ∣ n := by rw [pow_two] at h -- h : 2 ∣ n * n have h2 : 2 ∣ n ∨ 2 ∣ n := (Prime.dvd_mul prime_two).mp h tauto example : ¬∃ m n, coprime m n ∧ m ^ 2 = 2 * n ^ 2 := by rintro ⟨m, n, ⟨h1, h2⟩⟩ -- m n : ℕ -- h1 : coprime m n -- h2 : m ^ 2 = 2 * n ^ 2 -- ⊢ False have h3 : ¬(2 ∣ 1) := by norm_num have h4 : 2 ∣ 1 := by have h5 : Nat.gcd m n = 1 := h1 rw [← h5] -- ⊢ 2 ∣ Nat.gcd m n have h6 : 2 ∣ m := by apply par_si_cuadrado_par -- ⊢ 2 ∣ m ^ 2 rw [h2] -- ⊢ 2 ∣ 2 * n ^ 2 exact Nat.dvd_mul_right 2 (n ^ 2) have h7 : 2 ∣ n := by have h8 : ∃ k, m = 2 * k := h6 rcases h8 with ⟨k, h9⟩ -- k : ℕ -- h9 : m = 2 * k have h10 : 2 * k ^ 2 = n ^ 2 := by have h10a : 2 * (2 * k ^ 2) = 2 * n ^ 2 := calc 2 * (2 * k ^ 2) = (2 * k) ^ 2 := by nlinarith _ = m ^ 2 := by rw [← h9] _ = 2 * n ^ 2 := h2 show 2 * k ^ 2 = n ^ 2 exact (mul_right_inj' (by norm_num : 2 ≠ 0)).mp h10a have h11 : 2 ∣ n ^ 2 := by rw [← h10] -- ⊢ 2 ∣ 2 * k ^ 2 exact Nat.dvd_mul_right 2 (k ^ 2) show 2 ∣ n exact par_si_cuadrado_par h11 show 2 ∣ Nat.gcd m n exact Nat.dvd_gcd h6 h7 show False exact h3 h4 -- Lemas usados -- ============ -- variable (p k : ℕ) -- #check (pow_two n : n ^ 2 = n * n) -- #check (Prime.dvd_mul : Nat.Prime p → (p ∣ m * n ↔ p ∣ m ∨ p ∣ n)) -- #check (prime_two : Nat.Prime 2) -- #check (Nat.dvd_gcd : k ∣ m → k ∣ n → k ∣ Nat.gcd m n) -- #check (Nat.dvd_mul_right m n : m ∣ m * n) -- #check (mul_right_inj' : k ≠ 0 → (k * m = k * n ↔ m = n)) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
