Título | Autor |
---|---|
(a+b)(a-b) = a^2-b^2 |
José A. Alonso |
Demostrar con Lean4 que si a y b son números reales, entonces
(a + b) * (a - b) = a^2 - b^2
Para ello, completar la siguiente teoría de Lean4:
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
[mathjax] 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
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.