{"id":8076,"date":"2024-01-27T10:23:59","date_gmt":"2024-01-27T09:23:59","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=8076"},"modified":"2024-01-27T10:27:59","modified_gmt":"2024-01-27T09:27:59","slug":"27-ene-24","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/27-ene-24\/","title":{"rendered":"La semana en Calculemus (27 de enero de 2024)"},"content":{"rendered":"\n<p>Esta semana 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. En \u211d, x\u00b2 = y\u00b2 \u2192 x = y \u2228 x = -y<\/a><\/li>\n<li><a href=\"#ej2\">2. \u00ac\u00acP \u2192 P<\/a><\/li>\n<li><a href=\"#ej3\">3. (P \u2192 Q) \u2194 \u00acP \u2228 Q<\/a><\/li>\n<li><a href=\"#ej4\">4. Existen infinitos n\u00fameros primos<\/a><\/li>\n<li><a href=\"#ej5\">5. Si n\u00b2 es par, entonces n es par<\/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. En \u211d, x\u00b2 = y\u00b2 \u2192 x = y \u2228 x = -y<\/h3>\n<p>Demostrar con Lean4 que en &#92;(\u211d&#92;),<br \/>\n&#92;[x\u00b2 = y\u00b2 \u2192 x = y \u2228 x = -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^2 = y^2)\n  : x = y \u2228 x = -y :=\nby sorry\n<\/pre>\n<p><b>1. Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p>Usaremos los siguientes lemas<br \/>\n&#92;begin{align}<br \/>\n   &amp;(\u2200 x \u2208 \u211d)[x &#8211; x = 0]                                           &#92;tag{L1} &#92;&#92;<br \/>\n   &amp;(\u2200 x, y \u2208 \u211d)[xy = 0 \u2192 x = 0 \u2228 y = 0]                           &#92;tag{L2} &#92;&#92;<br \/>\n   &amp;(\u2200 x, y \u2208 \u211d)[x &#8211; y = 0 \u2194 x = y]                                &#92;tag{L3} &#92;&#92;<br \/>\n   &amp;(\u2200 x, y \u2208 \u211d)[x + y = 0 \u2192 x = -y]                               &#92;tag{L4}<br \/>\n&#92;end{align}<\/p>\n<p>Se tiene que<br \/>\n&#92;begin{align}<br \/>\n   (x &#8211; y)(x + y) &amp;= x\u00b2 &#8211; y\u00b2    &#92;&#92;<br \/>\n                  &amp;= y\u00b2 &#8211; y\u00b2    &amp;&amp;&#92;text{[por la hip\u00f3tesis]} &#92;&#92;<br \/>\n                  &amp;= 0          &amp;&amp;&#92;text{[por L1]}<br \/>\n&#92;end{align}<br \/>\ny, por el lema L2, se tiene que<br \/>\n&#92;[ x &#8211; y = 0 \u2228 x + y = 0 &#92;]<\/p>\n<p>Acabaremos la demostraci\u00f3n por casos.<\/p>\n<p>Primer caso:<br \/>\n&#92;begin{align}<br \/>\n  x &#8211; y = 0 &amp;\u27f9 x = y             &amp;&amp;&#92;text{[por L3]} &#92;&#92;<br \/>\n            &amp;\u27f9 x = y \u2228 x = -y<br \/>\n&#92;end{align}<\/p>\n<p>Segundo caso:<br \/>\n&#92;begin{align}<br \/>\n  x + y = 0 &amp;\u27f9 x = -y            &amp;&amp;&#92;text{[por L4]} &#92;&#92;<br \/>\n            &amp;\u27f9 x = y \u2228 x = -y<br \/>\n&#92;end{align}<\/p>\n<p><b>2. 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^2 = y^2)\n  : x = y \u2228 x = -y :=\nby\n  have h1 : (x - y) * (x + y) = 0 := by\n    calc (x - y) * (x + y) = x^2 - y^2 := by ring\n                         _ = y^2 - y^2 := by rw [h]\n                         _ = 0         := sub_self (y ^ 2)\n  have h2 : x - y = 0 \u2228 x + y = 0 := by\n    apply eq_zero_or_eq_zero_of_mul_eq_zero h1\n  rcases h2 with h3 | h4\n  . -- h3 : x - y = 0\n    left\n    -- \u22a2 x = y\n    exact sub_eq_zero.mp h3\n  . -- h4 : x + y = 0\n    right\n    -- \u22a2 x = -y\n    exact eq_neg_of_add_eq_zero_left h4\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : x^2 = y^2)\n  : x = y \u2228 x = -y :=\nby\n  have h1 : (x - y) * (x + y) = 0 := by nlinarith\n  have h2 : x - y = 0 \u2228 x + y = 0 := by aesop\n  rcases h2 with h3 | h4\n  . -- h3 : x - y = 0\n    left\n    -- \u22a2 x = y\n    linarith\n  . -- h4 : x + y = 0\n    right\n    -- \u22a2 x = -y\n    linarith\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : x^2 = y^2)\n  : x = y \u2228 x = -y :=\nsq_eq_sq_iff_eq_or_eq_neg.mp h\n\n-- Lemas usados\n-- ============\n\n-- #check (eq_neg_of_add_eq_zero_left : x + y = 0 \u2192 x = -y)\n-- #check (eq_zero_or_eq_zero_of_mul_eq_zero : x * y = 0 \u2192 x = 0 \u2228 y = 0)\n-- #check (sq_eq_sq_iff_eq_or_eq_neg : x ^ 2 = y ^ 2 \u2194 x = y \u2228 x = -y)\n-- #check (sub_eq_zero : x - y = 0 \u2194 x = y)\n-- #check (sub_self x : x - x = 0)\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\/Cuadrado_igual_a_cuadrado.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. 39.<\/li>\n<\/ul>\n<p><b>3. Demostraciones con Isabelle\/HOL<\/b><\/p>\n<pre lang=\"isar\">\ntheory Cuadrado_igual_a_uno\n  imports Main HOL.Real\nbegin\n\n(* 1\u00aa demostraci\u00f3n *)\nlemma\n  fixes x :: real\n  assumes \"x^2 = 1\"\n  shows \"x = 1 \u2228 x = -1\"\nproof -\n  have \"(x - 1) * (x + 1) = x^2 - 1\"\n    by algebra\n  also have \"... = 0\"\n    using assms by simp\n  finally have \"(x - 1) * (x + 1) = 0\" .\n  moreover\n  { assume \"(x - 1) = 0\"\n    then have \"x = 1\"\n      by simp }\n  moreover\n  { assume \"(x + 1) = 0\"\n    then have \"x = -1\"\n      by simp }\n  ultimately show \"x = 1 \u2228 x = -1\"\n    by auto\nqed\n\n(* 2\u00aa demostraci\u00f3n *)\nlemma\n  fixes x :: real\n  assumes \"x^2 = 1\"\n  shows \"x = 1 \u2228 x = -1\"\nproof -\n  have \"(x - 1) * (x + 1) = x^2 - 1\"\n    by algebra\n  also have \"... = 0\"\n    using assms by simp\n  finally have \"(x - 1) * (x + 1) = 0\" .\n  then show \"x = 1 \u2228 x = -1\"\n    by auto\nqed\n\n(* 3\u00aa demostraci\u00f3n *)\nlemma\n  fixes x :: real\n  assumes \"x^2 = 1\"\n  shows \"x = 1 \u2228 x = -1\"\nproof -\n  have \"(x - 1) * (x + 1) = 0\"\n  proof -\n    have \"(x - 1) * (x + 1) = x^2 - 1\" by algebra\n    also have \"\u2026 = 0\" by (simp add: assms)\n    finally show ?thesis .\n  qed\n  then show \"x = 1 \u2228 x = -1\"\n    by auto\nqed\n\n(* 4\u00aa demostraci\u00f3n *)\nlemma\n  fixes x :: real\n  assumes \"x^2 = 1\"\n  shows \"x = 1 \u2228 x = -1\"\nusing assms power2_eq_1_iff by blast\n\nend\n<\/pre>\n<p><a name=\"ej2\"><\/a><\/p>\n<h3>2. \u00ac\u00acP \u2192 P<\/h3>\n<p>Demostrar con Lean4 que<br \/>\n&#92;[ \u00ac\u00acP \u2192 P &#92;]<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Tactic\nvariable (P : Prop)\n\nexample : \u00ac\u00acP \u2192 P :=\nby sorry\n<\/pre>\n<p><b>1. Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p>Supongamos que<br \/>\n&#92;[ \u00ac\u00acP  &#92;tag{1} &#92;]<\/p>\n<p>Por el principio del tercio excluso, se tiene<br \/>\n&#92;[ P \u2228 \u00acP &#92;]<br \/>\nlo que da lugar a dos casos.<\/p>\n<p>En el primer caso, se supone &#92;(P&#92;) que es lo que hay que demostrar.<\/p>\n<p>En el primer caso, se supone &#92;(\u00acP&#92;) que es una contradicci\u00f3n con (1).<\/p>\n<p><b>2. Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Tactic\nvariable (P : Prop)\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample : \u00ac\u00acP \u2192 P :=\nby\n  intro h1\n  -- h1 : \u00ac\u00acP\n  -- \u22a2 P\n  have h2 : P \u2228 \u00ac P := em P\n  rcases h2 with h3 | h4\n  . -- h3 : P\n    exact h3\n  . -- h4 : \u00acP\n    exfalso\n    -- \u22a2 False\n    exact h1 h4\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : \u00ac\u00acP \u2192 P :=\nby\n  intro h1\n  -- h1 : \u00ac\u00acP\n  -- \u22a2 P\n  rcases em P with h2 | h3\n  . -- h2 : P\n    exact h2\n  . -- h3 : \u00acP\n    exact absurd h3 h1\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : \u00ac\u00acP \u2192 P :=\nby\n  intro h1\n  -- h1 : \u00ac\u00acP\n  -- \u22a2 P\n  cases em P\n  . -- h2 : P\n    assumption\n  . -- h3 : \u00acP\n    contradiction\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample : \u00ac\u00acP \u2192 P :=\nby\n  intro h\n  by_cases P\n  . assumption\n  . contradiction\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample : \u00ac\u00acP \u2192 P :=\nby\n  intro h1\n  -- h1 : \u00ac\u00acP\n  -- \u22a2 P\n  by_contra h\n  -- h : \u00acP\n  -- \u22a2 False\n  exact h1 h\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample : \u00ac\u00acP \u2192 P :=\nby tauto\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_doble_negacion.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. 40.<\/li>\n<\/ul>\n<p><b>3. Demostraciones con Isabelle\/HOL<\/b><\/p>\n<pre lang=\"isar\">\ntheory Eliminacion_de_la_doble_negacion\n  imports Main\nbegin\n\n(* 1\u00aa demostraci\u00f3n *)\nlemma \"\u00ac\u00acP \u27f6 P\"\nproof\n  assume h1 : \"\u00ac\u00acP\"\n  have \"\u00acP \u2228 P\" by (rule excluded_middle)\n  then show \"P\"\n  proof\n    assume \"\u00acP\"\n    then show \"P\" using h1 by (simp only: notE)\n  next\n    assume \"P\"\n    then show \"P\" .\n  qed\nqed\n\n(* 2\u00aa demostraci\u00f3n *)\nlemma \"\u00ac\u00acP \u27f6 P\"\nproof\n  assume h1 : \"\u00ac\u00acP\"\n  show \"P\"\n  proof (rule ccontr)\n    assume \"\u00acP\"\n    then show False using h1 by simp\n  qed\nqed\n\n(* 3\u00aa demostraci\u00f3n *)\nlemma \"\u00ac\u00acP \u27f6 P\"\n  by simp\n\nend\n<\/pre>\n<p><a name=\"ej3\"><\/a><\/p>\n<h3>3. (P \u2192 Q) \u2194 \u00acP \u2228 Q<\/h3>\n<p>Demostrar con Lean4 que<br \/>\n&#92;[ (P \u2192 Q) \u2194 \u00acP \u2228 Q &#92;]<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Tactic\nvariable (P Q : Prop)\n\nexample\n  : (P \u2192 Q) \u2194 \u00acP \u2228 Q :=\nby sorry\n<\/pre>\n<p><b>1. Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p>Demostraremos cada una de las implicaciones.<\/p>\n<p>(==>) Supongamos que &#92;(P \u2192 Q&#92;). Distinguimos dos subcasos seg\u00fan el valor de &#92;(P&#92;).<\/p>\n<p>Primer subcaso: suponemos &#92;(P&#92;). Entonces, tenemos &#92;(Q&#92;) (porque &#92;(P \u2192 Q&#92;)) y. por tanto, &#92;(\u00acP \u2228 Q&#92;).<\/p>\n<p>Segundo subcaso: suponemos &#92;(\u00acP&#92;). Entonces. tenemos &#92;(\u00acP \u2228 Q&#92;).<\/p>\n<p>(&lt;==) Supongamos que &#92;(\u00acP \u2228 Q&#92;) y &#92;(P&#92;) y tenemos que demostrar &#92;(Q&#92;). Distinguimos dos subcasos seg\u00fan &#92;(\u00acP \u2228 Q&#92;).<\/p>\n<p>Primer subcaso: Suponemos &#92;(\u00acP&#92;). Entonces tenemos una contradicci\u00f3n con &#92;(P&#92;).<\/p>\n<p>Segundo subcaso: Suponemos &#92;(Q&#92;), que es lo que tenemos que demostrar.<\/p>\n<p><b>2. Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Tactic\nvariable (P Q : Prop)\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  : (P \u2192 Q) \u2194 \u00acP \u2228 Q :=\nby\n  constructor\n  . -- \u22a2 (P \u2192 Q) \u2192 \u00acP \u2228 Q\n    intro h1\n    -- h1 : P \u2192 Q\n    -- \u22a2 \u00acP \u2228 Q\n    by_cases h2 : P\n    . -- h2 : P\n      right\n      -- \u22a2 Q\n      apply h1\n      -- \u22a2 P\n      exact h2\n    . -- h2 : \u00acP\n      left\n      -- \u22a2 \u00acP\n      exact h2\n  . -- \u22a2 \u00acP \u2228 Q \u2192 P \u2192 Q\n    intros h3 h4\n    -- h3 : \u00acP \u2228 Q\n    -- h4 : P\n    -- \u22a2 Q\n    rcases h3 with h3a | h3b\n    . -- h : \u00acP\n      exact absurd h4 h3a\n    . -- h : Q\n      exact h3b\n  done\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  : (P \u2192 Q) \u2194 \u00acP \u2228 Q :=\nby\n  constructor\n  . -- \u22a2 (P \u2192 Q) \u2192 \u00acP \u2228 Q\n    intro h1\n    -- h1 : P \u2192 Q\n    -- \u22a2 \u00acP \u2228 Q\n    by_cases h2: P\n    . -- h2 : P\n      right\n      -- \u22a2 Q\n      exact h1 h2\n    . -- h2 : \u00acP\n      left\n      -- \u22a2 \u00acP\n      exact h2\n  . -- \u22a2 \u00acP \u2228 Q \u2192 P \u2192 Q\n    intros h3 h4\n    -- h3 : \u00acP \u2228 Q\n    -- h4 : P\n    -- \u22a2 Q\n    cases h3\n    . -- h : \u00acP\n      contradiction\n    . -- h : Q\n      assumption\n  done\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (P Q : Prop)\n  : (P \u2192 Q) \u2194 \u00acP \u2228 Q :=\nimp_iff_not_or\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (P Q : Prop)\n  : (P \u2192 Q) \u2194 \u00acP \u2228 Q :=\nby tauto\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\/Implicacion_mediante_disyuncion_y_negacion.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. 40.<\/li>\n<\/ul>\n<p><b>3. Demostraciones con Isabelle\/HOL<\/b><\/p>\n<pre lang=\"isar\">\ntheory Implicacion_mediante_disyuncion_y_negacion\nimports Main\nbegin\n\n(* 1\u00aa demostraci\u00f3n *)\nlemma \"(P \u27f6 Q) \u27f7 (\u00acP \u2228 Q)\"\nproof\n  assume \"P \u27f6 Q\"\n  show \"\u00acP \u2228 Q\"\n  proof -\n    have \"\u00acP \u2228 P\" by (rule excluded_middle)\n    then show \"\u00acP \u2228 Q\"\n    proof (rule disjE)\n      assume \"\u00acP\"\n      then show \"\u00acP \u2228 Q\" by (rule disjI1)\n    next\n      assume 2: \"P\"\n      with `P \u27f6 Q` have \"Q\" by (rule mp)\n      then show \"\u00acP \u2228 Q\" by (rule disjI2)\n    qed\n  qed\nnext\n  assume \"\u00acP \u2228 Q\"\n  show \"P \u27f6 Q\"\n  proof\n    assume \"P\"\n    note `\u00acP \u2228 Q`\n    then show \"Q\"\n    proof (rule disjE)\n      assume \"\u00acP\"\n      then show Q using `P` by (rule notE)\n    next\n      assume \"Q\"\n      then show \"Q\" by this\n    qed\n  qed\nqed\n\n(* 2\u00aa demostraci\u00f3n *)\nlemma \"(P \u27f6 Q) \u27f7 (\u00acP \u2228 Q)\"\nproof\n  assume \"P \u27f6 Q\"\n  show \"\u00acP \u2228 Q\"\n  proof -\n    have \"\u00acP \u2228 P\" by (rule excluded_middle)\n    then show \"\u00acP \u2228 Q\"\n    proof\n      assume \"\u00acP\"\n      then show \"\u00acP \u2228 Q\" ..\n    next\n      assume 2: \"P\"\n      with `P \u27f6 Q` have \"Q\" ..\n      then show \"\u00acP \u2228 Q\" ..\n    qed\n  qed\nnext\n  assume \"\u00acP \u2228 Q\"\n  show \"P \u27f6 Q\"\n  proof\n    assume \"P\"\n    note `\u00acP \u2228 Q`\n    then show \"Q\"\n    proof\n      assume \"\u00acP\"\n      then show Q using `P` ..\n    next\n      assume \"Q\"\n      then show \"Q\" .\n    qed\n  qed\nqed\n\n(* 3\u00aa demostraci\u00f3n *)\nlemma \"(P \u27f6 Q) \u27f7 (\u00acP \u2228 Q)\"\n  by simp\n\nend\n<\/pre>\n<p><a name=\"ej4\"><\/a><\/p>\n<h3>4. Existen infinitos n\u00fameros primos<\/h3>\n<p>Demostrar con Lean4 que existen infinitos n\u00fameros primos.<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Tactic\nimport Mathlib.Data.Nat.Prime\nopen Nat\n\nexample\n  (n : \u2115) :\n  \u2203 p, n \u2264 p \u2227 Nat.Prime p :=\nby sorry\n<\/pre>\n<p><b>1. Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p>Se usar\u00e1n los siguientes lemas de los n\u00fameros naturales, donde &#92;(&#92;text{Primo}(n)&#92;) se verifica si &#92;(n&#92;) es primo y &#92;(&#92;text{minFac}(n)&#92;) es el menor factor primo de &#92;(n&#92;).<\/p>\n<p>&#92;begin{align}<br \/>\n   &amp;n \u2260 1 \u2192 &#92;text{Primo}(&#92;text{minFac}(n)) &#92;tag{L1} &#92;&#92;<br \/>\n   &amp;n! > 0                                 &#92;tag{L2} &#92;&#92;<br \/>\n   &amp;0 &lt; k \u2192 n &lt; k + n                      &#92;tag{L3} &#92;&#92;<br \/>\n   &amp;k &lt; n \u2192 n \u2260 k                          &#92;tag{L4} &#92;&#92;<br \/>\n   &amp;k \u2271 n \u2192 k \u2264 n                          &#92;tag{L5} &#92;&#92;<br \/>\n   &amp;0 &lt; k \u2192 k \u2264 n \u2192 k \u2223 n!                 &#92;tag{L6} &#92;&#92;<br \/>\n   &amp;0 &lt; &#92;text{minFac}(n)                   &#92;tag{L7} &#92;&#92;<br \/>\n   &amp;k \u2223 m \u2192 (k \u2223 n \u2194 k \u2223 m + n)            &#92;tag{L8} &#92;&#92;<br \/>\n   &amp;&#92;text{minFac}(n) \u2223 n                   &#92;tag{L9} &#92;&#92;<br \/>\n   &amp;&#92;text{Primo}(n) \u2192 \u00acn \u2223 1               &#92;tag{L10}<br \/>\n&#92;end{align}<\/p>\n<p>Sea &#92;(p&#92;) el menor factor primo de &#92;(n! + 1&#92;). Tenemos que demostrar que &#92;(n \u2264 p&#92;) y que &#92;(p&#92;) es primo.<\/p>\n<p>Para demostrar que &#92;(p&#92;) es primo, por el lema L1, basta demostrar que<br \/>\n&#92;[ n! + 1 \u2260 1 &#92;]<br \/>\nSu demostraci\u00f3n es<br \/>\n&#92;begin{align}<br \/>\n   &amp;n ! > 0          &amp;&amp;&#92;text{[por L2]} &#92;&#92;<br \/>\n   &amp;\u27f9 n ! + 1 > 1   &amp;&amp;&#92;text{[por L3]} &#92;&#92;<br \/>\n   &amp;\u27f9 n ! + 1 \u2260 1   &amp;&amp;&#92;text{[por L4]}<br \/>\n&#92;end{align}<\/p>\n<p>Para demostrar &#92;(n \u2264 p&#92;), por el lema L5, basta demostrar que &#92;(n \u2271 p&#92;). Su demostraci\u00f3n es<br \/>\n&#92;begin{align}<br \/>\n   &amp;n \u2265 p        &#92;&#92;<br \/>\n   &amp;\u27f9 p \u2223 n!    &amp;&amp;&#92;text{[por L6 y L7]} &#92;&#92;<br \/>\n   &amp;\u27f9 p | 1     &amp;&amp;&#92;text{[por L8 y L9]} &#92;&#92;<br \/>\n   &amp;\u27f9 Falso     &amp;&amp;&#92;text{[por L10 y &#92;(p&#92;) es primo]}<br \/>\n&#92;end{align}<\/p>\n<p><b>2. Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Tactic\nimport Mathlib.Data.Nat.Prime\nopen Nat\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (n : \u2115) :\n  \u2203 p, n \u2264 p \u2227 Nat.Prime p :=\nby\n  let p := minFac (n !  + 1)\n  have h1 : Nat.Prime p := by\n    apply minFac_prime\n    -- \u22a2 n ! + 1 \u2260 1\n    have h3 : n ! > 0     := factorial_pos n\n    have h4 : n ! + 1 > 1 := Nat.lt_add_of_pos_left h3\n    show n ! + 1 \u2260 1\n    exact Nat.ne_of_gt h4\n  use p\n  constructor\n  . -- \u22a2 n \u2264 p\n    apply le_of_not_ge\n    -- \u22a2 \u00acn \u2265 p\n    intro h5\n    -- h5 : n \u2265 p\n    -- \u22a2 False\n    have h6 : p \u2223 n ! := dvd_factorial (minFac_pos _) h5\n    have h7 : p \u2223 1   := (Nat.dvd_add_iff_right h6).mpr (minFac_dvd _)\n    show False\n    exact (Nat.Prime.not_dvd_one h1) h7\n  . -- \u22a2 Nat.Prime p\n    exact h1\n  done\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (n : \u2115) :\n  \u2203 p, n \u2264 p \u2227 Nat.Prime p :=\nexists_infinite_primes n\n\n-- Lemas usados\n-- ============\n\n-- variable (k m n : \u2115)\n-- #check (Nat.Prime.not_dvd_one : Nat.Prime n \u2192 \u00acn \u2223 1)\n-- #check (Nat.dvd_add_iff_right : k \u2223 m \u2192 (k \u2223 n \u2194 k \u2223 m + n))\n-- #check (Nat.dvd_one : n \u2223 1 \u2194 n = 1)\n-- #check (Nat.lt_add_of_pos_left : 0 < k \u2192 n < k + n)\n-- #check (Nat.ne_of_gt : k < n \u2192 n \u2260 k)\n-- #check (dvd_factorial : 0 < k \u2192 k \u2264 n \u2192 k \u2223 n !)\n-- #check (factorial_pos n: n ! > 0)\n-- #check (le_of_not_ge : \u00ack \u2265 n \u2192 k \u2264 n)\n-- #check (minFac_dvd n : minFac n \u2223 n)\n-- #check (minFac_pos n : 0 < minFac n)\n-- #check (minFac_prime : n \u2260 1 \u2192 Nat.Prime (minFac 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\/Infinitud_de_primos.lean\" rel=\"noopener noreferrer\" target=\"_blank\">Lean 4 Web<\/a>.<\/p>\n<p><a name=\"ej5\"><\/a><\/p>\n<h3>5. Si n\u00b2 es par, entonces n es par<\/h3>\n<p>Demostrar con Lean4 que si &#92;(n\u00b2&#92;) es par, entonces &#92;(n&#92;) es par.<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Tactic\nopen Nat\nvariable (n : \u2115)\n\nexample\n  (h : 2 \u2223 n ^ 2)\n  : 2 \u2223 n :=\nby sorry\n<\/pre>\n<p><b>1. Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p>Se usar\u00e1 el siguiente lema: Si &#92;(p&#92;) es primo, entonces<br \/>\n&#92;[ (\u2200 a, b \u2208 \u2115)[p \u2223 ab \u2194 p \u2223 a \u2228 p \u2223 b] &#92;]<\/p>\n<p>Si &#92;(n\u00b2&#92;) es par, entonces &#92;(2&#92;) divide a &#92;(n.n&#92;) y, por el lema, &#92;(2&#92;) divide a &#92;(n&#92;).<\/p>\n<p><b>2. Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Tactic\nopen Nat\nvariable (n : \u2115)\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : 2 \u2223 n ^ 2)\n  : 2 \u2223 n :=\nby\n  rw [pow_two] at h\n  -- h : 2 \u2223 n * n\n  have h1 : Nat.Prime 2 := prime_two\n  have h2 : 2 \u2223 n \u2228 2 \u2223 n := (Prime.dvd_mul h1).mp h\n  rcases h2 with h3 | h4\n  \u00b7 -- h3 : 2 \u2223 n\n    exact h3\n  \u00b7 -- h4 : 2 \u2223 n\n    exact h4\n  done\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : 2 \u2223 n ^ 2)\n  : 2 \u2223 n :=\nby\n  rw [pow_two] at h\n  -- h : 2 \u2223 n * n\n  have h2 : 2 \u2223 n \u2228 2 \u2223 n := (Prime.dvd_mul prime_two).mp h\n  rcases h2 with h3 | h4\n  \u00b7 exact h3\n  \u00b7 exact h4\n  done\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : 2 \u2223 n ^ 2)\n  : 2 \u2223 n :=\nby\n  rw [pow_two] at h\n  -- h : 2 \u2223 n * n\n  have h2 : 2 \u2223 n \u2228 2 \u2223 n := (Prime.dvd_mul prime_two).mp h\n  tauto\n  done\n\n-- Lemas usados\n-- ============\n\n-- variable (p a b : \u2115)\n-- #check (prime_two : Nat.Prime 2)\n-- #check (Prime.dvd_mul : Nat.Prime p \u2192 (p \u2223 a * b \u2194 p \u2223 a \u2228 p \u2223 b))\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\/Par_si_cuadrado_par.lean\" rel=\"noopener noreferrer\" target=\"_blank\">Lean 4 Web<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Esta semana he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades: 1. En \u211d, x\u00b2 = y\u00b2 \u2192 x = y \u2228 x = -y 2. \u00ac\u00acP \u2192 P 3. (P \u2192 Q) \u2194 \u00acP \u2228 Q 4. Existen infinitos n\u00fameros primos 5. Si n\u00b2 es par, entonces n es par A&#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\/8076"}],"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=8076"}],"version-history":[{"count":5,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/8076\/revisions"}],"predecessor-version":[{"id":8081,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/8076\/revisions\/8081"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=8076"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=8076"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=8076"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}