\n S = 0 + 1 + 2 + ... + (n-3) + (n-2) + (n-1)\n S = (n-1) + (n-2) + (n-3) + ... + 2 + 1 + 0\n<\/pre>\nAl sumar, se observa que cada par de n\u00fameros de la misma columna da como suma (n-1), y puesto que hay n columnas en total, se sigue<\/p>\n
\n 2S = n(n-1)\n<\/pre>\nlo que prueba la f\u00f3rmula.<\/p>\n
Demostrar la f\u00f3rmula de Gauss siguiendo el procedimiento anterior.<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean:<\/p>\n
\nimport algebra.big_operators.basic\nimport algebra.big_operators.intervals\n\nopen_locale big_operators\nopen finset nat\n\nvariables (n i : \u2115)\n\nexample :\n (\u2211 i in range n, i) * 2 = n * (n - 1) :=\nsorry\n<\/pre>\n[expand title=\u00bbSoluciones con Lean\u00bb]<\/p>\n
\r\nimport algebra.big_operators.basic\r\nimport algebra.big_operators.intervals\r\n\r\nopen_locale big_operators\r\nopen finset nat\r\n\r\nvariables (n i : \u2115)\r\n\r\n-- Lema auxiliar\r\n-- =============\r\n\r\n-- Se usar\u00e1 el siguiente lema auxiliar del que se presentan distintas\r\n-- demostraciones.\r\n\r\n-- 1\u00aa demostraci\u00f3n del lema auxiliar\r\nexample : \u2200 x, x \u2208 range n \u2192 x + (n - 1 - x) = n - 1 :=\r\nbegin\r\n intros x hx,\r\n replace hx : x < n := mem_range.1 hx,\r\n replace hx : x \u2264 n - 1 := le_pred_of_lt hx,\r\n exact nat.add_sub_cancel' hx,\r\nend\r\n\r\n-- 2\u00aa demostraci\u00f3n del lema auxiliar\r\nexample : \u2200 x, x \u2208 range n \u2192 x + (n - 1 - x) = n - 1 :=\r\nbegin\r\n intros x hx,\r\n exact nat.add_sub_cancel' (le_pred_of_lt (mem_range.1 hx)),\r\nend\r\n\r\n-- 3\u00aa demostraci\u00f3n del lema auxiliar\r\nlemma auxiliar : \u2200 x, x \u2208 range n \u2192 x + (n - 1 - x) = n - 1 :=\r\n\u03bb x hx, nat.add_sub_cancel' (le_pred_of_lt (mem_range.1 hx))\r\n\r\n-- Lema principal\r\n-- ==============\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\nexample :\r\n (\u2211 i in range n, i) * 2 = n * (n - 1) :=\r\ncalc (\u2211 i in range n, i) * 2\r\n = (\u2211 i in range n, i) + (\u2211 i in range n, i)\r\n : mul_two _\r\n ... = (\u2211 i in range n, i) + (\u2211 i in range n, (n - 1 - i))\r\n : congr_arg2 (+) rfl (sum_range_reflect id n).symm\r\n ... = \u2211 i in range n, (i + (n - 1 - i))\r\n : sum_add_distrib.symm\r\n ... = \u2211 i in range n, (n - 1)\r\n : sum_congr rfl (auxiliar n)\r\n ... = card (range n) \u2022 (n - 1)\r\n : sum_const (n - 1)\r\n ... = card (range n) * (n - 1)\r\n : nat.nsmul_eq_mul _ _\r\n ... = n * (n - 1)\r\n : congr_arg2 (*) (card_range n) rfl\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\nexample :\r\n (\u2211 i in range n, i) * 2 = n * (n - 1) :=\r\ncalc (\u2211 i in range n, i) * 2\r\n = (\u2211 i in range n, i) + (\u2211 i in range n, (n - 1 - i))\r\n : by rw [sum_range_reflect (\u03bb i, i) n, mul_two]\r\n ... = \u2211 i in range n, (i + (n - 1 - i))\r\n : sum_add_distrib.symm\r\n ... = \u2211 i in range n, (n - 1)\r\n : sum_congr rfl (auxiliar n)\r\n ... = n * (n - 1)\r\n : by rw [sum_const, card_range, nat.nsmul_eq_mul]\r\n<\/pre>\nSe puede interactuar con la prueba anterior en esta sesi\u00f3n con Lean<\/a>.<\/p>\nEn los comentarios se pueden escribir otras soluciones, escribiendo el c\u00f3digo entre una l\u00ednea con <pre lang="lean"> y otra con <\/pre>
\n[\/expand]<\/p>\n
[expand title=\"Soluciones con Isabelle\/HOL\"]<\/p>\n
\r\ntheory Formula_de_Gauss_de_la_suma\r\nimports Main\r\nbegin\r\n\r\nlemma\r\n fixes n :: nat\r\n shows \"2 * (\u2211i\nEn los comentarios se pueden escribir otras soluciones, escribiendo el c\u00f3digo entre una l\u00ednea con <pre lang="isar"> y otra con <\/pre>
\n[\/expand]<\/p>\n","protected":false},"excerpt":{"rendered":"
La f\u00f3rmula de Gauss para la suma de los primeros n\u00fameros naturales es 0 + 1 + 2 + … + (n-1) = n(n-1)\/2 En un ejercicio anterior se ha demostrado dicha f\u00f3rmula por inducci\u00f3n. Otra forma de demostrarla, sin usar inducci\u00f3n, es la siguiente: La suma se puede escribir de dos maneras S = 0 + 1 + 2 + … + (n-3) + (n-2) + (n-1) S = (n-1) + (n-2) + (n-3) + … + 2 + 1 + 0 Al sumar, se observa que cada par de n\u00fameros de la misma columna da como suma (n-1), y puesto que hay n columnas en total, se sigue 2S = n(n-1) lo que prueba la f\u00f3rmula. Demostrar la f\u00f3rmula de Gauss siguiendo el…<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","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,"_jetpack_memberships_contains_paid_content":false,"footnotes":""},"categories":[280],"tags":[],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/787"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/comments?post=787"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/787\/revisions"}],"predecessor-version":[{"id":788,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/787\/revisions\/788"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/media?parent=787"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/categories?post=787"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/tags?post=787"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}