Si a, b, c, d, e y f son números reales tales que a * b = c * d y e = f entonces, a * (b * e) = c * (d * f)
Demostrar que si a, b, c, d, e y f son números reales tales que
|
1 2 |
a * b = c * d e = f |
Entonces,
|
1 |
a * (b * e) = c * (d * f) |
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 |
import data.real.basic variables a b c d e f : ℝ example (h1 : a * b = c * d) (h2 : e = f) : a * (b * e) = c * (d * f) := |
Soluciones 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 36 37 38 39 40 41 42 43 44 |
import data.real.basic variables a b c d e f : ℝ -- 1ª demostración example (h1 : a * b = c * d) (h2 : e = f) : a * (b * e) = c * (d * f) := begin rw h2, rw ←mul_assoc, rw h1, rw mul_assoc, end -- 2ª demostración example (h1 : a * b = c * d) (h2 : e = f) : a * (b * e) = c * (d * f) := calc a * (b * e) = a * (b * f) : by rw h2 ... = (a * b) * f : by rw ←mul_assoc ... = (c * d) * f : by rw h1 ... = c * (d * f) : by rw mul_assoc -- 3ª demostración example (h1 : a * b = c * d) (h2 : e = f) : a * (b * e) = c * (d * f) := calc a * (b * e) = a * (b * f) : by rw h2 ... = (a * b) * f : by ring ... = (c * d) * f : by rw h1 ... = c * (d * f) : by ring -- 4ª demostración example (h1 : a * b = c * d) (h2 : e = f) : a * (b * e) = c * (d * f) := by finish |
Se puede interactuar con la prueba anterior en esta sesión con Lean.
Referencias
- J. Avigad, K. Buzzard, R.Y. Lewis y P. Massot. Mathematics in Lean, p. 6.
