Teorema de Nicómaco

PorJosé A. Alonso 30 enero 202021 agosto 2021

Demostrar el teorema de Nicómaco que afirma que la suma de los cubos de los n primeros números naturales es igual que el cuadrado de la suma de los n primeros números naturales; es decir, para todo número natural n se tiene que

1³ + 2³ + ... + n³ = (1 + 2 + ... + n)²

1	1³ + 2³ + ... + n³ = (1 + 2 + ... + n)²

Soluciones con Isabelle/HOL

theory Teorema_de_Nicomaco
imports Main
begin

(* (suma n) es la suma de los primeros números naturales. *)
fun suma :: "nat ⇒ nat" where
  "suma 0 = 0"
| "suma (Suc n) = suma n + Suc n"

(* (sumaCubos n) es la suma de los cubos primeros números naturales. *)
fun sumaCubos :: "nat ⇒ nat" where
  "sumaCubos 0 = 0"
| "sumaCubos (Suc n) = sumaCubos n + (Suc n)^3"

(* Fórmula para la suma *)
lemma "2 * suma n = n^2 + n"
proof (induct n)
  show "2 * suma 0 = 0^2 + 0" by simp
next
  fix n
  assume "2 * suma n = n^2 + n"
  then have "2 * suma (Suc n) = n^2 + n + 2 + 2 * n"
    by simp
  also have "… = (Suc n)^2 + Suc n"
    by (simp add: power2_eq_square)
  finally show "2 * suma (Suc n) = (Suc n)^2 + Suc n"
    by this
qed

(* Demostración automática de la propiedad anterior *)
lemma formula_suma:
  "2 * suma n = n^2 + n"
  by (induct n) (auto simp add: power2_eq_square)

lemma "4 * sumaCubos n = (n^2 + n)^2"
proof (induct n)
  show "4 * sumaCubos 0 = (0^2 + 0)^2"
    by simp
next
  fix n
  assume "4 * sumaCubos n = (n^2 + n)^2"
  then have "4 * sumaCubos (Suc n) = (n^2 + n)^2 + 4 * (Suc n)^3"
    by simp
  then show "4 * sumaCubos (Suc n) = ((Suc n)^2 + Suc n)^2"
  by (simp add: algebra_simps
                power2_eq_square
                power3_eq_cube )
qed

(* Demostración automática de la propiedad anterior *)
lemma formula_sumaCubos:
  "4 * sumaCubos n = (n^2 + n)^2"
  by (induct n) (auto simp add: algebra_simps
                                power2_eq_square
                                power3_eq_cube)

(* Lema auxiliar *)
lemma aux: "4 * (m::nat) = (2 * n)^2 ⟹ m = n^2"
  by (simp add: power2_eq_square)

(* Teorema de Nicómaco *)
theorem teorema_de_Nicomaco:
  "sumaCubos n = (suma n)^2"
  by (simp only: formula_suma formula_sumaCubos aux)

end

theory Teorema_de_Nicomaco

imports Main

begin

(* (suma n) es la suma de los primeros números naturales. *)

fun suma :: "nat ⇒ nat" where

"suma 0 = 0"

| "suma (Suc n) = suma n + Suc n"

(* (sumaCubos n) es la suma de los cubos primeros números naturales. *)

fun sumaCubos :: "nat ⇒ nat" where

"sumaCubos 0 = 0"

| "sumaCubos (Suc n) = sumaCubos n + (Suc n)^3"

(* Fórmula para la suma *)

lemma "2 * suma n = n^2 + n"

proof (induct n)

show "2 * suma 0 = 0^2 + 0" by simp

fix n

assume "2 * suma n = n^2 + n"

then have "2 * suma (Suc n) = n^2 + n + 2 + 2 * n"

by simp

also have "… = (Suc n)^2 + Suc n"

by (simp add: power2_eq_square)

finally show "2 * suma (Suc n) = (Suc n)^2 + Suc n"

by this

qed

(* Demostración automática de la propiedad anterior *)

lemma formula_suma:

"2 * suma n = n^2 + n"

by (induct n) (auto simp add: power2_eq_square)

lemma "4 * sumaCubos n = (n^2 + n)^2"

proof (induct n)

show "4 * sumaCubos 0 = (0^2 + 0)^2"

by simp

fix n

assume "4 * sumaCubos n = (n^2 + n)^2"

then have "4 * sumaCubos (Suc n) = (n^2 + n)^2 + 4 * (Suc n)^3"

by simp

