{"id":972,"date":"2022-08-24T16:00:24","date_gmt":"2022-08-24T14:00:24","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=972"},"modified":"2022-09-11T13:39:07","modified_gmt":"2022-09-11T11:39:07","slug":"cuadrado-del-binomio","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/cuadrado-del-binomio\/","title":{"rendered":"Si a y b son n\u00fameros reales, entonces (a + b) * (a + b) = a * a + 2 * (a * b) + b * b"},"content":{"rendered":"

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

\n(a + b) * (a + b) = a * a + 2 * (a * b) + b * b\n<\/pre>\n
Para ello, completar la siguiente teor\u00eda de Lean:<\/p>\n
\nimport data.real.basic\n\nvariables a b : \u211d\n\nexample :\n  (a + b) * (a + b) = a * a + 2 * (a * b) + b * b :=\nsorry\n<\/pre>\n
<\/p>\n
Soluciones con Lean<\/b><\/p>\n
\nimport data.real.basic\n\nvariables a b : \u211d\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample :\n  (a + b) * (a + b) = a * a + 2 * (a * b) + b * b :=\ncalc\n  (a + b) * (a + b)\n      = (a + b) * a + (a + b) * b       : by rw mul_add\n  ... = a * a + b * a + (a + b) * b     : by rw add_mul\n  ... = a * a + b * a + (a * b + b * b) : by rw add_mul\n  ... = a * a + b * a + a * b + b * b   : by rw \u2190 add_assoc\n  ... = a * a + (b * a + a * b) + b * b : by rw add_assoc (a * a)\n  ... = a * a + (a * b + a * b) + b * b : by rw mul_comm b a\n  ... = a * a + 2 * (a * b) + b * b     : by rw \u2190 two_mul\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample :\n  (a + b) * (a + b) = a * a + 2 * (a * b) + b * b :=\ncalc\n  (a + b) * (a + b)\n      = a * a + b * a + (a * b + b * b) : by rw [mul_add, add_mul, add_mul]\n  ... = a * a + (b * a + a * b) + b * b : by rw [\u2190add_assoc, add_assoc (a * a)]\n  ... = a * a + 2 * (a * b) + b * b     : by rw [mul_comm b a, \u2190two_mul]\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample :\n  (a + b) * (a + b) = a * a + 2 * (a * b) + b * b :=\ncalc\n  (a + b) * (a + b)\n      = a * a + b * a + (a * b + b * b) : by ring\n  ... = a * a + (b * a + a * b) + b * b : by ring\n  ... = a * a + 2 * (a * b) + b * b     : by ring\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample :\n  (a + b) * (a + b) = a * a + 2 * (a * b) + b * b :=\nby ring\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample :\n  (a + b) * (a + b) = a * a + 2 * (a * b) + b * b :=\nbegin\n  rw mul_add,\n  rw add_mul,\n  rw add_mul,\n  rw \u2190 add_assoc,\n  rw add_assoc (a * a),\n  rw mul_comm b a,\n  rw \u2190 two_mul,\nend\n\n-- 6\u00aa demostraci\u00f3n\n-- ===============\n\nexample :\n  (a + b) * (a + b) = a * a + 2 * (a * b) + b * b :=\nbegin\n  rw [mul_add, add_mul, add_mul],\n  rw [\u2190add_assoc, add_assoc (a * a)],\n  rw [mul_comm b a, \u2190two_mul],\nend\n<\/pre>\n
Se puede interactuar con la prueba anterior en esta sesi\u00f3n con Lean<\/a>.<\/p>\n
Referencias<\/b><\/p>\n