Si x, y, z ∈ ℕ, entonces x divide a yxz
Demostrar con Lean4 que si \(x, y, z ∈ ℕ\), entonces \(x\) divide a \(yxz\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 |
import Mathlib.Data.Real.Basic variable (x y z : ℕ) example : x ∣ y * x * z := by sorry |
Demostración en lenguaje natural
Por la transitividad de la divisibilidad aplicada a las relaciones
\begin{align}
x &\mid yx \\
yx &\mid yxz
\end{align}
Demostraciones con Lean4
|
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 |
import Mathlib.Data.Real.Basic variable (x y z : ℕ) -- 1ª demostración -- =============== example : x ∣ y * x * z := by have h1 : x ∣ y * x := dvd_mul_left x y have h2 : (y * x) ∣ (y * x * z) := dvd_mul_right (y * x) z show x ∣ y * x * z exact dvd_trans h1 h2 -- 2ª demostración -- =============== example : x ∣ y * x * z := dvd_trans (dvd_mul_left x y) (dvd_mul_right (y * x) z) -- 3ª demostración -- =============== example : x ∣ y * x * z := by apply dvd_mul_of_dvd_left apply dvd_mul_left -- Los lemas utilizados son: #check (dvd_mul_left x y : x ∣ y * x) #check (dvd_mul_right x y : x ∣ x * y) #check (dvd_trans : x ∣ y → y ∣ z → x ∣ z) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 19.
