Menu Close

Teorema de Nicómaco

José A. Alonso- -- 2 Comentarios

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)²

Soluciones

  • Las soluciones se pueden escribir en los comentarios.
  • El código se debe escribir entre una línea con <pre lang=»haskell»> y otra con </pre>

Pensamiento

«Las matemáticas son la reina de las ciencias y la teoría de los números es la reina de las matemáticas.»

Carl Friedrich Gauss.


2 Comments

  1. bencamdel
    Responder 
    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
  2. Diego
    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

Leave a Reply