En ℝ, si x² = 1 entonces x = 1 ó x = -1

Demostrar con Lean4 que en , si x²=1 entonces x=1 ó x=1.

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

Demostración en lenguaje natural

Usaremos los siguientes lemas
(x)[xx=0](x,y)[xy=0x=0y=0](x,y)[xy=0x=y](x,y)[x+y=0x=y]

Se tiene que
(x1)(x+1)=x²1=11[por la hipótesis]=0[por L1]
y, por el lema L2, se tiene que
x1=0x+1=0
Acabaremos la demostración por casos.

Primer caso:
x1=0x=1[por L3]x=1x=1

Segundo caso:
x+1=0x=1[por L4]x=1x=1

Demostraciones con Lean4

Demostraciones interactivas

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

Referencias

Demostraciones con Isabelle/HOL

Escribe un comentario