(a+b)(a-b) = a²-b²

Demostrar con Lean4 que si a y b son números reales, entonces

Para ello, completar la siguiente teoría de Lean4:

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

Demostraciones interactivas

Se puede interactuar con las demostraciones anteriores en Lean 4 Web.

Referencias

Escribe un comentario