{"id":1283,"date":"2023-07-19T06:00:35","date_gmt":"2023-07-19T04:00:35","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=1283"},"modified":"2023-07-19T18:34:33","modified_gmt":"2023-07-19T16:34:33","slug":"19-jul-23","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/19-jul-23\/","title":{"rendered":"(a + b)(a + b) = aa + 2ab + bb"},"content":{"rendered":"

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

\r\n   (a + b) * (a + b) = a * a + 2 * (a * b) + b * b\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 : \u211d)\r\n\r\nexample :\r\n  (a + b) * (a + b) = a * a + 2 * (a * b) + b * b :=\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)(a + b)
\n&= (a + b)a + (a + b)b    &&\\text{[por la distributiva]} \\\\
\n&= aa + ba + (a + b)b     &&\\text{[por la distributiva]} \\\\
\n&= aa + ba + (ab + bb)    &&\\text{[por la distributiva]} \\\\
\n&= aa + ba + ab + bb      &&\\text{[por la asociativa]} \\\\
\n&= aa + (ba + ab) + bb    &&\\text{[por la asociativa]} \\\\
\n&= aa + (ab + ab) + bb    &&\\text{[por la conmutativa]} \\\\
\n&= aa + 2(ab) + bb        &&\\text{[por def. de doble]} \\\\
\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 : \u211d)\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\nexample :\r\n  (a + b) * (a + b) = a * a + 2 * (a * b) + b * b :=\r\ncalc\r\n  (a + b) * (a + b)\r\n    = (a + b) * a + (a + b) * b       := by rw [mul_add]\r\n  _ = a * a + b * a + (a + b) * b     := by rw [add_mul]\r\n  _ = a * a + b * a + (a * b + b * b) := by rw [add_mul]\r\n  _ = a * a + b * a + a * b + b * b   := by rw [\u2190add_assoc]\r\n  _ = a * a + (b * a + a * b) + b * b := by rw [add_assoc (a * a)]\r\n  _ = a * a + (a * b + a * b) + b * b := by rw [mul_comm b a]\r\n  _ = a * a + 2 * (a * b) + b * b     := by rw [\u2190two_mul]\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\nexample :\r\n  (a + b) * (a + b) = a * a + 2 * (a * b) + b * b :=\r\ncalc\r\n  (a + b) * (a + b)\r\n    = a * a + b * a + (a * b + b * b) := by rw [mul_add, add_mul, add_mul]\r\n  _ = a * a + (b * a + a * b) + b * b := by rw [\u2190add_assoc, add_assoc (a * a)]\r\n  _ = a * a + 2 * (a * b) + b * b     := by rw [mul_comm b a, \u2190two_mul]\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\nexample :\r\n  (a + b) * (a + b) = a * a + 2 * (a * b) + b * b :=\r\ncalc\r\n  (a + b) * (a + b)\r\n    = a * a + b * a + (a * b + b * b) := by ring\r\n  _ = a * a + (b * a + a * b) + b * b := by ring\r\n  _ = a * a + 2 * (a * b) + b * b     := by ring\r\n\r\n-- 4\u00aa demostraci\u00f3n\r\nexample :\r\n  (a + b) * (a + b) = a * a + 2 * (a * b) + b * b :=\r\nby ring\r\n\r\n-- 5\u00aa demostraci\u00f3n\r\nexample :\r\n  (a + b) * (a + b) = a * a + 2 * (a * b) + b * b :=\r\nby\r\n  rw [mul_add]\r\n  rw [add_mul]\r\n  rw [add_mul]\r\n  rw [\u2190add_assoc]\r\n  rw [add_assoc (a * a)]\r\n  rw [mul_comm b a]\r\n  rw [\u2190two_mul]\r\n\r\n-- 6\u00aa demostraci\u00f3n\r\nexample :\r\n  (a + b) * (a + b) = a * a + 2 * (a * b) + b * b :=\r\nby\r\n  rw [mul_add, add_mul, add_mul]\r\n  rw [\u2190add_assoc, add_assoc (a * a)]\r\n  rw [mul_comm b a, \u2190two_mul]\r\n\r\n-- 7\u00aa demostraci\u00f3n\r\nexample :\r\n  (a + b) * (a + b) = a * a + 2 * (a * b) + b * b :=\r\nby linarith\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