(a+b)(a+b)_eq_aa+2ab+bb.md

Título	Autor
(a + b)(a + b) = aa + 2ab + bb	José A. Alonso

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

   (a + b) * (a + b) = a * a + 2 * (a * b) + b * b

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

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

variable (a b c : ℝ)

example :
  (a + b) * (a + b) = a * a + 2 * (a * b) + b * b :=
sorry

Demostración en lenguaje natural

[mathjax] Por la siguiente cadena de igualdades \begin{align} (a + b)(a + b) &= (a + b)a + (a + b)b &&\text{[por la distributiva]} \ &= aa + ba + (a + b)b &&\text{[por la distributiva]} \ &= aa + ba + (ab + bb) &&\text{[por la distributiva]} \ &= aa + ba + ab + bb &&\text{[por la asociativa]} \ &= aa + (ba + ab) + bb &&\text{[por la asociativa]} \ &= aa + (ab + ab) + bb &&\text{[por la conmutativa]} \ &= aa + 2(ab) + bb &&\text{[por def. de doble]} \ \end{align}

Demostraciones con Lean4

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

variable (a b c : ℝ)

-- 1ª demostración
example :
  (a + b) * (a + b) = a * a + 2 * (a * b) + b * b :=
calc
  (a + b) * (a + b)
    = (a + b) * a + (a + b) * b       := by rw [mul_add]
  _ = a * a + b * a + (a + b) * b     := by rw [add_mul]
  _ = a * a + b * a + (a * b + b * b) := by rw [add_mul]
  _ = a * a + b * a + a * b + b * b   := by rw [←add_assoc]
  _ = a * a + (b * a + a * b) + b * b := by rw [add_assoc (a * a)]
  _ = a * a + (a * b + a * b) + b * b := by rw [mul_comm b a]
  _ = a * a + 2 * (a * b) + b * b     := by rw [←two_mul]

-- 2ª demostración
example :
  (a + b) * (a + b) = a * a + 2 * (a * b) + b * b :=
calc
  (a + b) * (a + b)
    = a * a + b * a + (a * b + b * b) := by rw [mul_add, add_mul, add_mul]
  _ = a * a + (b * a + a * b) + b * b := by rw [←add_assoc, add_assoc (a * a)]
  _ = a * a + 2 * (a * b) + b * b     := by rw [mul_comm b a, ←two_mul]

-- 3ª demostración
example :
  (a + b) * (a + b) = a * a + 2 * (a * b) + b * b :=
calc
  (a + b) * (a + b)
    = a * a + b * a + (a * b + b * b) := by ring
  _ = a * a + (b * a + a * b) + b * b := by ring
  _ = a * a + 2 * (a * b) + b * b     := by ring

-- 4ª demostración
example :
  (a + b) * (a + b) = a * a + 2 * (a * b) + b * b :=
by ring

-- 5ª demostración
example :
  (a + b) * (a + b) = a * a + 2 * (a * b) + b * b :=
by
  rw [mul_add]
  rw [add_mul]
  rw [add_mul]
  rw [←add_assoc]
  rw [add_assoc (a * a)]
  rw [mul_comm b a]
  rw [←two_mul]

-- 6ª demostración
example :
  (a + b) * (a + b) = a * a + 2 * (a * b) + b * b :=
by
  rw [mul_add, add_mul, add_mul]
  rw [←add_assoc, add_assoc (a * a)]
  rw [mul_comm b a, ←two_mul]

-- 7ª demostración
example :
  (a + b) * (a + b) = a * a + 2 * (a * b) + b * b :=
by linarith

Demostraciones interactivas

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

Referencias

• J. Avigad y P. Massot. Mathematics in Lean, p. 7.