{"id":1297,"date":"2023-07-25T06:00:10","date_gmt":"2023-07-25T04:00:10","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=1297"},"modified":"2023-07-21T18:30:36","modified_gmt":"2023-07-21T16:30:36","slug":"25-jul-23","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/25-jul-23\/","title":{"rendered":"Si a+b = c, entonces (a+b)(a+b) = ac+ bc"},"content":{"rendered":"

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

\r\n   a + b = c,\r\n<\/pre>\n
entonces<\/p>\n
\r\n   (a + b) * (a + b) = a * c + b * c\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  (h : a + b = c)\r\n  : (a + b) * (a + b) = a * c + b * c :=\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)c        &&\\text{[por la hip\u00f3tesis]}   \\\\
\n   &= ac + bc         &&\\text{[por la distributiva]}
\n\\end{align}<\/p>\n
Demostraciones con Lean<\/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  (h : a + b = c)\r\n  : (a + b) * (a + b) = a * c + b * c :=\r\ncalc\r\n  (a + b) * (a + b)\r\n    = (a + b) * c   := by exact congrArg (HMul.hMul (a + b)) h\r\n  _ = a * c + b * c := by rw [add_mul]\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\nexample\r\n  (h : a + b = c)\r\n  : (a + b) * (a + b) = a * c + b * c :=\r\nby\r\n  nth_rewrite 2 [h]\r\n  rw [add_mul]\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