Transitividad de la divisibilidad
Demostrar con Lean4 la transitividad de la divisibilidad.
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 (divab : a ∣ b) (divbc : b ∣ c) : a ∣ c := by sorry |
Demostración en lenguaje natural
Supongamos que \(a | b\) y \(b | c\). Entonces, existen \(d\) y \(e\) tales que
\begin{align}
b &= ad \tag{1} \\
c &= be \tag{2}
\end{align}
Por tanto,
\begin{align}
c &= be &&\text{[por (2)]} \\
&= (ad)e &&\text{[por (1)]} \\
&= a(de)
\end{align}
Por consiguiente, \(a | 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 |
import Mathlib.Tactic variable {a b c : ℕ} -- 1ª demostración example (divab : a ∣ b) (divbc : b ∣ c) : a ∣ c := by rcases divab with ⟨d, beq : b = a * d⟩ rcases divbc with ⟨e, ceq : c = b * e⟩ have h1 : c = a * (d * e) := calc c = b * e := ceq _ = (a * d) * e := congrArg (. * e) beq _ = a * (d * e) := mul_assoc a d e show a ∣ c exact Dvd.intro (d * e) h1.symm -- 2ª demostración example (divab : a ∣ b) (divbc : b ∣ c) : a ∣ c := by rcases divab with ⟨d, beq : b = a * d⟩ rcases divbc with ⟨e, ceq : c = b * e⟩ use (d * e) -- ⊢ c = a * (d * e) rw [ceq, beq] -- ⊢ (a * d) * e = a * (d * e) exact mul_assoc a d e -- 3ª demostración example (divab : a ∣ b) (divbc : b ∣ c) : a ∣ c := by rcases divbc with ⟨e, rfl⟩ -- ⊢ a ∣ b * e rcases divab with ⟨d, rfl⟩ -- ⊢ a ∣ a * d * e use (d * e) -- ⊢ a * d * e = a * (d * e) ring -- 4ª demostración example (divab : a ∣ b) (divbc : b ∣ c) : a ∣ c := by cases' divab with d beq -- d : ℕ -- beq : b = a * d cases' divbc with e ceq -- e : ℕ -- ceq : c = b * e rw [ceq, beq] -- ⊢ a ∣ a * d * e use (d * e) -- ⊢ (a * d) * e = a * (d * e) exact mul_assoc a d e -- 5ª demostración example (divab : a ∣ b) (divbc : b ∣ c) : a ∣ c := by exact dvd_trans divab divbc -- Lemas usados -- ============ -- #check (mul_assoc a b c : (a * b) * c = a * (b * c)) -- #check (Dvd.intro c : a * c = b → a ∣ b) -- #check (dvd_trans : a ∣ b → b ∣ c → 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.
