Si n² es par, entonces n es par
Demostrar con Lean4 que si \(n²\) es par, entonces \(n\) es par.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 |
import Mathlib.Tactic open Nat variable (n : ℕ) example (h : 2 ∣ n ^ 2) : 2 ∣ n := by sorry |
1. Demostración en lenguaje natural
Se usará el siguiente lema: Si \(p\) es primo, entonces
\[ (∀ a, b ∈ ℕ)[p ∣ ab ↔ p ∣ a ∨ p ∣ b] \]
Si \(n²\) es par, entonces \(2\) divide a \(n.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 |
import Mathlib.Tactic open Nat variable (n : ℕ) -- 1ª demostración -- =============== example (h : 2 ∣ n ^ 2) : 2 ∣ n := by rw [pow_two] at h -- h : 2 ∣ n * n have h1 : Nat.Prime 2 := prime_two have h2 : 2 ∣ n ∨ 2 ∣ n := (Prime.dvd_mul h1).mp h rcases h2 with h3 | h4 · -- h3 : 2 ∣ n exact h3 · -- h4 : 2 ∣ n exact h4 done -- 2ª demostración -- =============== example (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 rcases h2 with h3 | h4 · exact h3 · exact h4 done -- 3ª demostración -- =============== example (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 done -- Lemas usados -- ============ -- variable (p a b : ℕ) -- #check (prime_two : Nat.Prime 2) -- #check (Prime.dvd_mul : Nat.Prime p → (p ∣ a * b ↔ p ∣ a ∨ p ∣ b)) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
