Si a divide a b y a c, entonces divide a b+c
Demostrar con Lean4 que si \(a\) divide a \(b\) y a \(c\), entonces divide a \(b+c\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 |
import Mathlib.Tactic variable {a b c : ℕ} example (h1 : a ∣ b) (h2 : a ∣ c) : a ∣ (b + c) := by sorry |
Demostración en lenguaje natural
Puesto que \(a\) divide a \(b\) y a \(c\), existen \(d\) y \(e\) tales que
\begin{align}
b &= ad \tag{1} \\
c &= ae \tag{2}
\end{align}
Por tanto,
\begin{align}
b + c &= ad + c &&\text{[por (1)]} \\
&= ad + ae &&\text{[por (2)]} \\
&= a(d + e) &&\text{[por la distributiva]}
\end{align}
Por consiguiente, \(a\) divide a \(b + c\).
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 |
import Mathlib.Tactic variable {a b c : ℕ} -- 1ª demostración example (h1 : a ∣ b) (h2 : a ∣ c) : a ∣ (b + c) := by rcases h1 with ⟨d, beq : b = a * d⟩ rcases h2 with ⟨e, ceq: c = a * e⟩ have h1 : b + c = a * (d + e) := calc b + c = (a * d) + c := congrArg (. + c) beq _ = (a * d) + (a * e) := congrArg ((a * d) + .) ceq _ = a * (d + e) := by rw [← mul_add] show a ∣ (b + c) exact Dvd.intro (d + e) h1.symm -- 2ª demostración example (h1 : a ∣ b) (h2 : a ∣ c) : a ∣ (b + c) := by rcases h1 with ⟨d, beq : b = a * d⟩ rcases h2 with ⟨e, ceq: c = a * e⟩ have h1 : b + c = a * (d + e) := by linarith show a ∣ (b + c) exact Dvd.intro (d + e) h1.symm -- 3ª demostración example (h1 : a ∣ b) (h2 : a ∣ c) : a ∣ (b + c) := by rcases h1 with ⟨d, beq : b = a * d⟩ rcases h2 with ⟨e, ceq: c = a * e⟩ show a ∣ (b + c) exact Dvd.intro (d + e) (by linarith) -- 4ª demostración example (h1 : a ∣ b) (h2 : a ∣ c) : a ∣ (b + c) := by cases' h1 with d beq -- d : ℕ -- beq : b = a * d cases' h2 with e ceq -- e : ℕ -- ceq : c = a * e rw [ceq, beq] -- ⊢ a ∣ a * d + a * e use (d + e) -- ⊢ a * d + a * e = a * (d + e) ring -- 5ª demostración example (h1 : a ∣ b) (h2 : a ∣ c) : a ∣ (b + c) := by rcases h1 with ⟨d, rfl⟩ -- ⊢ a ∣ a * d + c rcases h2 with ⟨e, rfl⟩ -- ⊢ a ∣ a * d + a * e use (d + e) -- ⊢ a * d + a * e = a * (d + e) ring -- 6ª demostración example (h1 : a ∣ b) (h2 : a ∣ c) : a ∣ (b + c) := dvd_add h1 h2 -- Lemas usados -- ============ -- #check (Dvd.intro c : a * c = b → a ∣ b) -- #check (dvd_add : a ∣ b → a ∣ c → a ∣ (b + c)) -- #check (mul_add a b c : a * (b + c) = a * b + a * c) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 30.
