Skip to main content

Si a + b = c, entonces (a + b)(a + b) = ac + bc

Demostrar con Lean4 que si a, b y c son números reales tales que \[ a + b = c \] entonces \[ (a + b)·(a + b) = a·c + b·c \]

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

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

variable (a b c : ℝ)

example
  (h : a + b = c)
  : (a + b) * (a + b) = a * c + b * c :=
sorry

Demostración en lenguaje natural

Por la siguiente cadena de igualdades \begin{align} (a + b)(a + b) &= (a + b)c &&\text{[por la hipótesis]} \\ &= ac + bc &&\text{[por la distributiva]} \end{align}

Demostraciones con Lean

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

variable (a b c : ℝ)

-- 1ª demostración
example
  (h : a + b = c)
  : (a + b) * (a + b) = a * c + b * c :=
calc
  (a + b) * (a + b)
    = (a + b) * c   := by exact congrArg (HMul.hMul (a + b)) h
  _ = a * c + b * c := by rw [add_mul]

-- 2ª demostración
example
  (h : a + b = c)
  : (a + b) * (a + b) = a * c + b * c :=
by
  nth_rewrite 2 [h]
  rw [add_mul]

Demostraciones interactivas

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

Referencias