then show "4 * sumaCubos (Suc n) = ((Suc n)^2 + Suc n)^2"

by (simp add: algebra_simps

power2_eq_square

power3_eq_cube )

qed

(* Demostración automática de la propiedad anterior *)

lemma formula_sumaCubos:

"4 * sumaCubos n = (n^2 + n)^2"

by (induct n) (auto simp add: algebra_simps

power2_eq_square

power3_eq_cube)

(* Lema auxiliar *)

lemma aux: "4 * (m::nat) = (2 * n)^2 ⟹ m = n^2"

by (simp add: power2_eq_square)

(* Teorema de Nicómaco *)

theorem teorema_de_Nicomaco:

"sumaCubos n = (suma n)^2"

by (simp only: formula_suma formula_sumaCubos aux)

end

Otras soluciones

Se pueden escribir otras soluciones en los comentarios.
El código se debe escribir entre una línea con <pre lang="isar"> y otra con </pre>

José A. Alonso

2 Comentarios

theory Teorema_de_Nicomaco 
imports Main 
begin

(* (suma n) es la suma de los primeros números naturales. *)
fun suma :: "nat ⇒ nat" where
  "suma 0 = 0"
| "suma (Suc n) = suma n + Suc n"

(* (sumaCubos n) es la suma de los cubos primeros números naturales. *)
fun sumaCubos :: "nat ⇒ nat" where
  "sumaCubos 0 = 0"
| "sumaCubos (Suc n) = sumaCubos n + (Suc n)^3"

(* Fórmula para la suma *)
lemma "2 * suma n = n^2 + n"
proof (induct n)
  show "2 * suma 0 = 0^2 + 0" by simp
next
  fix n
  assume "2 * suma n = n^2 + n"
  then have "2 * suma (Suc n) = n^2 + n + 2 + 2 * n"
    by simp
  also have "… = (Suc n)^2 + Suc n"
    by (simp add: power2_eq_square)
  finally show "2 * suma (Suc n) = (Suc n)^2 + Suc n"
    by this
qed 

(* Demostración automática de la propiedad anterior *)
lemma formula_suma: 
  "2 * suma n = n^2 + n"
  by (induct n) (auto simp add: power2_eq_square)

lemma "4 * sumaCubos n = (n^2 + n)^2"
proof (induct n) 
  show "4 * sumaCubos 0 = (0^2 + 0)^2"
    by simp
next
  fix n
  assume "4 * sumaCubos n = (n^2 + n)^2"
  then have "4 * sumaCubos (Suc n) = (n^2 + n)^2 + 4 * (Suc n)^3"
    by simp
  then show "4 * sumaCubos (Suc n) = ((Suc n)^2 + Suc n)^2"
  by (simp add: algebra_simps 
                power2_eq_square 
                power3_eq_cube )
qed

(* Demostración automática de la propiedad anterior *)
lemma formula_sumaCubos: 
  "4 * sumaCubos n = (n^2 + n)^2"
  by (induct n) (auto simp add: algebra_simps 
                                power2_eq_square 
                                power3_eq_cube)

(* Lema auxiliar *)
lemma aux: "4 * (m::nat) = (2 * n)^2 ⟹ m = n^2"
  by (simp add: power2_eq_square)

(* Teorema de Nicómaco *)
theorem teorema_de_Nicomaco: 
  "sumaCubos n = (suma n)^2"
  by (simp only: formula_suma formula_sumaCubos aux)

end

theory Teorema_de_Nicomaco

imports Main

begin

(* (suma n) es la suma de los primeros números naturales. *)

fun suma :: "nat ⇒ nat" where

"suma 0 = 0"

| "suma (Suc n) = suma n + Suc n"

(* (sumaCubos n) es la suma de los cubos primeros números naturales. *)

fun sumaCubos :: "nat ⇒ nat" where

"sumaCubos 0 = 0"

| "sumaCubos (Suc n) = sumaCubos n + (Suc n)^3"

(* Fórmula para la suma *)

lemma "2 * suma n = n^2 + n"

proof (induct n)

show "2 * suma 0 = 0^2 + 0" by simp

fix n

assume "2 * suma n = n^2 + n"

then have "2 * suma (Suc n) = n^2 + n + 2 + 2 * n"

by simp

also have "… = (Suc n)^2 + Suc n"

by (simp add: power2_eq_square)

finally show "2 * suma (Suc n) = (Suc n)^2 + Suc n"

by this

qed

(* Demostración automática de la propiedad anterior *)

