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:
|
1 2 3 4 5 6 7 |
import Mathlib.Tactic variable {m n k : ℕ} example (h : m ∣ n ∨ m ∣ k) : m ∣ n * k := by sorry |
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
|
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 81 82 83 84 85 86 87 88 89 90 91 92 93 94 |
import Mathlib.Tactic variable {m n k : ℕ} -- 1ª demostración -- =============== example (h : m ∣ n ∨ m ∣ k) : m ∣ n * k := by rcases h with h1 | h2 . -- h1 : m ∣ n rcases h1 with ⟨a, ha⟩ -- a : ℕ -- ha : n = m * a rw [ha] -- ⊢ m ∣ (m * a) * k rw [mul_assoc] -- ⊢ m ∣ m * (a * k) exact dvd_mul_right m (a * k) . -- h2 : m ∣ k rcases h2 with ⟨b, hb⟩ -- b : ℕ -- hb : k = m * b rw [hb] -- ⊢ m ∣ n * (m * b) rw [mul_comm] -- ⊢ m ∣ (m * b) * n rw [mul_assoc] -- ⊢ m ∣ m * (b * n) exact dvd_mul_right m (b * n) -- 2ª demostración -- =============== example (h : m ∣ n ∨ m ∣ k) : m ∣ n * k := by rcases h with h1 | h2 . -- h1 : m ∣ n rcases h1 with ⟨a, ha⟩ -- a : ℕ -- ha : n = m * a rw [ha, mul_assoc] -- ⊢ m ∣ m * (a * k) exact dvd_mul_right m (a * k) . -- h2 : m ∣ k rcases h2 with ⟨b, hb⟩ -- b : ℕ -- hb : k = m * b rw [hb, mul_comm, mul_assoc] -- ⊢ m ∣ m * (b * n) exact dvd_mul_right m (b * n) -- 3ª demostración -- =============== example (h : m ∣ n ∨ m ∣ k) : m ∣ n * k := by rcases h with ⟨a, rfl⟩ | ⟨b, rfl⟩ . -- a : ℕ -- ⊢ m ∣ (m * a) * k rw [mul_assoc] -- ⊢ m ∣ m * (a * k) exact dvd_mul_right m (a * k) . -- ⊢ m ∣ n * (m * b) rw [mul_comm, mul_assoc] -- ⊢ m ∣ m * (b * n) exact dvd_mul_right m (b * n) -- 4ª demostración -- =============== example (h : m ∣ n ∨ m ∣ k) : m ∣ n * k := by rcases h with h1 | h2 . -- h1 : m ∣ n exact dvd_mul_of_dvd_left h1 k . -- h2 : m ∣ k exact dvd_mul_of_dvd_right h2 n -- Lemas usados -- ============ -- #check (dvd_mul_of_dvd_left : m ∣ n → ∀ (c : ℕ), m ∣ n * c) -- #check (dvd_mul_of_dvd_right : m ∣ n → ∀ (c : ℕ), m ∣ c * n) -- #check (dvd_mul_right m n : m ∣ m * n) -- #check (mul_assoc m n k : m * n * k = m * (n * k)) -- #check (mul_comm m n : m * n = n * m) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 39.
Demostraciones con Isabelle/HOL
|
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 |
theory CS_de_divisibilidad_del_producto imports Main begin (* 1ª demostración *) lemma fixes n m k :: nat assumes "m dvd n ∨ m dvd k" shows "m dvd (n * k)" using assms proof assume "m dvd n" then obtain a where "n = m * a" by auto then have "n * k = m * (a * k)" by simp then show ?thesis by auto next assume "m dvd k" then obtain b where "k = m * b" by auto then have "n * k = m * (n * b)" by simp then show ?thesis by auto qed (* 2ª demostración *) lemma fixes n m k :: nat assumes "m dvd n ∨ m dvd k" shows "m dvd (n * k)" using assms by auto end |
