{"id":1761,"date":"2023-11-07T06:00:01","date_gmt":"2023-11-07T04:00:01","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=1761"},"modified":"2023-11-07T19:38:03","modified_gmt":"2023-11-07T17:38:03","slug":"07-nov-23","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/07-nov-23\/","title":{"rendered":"Si a divide a b y a c, entonces divide a b+c"},"content":{"rendered":"\n

Demostrar con Lean4 que si \(a\) divide a \(b\) y a \(c\), entonces divide a \(b+c\).<\/p>\n

Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n

\nimport Mathlib.Tactic\n\nvariable {a b c : \u2115}\n\nexample\n  (h1 : a \u2223 b)\n  (h2 : a \u2223 c)\n  : a \u2223 (b + c) :=\nby sorry\n<\/pre>\n
<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n
Puesto que \(a\) divide a \(b\) y a \(c\), existen \(d\) y \(e\) tales que
\n\begin{align}
\n   b &= ad \tag{1} \\
\n   c &= ae \tag{2}
\n\end{align}
\nPor tanto,
\n\begin{align}
\n   b + c &= ad + c     &&\text{[por (1)]} \\
\n         &= ad + ae    &&\text{[por (2)]} \\
\n         &= a(d + e)   &&\text{[por la distributiva]}
\n\end{align}
\nPor consiguiente, \(a\) divide a \(b + c\).<\/p>\n
Demostraciones con Lean4<\/b><\/p>\n
\nimport Mathlib.Tactic\n\nvariable {a b c : \u2115}\n\n-- 1\u00aa demostraci\u00f3n\nexample\n  (h1 : a \u2223 b)\n  (h2 : a \u2223 c)\n  : a \u2223 (b + c) :=\nby\n  rcases h1 with \u27e8d, beq : b = a * d\u27e9\n  rcases h2 with \u27e8e, ceq: c = a * e\u27e9\n  have h1 : b + c = a * (d + e) :=\n    calc b + c\n         = (a * d) + c       := congrArg (. + c) beq\n       _ = (a * d) + (a * e) := congrArg ((a * d) + .) ceq\n       _ = a * (d + e)       := by rw [\u2190 mul_add]\n  show a \u2223 (b + c)\n  exact Dvd.intro (d + e) h1.symm\n\n-- 2\u00aa demostraci\u00f3n\nexample\n  (h1 : a \u2223 b)\n  (h2 : a \u2223 c)\n  : a \u2223 (b + c) :=\nby\n  rcases h1 with \u27e8d, beq : b = a * d\u27e9\n  rcases h2 with \u27e8e, ceq: c = a * e\u27e9\n  have h1 : b + c = a * (d + e) := by linarith\n  show a \u2223 (b + c)\n  exact Dvd.intro (d + e) h1.symm\n\n-- 3\u00aa demostraci\u00f3n\nexample\n  (h1 : a \u2223 b)\n  (h2 : a \u2223 c)\n  : a \u2223 (b + c) :=\nby\n  rcases h1 with \u27e8d, beq : b = a * d\u27e9\n  rcases h2 with \u27e8e, ceq: c = a * e\u27e9\n  show a \u2223 (b + c)\n  exact Dvd.intro (d + e) (by linarith)\n\n-- 4\u00aa demostraci\u00f3n\nexample\n  (h1 : a \u2223 b)\n  (h2 : a \u2223 c)\n  : a \u2223 (b + c) :=\nby\n  cases' h1 with d beq\n  -- d : \u2115\n  -- beq : b = a * d\n  cases' h2 with e ceq\n  -- e : \u2115\n  -- ceq : c = a * e\n  rw [ceq, beq]\n  -- \u22a2 a \u2223 a * d + a * e\n  use (d + e)\n  -- \u22a2 a * d + a * e = a * (d + e)\n  ring\n\n-- 5\u00aa demostraci\u00f3n\nexample\n  (h1 : a \u2223 b)\n  (h2 : a \u2223 c)\n  : a \u2223 (b + c) :=\nby\n  rcases h1 with \u27e8d, rfl\u27e9\n  -- \u22a2 a \u2223 a * d + c\n  rcases h2 with \u27e8e, rfl\u27e9\n  -- \u22a2 a \u2223 a * d + a * e\n  use (d + e)\n  -- \u22a2 a * d + a * e = a * (d + e)\n  ring\n\n-- 6\u00aa demostraci\u00f3n\nexample\n  (h1 : a \u2223 b)\n  (h2 : a \u2223 c)\n  : a \u2223 (b + c) :=\ndvd_add h1 h2\n\n-- Lemas usados\n-- ============\n\n-- #check (Dvd.intro c : a * c = b \u2192 a \u2223 b)\n-- #check (dvd_add : a \u2223 b \u2192  a \u2223 c \u2192 a \u2223 (b + c))\n-- #check (mul_add a b c : a * (b + c) = a * b + a * c)\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