Si c = ba-d y d = ab, entonces c = 0
Demostrar con Lean4 que si a, b, c y d son números reales tales
|
1 2 |
c = b * a - d d = a * b |
entonces
|
1 |
c = 0 |
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 |
import Mathlib.Data.Real.Basic import Mathlib.Tactic example (a b c d : ℝ) (h1 : c = b * a - d) (h2 : d = a * b) : c = 0 := by sorry |
Demostración en lenguaje natural
Por la siguiente cadena de igualdades
\[
\begin{align}
c &= ba – d &&\text{[por la primera hipótesis]} \\
&= ab – d &&\text{[por la conmutativa]} \\
&= ab – ab &&\text{[por la segunda hipótesis]} \\
&= 0
\end{align}
\]
Demostraciones con Lean
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 |
import Mathlib.Data.Real.Basic import Mathlib.Tactic -- 1ª demostración example (a b c d : ℝ) (h1 : c = b * a - d) (h2 : d = a * b) : c = 0 := calc c = b * a - d := by rw [h1] _ = a * b - d := by rw [mul_comm] _ = a * b - a * b := by rw [h2] _ = 0 := by rw [sub_self] -- 2ª demostración example (a b c d : ℝ) (h1 : c = b * a - d) (h2 : d = a * b) : c = 0 := by rw [h1] rw [mul_comm] rw [h2] rw [sub_self] -- 3ª demostración example (a b c d : ℝ) (h1 : c = b * a - d) (h2 : d = a * b) : c = 0 := by rw [h1, mul_comm, h2, sub_self] |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 7.
