Demostrar con Lean4 que si \\(x\\) divide a \\(w\\), entonces tambi\u00e9n divide a \\(y(xz)+x^2+w^2\\).<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\r\nimport Mathlib.Data.Real.Basic\r\nvariable (w x y z : \u2115)\r\n\r\nexample\r\n (h : x \u2223 w)\r\n : x \u2223 y * (x * z) + x^2 + w^2 :=\r\nby sorry\r\n<\/pre>\n<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n
\nPor la divisibilidad de la suma basta probar que
\n\\begin{align}
\n x &\\mid yxz \\tag{1} \\\\
\n x &\\mid x^2 \\tag{2} \\\\
\n x &\\mid w^2 \\tag{3}
\n\\end{align}<\/p>\n
Para demostrar (1), por la divisibilidad del producto se tiene
\n\\[ x \\mid xz\\]
\ny, de nuevo por la divisibilidad del producto,
\n\\[ x \\mid y(xz)\\]<\/p>\n
La propiedad (2) se tiene por la definici\u00f3n de cuadrado y la divisibilidad del producto.<\/p>\n
La propiedad (3) se tiene por la definici\u00f3n de cuadrado, la hip\u00f3tesis y la divisibilidad del producto.<\/p>\n
Demostraciones con Lean4<\/b><\/p>\n\r\nimport Mathlib.Data.Real.Basic\r\nvariable (w x y z : \u2115)\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\nexample\r\n (h : x \u2223 w)\r\n : x \u2223 y * (x * z) + x^2 + w^2 :=\r\nby\r\n have h1 : x \u2223 x * z :=\r\n dvd_mul_right x z\r\n have h2 : x \u2223 y * (x * z) :=\r\n dvd_mul_of_dvd_right h1 y\r\n have h3 : x \u2223 x^2 := by\r\n apply dvd_mul_left\r\n have h4 : x \u2223 w * w :=\r\n dvd_mul_of_dvd_left h w\r\n have h5 : x \u2223 w^2 := by\r\n rwa [\u2190 pow_two w] at h4\r\n have h6 : x \u2223 y * (x * z) + x^2 :=\r\n dvd_add h2 h3\r\n show x \u2223 y * (x * z) + x^2 + w^2\r\n exact dvd_add h6 h5\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\nexample\r\n (h : x \u2223 w)\r\n : x \u2223 y * (x * z) + x^2 + w^2 :=\r\nby\r\n apply dvd_add\r\n { apply dvd_add\r\n { apply dvd_mul_of_dvd_right\r\n apply dvd_mul_right }\r\n { rw [pow_two]\r\n apply dvd_mul_right }}\r\n { rw [pow_two]\r\n apply dvd_mul_of_dvd_left h }\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\nexample\r\n (h : x \u2223 w)\r\n : x \u2223 y * (x * z) + x^2 + w^2 :=\r\nby\r\n repeat' apply dvd_add\r\n { apply dvd_mul_of_dvd_right\r\n apply dvd_mul_right }\r\n { rw [pow_two]\r\n apply dvd_mul_right }\r\n { rw [pow_two]\r\n apply dvd_mul_of_dvd_left h }\r\n\r\n-- Lemas usados\r\n-- ============\r\n\r\n-- #check (dvd_add : x \u2223 y \u2192 x \u2223 z \u2192 x \u2223 y + z)\r\n-- #check (dvd_mul_left x y : x \u2223 y * x)\r\n-- #check (dvd_mul_right x y : x \u2223 x * y)\r\n-- #check (dvd_mul_of_dvd_left : x \u2223 y \u2192 \u2200 (c : \u2115), x \u2223 y * c)\r\n-- #check (dvd_mul_of_dvd_right : x \u2223 y \u2192 \u2200 (c : \u2115), x \u2223 c * y)\r\n-- #check (pow_two x : x ^ 2 = x * x)\r\n<\/pre>\nDemostraciones interactivas<\/b><\/p>\n
Se puede interactuar con las demostraciones anteriores en Lean 4 Web<\/a>.<\/p>\nReferencias<\/b><\/p>\n