Skip to main content

En ℝ, (a + b)(c + d) = ac + ad + bc + bd

Demostrar con Lean4 que si \(a\), \(b\), \(c\) y \(d\) son números reales, entonces \[ (a + b)(c + d) = ac + ad + bc + bd \]

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

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]} \newline &= ac + ad + b(c + d) &&\text{[por la distributiva]} \newline &= ac + ad + (bc + bd) &&\text{[por la distributiva]} \newline &= ac + ad + bc + bd &&\text{[por la asociativa]} \end{align}

Demostraciones con Lean4

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