(a + b) (c + d) = ac + ad + bc + bd
Demostrar con Lean4 que si a, b, c y d son números reales, entonces
|
1 |
(a + b) * (c + d) = a * c + a * d + b * c + b * d |
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 |
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable (a b c d : ℝ) example : (a + b) * (c + d) = a * c + a * d + b * c + b * d := sorry |
Demostración en lenguaje natural
Por la siguiente cadena de igualdades
\begin{align}
(a + b)(c + d)
&= a(c + d) + b(c + d) &&\text{[por la distributiva]} \\
&= ac + ad + b(c + d) &&\text{[por la distributiva]} \\
&= ac + ad + (bc + bd) &&\text{[por la distributiva]} \\
&= ac + ad + bc + bd &&\text{[por la asociativa]}
\end{align}
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 |
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable (a b c d : ℝ) -- 1ª demostración example : (a + b) * (c + d) = a * c + a * d + b * c + b * d := calc (a + b) * (c + d) = a * (c + d) + b * (c + d) := by rw [add_mul] _ = a * c + a * d + b * (c + d) := by rw [mul_add] _ = a * c + a * d + (b * c + b * d) := by rw [mul_add] _ = a * c + a * d + b * c + b * d := by rw [←add_assoc] -- 2ª demostración example : (a + b) * (c + d) = a * c + a * d + b * c + b * d := calc (a + b) * (c + d) = a * (c + d) + b * (c + d) := by ring _ = a * c + a * d + b * (c + d) := by ring _ = a * c + a * d + (b * c + b * d) := by ring _ = a * c + a * d + b * c + b * d := by ring -- 3ª demostración example : (a + b) * (c + d) = a * c + a * d + b * c + b * d := by ring -- 4ª demostración example : (a + b) * (c + d) = a * c + a * d + b * c + b * d := by rw [add_mul] rw [mul_add] rw [mul_add] rw [← add_assoc] -- 5ª demostración example : (a + b) * (c + d) = a * c + a * d + b * c + b * d := by rw [add_mul, mul_add, mul_add, ←add_assoc] |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 8.
