Si (m ∣ n ∧ m ≠ n), entonces (m ∣ n ∧ ¬(n ∣ m))
Demostrar con Lean4 que si (m ∣ n ∧ m ≠ n), entonces (m ∣ n ∧ ¬(n ∣ m)).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 |
import Mathlib.Data.Nat.GCD.Basic variable {m n : ℕ} example (h : m ∣ n ∧ m ≠ n) : m ∣ n ∧ ¬ n ∣ m := by sorry |
Demostración en lenguaje natural
La primera parte de la conclusión coincide con la primera de la hipótesis. Nos queda demostrar la segunda parte; es decir, que (¬(n | m)). Para ello, supongamos que (n | m). Entonces, por la propiedad antisimétrica de la divisibilidad y la primera parte de la hipótesis, se tiene que (m = n) en contradicción con la segunda parte de la hipótesis.
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 67 68 69 70 71 72 73 74 75 76 77 78 79 80 |
import Mathlib.Data.Nat.GCD.Basic variable {m n : ℕ} -- 1ª demostración -- =============== example (h : m ∣ n ∧ m ≠ n) : m ∣ n ∧ ¬ n ∣ m := by constructor . show m ∣ n exact h.left . show ¬n ∣ m { intro (h1 : n ∣ m) have h2 : m = n := dvd_antisymm h.left h1 show False exact h.right h2 } -- 2ª demostración -- =============== example (h : m ∣ n ∧ m ≠ n) : m ∣ n ∧ ¬ n ∣ m := by constructor . exact h.left . intro (h1 : n ∣ m) exact h.right (dvd_antisymm h.left h1) -- 3ª demostración -- =============== example (h : m ∣ n ∧ m ≠ n) : m ∣ n ∧ ¬ n ∣ m := ⟨h.left, fun h1 ↦ h.right (dvd_antisymm h.left h1)⟩ -- 4ª demostración -- =============== example (h : m ∣ n ∧ m ≠ n) : m ∣ n ∧ ¬ n ∣ m := by cases' h with h1 h2 -- h1 : m ∣ n -- h2 : m ≠ n constructor . -- ⊢ m ∣ n exact h1 . -- ⊢ ¬n ∣ m contrapose! h2 -- h2 : n ∣ m -- ⊢ m = n apply dvd_antisymm h1 h2 -- 5ª demostración -- =============== example (h : m ∣ n ∧ m ≠ n) : m ∣ n ∧ ¬ n ∣ m := by rcases h with ⟨h1 : m ∣ n, h2 : m ≠ n⟩ constructor . -- ⊢ m ∣ n exact h1 . -- ⊢ ¬n ∣ m contrapose! h2 -- h2 : n ∣ m -- ⊢ m = n apply dvd_antisymm h1 h2 -- Lemas usados -- ============ -- #check (dvd_antisymm : m ∣ n → n ∣ m → m = n) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 36.