lemma formula_suma:

"2 * suma n = n^2 + n"

by (induct n) (auto simp add: power2_eq_square)

lemma "4 * sumaCubos n = (n^2 + n)^2"

proof (induct n)

show "4 * sumaCubos 0 = (0^2 + 0)^2"

by simp

fix n

assume "4 * sumaCubos n = (n^2 + n)^2"

then have "4 * sumaCubos (Suc n) = (n^2 + n)^2 + 4 * (Suc n)^3"

by simp

then show "4 * sumaCubos (Suc n) = ((Suc n)^2 + Suc n)^2"

by (simp add: algebra_simps

power2_eq_square

power3_eq_cube )

qed

(* Demostración automática de la propiedad anterior *)

lemma formula_sumaCubos:

"4 * sumaCubos n = (n^2 + n)^2"

by (induct n) (auto simp add: algebra_simps

power2_eq_square

power3_eq_cube)

(* Lema auxiliar *)

lemma aux: "4 * (m::nat) = (2 * n)^2 ⟹ m = n^2"

by (simp add: power2_eq_square)

(* Teorema de Nicómaco *)

theorem teorema_de_Nicomaco:

"sumaCubos n = (suma n)^2"

by (simp only: formula_suma formula_sumaCubos aux)

end

Responder

Hecho en Lean con mathlib. Es bastante mejorable.

import algebra.big_operators tactic.ring

open finset nat

lemma sumaArit (n : ℕ) : 2 * ((range (n + 1)).sum id) = n * (n + 1) :=
begin
  induction n with n ih,
  { refl },
  { rw [sum_range_succ, mul_add, ih, id.def, nat.succ_eq_add_one],
    ring }
end

lemma sumaCubos (n : ℕ) : 4 * (range (n + 1)).sum (λx, x^3) = n^2 * (n + 1)^2 :=
begin
  induction n with n ih,
  { refl },
  { rw [sum_range_succ, mul_add, ih, nat.succ_eq_add_one],
    ring }
end

lemma sqrt4 : 2^2 = 4 := by rw [nat.pow_succ,  nat.pow_one]; refl

def nicomaco_aux (n : ℕ) : 4*((range (n+1)).sum (λx, x^3)) = 4*(((range (n+1)).sum id)^2) :=
by rw [← sqrt4, ← nat.mul_pow, sqrt4, 
       sumaCubos, sumaArit, nat.mul_pow]

theorem nicomaco (n : ℕ) : (range (n + 1)).sum (λx, x^3) = ((range (n + 1)).sum id)^2 :=
calc (range (n + 1)).sum (λx, x^3) = 4 * (range (n+1)).sum (λx, x^3) / 4 : by simp
  ... = 4 * ((range (n+1)).sum id)^2 / 4 : by rw nicomaco_aux
  ... = (((range (n+1)).sum id)^2) : by simp

import algebra.big_operators tactic.ring

open finset nat

lemma sumaArit (n : ℕ) : 2 * ((range (n + 1)).sum id) = n * (n + 1) :=

begin

induction n with n ih,

{ refl },

{ rw [sum_range_succ, mul_add, ih, id.def, nat.succ_eq_add_one],

ring }

end

lemma sumaCubos (n : ℕ) : 4 * (range (n + 1)).sum (λx, x^3) = n^2 * (n + 1)^2 :=

begin

induction n with n ih,

{ refl },

{ rw [sum_range_succ, mul_add, ih, nat.succ_eq_add_one],

ring }

end

lemma sqrt4 : 2^2 = 4 := by rw [nat.pow_succ, nat.pow_one]; refl

def nicomaco_aux (n : ℕ) : 4*((range (n+1)).sum (λx, x^3)) = 4*(((range (n+1)).sum id)^2) :=

by rw [← sqrt4, ← nat.mul_pow, sqrt4,

sumaCubos, sumaArit, nat.mul_pow]

theorem nicomaco (n : ℕ) : (range (n + 1)).sum (λx, x^3) = ((range (n + 1)).sum id)^2 :=

calc (range (n + 1)).sum (λx, x^3) = 4 * (range (n+1)).sum (λx, x^3) / 4 : by simp

... = 4 * ((range (n+1)).sum id)^2 / 4 : by rw nicomaco_aux

... = (((range (n+1)).sum id)^2) : by simp

Responder

Soluciones con Isabelle/HOL

Otras soluciones

Share this:

2 Comentarios

Escribe un comentarioCancel reply