(a+b)(a-b) = a²-b²
Demostrar con Lean4 que si a y b son números reales, entonces
|
1 |
(a + b) * (a - b) = a^2 - b^2 |
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable (a b : ℝ) example : (a + b) * (a - b) = a^2 - b^2 := sorry |
Demostración en lenguaje natural
Por la siguiente cadena de igualdades:
\begin{align}
(a + b)(a – b)
&= a(a – b) + b(a – b) &&\text{[por la distributiva]} \\
&= (aa – ab) + b(a – b) &&\text{[por la distributiva]} \\
&= (a^2 – ab) + b(a – b) &&\text{[por def. de cuadrado]} \\
&= (a^2 – ab) + (ba – bb) &&\text{[por la distributiva]} \\
&= (a^2 – ab) + (ba – b^2) &&\text{[por def. de cuadrado]} \\
&= (a^2 + -(ab)) + (ba – b^2) &&\text{[por def. de resta]} \\
&= a^2 + (-(ab) + (ba – b^2)) &&\text{[por la asociativa]} \\
&= a^2 + (-(ab) + (ba + -b^2)) &&\text{[por def. de resta]} \\
&= a^2 + ((-(ab) + ba) + -b^2) &&\text{[por la asociativa]} \\
&= a^2 + ((-(ab) + ab) + -b^2) &&\text{[por la conmutativa]} \\
&= a^2 + (0 + -b^2) &&\text{[por def. de opuesto]} \\
&= (a^2 + 0) + -b^2 &&\text{[por asociativa]} \\
&= a^2 + -b^2 &&\text{[por def. de cero]} \\
&= a^2 – b^2 &&\text{[por def. de resta]}
\end{align}
Demostraciones con Lean
|
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 |
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable (a b : ℝ) -- 1ª demostración -- =============== example : (a + b) * (a - b) = a^2 - b^2 := calc (a + b) * (a - b) = a * (a - b) + b * (a - b) := by rw [add_mul] _ = (a * a - a * b) + b * (a - b) := by rw [mul_sub] _ = (a^2 - a * b) + b * (a - b) := by rw [← pow_two] _ = (a^2 - a * b) + (b * a - b * b) := by rw [mul_sub] _ = (a^2 - a * b) + (b * a - b^2) := by rw [← pow_two] _ = (a^2 + -(a * b)) + (b * a - b^2) := by ring _ = a^2 + (-(a * b) + (b * a - b^2)) := by rw [add_assoc] _ = a^2 + (-(a * b) + (b * a + -b^2)) := by ring _ = a^2 + ((-(a * b) + b * a) + -b^2) := by rw [← add_assoc (-(a * b)) (b * a) (-b^2)] _ = a^2 + ((-(a * b) + a * b) + -b^2) := by rw [mul_comm] _ = a^2 + (0 + -b^2) := by rw [neg_add_self (a * b)] _ = (a^2 + 0) + -b^2 := by rw [← add_assoc] _ = a^2 + -b^2 := by rw [add_zero] _ = a^2 - b^2 := by linarith -- 2ª demostración -- =============== example : (a + b) * (a - b) = a^2 - b^2 := calc (a + b) * (a - b) = a * (a - b) + b * (a - b) := by ring _ = (a * a - a * b) + b * (a - b) := by ring _ = (a^2 - a * b) + b * (a - b) := by ring _ = (a^2 - a * b) + (b * a - b * b) := by ring _ = (a^2 - a * b) + (b * a - b^2) := by ring _ = (a^2 + -(a * b)) + (b * a - b^2) := by ring _ = a^2 + (-(a * b) + (b * a - b^2)) := by ring _ = a^2 + (-(a * b) + (b * a + -b^2)) := by ring _ = a^2 + ((-(a * b) + b * a) + -b^2) := by ring _ = a^2 + ((-(a * b) + a * b) + -b^2) := by ring _ = a^2 + (0 + -b^2) := by ring _ = (a^2 + 0) + -b^2 := by ring _ = a^2 + -b^2 := by ring _ = a^2 - b^2 := by ring -- 3ª demostración -- =============== example : (a + b) * (a - b) = a^2 - b^2 := by ring -- 4ª demostración (por reescritura usando el lema anterior) -- ========================================================= -- El lema anterior es lemma aux : (a + b) * (c + d) = a * c + a * d + b * c + b * d := by ring -- La demostración es example : (a + b) * (a - b) = a^2 - b^2 := by rw [sub_eq_add_neg] rw [aux] rw [mul_neg] rw [add_assoc (a * a)] rw [mul_comm b a] rw [neg_add_self] rw [add_zero] rw [← pow_two] rw [mul_neg] rw [← pow_two] rw [← sub_eq_add_neg] |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 8.
