{"id":8062,"date":"2023-12-30T08:48:23","date_gmt":"2023-12-30T07:48:23","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=8062"},"modified":"2023-12-30T08:53:38","modified_gmt":"2023-12-30T07:53:38","slug":"30-dic-23","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/30-dic-23\/","title":{"rendered":"La semana en Calculemus (30 de diciembre de 2023)"},"content":{"rendered":"\n<p>Estas 3 \u00faltimas semanas he publicado en <a href=\"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/\">Calculemus<\/a> las demostraciones con Lean4 de las siguientes propiedades:<\/p>\n<ul>\n<li><a href=\"#ej1\">1. {x \u2264 y, y \u2270 x} \u22a2 x \u2264 y \u2227 x \u2260 y<\/a><\/li>\n<li><a href=\"#ej2\">2. x \u2264 y \u2227 x \u2260 y \u22a2 y \u2270 x<\/a><\/li>\n<li><a href=\"#ej3\">3. Si (m \u2223 n \u2227 m \u2260 n), entonces (m \u2223 n \u2227 \u00ac(n \u2223 m))<\/a><\/li>\n<li><a href=\"#ej4\">4. (\u2203x \u2208 \u211d)(2 &lt; x &lt; 3)<\/a><\/li>\n<li><a href=\"#ej5\">5. Si (\u2203z \u2208 \u211d)(x &lt; z &lt; y), entonces x &lt; y<\/a><\/li>\n<li><a href=\"#ej6\">6. Existen n\u00fameros primos m y n tales que 4 &lt; m &lt; n &lt; 10<\/a><\/li>\n<li><a href=\"#ej7\">7. En \u211d, x \u2264 y \u2227 x \u2260 y \u2192 x \u2264 y \u2227 y \u2270 x<\/a><\/li>\n<li><a href=\"#ej8\">8. En \u211d, si x \u2264 y, entonces y \u2270 x \u2194 x \u2260 y<\/a><\/li>\n<li><a href=\"#ej9\">9. En \u211d, x\u00b2 + y\u00b2 = 0 \u2194 x = 0 \u2227 y = 0<\/a><\/li>\n<li><a href=\"#ej10\">10. Si |x + 3| &lt; 5, entonces -8 &lt; x &lt; 2<\/a><\/li>\n<li><a href=\"#ej11\">11. 3 divide al m\u00e1ximo com\u00fan divisor de 6 y 15<\/a><\/li>\n<\/ul>\n<p>A continuaci\u00f3n se muestran las soluciones.<br \/>\n<!--more--><br \/>\n<a name=\"ej1\"><\/a><\/p>\n<h3>1. {x \u2264 y, y \u2270 x} \u22a2 x \u2264 y \u2227 x \u2260 y<\/h3>\n<p>Demostrar con Lean4 que<br \/>\n&#92;[&#92;{x \u2264 y, y \u2270 x&#92;} \u22a2 x \u2264 y \u2227 x \u2260 y&#92;]<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\n\nvariable {x y : \u211d}\n\nexample\n  (h1 : x \u2264 y)\n  (h2 : \u00acy \u2264 x)\n  : x \u2264 y \u2227 x \u2260 y :=\nby sorry\n<\/pre>\n<p><b>Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p>Como la conclusi\u00f3n es una conjunci\u00f3n, tenemos que desmostrar sus  partes. La primera parte (&#92;(x \u2264 y&#92;)) coincide con la hip\u00f3tesis. Para demostrar la segunda parte (&#92;(x \u2260 y&#92;)), supongamos que &#92;(x = y&#92;); entonces &#92;(y \u2264 x&#92;) en contradicci\u00f3n con la segunda hip\u00f3tesis.<\/p>\n<p><b>Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\n\nvariable {x y : \u211d}\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h1 : x \u2264 y)\n  (h2 : \u00acy \u2264 x)\n  : x \u2264 y \u2227 x \u2260 y :=\nby\n  constructor\n  . -- \u22a2 x \u2264 y\n    exact h1\n  . -- \u22a2 x \u2260 y\n    intro h3\n    -- h3 : x = y\n    -- \u22a2 False\n    have h4 : y \u2264 x := h3.symm.le\n    show False\n    exact h2 h4\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h1 : x \u2264 y)\n  (h2 : \u00acy \u2264 x)\n  : x \u2264 y \u2227 x \u2260 y :=\nby\n  constructor\n  . -- \u22a2 x \u2264 y\n    exact h1\n  . -- \u22a2 x \u2260 y\n    intro h3\n    -- h3 : x = y\n    -- \u22a2 False\n    exact h2 (h3.symm.le)\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h1 : x \u2264 y)\n  (h2 : \u00acy \u2264 x)\n  : x \u2264 y \u2227 x \u2260 y :=\n\u27e8h1, fun h3 \u21a6 h2 (h3.symm.le)\u27e9\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h1 : x \u2264 y)\n  (h2 : \u00acy \u2264 x)\n  : x \u2264 y \u2227 x \u2260 y :=\nby\n  constructor\n  . -- \u22a2 x \u2264 y\n    exact h1\n  . -- \u22a2 x \u2260 y\n    intro h3\n    -- h3 : x = y\n    -- \u22a2 False\n    apply h2\n    -- \u22a2 y \u2264 x\n    rw [h3]\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h1 : x \u2264 y)\n  (h2 : \u00acy \u2264 x)\n  : x \u2264 y \u2227 x \u2260 y :=\nby\n  constructor\n  . -- \u22a2 x \u2264 y\n    exact h1\n  . -- \u22a2 x \u2260 y\n    intro h3\n    -- h3 : x = y\n    -- \u22a2 False\n    exact h2 (by rw [h3])\n\n-- 6\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h1 : x \u2264 y)\n  (h2 : \u00ac y \u2264 x)\n  : x \u2264 y \u2227 x \u2260 y :=\n\u27e8h1, fun h \u21a6 h2 (by rw [h])\u27e9\n\n-- 7\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h1 : x \u2264 y)\n  (h2 : \u00ac y \u2264 x)\n  : x \u2264 y \u2227 x \u2260 y :=\nby\n  have h3 : x \u2260 y\n  . contrapose! h2\n    -- \u22a2 y \u2264 x\n    rw [h2]\n  exact \u27e8h1, h3\u27e9\n\n-- 8\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h1 : x \u2264 y)\n  (h2 : \u00ac y \u2264 x)\n  : x \u2264 y \u2227 x \u2260 y :=\nby aesop\n<\/pre>\n<p><b>Demostraciones interactivas<\/b><\/p>\n<p>Se puede interactuar con las demostraciones anteriores en <a href=\"https:\/\/live.lean-lang.org\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus2\/main\/src\/Introduccion_de_la_conjuncion.lean\" rel=\"noopener noreferrer\" target=\"_blank\">Lean 4 Web<\/a>.<\/p>\n<p><b>Referencias<\/b><\/p>\n<ul>\n<li> J. Avigad y P. Massot. <a href=\"https:\/\/bit.ly\/3U4UjBk\">Mathematics in Lean<\/a>, p. 35.<\/li>\n<\/ul>\n<p><a name=\"ej2\"><\/a><\/p>\n<h3>2. x \u2264 y \u2227 x \u2260 y \u22a2 y \u2270 x<\/h3>\n<p>Demostrar con Lean4 que<br \/>\n&#92;[x \u2264 y \u2227 x \u2260 y \u22a2 y \u2270 x&#92;]<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\n\nvariable {x y : \u211d}\n\nexample\n  (h : x \u2264 y \u2227 x \u2260 y)\n  : \u00ac y \u2264 x :=\nby sorry\n<\/pre>\n<p><b>Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p>Supongamos que &#92;(y \u2264 x&#92;). Entonces, por la antisimetr\u00eda y la primera parte de la hip\u00f3tesis, se tiene que &#92;(x = y&#92;) que contradice la segunda parte de la hip\u00f3tesis.<\/p>\n<p><b>Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\n\nvariable {x y : \u211d}\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : x \u2264 y \u2227 x \u2260 y)\n  : \u00ac y \u2264 x :=\nby\n  intro h1\n  cases' h with h2 h3\n  -- h2 : x \u2264 y\n  -- h3 : x \u2260 y\n  have h4 : x = y := le_antisymm h2 h1\n  show False\n  exact h3 h4\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : x \u2264 y \u2227 x \u2260 y)\n  : \u00ac y \u2264 x :=\nby\n  intro h1\n  have h4 : x = y := le_antisymm h.1 h1\n  show False\n  exact h.2 h4\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : x \u2264 y \u2227 x \u2260 y)\n  : \u00ac y \u2264 x :=\nby\n  intro h1\n  show False\n  exact h.2 (le_antisymm h.1 h1)\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : x \u2264 y \u2227 x \u2260 y)\n  : \u00ac y \u2264 x :=\nfun h1 \u21a6 h.2 (le_antisymm h.1 h1)\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : x \u2264 y \u2227 x \u2260 y)\n  : \u00ac y \u2264 x :=\nby\n  intro h'\n  -- h' : y \u2264 x\n  -- \u22a2 False\n  apply h.right\n  -- \u22a2 x = y\n  exact le_antisymm h.left h'\n\n-- 6\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : x \u2264 y \u2227 x \u2260 y)\n  : \u00ac y \u2264 x :=\nby\n  cases' h with h1 h2\n  -- h1 : x \u2264 y\n  -- h2 : x \u2260 y\n  contrapose! h2\n  -- h2 : y \u2264 x\n  -- \u22a2 x = y\n  exact le_antisymm h1 h2\n\n-- 7\u00aa demostraci\u00f3n\n-- ===============\n\nexample : x \u2264 y \u2227 x \u2260 y \u2192 \u00ac y \u2264 x :=\nby\n  rintro \u27e8h1, h2\u27e9 h'\n  -- h1 : x \u2264 y\n  -- h2 : x \u2260 y\n  -- h' : y \u2264 x\n  -- \u22a2 False\n  exact h2 (le_antisymm h1 h')\n\n-- 8\u00aa demostraci\u00f3n\n-- ===============\n\nexample : x \u2264 y \u2227 x \u2260 y \u2192 \u00ac y \u2264 x :=\nfun \u27e8h1, h2\u27e9 h' \u21a6 h2 (le_antisymm h1 h')\n\n-- Lemas usados\n-- ============\n\n-- #check (le_antisymm : x \u2264 y \u2192 y \u2264 x \u2192 x = y)\n<\/pre>\n<p><b>Demostraciones interactivas<\/b><\/p>\n<p>Se puede interactuar con las demostraciones anteriores en <a href=\"https:\/\/live.lean-lang.org\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus2\/main\/src\/Eliminacion_de_la_conjuncion.lean\" rel=\"noopener noreferrer\" target=\"_blank\">Lean 4 Web<\/a>.<\/p>\n<p><b>Referencias<\/b><\/p>\n<ul>\n<li> J. Avigad y P. Massot. <a href=\"https:\/\/bit.ly\/3U4UjBk\">Mathematics in Lean<\/a>, p. 35.<\/li>\n<\/ul>\n<p><a name=\"ej3\"><\/a><\/p>\n<h3>3. Si (m \u2223 n \u2227 m \u2260 n), entonces (m \u2223 n \u2227 \u00ac(n \u2223 m))<\/h3>\n<p>Demostrar con Lean4 que si &#40;m \u2223 n \u2227 m \u2260 n&#41;, entonces &#40;m \u2223 n \u2227 \u00ac(n \u2223 m)&#41;.<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Nat.GCD.Basic\n\nvariable {m n : \u2115}\n\nexample\n  (h : m \u2223 n \u2227 m \u2260 n)\n  : m \u2223 n \u2227 \u00ac n \u2223 m :=\nby sorry\n<\/pre>\n<p><b>Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p>La primera parte de la conclusi\u00f3n coincide con la primera de la hip\u00f3tesis. Nos queda demostrar la segunda parte; es decir, que &#40;\u00ac(n | m)&#41;. Para ello, supongamos que &#40;n | m&#41;. Entonces, por la propiedad antisim\u00e9trica de la divisibilidad y la primera parte de la hip\u00f3tesis, se tiene que &#40;m = n&#41; en contradicci\u00f3n con la segunda parte de la hip\u00f3tesis.<\/p>\n<p><b>Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Nat.GCD.Basic\n\nvariable {m n : \u2115}\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : m \u2223 n \u2227 m \u2260 n)\n  : m \u2223 n \u2227 \u00ac n \u2223 m :=\nby\n  constructor\n  . show m \u2223 n\n    exact h.left\n  . show \u00acn \u2223 m\n    { intro (h1 : n \u2223 m)\n      have h2 : m = n := dvd_antisymm h.left h1\n      show False\n      exact h.right h2 }\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : m \u2223 n \u2227 m \u2260 n)\n  : m \u2223 n \u2227 \u00ac n \u2223 m :=\nby\n  constructor\n  . exact h.left\n  . intro (h1 : n \u2223 m)\n    exact h.right (dvd_antisymm h.left h1)\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : m \u2223 n \u2227 m \u2260 n)\n  : m \u2223 n \u2227 \u00ac n \u2223 m :=\n\u27e8h.left, fun h1 \u21a6 h.right (dvd_antisymm h.left h1)\u27e9\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : m \u2223 n \u2227 m \u2260 n)\n  : m \u2223 n \u2227 \u00ac n \u2223 m :=\nby\n  cases' h with h1 h2\n  -- h1 : m \u2223 n\n  -- h2 : m \u2260 n\n  constructor\n  . -- \u22a2 m \u2223 n\n    exact h1\n  . -- \u22a2 \u00acn \u2223 m\n    contrapose! h2\n    -- h2 : n \u2223 m\n    -- \u22a2 m = n\n    apply dvd_antisymm h1 h2\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : m \u2223 n \u2227 m \u2260 n)\n  : m \u2223 n \u2227 \u00ac n \u2223 m :=\nby\n  rcases h with \u27e8h1 : m \u2223 n, h2 : m \u2260 n\u27e9\n  constructor\n  . -- \u22a2 m \u2223 n\n    exact h1\n  . -- \u22a2 \u00acn \u2223 m\n    contrapose! h2\n    -- h2 : n \u2223 m\n    -- \u22a2 m = n\n    apply dvd_antisymm h1 h2\n\n-- Lemas usados\n-- ============\n\n-- #check (dvd_antisymm : m \u2223 n \u2192 n \u2223 m \u2192 m = n)\n<\/pre>\n<p><b>Demostraciones interactivas<\/b><\/p>\n<p>Se puede interactuar con las demostraciones anteriores en <a href=\"https:\/\/live.lean-lang.org\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus2\/main\/src\/Uso_de_conjuncion.lean\" rel=\"noopener noreferrer\" target=\"_blank\">Lean 4 Web<\/a>.<\/p>\n<p><b>Referencias<\/b><\/p>\n<ul>\n<li> J. Avigad y P. Massot. <a href=\"https:\/\/bit.ly\/3U4UjBk\">Mathematics in Lean<\/a>, p. 36.<\/li>\n<\/ul>\n<p><a name=\"ej4\"><\/a><\/p>\n<h3>4. (\u2203x \u2208 \u211d)[2 &lt; x &lt; 3]<\/h3>\n<p>Demostrar con Lean4 que &#92;((\u2203x \u2208 \u211d)[2 &lt; x &lt; 3]&#92;).<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\n\nexample : \u2203 x : \u211d, 2 < x \u2227 x < 3 :=\nby sorry\n<\/pre>\n<p><b>Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p>Podemos usar el n\u00famero &#92;(&#92;dfrac{5}{2}&#92;) y comprobar que &#92;(2 &lt; &#92;dfrac{5}{2} &lt; 3&#92;).<\/p>\n<p><b>Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample : \u2203 x : \u211d, 2 < x \u2227 x < 3 :=\nby\n  use 5 \/ 2\n  show 2 < 5 \/ 2 \u2227 5 \/ 2 < 3\n  constructor\n  . show 2 < 5 \/ 2\n    norm_num\n  . show 5 \/ 2 < 3\n    norm_num\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : \u2203 x : \u211d, 2 < x \u2227 x < 3 :=\nby\n  use 5 \/ 2\n  constructor\n  . norm_num\n  . norm_num\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : \u2203 x : \u211d, 2 < x \u2227 x < 3 :=\nby\n  use 5 \/ 2\n  constructor <;> norm_num\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample : \u2203 x : \u211d, 2 < x \u2227 x < 3 :=\n\u27e85\/2, by norm_num\u27e9\n<\/pre>\n<p><b>Demostraciones interactivas<\/b><\/p>\n<p>Se puede interactuar con las demostraciones anteriores en <a href=\"https:\/\/live.lean-lang.org\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus2\/main\/src\/Entre_2_y_3.lean\" rel=\"noopener noreferrer\" target=\"_blank\">Lean 4 Web<\/a>.<\/p>\n<p><b>Referencias<\/b><\/p>\n<ul>\n<li> J. Avigad y P. Massot. <a href=\"https:\/\/bit.ly\/3U4UjBk\">Mathematics in Lean<\/a>, p. 36.<\/li>\n<\/ul>\n<p><a name=\"ej5\"><\/a><\/p>\n<h3>5. Si (\u2203z \u2208 \u211d)[x &lt; z &lt; y], entonces x &lt; y<\/h3>\n<p>Demostrar con Lean4 que si &#92;((\u2203z \u2208 \u211d)[x &lt; z &lt; y]&#92;), entonces &#92;(x &lt; y&#92;).<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\nvariable (x y : \u211d)\n\nexample : (\u2203 z : \u211d, x < z \u2227 z < y) \u2192 x < y :=\nby sorry\n<\/pre>\n<p><b>Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p>Sea &#92;(z&#92;) tal que verifica las siguientes relaciones:<br \/>\n&#92;begin{align}<br \/>\n   x &lt; z &#92;tag{1} &#92;&#92;<br \/>\n   z &lt; y &#92;tag{2}<br \/>\n&#92;end{align}<br \/>\nAplicando la propiedad transitiva a (1) y (2) se tiene que<br \/>\n&#92;[ x &lt; y &#92;]<\/p>\n<p><b>Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\nvariable (x y : \u211d)\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (\u2203 z : \u211d, x < z \u2227 z < y) \u2192 x < y :=\nby\n  rintro \u27e8z, h1 : x < z, h2 : z < y\u27e9\n  show x < y\n  exact lt_trans h1 h2\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (\u2203 z : \u211d, x < z \u2227 z < y) \u2192 x < y :=\nby\n  rintro \u27e8z, h1, h2\u27e9\n  exact lt_trans h1 h2\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (\u2203 z : \u211d, x < z \u2227 z < y) \u2192 x < y :=\nfun \u27e8_, h1, h2\u27e9 \u21a6 lt_trans h1 h2\n\n-- Lemas usados\n-- ============\n\n-- variable (a b c : \u211d)\n-- #check (lt_trans : a < b \u2192 b < c \u2192 a < c)\n<\/pre>\n<p><b>Demostraciones interactivas<\/b><\/p>\n<p>Se puede interactuar con las demostraciones anteriores en <a href=\"https:\/\/live.lean-lang.org\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus2\/main\/src\/Menor_por_intermedio.lean\" rel=\"noopener noreferrer\" target=\"_blank\">Lean 4 Web<\/a>.<\/p>\n<p><b>Referencias<\/b><\/p>\n<ul>\n<li> J. Avigad y P. Massot. <a href=\"https:\/\/bit.ly\/3U4UjBk\">Mathematics in Lean<\/a>, p. 36.<\/li>\n<\/ul>\n<p><a name=\"ej6\"><\/a><\/p>\n<h3>6. Existen n\u00fameros primos m y n tales que 4 &lt; m &lt; n &lt; 10<\/h3>\n<p>Demostrar con Lean4 que existen n\u00fameros primos &#92;(m&#92;) y &#92;(n&#92;) tales que &#92;(4 &lt; m &lt; n &lt; 10&#92;).<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Nat.Prime\nimport Mathlib.Tactic\n\nexample :\n  \u2203 m n : \u2115, 4 < m \u2227 m < n \u2227 n < 10 \u2227 Nat.Prime m \u2227 Nat.Prime n :=\nby sorry\n<\/pre>\n<p><b>Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p>Basta considerar los n\u00fameros &#92;(5&#92;) y &#92;(7&#92;), ya que son primos y &#92;(4 &lt; 5 &lt; 7 &lt; 10&#92;).<\/p>\n<p><b>Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Nat.Prime\nimport Mathlib.Tactic\n\nexample :\n  \u2203 m n : \u2115, 4 < m \u2227 m < n \u2227 n < 10 \u2227 Nat.Prime m \u2227 Nat.Prime n :=\nby\n  use 5, 7\n  norm_num\n<\/pre>\n<p><b>Demostraciones interactivas<\/b><\/p>\n<p>Se puede interactuar con las demostraciones anteriores en <a href=\"https:\/\/live.lean-lang.org\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus2\/main\/src\/Primos_intermedios.lean\" rel=\"noopener noreferrer\" target=\"_blank\">Lean 4 Web<\/a>.<\/p>\n<p><b>Referencias<\/b><\/p>\n<ul>\n<li> J. Avigad y P. Massot. <a href=\"https:\/\/bit.ly\/3U4UjBk\">Mathematics in Lean<\/a>, p. 36.<\/li>\n<\/ul>\n<p><a name=\"ej7\"><\/a><\/p>\n<h3>7. En \u211d, x \u2264 y \u2227 x \u2260 y \u2192 x \u2264 y \u2227 y \u2270 x<\/h3>\n<p>Demostrar con Lean4 que. en &#92;(\u211d&#92;), &#92;(x \u2264 y \u2227 x \u2260 y \u2192 x \u2264 y \u2227 y \u2270 x&#92;).<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\nvariable (x y : \u211d)\n\nexample : x \u2264 y \u2227 x \u2260 y \u2192 x \u2264 y \u2227 \u00ac y \u2264 x :=\nby sorry\n<\/pre>\n<p><b>Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p>Supongamos que<br \/>\n&#92;begin{align}<br \/>\n   x \u2264 y &#92;tag{1} &#92;&#92;<br \/>\n   x \u2260 y &#92;tag{2}<br \/>\n&#92;end{align}<br \/>\nEntonces, se tiene &#92;(x \u2264 y&#92;) (por (1)) y, para probar &#92;(y \u2270 x&#92;), supongamos que<br \/>\n&#92;[ y \u2264 x &#92;tag{3}&#92;]<br \/>\nAplicando la propiedad antim\u00e9trica a (1) y (3), se obtiene que &#92;(x = y&#92;), en contradicci\u00f3n con (2).<\/p>\n<p><b>Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\nvariable (x y : \u211d)\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample : x \u2264 y \u2227 x \u2260 y \u2192 x \u2264 y \u2227 \u00ac y \u2264 x :=\nby\n  rintro \u27e8h1 : x \u2264 y, h2 : x \u2260 y\u27e9\n  constructor\n  . show x \u2264 y\n    exact h1\n  . show \u00ac y \u2264 x\n    rintro h3 : y \u2264 x\n    -- \u22a2 False\n    have h4 : x = y := le_antisymm h1 h3\n    show False\n    exact h2 h4\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : x \u2264 y \u2227 x \u2260 y \u2192 x \u2264 y \u2227 \u00ac y \u2264 x :=\nby\n  rintro \u27e8h1 : x \u2264 y, h2 : x \u2260 y\u27e9\n  -- \u22a2 x \u2264 y \u2227 \u00acy \u2264 x\n  constructor\n  . show x \u2264 y\n    exact h1\n  . show \u00ac y \u2264 x\n    rintro h3 : y \u2264 x\n    -- \u22a2 False\n    show False\n    exact h2 (le_antisymm h1 h3)\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : x \u2264 y \u2227 x \u2260 y \u2192 x \u2264 y \u2227 \u00ac y \u2264 x :=\nby\n  rintro \u27e8h1 : x \u2264 y, h2 : x \u2260 y\u27e9\n  constructor\n  . show x \u2264 y\n    exact h1\n  . show \u00ac y \u2264 x\n    exact fun h3 \u21a6 h2 (le_antisymm h1 h3)\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample : x \u2264 y \u2227 x \u2260 y \u2192 x \u2264 y \u2227 \u00ac y \u2264 x :=\nby\n  rintro \u27e8h1, h2\u27e9\n  exact \u27e8h1, fun h3 \u21a6 h2 (le_antisymm h1 h3)\u27e9\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample : x \u2264 y \u2227 x \u2260 y \u2192 x \u2264 y \u2227 \u00ac y \u2264 x :=\n  fun \u27e8h1, h2\u27e9 \u21a6 \u27e8h1, fun h3 \u21a6 h2 (le_antisymm h1 h3)\u27e9\n\n-- 6\u00aa demostraci\u00f3n\n-- ===============\n\nexample : x \u2264 y \u2227 x \u2260 y \u2192 x \u2264 y \u2227 \u00ac y \u2264 x :=\nby\n  rintro \u27e8h1 : x \u2264 y, h2 : x \u2260 y\u27e9\n  use h1\n  exact fun h3 \u21a6 h2 (le_antisymm h1 h3)\n\n-- 7\u00aa demostraci\u00f3n\n-- ===============\n\nexample : x \u2264 y \u2227 x \u2260 y \u2192 x \u2264 y \u2227 \u00ac y \u2264 x :=\nby\n  rintro \u27e8h1, h2\u27e9\n  -- h1 : x \u2264 y\n  -- h2 : x \u2260 y\n  -- \u22a2 x \u2264 y \u2227 \u00acy \u2264 x\n  use h1\n  -- \u00acy \u2264 x\n  contrapose! h2\n  -- h2 : y \u2264 x\n  -- \u22a2 x = y\n  apply le_antisymm h1 h2\n\n-- Lemas usados\n-- ============\n\n-- #check (le_antisymm : x \u2264 y \u2192 y \u2264 x \u2192 x = y)\n<\/pre>\n<p><b>Demostraciones interactivas<\/b><\/p>\n<p>Se puede interactuar con las demostraciones anteriores en <a href=\"https:\/\/live.lean-lang.org\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus2\/main\/src\/Entre_desigualdades.lean\" rel=\"noopener noreferrer\" target=\"_blank\">Lean 4 Web<\/a>.<\/p>\n<p><b>Referencias<\/b><\/p>\n<ul>\n<li> J. Avigad y P. Massot. <a href=\"https:\/\/bit.ly\/3U4UjBk\">Mathematics in Lean<\/a>, p. 36.<\/li>\n<\/ul>\n<p><a name=\"ej8\"><\/a><\/p>\n<h3>8. En \u211d, si x \u2264 y, entonces y \u2270 x \u2194 x \u2260 y<\/h3>\n<p>Demostrar con Lean4 que si &#92;(x&#92;) e &#92;(y&#92;) son n\u00fameros reales tales que &#92;(x \u2264 y&#92;), entonces &#92;(y \u2270 x \u2194 x \u2260 y&#92;).<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\nvariable {x y : \u211d}\n\nexample\n  (h : x \u2264 y)\n  : \u00acy \u2264 x \u2194 x \u2260 y :=\nby sorry\n<\/pre>\n<p><b>Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p>Para demostrar la equivalencia, demostraremos cada una de las implicaciones.<\/p>\n<p>Para demostrar la primera, supongamos que &#92;(y \u2270 x&#92;) y que &#92;(x = y&#92;). Entonces, &#92;(y \u2264 x&#92;) que es una contradicci\u00f3n.<\/p>\n<p>Para demostrar la segunda, supongamos que &#92;(x \u2260 y&#92;) y que &#92;(y \u2264 x&#92;). Entonces, por la hip\u00f3tesis y la antisimetr\u00eda, se tiene que &#92;(x = y&#92;) lo que es una contradicci\u00f3n.<\/p>\n<p><b>Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\nvariable {x y : \u211d}\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : x \u2264 y)\n  : \u00acy \u2264 x \u2194 x \u2260 y :=\nby\n  constructor\n  . show \u00acy \u2264 x \u2192 x \u2260 y\n    { intro h1\n      -- h1 : \u00acy \u2264 x\n      -- \u22a2 x \u2260 y\n      intro h2\n      -- h2 : x = y\n      -- \u22a2 False\n      have h3 : y \u2264 x := by rw [h2]\n      show False\n      exact h1 h3 }\n  . show x \u2260 y \u2192 \u00acy \u2264 x\n    { intro h1\n      -- h1 : x \u2260 y\n      -- \u22a2 \u00acy \u2264 x\n      intro h2\n      -- h2 : y \u2264 x\n      -- \u22a2 False\n      have h3 : x = y := le_antisymm h h2\n      show False\n      exact h1 h3 }\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : x \u2264 y)\n  : \u00acy \u2264 x \u2194 x \u2260 y :=\nby\n  constructor\n  . show \u00acy \u2264 x \u2192 x \u2260 y\n    { intro h1\n      -- h1 : \u00acy \u2264 x\n      -- \u22a2 x \u2260 y\n      intro h2\n      -- h2 : x = y\n      -- \u22a2 False\n      show False\n      exact h1 (by rw [h2]) }\n  . show x \u2260 y \u2192 \u00acy \u2264 x\n    { intro h1\n      -- h1 : x \u2260 y\n      -- \u22a2 \u00acy \u2264 x\n      intro h2\n      -- h2 : y \u2264 x\n      -- \u22a2 False\n      show False\n      exact h1 (le_antisymm h h2) }\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : x \u2264 y)\n  : \u00acy \u2264 x \u2194 x \u2260 y :=\nby\n  constructor\n  . show \u00acy \u2264 x \u2192 x \u2260 y\n    { intro h1 h2\n      exact h1 (by rw [h2]) }\n  . show x \u2260 y \u2192 \u00acy \u2264 x\n    { intro h1 h2\n      exact h1 (le_antisymm h h2) }\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : x \u2264 y)\n  : \u00acy \u2264 x \u2194 x \u2260 y :=\nby\n  constructor\n  . intro h1 h2\n    exact h1 (by rw [h2])\n  . intro h1 h2\n    exact h1 (le_antisymm h h2)\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : x \u2264 y)\n  : \u00acy \u2264 x \u2194 x \u2260 y :=\nby\n  constructor\n  . exact fun h1 h2 \u21a6 h1 (by rw [h2])\n  . exact fun h1 h2 \u21a6 h1 (le_antisymm h h2)\n\n-- 6\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : x \u2264 y)\n  : \u00acy \u2264 x \u2194 x \u2260 y :=\n  \u27e8fun h1 h2 \u21a6 h1 (by rw [h2]),\n   fun h1 h2 \u21a6 h1 (le_antisymm h h2)\u27e9\n\n-- 7\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : x \u2264 y)\n  : \u00acy \u2264 x \u2194 x \u2260 y :=\nby\n  constructor\n  . show \u00acy \u2264 x \u2192 x \u2260 y\n    { intro h1\n      -- h1 : \u00acy \u2264 x\n      -- \u22a2 x \u2260 y\n      contrapose! h1\n      -- h1 : x = y\n      -- \u22a2 y \u2264 x\n      calc y = x := h1.symm\n           _ \u2264 x := by rfl }\n  . show x \u2260 y \u2192 \u00acy \u2264 x\n    { intro h2\n      -- h2 : x \u2260 y\n      -- \u22a2 \u00acy \u2264 x\n      contrapose! h2\n      -- h2 : y \u2264 x\n      -- \u22a2 x = y\n      show x = y\n      exact le_antisymm h h2 }\n\n-- 8\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : x \u2264 y)\n  : \u00acy \u2264 x \u2194 x \u2260 y :=\nby\n  constructor\n  \u00b7 -- \u22a2 \u00acy \u2264 x \u2192 x \u2260 y\n    contrapose!\n    -- \u22a2 x = y \u2192 y \u2264 x\n    rintro rfl\n    -- \u22a2 x \u2264 x\n    rfl\n  . -- \u22a2 x \u2260 y \u2192 \u00acy \u2264 x\n    contrapose!\n    -- \u22a2 y \u2264 x \u2192 x = y\n    exact le_antisymm h\n<\/pre>\n<p><b>Demostraciones interactivas<\/b><\/p>\n<p>Se puede interactuar con las demostraciones anteriores en <a href=\"https:\/\/live.lean-lang.org\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus2\/main\/src\/CNS_de_distintos.lean\" rel=\"noopener noreferrer\" target=\"_blank\">Lean 4 Web<\/a>.<\/p>\n<p><b>Referencias<\/b><\/p>\n<ul>\n<li> J. Avigad y P. Massot. <a href=\"https:\/\/bit.ly\/3U4UjBk\">Mathematics in Lean<\/a>, p. 36.<\/li>\n<\/ul>\n<p><a name=\"ej9\"><\/a><\/p>\n<h3>9. En \u211d, x\u00b2 + y\u00b2 = 0 \u2194 x = 0 \u2227 y = 0<\/h3>\n<p>Demostrar con Lean4 que si &#92;(x, y \u2208 \u211d&#92;), entonces<br \/>\n&#92;[ x^2 + y^2 = 0 \u2194 x = 0 \u2227 y = 0 &#92;]<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\nvariable {x y : \u211d}\n\nexample : x^2 + y^2 = 0 \u2194 x = 0 \u2227 y = 0 :=\nby sorry\n<\/pre>\n<p><b>Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p>En la demostraci\u00f3n usaremos el siguiente lema auxiliar<br \/>\n&#92;[ (\u2200 x, y \u2208 \u211d)[x\u00b2 + y\u00b2 = 0 \u2192 x = 0] &#92;]<\/p>\n<p>Para la primera implicaci\u00f3n, supongamos que<br \/>\n&#92;[ x\u00b2 + y\u00b2 = 0 &#92;tag{1} &#92;]<br \/>\nEntonces, por el lema auxiliar,<br \/>\n&#92;[ x = 0 &#92;tag{2} &#92;]<br \/>\nAdem\u00e1s, aplicando la conmutativa a (1), se tiene<br \/>\n&#92;[ y\u00b2 + x\u00b2 = 0 &#92;]<br \/>\ny, por el lema auxiliar,<br \/>\n&#92;[ y = 0 &#92;tag{3} &#92;]<br \/>\nDe (2) y (3) se tiene<br \/>\n&#92;[ x = 0 \u2227 y = 0 &#92;]<\/p>\n<p>Para la segunda implicaci\u00f3n, supongamos que<br \/>\n&#92;[ x = 0 \u2227 y = 0 &#92;]<br \/>\nPor tanto,<br \/>\n&#92;begin{align}<br \/>\n   x\u00b2 + y\u00b2 &amp;= 0\u00b2 + 0\u00b2 &#92;&#92;<br \/>\n           &amp;= 0<br \/>\n&#92;end{align}<\/p>\n<p>En la demostraci\u00f3n del lema auxiliar se usar\u00e1n los siguientes lemas<br \/>\n&#92;begin{align}<br \/>\n   &amp;(\u2200 x \u2208 \u211d)(\u2200 n \u2208 \u2115)[x^n = 0 \u2192 x = 0]  &#92;tag{L1} &#92;&#92;<br \/>\n   &amp;(\u2200 x, y \u2208 \u211d)[x \u2264 y \u2192 y \u2264 x \u2192 x = y]  &#92;tag{L2} &#92;&#92;<br \/>\n   &amp;(\u2200 x, y \u2208 \u211d)[0 \u2264 y \u2192 x \u2264 x + y]      &#92;tag{L3} &#92;&#92;<br \/>\n   &amp;(\u2200 x \u2208 \u211d)[0 \u2264 x\u00b2]                    &#92;tag{L4}<br \/>\n&#92;end{align}<\/p>\n<p>Por el lema L1, para demostrar el lema auxiliar basta demostrar<br \/>\n&#92;[ x\u00b2 = 0 &#92;tag{1} &#92;]<br \/>\ny, por el lema L2, basta demostrar las siguientes desigualdades<br \/>\n&#92;begin{align}<br \/>\n    &amp;x\u00b2 \u2264 0 &#92;tag{2} &#92;&#92;<br \/>\n    &amp;0 \u2264 x\u00b2 &#92;tag{3}<br \/>\n&#92;end{align}<\/p>\n<p>La prueba de la (2) es<br \/>\n&#92;begin{align}<br \/>\n   x\u00b2 &amp;\u2264 x\u00b2 + y\u00b2   &amp;&amp;&#92;text{[por L3 y L4]} &#92;&#92;<br \/>\n      &amp;= 0         &amp;&amp;&#92;text{[por la hip\u00f3tesis]}<br \/>\n&#92;end{align}<\/p>\n<p>La (3) se tiene por el lema L4.<\/p>\n<p><b>Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\nvariable {x y : \u211d}\n\n-- 1\u00aa demostraci\u00f3n del lema auxiliar\n-- =================================\n\nexample\n  (h : x^2 + y^2 = 0)\n  : x = 0 :=\nby\n  have h' : x^2 = 0 := by\n  { apply le_antisymm\n    . show x ^ 2 \u2264 0\n      calc x ^ 2 \u2264 x^2 + y^2 := by simp [le_add_of_nonneg_right,\n                                         pow_two_nonneg]\n               _ = 0         := by exact h\n    . show 0 \u2264 x ^ 2\n      apply pow_two_nonneg }\n  show x = 0\n  exact pow_eq_zero h'\n\n-- 2\u00aa demostraci\u00f3n lema auxiliar\n-- =============================\n\nexample\n  (h : x^2 + y^2 = 0)\n  : x = 0 :=\nby\n  have h' : x^2 = 0 := by\n  { apply le_antisymm\n    . -- \u22a2 x ^ 2 \u2264 0\n      calc x ^ 2 \u2264 x^2 + y^2 := by simp [le_add_of_nonneg_right,\n                                         pow_two_nonneg]\n               _ = 0         := by exact h\n    . -- \u22a2 0 \u2264 x ^ 2\n      apply pow_two_nonneg }\n  exact pow_eq_zero h'\n\n-- 3\u00aa demostraci\u00f3n lema auxiliar\n-- =============================\n\nlemma aux\n  (h : x^2 + y^2 = 0)\n  : x = 0 :=\n  have h' : x ^ 2 = 0 := by linarith [pow_two_nonneg x, pow_two_nonneg y]\n  pow_eq_zero h'\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample : x^2 + y^2 = 0 \u2194 x = 0 \u2227 y = 0 :=\nby\n  constructor\n  . -- \u22a2 x ^ 2 + y ^ 2 = 0 \u2192 x = 0 \u2227 y = 0\n    intro h\n    -- h : x ^ 2 + y ^ 2 = 0\n    -- \u22a2 x = 0 \u2227 y = 0\n    constructor\n    . -- \u22a2 x = 0\n      exact aux h\n    . -- \u22a2 y = 0\n      rw [add_comm] at h\n      -- h : x ^ 2 + y ^ 2 = 0\n      exact aux h\n  . -- \u22a2 x = 0 \u2227 y = 0 \u2192 x ^ 2 + y ^ 2 = 0\n    intro h1\n    -- h1 : x = 0 \u2227 y = 0\n    -- \u22a2 x ^ 2 + y ^ 2 = 0\n    rcases h1 with \u27e8h2, h3\u27e9\n    -- h2 : x = 0\n    -- h3 : y = 0\n    rw [h2, h3]\n    -- \u22a2 0 ^ 2 + 0 ^ 2 = 0\n    norm_num\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : x^2 + y^2 = 0 \u2194 x = 0 \u2227 y = 0 :=\nby\n  constructor\n  . -- \u22a2 x ^ 2 + y ^ 2 = 0 \u2192 x = 0 \u2227 y = 0\n    intro h\n    -- h : x ^ 2 + y ^ 2 = 0\n    -- \u22a2 x = 0 \u2227 y = 0\n    constructor\n    . -- \u22a2 x = 0\n      exact aux h\n    . -- \u22a2 y = 0\n      rw [add_comm] at h\n      -- h : x ^ 2 + y ^ 2 = 0\n      exact aux h\n  . -- \u22a2 x = 0 \u2227 y = 0 \u2192 x ^ 2 + y ^ 2 = 0\n    rintro \u27e8h1, h2\u27e9\n    -- h1 : x = 0\n    -- h2 : y = 0\n    -- \u22a2 x ^ 2 + y ^ 2 = 0\n    rw [h1, h2]\n    -- \u22a2 0 ^ 2 + 0 ^ 2 = 0\n    norm_num\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : x ^ 2 + y ^ 2 = 0 \u2194 x = 0 \u2227 y = 0 := by\n  constructor\n  \u00b7 -- \u22a2 x ^ 2 + y ^ 2 = 0 \u2192 x = 0 \u2227 y = 0\n    intro h\n    -- h : x ^ 2 + y ^ 2 = 0\n    -- \u22a2 x = 0 \u2227 y = 0\n    constructor\n    \u00b7 -- x = 0\n      exact aux h\n    . -- \u22a2 y = 0\n      rw [add_comm] at h\n      -- h : y ^ 2 + x ^ 2 = 0\n      exact aux h\n  . -- \u22a2 x = 0 \u2227 y = 0 \u2192 x ^ 2 + y ^ 2 = 0\n    rintro \u27e8rfl, rfl\u27e9\n    -- \u22a2 0 ^ 2 + 0 ^ 2 = 0\n    norm_num\n\n-- Lemas usados\n-- ============\n\n-- #check (add_comm x y : x + y = y + x)\n-- #check (le_add_of_nonneg_right : 0 \u2264 y \u2192 x \u2264 x + y)\n-- #check (le_antisymm : x \u2264 y \u2192 y \u2264 x \u2192 x = y)\n-- #check (pow_eq_zero : \u2200 {n : \u2115}, x ^ n = 0 \u2192 x = 0)\n-- #check (pow_two_nonneg x : 0 \u2264 x ^ 2)\n<\/pre>\n<p><b>Demostraciones interactivas<\/b><\/p>\n<p>Se puede interactuar con las demostraciones anteriores en <a href=\"https:\/\/live.lean-lang.org\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus2\/main\/src\/Suma_nula_de_dos_cuadrados.lean\" rel=\"noopener noreferrer\" target=\"_blank\">Lean 4 Web<\/a>.<\/p>\n<p><b>Referencias<\/b><\/p>\n<ul>\n<li> J. Avigad y P. Massot. <a href=\"https:\/\/bit.ly\/3U4UjBk\">Mathematics in Lean<\/a>, p. 37.<\/li>\n<\/ul>\n<p><a name=\"ej10\"><\/a><\/p>\n<h3>10. Si |x + 3| &lt; 5, entonces -8 &lt; x &lt; 2<\/h3>\n<p>Demostrar con Lean4 que si &#92;(|x + 3| &lt; 5&#92;), entonces &#92;(-8 &lt; x &lt; 2&#92;).<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\nvariable (x y : \u211d)\n\nexample\n  : |x + 3| < 5 \u2192 -8 < x \u2227 x < 2 :=\nby sorry\n<\/pre>\n<p><b>Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p>Supongamos que<br \/>\n&#92;[ |x + 3| &lt; 5 &#92;]<br \/>\nentonces<br \/>\n&#92;[ -5 &lt; x + 3 &lt; 5 &#92;]<br \/>\npor tanto<br \/>\n&#92;[ -8 &lt; x &lt; 2 &#92;]<\/p>\n<p><b>Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\nvariable (x y : \u211d)\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  : |x + 3| < 5 \u2192 -8 < x \u2227 x < 2 :=\nby\n  rw [abs_lt]\n  -- \u22a2 -5 < x + 3 \u2227 x + 3 < 5 \u2192 -8 < x \u2227 x < 2\n  intro h\n  -- h : -5 < x + 3 \u2227 x + 3 < 5\n  -- \u22a2 -8 < x \u2227 x < 2\n  constructor\n  . -- \u22a2 -8 < x\n    linarith\n  . -- x < 2\n    linarith\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  : |x + 3| < 5 \u2192 -8 < x \u2227 x < 2 :=\nby\n  rw [abs_lt]\n  intro h\n  constructor <;> linarith\n\n-- Comentario: La composici\u00f3n (constructor <;> linarith) aplica constructor y a\n-- continuaci\u00f3n le aplica linarith a cada subojetivo.\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  : |x + 3| < 5 \u2192 -8 < x \u2227 x < 2 :=\nby\n  rw [abs_lt]\n  exact fun _ \u21a6 \u27e8by linarith, by linarith\u27e9\n\n-- Lemas usados\n-- ============\n\n-- #check (abs_lt: |x| < y \u2194 -y < x \u2227 x < y)\n<\/pre>\n<p><b>Demostraciones interactivas<\/b><\/p>\n<p>Se puede interactuar con las demostraciones anteriores en <a href=\"https:\/\/live.lean-lang.org\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus2\/main\/src\/Acotacion_del_valor_absoluto.lean\" rel=\"noopener noreferrer\" target=\"_blank\">Lean 4 Web<\/a>.<\/p>\n<p><b>Referencias<\/b><\/p>\n<ul>\n<li> J. Avigad y P. Massot. <a href=\"https:\/\/bit.ly\/3U4UjBk\">Mathematics in Lean<\/a>, p. 37.<\/li>\n<\/ul>\n<p><a name=\"ej11\"><\/a><\/p>\n<h3>11. 3 divide al m\u00e1ximo com\u00fan divisor de 6 y 15<\/h3>\n<p>Demostrar con Lean4 que 3 divide al m\u00e1ximo com\u00fan divisor de 6 y 15.<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\nimport Mathlib.Data.Nat.GCD.Basic\n\nopen Nat\n\nexample : 3 \u2223 gcd 6 15 :=\nby sorry\n<\/pre>\n<p><b>Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p>Se usar\u00e1 el siguiente lema<br \/>\n&#92;[ (\u2200 k, m, n \u2208 \u2115)[k \u2223 \\gcd(m, n) \u2194 k \u2223 m \u2227 k \u2223 n] &#92;]<\/p>\n<p>Por el lema,<br \/>\n&#92;[ 3 \u2223 \\gcd(6, 15) &#92;]<br \/>\nse reduce a<br \/>\n&#92;[ 3 \u2223 6 \u2227 3 \u2223 15 &#92;]<br \/>\nque se verifican f\u00e1cilmente.<\/p>\n<p><b>Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\nimport Mathlib.Data.Nat.GCD.Basic\n\nopen Nat\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample : 3 \u2223 gcd 6 15 :=\nby\n  rw [dvd_gcd_iff]\n  -- \u22a2 3 \u2223 6 \u2227 3 \u2223 15\n  constructor\n  . -- 3 \u2223 6\n    norm_num\n  . -- \u22a2 3 \u2223 15\n    norm_num\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : 3 \u2223 gcd 6 15 :=\nby\n  rw [dvd_gcd_iff]\n  -- \u22a2 3 \u2223 6 \u2227 3 \u2223 15\n  constructor <;> norm_num\n\n-- Lemas usados\n-- ============\n\n-- variable (k m n : \u2115)\n-- #check (dvd_gcd_iff : k \u2223 gcd m n \u2194 k \u2223 m \u2227 k \u2223 n)\n<\/pre>\n<p><b>Demostraciones interactivas<\/b><\/p>\n<p>Se puede interactuar con las demostraciones anteriores en <a href=\"https:\/\/live.lean-lang.org\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus2\/main\/src\/Divisor_del_mcd.lean\" rel=\"noopener noreferrer\" target=\"_blank\">Lean 4 Web<\/a>.<\/p>\n<p><b>Referencias<\/b><\/p>\n<ul>\n<li> J. Avigad y P. Massot. <a href=\"https:\/\/bit.ly\/3U4UjBk\">Mathematics in Lean<\/a>, p. 37.<\/li>\n<\/ul>\n","protected":false},"excerpt":{"rendered":"<p>Estas 3 \u00faltimas semanas he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades: 1. {x \u2264 y, y \u2270 x} \u22a2 x \u2264 y \u2227 x \u2260 y 2. x \u2264 y \u2227 x \u2260 y \u22a2 y \u2270 x 3. Si (m \u2223 n \u2227 m \u2260 n), entonces (m \u2223&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"closed","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[335],"tags":[],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/8062"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/comments?post=8062"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/8062\/revisions"}],"predecessor-version":[{"id":8064,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/8062\/revisions\/8064"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=8062"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=8062"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=8062"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}