{"id":1286,"date":"2023-07-20T06:00:50","date_gmt":"2023-07-20T04:00:50","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=1286"},"modified":"2023-07-19T18:46:49","modified_gmt":"2023-07-19T16:46:49","slug":"20-jul-23","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/20-jul-23\/","title":{"rendered":"(a + b) (c + d) = ac + ad + bc + bd"},"content":{"rendered":"

Demostrar con Lean4 que si a, b, c y d son n\u00fameros reales, entonces<\/p>\n

\r\n   (a + b) * (c + d) = a * c + a * d + b * c + b * d\r\n<\/pre>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\r\nimport Mathlib.Data.Real.Basic\r\nimport Mathlib.Tactic\r\n\r\nvariable (a b c d : \u211d)\r\n\r\nexample\r\n  : (a + b) * (c + d) = a * c + a * d + b * c + b * d :=\r\nsorry\r\n<\/pre>\n
<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n

\nPor la siguiente cadena de igualdades
\n\\begin{align}
\n(a + b)(c + d)
\n&= a(c + d) + b(c + d)    &&\\text{[por la distributiva]} \\\\
\n&= ac + ad + b(c + d)     &&\\text{[por la distributiva]} \\\\
\n&= ac + ad + (bc + bd)    &&\\text{[por la distributiva]} \\\\
\n&= ac + ad + bc + bd      &&\\text{[por la asociativa]}
\n\\end{align}<\/p>\n
Demostraciones con Lean4<\/b><\/p>\n
\r\nimport Mathlib.Data.Real.Basic\r\nimport Mathlib.Tactic\r\n\r\nvariable (a b c d : \u211d)\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\nexample\r\n  : (a + b) * (c + d) = a * c + a * d + b * c + b * d :=\r\ncalc\r\n  (a + b) * (c + d)\r\n    = a * (c + d) + b * (c + d)       := by rw [add_mul]\r\n  _ = a * c + a * d + b * (c + d)     := by rw [mul_add]\r\n  _ = a * c + a * d + (b * c + b * d) := by rw [mul_add]\r\n  _ = a * c + a * d + b * c + b * d   := by rw [\u2190add_assoc]\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\nexample\r\n  : (a + b) * (c + d) = a * c + a * d + b * c + b * d :=\r\ncalc\r\n  (a + b) * (c + d)\r\n    = a * (c + d) + b * (c + d)       := by ring\r\n  _ = a * c + a * d + b * (c + d)     := by ring\r\n  _ = a * c + a * d + (b * c + b * d) := by ring\r\n  _ = a * c + a * d + b * c + b * d   := by ring\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\nexample : (a + b) * (c + d) = a * c + a * d + b * c + b * d :=\r\nby ring\r\n\r\n-- 4\u00aa demostraci\u00f3n\r\nexample\r\n  : (a + b) * (c + d) = a * c + a * d + b * c + b * d :=\r\nby\r\n   rw [add_mul]\r\n   rw [mul_add]\r\n   rw [mul_add]\r\n   rw [\u2190 add_assoc]\r\n\r\n-- 5\u00aa demostraci\u00f3n\r\nexample : (a + b) * (c + d) = a * c + a * d + b * c + b * d :=\r\nby rw [add_mul, mul_add, mul_add, \u2190add_assoc]\r\n<\/pre>\n
Demostraciones interactivas<\/b><\/p>\n
Se puede interactuar con las demostraciones anteriores en Lean 4 Web<\/a>.<\/p>\n
Referencias<\/b><\/p>\n