:: Polygonal Numbers :: by Adam Grabowski :: :: Received May 19, 2013 :: Copyright (c) 2013-2016 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies ORDINAL2, FINSEQ_1, ARYTM_3, ARYTM_1, RELAT_1, FUNCT_1, FINSEQ_2, INT_1, SQUARE_1, SEQ_1, NUMPOLY1, REALSET1, SERIES_1, POWER, SEQ_2, ASYMPT_1, FUNCT_7, CARD_1, EUCLID_3, GR_CY_3, ABIAN, TOPGEN_1, FINSET_1, TARSKI, PYTHTRIP, EC_PF_2, NEWTON, XXREAL_0, ORDINAL4, XBOOLE_0, REAL_1, INT_2, NAT_1, XREAL_0, CARD_3, XCMPLX_0, ORDINAL1, SUBSET_1, ZFMISC_1, NUMBERS; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0, VALUED_1, ZFMISC_1, SQUARE_1, INT_1, INT_2, XREAL_0, FUNCT_1, FINSET_1, FINSEQ_1, FUNCOP_1, NEWTON, NAT_D, SEQ_1, SEQ_2, FINSEQ_2, RVSUM_1, SERIES_1, POWER, ABIAN, PYTHTRIP, PEPIN, GR_CY_3, NAT_5, EC_PF_2; constructors SEQ_1, COMSEQ_2, GR_CY_3, NAT_5, ABIAN, EC_PF_2, MOEBIUS1, RVSUM_1, SERIES_1, SEQ_2, REAL_1, PEPIN, POLYEQ_3, RELSET_1, NAT_D, PYTHTRIP, FINSET_1; registrations RELSET_1, FINSEQ_2, INT_1, XREAL_0, NAT_1, MEMBERED, FINSEQ_1, RVSUM_1, XXREAL_0, NAT_2, NEWTON, SEQ_1, XCMPLX_0, NUMBERS, SEQ_2, POWER, ABIAN, PYTHTRIP, SQUARE_1, ORDINAL1, XBOOLE_0, FUNCT_2, VALUED_0, VALUED_1; requirements REAL, NUMERALS, SUBSET, ARITHM; definitions ORDINAL1, TARSKI, XBOOLE_0, FUNCT_2; equalities POWER, NEWTON, SERIES_1, SQUARE_1, GR_CY_3, XBOOLE_0; expansions ORDINAL1; theorems FINSEQ_2, RVSUM_1, XCMPLX_1, ORDINAL1, SQUARE_1, NAT_1, POWER, NEWTON, XREAL_1, FINSEQ_1, RELAT_1, XREAL_0, SEQ_2, SERIES_1, SEQ_4, SEQ_1, XXREAL_0, INT_2, PEPIN, NAT_D, POLYEQ_3, VALUED_1, INT_1, INT_4, GR_CY_3, NAT_5, PYTHTRIP, ABIAN, NAT_2, CHORD, EC_PF_2, SUBSET_1, TARSKI, XBOOLE_0; schemes NAT_1, SEQ_1, FINSEQ_2, NAT_2; begin :: Preliminaries scheme LNatRealSeq {F(set) -> Real}: (ex seq being Real_Sequence st for n being Nat holds seq.n = F(n)) & (for seq1, seq2 being Real_Sequence st (for n being Nat holds seq1.n = F(n)) & (for n being Nat holds seq2.n = F(n)) holds seq1 = seq2) proof consider seq being Real_Sequence such that A1: for n being Nat holds seq.n = F(n) from SEQ_1:sch 1; thus ex seq being Real_Sequence st for n being Nat holds seq.n=F(n) by A1; let seq1, seq2 be Real_Sequence; assume that A2: for n being Nat holds seq1.n = F(n) and A3: for n being Nat holds seq2.n = F(n); let n be Element of NAT; thus seq1.n = F(n) by A2 .= seq2.n by A3; end; theorem Th1: for n, a being non zero Nat holds 1 <= a * n proof let n,a be non zero Nat; 0 + 1 <= a * n by NAT_1:13; hence thesis; end; Lm1: for n being Integer holds n * (n - 1) is even proof let n be Integer; per cases; suppose n is even; hence thesis; end; suppose n is odd; hence thesis; end; end; Lm2: for n being Integer holds n * (n + 1) is even proof let n be Integer; per cases; suppose n is even; hence thesis; end; suppose n is odd; hence thesis; end; end; registration let n be Integer; cluster n * (n - 1) -> even; coherence by Lm1; cluster n * (n + 1) -> even; coherence by Lm2; end; theorem Th2: for n being even Integer holds n / 2 is Integer proof let n be even Integer; consider j being Integer such that A1: n = 2 * j by ABIAN:11; thus thesis by A1; end; registration let n be even Nat; cluster n / 2 -> natural; coherence proof ex k being Nat st n = 2 * k by ABIAN:def 2; hence thesis; end; end; registration let n be odd Nat; cluster n - 1 -> natural; coherence by CHORD:2; end; registration let n be odd Nat; cluster n - 1 -> even; coherence; end; reserve n,s for Nat; theorem Th3: n mod 5 = 0 or ... or n mod 5 = 4 proof n mod 5 < 4 + 1 by NAT_D:1; then n mod 5 <= 4 by NAT_1:13; hence thesis; end; theorem Th4: ::: NTALGO_1:8, 9 should be improved for k be Nat st k <> 0 holds n, n mod k are_congruent_mod k proof let k be Nat; assume k <> 0; then (n mod k) - 0 = n - (n div k) * k by INT_1:def 10; then k divides n - (n mod k) by INT_1:def 3; hence thesis by INT_1:def 4; end; theorem Th5: n, 0 are_congruent_mod 5 or ... or n, 4 are_congruent_mod 5 proof n mod 5 = 0 or ... or n mod 5 = 4 by Th3; hence thesis by Th4; end; theorem Th6: not n * n + n, 4 are_congruent_mod 5 proof assume n * n + n, 4 are_congruent_mod 5; then A1: 4, n * n + n are_congruent_mod 5 by INT_1:14; n, 0 are_congruent_mod 5 or ... or n, 4 are_congruent_mod 5 by Th5; then per cases; suppose A2: n, 0 are_congruent_mod 5; then n * n, 0 * 0 are_congruent_mod 5 by INT_1:18; then n * n + n, 0 + 0 are_congruent_mod 5 by A2,INT_1:16; then 5 divides 4 - 0 by INT_1:def 4,A1,INT_1:15; hence thesis by NAT_D:7; end; suppose A3: n, 1 are_congruent_mod 5; then n * n, 1 * 1 are_congruent_mod 5 by INT_1:18; then n * n + n, 1 + 1 are_congruent_mod 5 by A3,INT_1:16; then 5 divides 4 - 2 by INT_1:def 4,A1,INT_1:15; hence thesis by NAT_D:7; end; suppose A4: n, 2 are_congruent_mod 5; then n * n, 2 * 2 are_congruent_mod 5 by INT_1:18; then n * n + n, 4 + 2 are_congruent_mod 5 by A4,INT_1:16; then 6, n * n + n are_congruent_mod 5 by INT_1:14; then 6 - 5, n * n + n are_congruent_mod 5 by INT_1:22; then n * n + n, 1 are_congruent_mod 5 by INT_1:14; then 5 divides 4 - 1 by INT_1:def 4,A1,INT_1:15; then 5 <= 3 by NAT_D:7; hence thesis; end; suppose A5: n, 3 are_congruent_mod 5; then n * n, 3 * 3 are_congruent_mod 5 by INT_1:18; then n * n + n, 9 + 3 are_congruent_mod 5 by A5,INT_1:16; then 12, n * n + n are_congruent_mod 5 by INT_1:14; then 12 - 5, n * n + n are_congruent_mod 5 by INT_1:22; then 7 - 5, n * n + n are_congruent_mod 5 by INT_1:22; then n * n + n, 2 are_congruent_mod 5 by INT_1:14; then 5 divides 4 - 2 by INT_1:def 4,A1,INT_1:15; hence thesis by NAT_D:7; end; suppose A6: n, 4 are_congruent_mod 5; then n * n, 4 * 4 are_congruent_mod 5 by INT_1:18; then n * n + n, 16 + 4 are_congruent_mod 5 by A6,INT_1:16; then 20, n * n + n are_congruent_mod 5 by INT_1:14; then 20 - 5, n * n + n are_congruent_mod 5 by INT_1:22; then 15 - 5, n * n + n are_congruent_mod 5 by INT_1:22; then 10 - 5, n * n + n are_congruent_mod 5 by INT_1:22; then 5 - 5, n * n + n are_congruent_mod 5 by INT_1:22; then n * n + n, 0 are_congruent_mod 5 by INT_1:14; then 5 divides 4 - 0 by INT_1:def 4,A1,INT_1:15; hence thesis by NAT_D:7; end; end; theorem Th7: not n * n + n, 3 are_congruent_mod 5 proof assume n * n + n, 3 are_congruent_mod 5; then A1: 3, n * n + n are_congruent_mod 5 by INT_1:14; n, 0 are_congruent_mod 5 or ... or n, 4 are_congruent_mod 5 by Th5; then per cases; suppose A2: n, 0 are_congruent_mod 5; then n * n, 0 * 0 are_congruent_mod 5 by INT_1:18; then n * n + n, 0 + 0 are_congruent_mod 5 by A2,INT_1:16; then 5 divides 3 - 0 by INT_1:def 4,A1,INT_1:15; hence thesis by NAT_D:7; end; suppose A3: n, 1 are_congruent_mod 5; then n * n, 1 * 1 are_congruent_mod 5 by INT_1:18; then n * n + n, 1 + 1 are_congruent_mod 5 by A3,INT_1:16; then 5 divides 3 - 2 by INT_1:def 4,A1,INT_1:15; then 5 <= 1 by NAT_D:7; hence thesis; end; suppose A4: n, 2 are_congruent_mod 5; then n * n, 2 * 2 are_congruent_mod 5 by INT_1:18; then n * n + n, 4 + 2 are_congruent_mod 5 by A4,INT_1:16; then 6, n * n + n are_congruent_mod 5 by INT_1:14; then 6 - 5, n * n + n are_congruent_mod 5 by INT_1:22; then n * n + n, 1 are_congruent_mod 5 by INT_1:14; then 5 divides 3 - 1 by INT_1:def 4,A1,INT_1:15; then 5 <= 2 by NAT_D:7; hence thesis; end; suppose A5: n, 3 are_congruent_mod 5; then n * n, 3 * 3 are_congruent_mod 5 by INT_1:18; then n * n + n, 9 + 3 are_congruent_mod 5 by A5,INT_1:16; then 12, n * n + n are_congruent_mod 5 by INT_1:14; then 12 - 5, n * n + n are_congruent_mod 5 by INT_1:22; then 7 - 5, n * n + n are_congruent_mod 5 by INT_1:22; then n * n + n, 2 are_congruent_mod 5 by INT_1:14; then 5 divides 3 - 2 by INT_1:def 4,A1,INT_1:15; then 5 <= 1 by NAT_D:7; hence thesis; end; suppose A6: n, 4 are_congruent_mod 5; then n * n, 4 * 4 are_congruent_mod 5 by INT_1:18; then n * n + n, 16 + 4 are_congruent_mod 5 by A6,INT_1:16; then 20, n * n + n are_congruent_mod 5 by INT_1:14; then 20 - 5, n * n + n are_congruent_mod 5 by INT_1:22; then 15 - 5, n * n + n are_congruent_mod 5 by INT_1:22; then 10 - 5, n * n + n are_congruent_mod 5 by INT_1:22; then 5 - 5, n * n + n are_congruent_mod 5 by INT_1:22; then n * n + n, 0 are_congruent_mod 5 by INT_1:14; then 5 divides 3 - 0 by INT_1:def 4,A1,INT_1:15; hence thesis by NAT_D:7; end; end; theorem Th8: n mod 10 = 0 or ... or n mod 10 = 9 proof n mod 10 < 9 + 1 by NAT_D:1; then n mod 10 <= 9 by NAT_1:13; hence thesis; end; theorem Th9: n, 0 are_congruent_mod 10 or ... or n, 9 are_congruent_mod 10 proof n mod 10 = 0 or ... or n mod 10 = 9 by Th8; hence thesis by Th4; end; registration cluster non trivial -> 2_or_greater for Nat; coherence by EC_PF_2:def 1,NAT_2:29; cluster 2_or_greater -> non trivial for Nat; coherence proof let n be Nat; assume n is 2_or_greater; then n <> 0 & n <> 1 by EC_PF_2:def 1; hence thesis by NAT_2:def 1; end; end; registration cluster 4_or_greater -> 3_or_greater non zero for Nat; coherence proof let n be Nat; assume n is 4_or_greater; then n >= 4 by EC_PF_2:def 1; hence thesis by EC_PF_2:def 1,XXREAL_0:2; end; end; registration cluster 4_or_greater -> non trivial for Nat; coherence proof let n be Nat; assume n is 4_or_greater; then n <> 1 & n <> 0 by EC_PF_2:def 1; hence thesis by NAT_2:def 1; end; end; registration cluster 4_or_greater for Nat; existence by EC_PF_2:def 1; cluster 3_or_greater for Nat; existence by EC_PF_2:def 1; end; begin :: Triangular Numbers definition let n be Nat; func Triangle n -> Real equals Sum idseq n; coherence; end; definition let n be object; attr n is triangular means :Def2: ex k being Nat st n = Triangle k; end; registration let n be zero number; cluster Triangle n -> zero; coherence by RVSUM_1:72; end; theorem Th10: Triangle (n + 1) = (Triangle n) + (n + 1) proof defpred P[Nat] means (Triangle \$1) + (\$1 + 1) = Triangle(\$1+1); A1: P[0] by FINSEQ_2:50,RVSUM_1:73; A2: for k being Nat st P[k] holds P[k+1] proof let k be Nat such that P[k]; reconsider k1 = k as Element of NAT by ORDINAL1:def 12; (Triangle (k+1)) + k + 1 + 1 = Sum ((idseq k1) ^ <*k1 + 1*>) + k + 1 + 1 by FINSEQ_2:51 .= Sum ((idseq k1) ^ <*k1 + 1*>) + (k + 1 + 1) .= Sum (idseq (k1 + 1)) + (k1 + 1 + 1) by FINSEQ_2:51 .= Sum ((idseq (k1 + 1)) ^ <*k1 + 1 + 1*>) by RVSUM_1:74 .= Triangle (k + 1 + 1) by FINSEQ_2:51; hence thesis; end; for n being Nat holds P[n] from NAT_1:sch 2(A1,A2); hence thesis; end; theorem Th11: Triangle 1 = 1 by FINSEQ_2:50,RVSUM_1:73; theorem Th12: Triangle 2 = 3 proof thus Triangle 2 = 1 + 2 by RVSUM_1:77,FINSEQ_2:52 .= 3; end; theorem Th13: Triangle 3 = 6 proof thus Triangle 3 = 1 + 2 + 3 by RVSUM_1:78,FINSEQ_2:53 .= 6; end; theorem Th14: Triangle 4 = 10 proof thus Triangle 4 = Triangle 3 + (3 + 1) by Th10 .= 10 by Th13; end; theorem Th15: Triangle 5 = 15 proof thus Triangle 5 = Triangle 4 + (4 + 1) by Th10 .= 15 by Th14; end; theorem Th16: Triangle 6 = 21 proof thus Triangle 6 = Triangle 5 + (5 + 1) by Th10 .= 21 by Th15; end; theorem Th17: Triangle 7 = 28 proof thus Triangle 7 = Triangle 6 + (6 + 1) by Th10 .= 28 by Th16; end; theorem Th18: Triangle 8 = 36 proof thus Triangle 8 = Triangle 7 + (7 + 1) by Th10 .= 36 by Th17; end; theorem Th19: Triangle n = n * (n + 1) / 2 proof defpred P[Nat] means Triangle \$1 = \$1 * (\$1 + 1) / 2; A1: P[0]; A2: for k being Nat st P[k] holds P[k+1] proof let k be Nat such that A3: P[k]; Triangle (k + 1) = (Triangle k) + (k + 1) by Th10 .= (k + 1) * (k + 2) / 2 by A3; hence thesis; end; for n being Nat holds P[n] from NAT_1:sch 2(A1,A2); hence thesis; end; theorem Th20: Triangle n >= 0 proof A1: Triangle n = n * (n + 1) / 2 by Th19; thus thesis by A1; end; registration let n be Nat; cluster Triangle n -> non negative; coherence by Th20; end; registration let n be non zero Nat; cluster Triangle n -> positive; coherence proof n * (n + 1) / 2 > 0; hence thesis by Th19; end; end; registration let n be Nat; cluster Triangle n -> natural; coherence proof Triangle n = n * (n + 1) / 2 by Th19; hence thesis; end; end; Lm3: 0 - 1 < 0; theorem Th21: Triangle (n -' 1) = n * (n - 1) / 2 proof per cases; suppose n <> 0; then A1: 1 <= 1 * n by Th1; Triangle (n -' 1) = (n -' 1) * (n -' 1 + 1) / 2 by Th19 .= (n -' 1) * n / 2 by XREAL_1:235,A1; hence thesis by XREAL_1:233,A1; end; suppose A2: n = 0; then Triangle (n -' 1) = Triangle 0 by XREAL_0:def 2,Lm3 .= n * (n - 1) / 2 by A2; hence thesis; end; end; registration cluster triangular -> natural for number; coherence; end; registration cluster triangular non zero for number; existence proof reconsider a = Triangle 1 as number by TARSKI:1; take a; thus thesis; end; end; theorem Th22: for n being triangular number holds not n, 7 are_congruent_mod 10 proof let n be triangular number; consider k being Nat such that A1: n = Triangle k by Def2; A2: 4 * 5 = 20; A3: n = k * (k + 1) / 2 by A1,Th19; assume n, 7 are_congruent_mod 10; then k * (k + 1) / 2 * 2, 7 * 2 are_congruent_mod (10 * 2) by A3,INT_4:10; then k * (k + 1), 14 are_congruent_mod 5 by A2,INT_1:20; then 14, k * (k + 1) are_congruent_mod 5 by INT_1:14; then 14 - 5, k * (k + 1) are_congruent_mod 5 by INT_1:22; then 9 - 5, k * (k + 1) are_congruent_mod 5 by INT_1:22; then 4, k * k + k are_congruent_mod 5; hence thesis by Th6,INT_1:14; end; theorem Th23: for n being triangular number holds not n, 9 are_congruent_mod 10 proof let n be triangular number; consider k being Nat such that A1: n = Triangle k by Def2; A2: 4 * 5 = 20; A3: n = k * (k + 1) / 2 by A1,Th19; assume n, 9 are_congruent_mod 10; then k * (k + 1) / 2 * 2, 9 * 2 are_congruent_mod (10 * 2) by A3,INT_4:10; then k * (k + 1), 18 are_congruent_mod 5 by A2,INT_1:20; then 18, k * (k + 1) are_congruent_mod 5 by INT_1:14; then 18 - 5, k * (k + 1) are_congruent_mod 5 by INT_1:22; then 13 - 5, k * (k + 1) are_congruent_mod 5 by INT_1:22; then 8 - 5, k * (k + 1) are_congruent_mod 5 by INT_1:22; then 3, k * k + k are_congruent_mod 5; hence thesis by Th7,INT_1:14; end; theorem Th24: for n being triangular number holds not n, 2 are_congruent_mod 10 proof let n be triangular number; consider k being Nat such that A1: n = Triangle k by Def2; A2: 4 * 5 = 20; A3: n = k * (k + 1) / 2 by A1,Th19; assume n, 2 are_congruent_mod 10; then k * (k + 1) / 2 * 2, 2 * 2 are_congruent_mod (10 * 2) by A3,INT_4:10; then k * (k + 1), 4 are_congruent_mod 5 by A2,INT_1:20; then 4, k * k + k are_congruent_mod 5 by INT_1:14; hence thesis by Th6,INT_1:14; end; theorem Th25: for n being triangular number holds not n, 4 are_congruent_mod 10 proof let n be triangular number; consider k being Nat such that A1: n = Triangle k by Def2; A2: 4 * 5 = 20; A3: n = k * (k + 1) / 2 by A1,Th19; assume n, 4 are_congruent_mod 10; then k * (k + 1) / 2 * 2, 4 * 2 are_congruent_mod (10 * 2) by A3,INT_4:10; then k * (k + 1), 8 are_congruent_mod 5 by A2,INT_1:20; then 8, k * (k + 1) are_congruent_mod 5 by INT_1:14; then 8 - 5, k * (k + 1) are_congruent_mod 5 by INT_1:22; then 3, k * k + k are_congruent_mod 5; hence thesis by Th7,INT_1:14; end; theorem for n being triangular number holds n, 0 are_congruent_mod 10 or n, 1 are_congruent_mod 10 or n, 3 are_congruent_mod 10 or n, 5 are_congruent_mod 10 or n, 6 are_congruent_mod 10 or n, 8 are_congruent_mod 10 proof let n be triangular number; n, 0 are_congruent_mod 10 or ... or n, 9 are_congruent_mod 10 by Th9; then per cases; suppose n, 0 are_congruent_mod 10; hence thesis; end; suppose n, 1 are_congruent_mod 10; hence thesis; end; suppose n, 2 are_congruent_mod 10; hence thesis by Th24; end; suppose n, 3 are_congruent_mod 10; hence thesis; end; suppose n, 4 are_congruent_mod 10; hence thesis by Th25; end; suppose n, 5 are_congruent_mod 10; hence thesis; end; suppose n, 6 are_congruent_mod 10; hence thesis; end; suppose n, 7 are_congruent_mod 10; hence thesis by Th22; end; suppose n, 8 are_congruent_mod 10; hence thesis; end; suppose n, 9 are_congruent_mod 10; hence thesis by Th23; end; end; begin :: Polygonal Numbers definition let s, n be natural Number; func Polygon (s,n) -> Integer equals (n ^2 * (s - 2) - n * (s - 4)) / 2; coherence proof n * (n - 1) * (s - 2) is even; then (n * (s - 2) * (n - 1)) / 2 is Integer by Th2; then (n * (s - 2) * (n - 1)) / 2 + n is Integer; hence thesis; end; end; theorem Th27: s >= 2 implies Polygon (s,n) is natural proof assume s >= 2; then A1: s - 2 >= 2 - 2 by XREAL_1:9; per cases; suppose n = 0; hence thesis; end; suppose n > 0; then n >= 0 + 1 by NAT_1:13; then n - 1 >= 1 - 1 by XREAL_1:9; then (n * (s - 2) * (n - 1)) / 2 + n >= 0 by A1; hence Polygon (s,n) in NAT by INT_1:3; end; end; theorem Polygon (s,n) = (n * (s - 2) * (n - 1)) / 2 + n; definition let s be Nat; let x be object; attr x is s-gonal means :Def4: ex n being Nat st x = Polygon (s,n); end; definition let x be object; attr x is polygonal means ex s being Nat st x is s-gonal; end; theorem Polygon (s,1) = 1; theorem Polygon (s,2) = s; registration let s be Nat; cluster s-gonal for number; existence proof reconsider a = Polygon (s,2) as number; take a; thus thesis; end; end; registration let s be non zero Nat; cluster non zero s-gonal for number; existence proof reconsider a = Polygon (s,2) as number; take a; thus thesis; end; end; registration let s be Nat; cluster s-gonal -> real for number; coherence; end; registration let s be non trivial Nat; cluster s-gonal -> natural for number; coherence by EC_PF_2:def 1,Th27; end; theorem Polygon (s,n + 1) - Polygon (s,n) = (s - 2) * n + 1; definition let s be Nat, x be s-gonal number; func IndexPoly (s,x) -> Real equals (sqrt (((8 * s - 16) * x) + (s - 4) ^2) + s - 4) / (2 * s - 4); coherence; end; theorem for s being non zero Nat, x be non zero s-gonal number st x = Polygon (s,n) holds ((8*s - 16) * x) + (s - 4) ^2 = (2 * n * (s - 2) - (s - 4)) ^2; theorem for s being non zero Nat, x be non zero s-gonal number st s >= 4 holds ((8*s - 16) * x) + (s - 4) ^2 is square proof let s be non zero Nat, x be non zero s-gonal number; assume A1: s >= 4; consider n being Nat such that A2: x = Polygon (s,n) by Def4; A3: ((8 * s - 16) * x) + (s - 4) ^2 = (2 * n * (s - 2) - (s - 4)) ^2 by A2; n <> 0 by A2; then A4: 2 * n >= 1 by Th1; s >= 0 + 4 by A1; then A5: s - 4 >= 0 by XREAL_1:19; s - 2 >= s - 4 by XREAL_1:13; then 2 * n * (s - 2) >= 0 + 1 * (s - 4) by A4,A5,XREAL_1:66; then 2 * n * (s - 2) - (s - 4) in NAT by INT_1:3,XREAL_1:19; hence thesis by A3; end; theorem Th34: for s being non zero Nat, x being non zero s-gonal number st s >= 4 holds IndexPoly (s,x) in NAT proof let s be non zero Nat, x be non zero s-gonal number; assume A1: s >= 4; consider n being Nat such that A2: x = Polygon (s,n) by Def4; A3: ((8*s - 16) * x) + (s - 4) ^2 = (2 * n * (s - 2) - (s - 4)) ^2 by A2; A4: s - 2 <> 0 by A1; n <> 0 by A2; then A5: 2 * n >= 1 by Th1; s >= 0 + 4 by A1; then A6: s - 4 >= 0 by XREAL_1:19; s - 2 >= s - 4 by XREAL_1:13; then A7: 2 * n * (s - 2) >= 0 + 1 * (s - 4) by A5,A6,XREAL_1:66; IndexPoly (s,x) = ((2 * n * (s - 2) - (s - 4)) + s - 4) / (2 * s - 4) by SQUARE_1:22,A7,A3,XREAL_1:19 .= (2 * n * (s - 2)) / (2 * (s - 2)) .= (2 * n) / 2 by A4,XCMPLX_1:91 .= n; hence thesis by ORDINAL1:def 12; end; theorem Th35: for s being non trivial Nat, x being s-gonal number holds 0 <= ((8 * s - 16) * x) + (s - 4) ^2 proof let s be non trivial Nat; let x be s-gonal number; s - 2 >= 2 - 2 by XREAL_1:9,NAT_2:29; then 8 * (s - 2) >= 0; hence thesis; end; theorem Th36: for n being odd Nat st s >= 2 holds n divides Polygon (s,n) proof let n be odd Nat; assume A1: s >= 2; A2: Polygon (s,n) = (n * (s - 2) * (n - 1)) / 2 + n; A3: s - 0 >= 2 by A1; then s - 2 >= 0 by XREAL_1:11; then A4: n * (s - 2) * (n - 1) in NAT by INT_1:3; reconsider k = (n * (s - 2) * (n - 1)) / 2 as Nat by A4; A5: s - 2 in NAT by INT_1:3,A3,XREAL_1:11; k = n * ((s - 2) * ((n - 1) / 2)); then n divides k by NAT_D:def 3,A5; hence thesis by A2,NAT_D:8; end; begin :: Centered Polygonal Numbers ::\$N Centered polygonal number definition let s, n be Nat; func CenterPolygon (s,n) -> Integer equals (s * n) / 2 * (n - 1) + 1; coherence proof (n * (n - 1)) / 2 is Integer by Th2; then s * (n / 2 * (n - 1)) + 1 is Integer; hence thesis; end; end; registration let s be Nat; let n be non zero Nat; cluster CenterPolygon (s,n) -> natural; coherence proof n - 0 >= 1 by NAT_1:14; then n - 1 >= 0 by XREAL_1:11; hence thesis by INT_1:3; end; end; theorem CenterPolygon (0,n) = 1; theorem CenterPolygon (s,0) = 1; theorem CenterPolygon (s,n) = s * (Triangle (n -' 1)) + 1 proof CenterPolygon (s,n) = s * ((n * (n - 1)) / 2) + 1 .= s * (Triangle (n -' 1)) + 1 by Th21; hence thesis; end; begin :: On the Connection between Triangular and Other Polygonal Numbers theorem Th40: Triangle n = Polygon (3, n) proof Polygon (3, n) = n * (n + 1) / 2; hence thesis by Th19; end; theorem Th41: for n being odd Nat holds n divides Triangle n proof let n be odd Nat; n divides Polygon (3,n) by Th36; hence thesis by Th40; end; theorem Th42: Triangle n <= Triangle (n + 1) proof Triangle (n + 1) = Triangle (n) + (n + 1) by Th10; hence thesis by NAT_1:16; end; theorem for k being Nat st k <= n holds Triangle k <= Triangle n proof let k be Nat; assume k <= n; then consider i being Nat such that A1: n = k + i by NAT_1:10; defpred P[Nat] means for n being Nat holds Triangle n <= Triangle (n + \$1); A2: P[0]; A3: for k being Nat st P[k] holds P[k+1] proof let k be Nat; assume A4: P[k]; let n be Nat; A5: Triangle n <= Triangle (n + k) by A4; Triangle (n + k) <= Triangle (n + k + 1) by Th42; hence thesis by A5,XXREAL_0:2; end; for n being Nat holds P[n] from NAT_1:sch 2(A2,A3); hence thesis by A1; end; theorem Th44: n <= Triangle n proof defpred P[Nat] means \$1 <= Triangle \$1; A1: P[0]; A2: for k being Nat st P[k] holds P[k+1] proof let k be Nat; assume P[k]; Triangle (k + 1) = Triangle (k) + (k + 1) by Th10; hence thesis by NAT_1:11; end; for n being Nat holds P[n] from NAT_1:sch 2(A1,A2); hence thesis; end; theorem Th45: for n being non trivial Nat holds n < Triangle n proof let n be non trivial Nat; defpred P[Nat] means \$1 < Triangle \$1; A1: P[2] by Th12; A2: for k being non trivial Nat st P[k] holds P[k+1] proof let k be non trivial Nat; assume P[k]; Triangle (k + 1) = Triangle (k) + (k + 1) by Th10; hence thesis by NAT_1:16; end; for n being non trivial Nat holds P[n] from NAT_2:sch 2(A1,A2); hence thesis; end; theorem Th46: n <> 2 implies Triangle n is non prime proof assume A1: n <> 2; assume A2: Triangle n is prime; then A3: n <> 1 by Th11,INT_2:def 4; n <> 0 by A2,INT_2:def 4; then A4: n is non trivial by NAT_2:def 1,A3; per cases; suppose n is odd; then n = 1 or n = Triangle n by INT_2:def 4,A2,Th41; hence thesis by Th45,A4,Th11; end; suppose n is even; then consider k being Nat such that A5: n = 2 * k by ABIAN:def 2; A6: k <> 0 by A2,INT_2:def 4,A5; A7: Triangle n = n * (n + 1) / 2 by Th19 .= k * (n + 1) by A5; then k divides Triangle n by NAT_D:def 3; then per cases by INT_2:def 4,A2; suppose k = 1; hence thesis by A1,A5; end; suppose A8: k = Triangle n; 1 = k / k by A6,XCMPLX_1:60 .= n + 1 by A6,XCMPLX_1:89,A7,A8; then n = 0; hence thesis by INT_2:def 4,A2; end; end; end; registration let n be 3_or_greater Nat; cluster Triangle n -> non prime; coherence proof n <> 2 by EC_PF_2:def 1; hence thesis by Th46; end; end; registration cluster triangular -> non prime for 4_or_greater Nat; coherence proof let n be 4_or_greater Nat; assume n is triangular; then consider k being Nat such that A1: n = Triangle k; k <> 2 by A1,EC_PF_2:def 1,Th12; hence thesis by A1,Th46; end; end; registration let s be 4_or_greater non zero Nat, x be non zero s-gonal number; cluster IndexPoly (s,x) -> natural; coherence by Th34,EC_PF_2:def 1; end; theorem for s being 4_or_greater Nat, x being non zero s-gonal number st s <> 2 holds Polygon (s, IndexPoly (s,x)) = x proof let s be 4_or_greater Nat, x be non zero s-gonal number; assume s <> 2; then A1: s - 2 <> 0; A2: 0 <= (((8 * s - 16) * x) + (s - 4) ^2) by Th35; set qq = sqrt (((8*s - 16) * x) + (s - 4) ^2); set w = IndexPoly (s,x); A3: w ^2 * (s - 2) = ((qq + s - 4)^2 / (2 * s - 4) ^2) * (s - 2) by XCMPLX_1:76 .= ((qq + s - 4)^2 / (4 * (s - 2) * (s - 2))) * (s - 2) .= ((qq^2 + (s - 4)^2 + 2*qq*(s-4))/ (4 * (s - 2))) by XCMPLX_1:92,A1; A4: w * (s - 4) = (qq + s - 4) * (s - 4) / (2 * s - 4) by XCMPLX_1:74 .= 2 * (qq * (s - 4) + (s - 4)^2) / (2 * (2*(s - 2))) by XCMPLX_1:91 .= 2 * (qq * (s - 4) + (s - 4)^2) / (4 * (s - 2)); A5: qq^2 = ((8 * s - 16) * x) + (s - 4) ^2 by SQUARE_1:def 2,A2; Polygon (s, w) = ( (qq^2 + (s - 4)^2 + 2 * qq * (s - 4)) - 2 * (qq * (s - 4) + (s - 4)^2)) / (4 * (s - 2)) / 2 by XCMPLX_1:120,A3,A4 .= ( (qq^2 + (s - 4)^2 + 2 * qq * (s - 4)) - 2 * (qq * (s - 4) + (s - 4)^2)) / ((4 * (s - 2) * 2)) by XCMPLX_1:78 .= x by A1,XCMPLX_1:89,A5; hence thesis; end; theorem 36 is square triangular proof A1: 6 ^2 = 36; Triangle 8 = (8 + 1) * 8 / 2 by Th19 .= 36; hence thesis by A1; end; registration let n be Nat; cluster Polygon (3,n) -> natural; coherence proof Triangle n = Polygon (3, n) by Th40; hence thesis; end; end; registration let n be Nat; cluster Polygon (3,n) -> triangular; coherence proof Triangle n = Polygon (3, n) by Th40; hence thesis; end; end; theorem Th49: Polygon (s,n) = (s - 2) * Triangle (n -' 1) + n proof Polygon (s,n) = (s - 2) * (n * (n - 1) / 2) + n .= (s - 2) * Triangle (n -' 1) + n by Th21; hence thesis; end; theorem Polygon (s,n) = (s - 3) * Triangle (n -' 1) + Triangle n proof (s - 3) * Triangle (n -' 1) + Triangle n = (s - 3) * (n * (n - 1) / 2) + Triangle n by Th21 .= (s - 3) * (n * (n - 1) / 2) + n * (n+1) / 2 by Th19; hence thesis; end; theorem Polygon (0,n) = n * (2 - n); theorem Polygon (1,n) = n * (3 - n) / 2; theorem Polygon (2,n) = n; registration let s be non trivial Nat, n be Nat; cluster Polygon (s,n) -> natural; coherence proof s >= 0 + 2 by NAT_2:29; then A1: s - 2 >= 0 by XREAL_1:19; Polygon (s,n) = (s - 2) * Triangle (n -' 1) + n by Th49; hence thesis by INT_1:3,A1; end; end; registration let n be Nat; cluster Polygon (4,n) -> square; coherence; end; registration cluster 3-gonal -> triangular for Nat; coherence; cluster triangular -> 3-gonal for Nat; coherence proof let x be Nat; assume x is triangular; then consider n being Nat such that A1: x = Triangle n; x = Polygon (3,n) by A1,Th40; hence thesis; end; cluster 4-gonal -> square for Nat; coherence; cluster square -> 4-gonal for Nat; coherence proof let x be Nat; assume x is square; then consider n being Nat such that A2: x = n^2 by PYTHTRIP:def 3; x = Polygon (4,n) by A2; hence thesis; end; end; theorem Triangle (n -' 1) + Triangle (n) = n^2 proof per cases; suppose n <> 0; then A1: n -' 1 = n - 1 by XREAL_1:233,NAT_1:14; Triangle (n -' 1) = (n - 1) * (n - 1 + 1) / 2 by Th19,A1; then Triangle (n -' 1) + Triangle (n) = (n - 1) * (n + 1 - 1) / 2 + n * (n + 1) / 2 by Th19 .= n ^2; hence thesis; end; suppose A2: n = 0; then Triangle (n -' 1) + Triangle (n) = Triangle (0 -' 1) + Triangle 0 .= n^2 by A2,XREAL_0:def 2,Lm3; hence thesis; end; end; theorem Th55: Triangle (n) + Triangle (n + 1) = (n + 1) ^2 proof Triangle n = n * (n + 1) / 2 by Th19; then Triangle n + Triangle (n + 1) = n * (n + 1) / 2 + (n + 1) * (n + 1 + 1) / 2 by Th19 .= (n + 1) ^2; hence thesis; end; registration let n be Nat; cluster Triangle n + Triangle (n + 1) -> square; coherence proof Triangle (n) + Triangle (n + 1) = (n + 1) ^2 by Th55; hence thesis; end; end; theorem for n being non trivial Nat holds (1 / 3) * Triangle (3 * n -' 1) = n * (3 * n - 1) / 2 proof let n be non trivial Nat; A1: (3*n)-'1 = (3*n)-1 by XREAL_1:233,Th1; Triangle (3*n-'1) = ((3*n-1) * (3*n-1+1)) / 2 by A1,Th19; hence thesis; end; theorem for n being non zero Nat holds Triangle (2 * n -' 1) = n * (4 * n - 2) / 2 proof let n be non zero Nat; A1: (2 * n) -' 1 = (2 * n) - 1 by XREAL_1:233,Th1; Triangle (2 * n -' 1) = ((2 * n - 1) * (2 * n - 1 + 1)) / 2 by A1,Th19; hence thesis; end; definition let n, k be Nat; func NPower (n, k) -> FinSequence of REAL means :Def8: dom it = Seg k & for i being Nat st i in dom it holds it.i = i |^ n; existence proof reconsider k1 = k as Element of NAT by ORDINAL1:def 12; deffunc f(Nat) = In (\$1 |^ n, REAL); consider e being FinSequence of REAL such that A1: len e = k1 & for i being Nat st i in dom e holds e.i = f(i) from FINSEQ_2:sch 1; take e; thus dom e = Seg k by FINSEQ_1:def 3,A1; let i be Nat; assume A2: i in dom e; f(i) = i |^ n; hence thesis by A2,A1; end; uniqueness proof deffunc f(Nat) = \$1 |^ n; let e1,e2 be FinSequence of REAL such that A3: dom e1 = Seg k & for i being Nat st i in dom e1 holds e1.i = f(i) and A4: dom e2 = Seg k & for i being Nat st i in dom e2 holds e2.i = f(i); for i be Nat st i in dom e1 holds e1.i = e2.i proof let i be Nat; assume A5: i in dom e1; hence e1.i = f(i) by A3 .= e2.i by A5,A3,A4; end; hence thesis by A3,A4,FINSEQ_1:13; end; end; theorem Th58: for k being Nat holds NPower (n,k+1) = NPower (n,k) ^ <*(k+1) |^ n*> proof let k be Nat; A1: dom NPower (n,k+1) = dom (NPower (n,k) ^ <*(k+1) |^ n*>) proof Seg (len NPower (n,k)) = dom NPower (n,k) by FINSEQ_1:def 3 .= Seg k by Def8; then A2: len NPower (n,k) = k by FINSEQ_1:6; A3: len <*(k+1) |^ n*> = 1 by FINSEQ_1:40; dom (NPower (n,k) ^ <*(k+1) |^ n*>) = Seg (len (NPower (n,k)) + len <*(k+1) |^ n*>) by FINSEQ_1:def 7 .= dom NPower (n,k+1) by Def8,A3,A2; hence thesis; end; for l being Nat st l in dom NPower (n,k+1) holds (NPower (n,k+1)).l = (NPower (n,k) ^ <*(k+1) |^ n*>).l proof let l be Nat; assume A4: l in dom NPower (n,k+1); then l in Seg (k+1) by Def8; then A5: 1 <= l & l <= k+1 by FINSEQ_1:1; set NP = (NPower (n,k) ^ <*(k+1) |^ n*>).l; (NPower (n,k) ^ <*(k+1) |^ n*>).l = l |^ n proof per cases by A5,NAT_1:8; suppose l <= k; then l in Seg k by A5,FINSEQ_1:1; then A6: l in dom NPower (n,k) by Def8; then NP = (NPower (n,k)).l by FINSEQ_1:def 7 .= l |^ n by Def8,A6; hence thesis; end; suppose A7: l = k + 1; Seg k = dom NPower (n,k) by Def8 .= Seg len NPower (n,k) by FINSEQ_1:def 3; then k = len NPower (n,k) by FINSEQ_1:6; hence thesis by A7,FINSEQ_1:42; end; end; hence thesis by Def8,A4; end; hence thesis by A1,FINSEQ_1:13; end; registration let n be Nat; reduce Sum NPower (n, 0) to 0; reducibility proof dom NPower (n,0) = Seg 0 by Def8 .= {}; hence thesis by RVSUM_1:72,RELAT_1:41; end; end; theorem (Triangle n) |^ 2 = Sum NPower (3, n) proof defpred P[Nat] means (Triangle \$1)|^2 = Sum NPower (3, \$1); A1: P[0] proof thus (Triangle 0) |^ 2 = 0 * 0 by NEWTON:81 .= Sum NPower (3, 0); end; A2: for k being Nat st P[k] holds P[k+1] proof let k be Nat such that A3: P[k]; reconsider k1 = k + 1 as Element of REAL by XREAL_0:def 1; (Triangle (k + 1)) |^ 2 = ((k + 1) * (k + 1 + 1) / 2) |^ 2 by Th19 .= ((k + 1) * (k + 2) / 2) * ((k + 1) * (k + 2) / 2) by NEWTON:81 .= (k + 1) * (k + 1) * (k + 2) * (k + 2) / (2 * 2) .= (k + 1) |^ 2 * (k + 2) * (k + 2) / (2 * 2) by NEWTON:81 .= (k + 1) |^ 2 * (k * k + 4 * k + 4) / (2 * 2) .= (k + 1) |^ 2 * (k |^ 2 + 4 * k + 4) / (2 * 2) by NEWTON:81 .= ((k + 1) |^ 2 * k |^ 2) / 4 + ((k + 1) |^ 2 * 4 * k) / 4 + ((k + 1) |^ 2 * 4) / 4 .= (((k + 1) * k) |^ 2) / (2 * 2) + ((k + 1) |^ 2 * 4 * k) / 4 + ((k + 1) |^ 2 * 4) / 4 by NEWTON:7 .= (((k + 1) * k) |^ 2) / (2 |^ 2) + ((k + 1) |^ 2 * 4 * k) / 4 + ((k + 1) |^ 2 * 4) / 4 by NEWTON:81 .= ((k + 1) |^ 2 * k |^ 2) / (2 |^ 2) + ((k + 1) |^ 2 * 4 * k) / 4 + ((k + 1) |^ 2 * 4) / 4 by NEWTON:7 .= (k + 1) * (k + 1) * k |^ 2 / (2 |^ 2) + ((k + 1) |^ 2 * 4 * k) / 4 + ((k + 1) |^ 2 * 4) / 4 by NEWTON:81 .= (k + 1) * (k + 1) * (k * k) / (2 |^ 2) + ((k + 1) |^ 2 * 4 * k) / 4 + ((k + 1) |^ 2 * 4) / 4 by NEWTON:81 .= (k + 1) * (k + 1) * k * k / (2 * 2) + ((k + 1) |^ 2 * 4 * k) / 4 + ((k + 1) |^ 2 * 4) / 4 by NEWTON:81 .= ((k + 1) * k / 2) * ((k + 1) * k / 2) + ((k + 1) |^ 2 * 4 * k) / 4 + ((k + 1) |^ 2 * 4) / 4 .= (Triangle k) * ((k + 1) * k / 2) + ((k + 1) |^ 2 * 4 * k) / 4 + ((k + 1) |^ 2 * 4) / 4 by Th19 .= (Triangle k) * (Triangle k) + ((k + 1) |^ 2 * 4 * k) / 4 + ((k + 1) |^ 2 * 4) / 4 by Th19 .= (Triangle k) |^ 2 + ((k + 1) |^ 2 * 4 * k) / 4 + ((k + 1) |^ 2 * 4) / 4 by NEWTON:81 .= Sum NPower (3, k) + (k + 1) |^2 * (k + 1) by A3 .= Sum NPower (3, k) + ((k + 1) * (k + 1) * (k + 1)) by NEWTON:81 .= Sum NPower (3, k) + ((k + 1) |^ 3) by POLYEQ_3:27 .= Sum (NPower (3, k) ^ <* k1 |^ 3 *>) by RVSUM_1:74 .= Sum NPower (3, k + 1) by Th58; hence thesis; end; for n being Nat holds P[n] from NAT_1:sch 2(A1,A2); hence thesis; end; theorem for n being non trivial Nat holds Triangle n + Triangle (n -' 1) * Triangle (n + 1) = (Triangle n) |^ 2 proof let n be non trivial Nat; A1:Triangle n = n * (n + 1) / 2 by Th19; 0 + 1 <= n by NAT_1:13; then A2: n -' 1 = n - 1 by XREAL_1:233; A3: Triangle (n -' 1) = (n -' 1) * (n -' 1 + 1) / 2 by Th19 .= (n - 1) * n / 2 by A2; Triangle (n + 1) = (n + 1) * (n + 1 + 1) / 2 by Th19 .= (n + 1) * (n + 2) / 2;then Triangle n + Triangle (n -' 1) * Triangle (n + 1) = Triangle n * Triangle n by A1,A3 .= (Triangle n) |^ 2 by NEWTON:81; hence thesis; end; theorem (Triangle n) |^ 2 + (Triangle (n + 1)) |^ 2 = Triangle ((n + 1) |^ 2) proof A1: Triangle (n + 1) = (n + 1) * (n + 1 + 1) / 2 by Th19 .= (n + 1) * (n + 2) / 2; A2: (n + 1) |^ 2 = (n + 1) * (n + 1) by NEWTON:81; (Triangle n) |^ 2 + (Triangle (n + 1)) |^ 2 = (n * (n + 1) / 2) |^ 2 + (Triangle (n + 1)) |^ 2 by Th19 .= (n * (n + 1) / 2) * (n * (n + 1) / 2) + ((n + 1) * (n + 2) / 2) |^ 2 by NEWTON:81,A1 .= (n * (n + 1) / 2) * (n * (n + 1) / 2) + ((n + 1) * (n + 2) / 2) * ((n + 1) * (n + 2) / 2) by NEWTON:81 .= (n + 1) |^ 2 * ((n + 1) |^ 2 + 1) / 2 by A2 .= Triangle (n + 1) |^ 2 by Th19; hence thesis; end; theorem (Triangle (n + 1)) |^ 2 - (Triangle n) |^ 2 = (n + 1) |^ 3 proof A1: Triangle (n + 1) = (n + 1) * (n + 1 + 1) / 2 by Th19 .= (n + 1) * (n + 2) / 2; A2: (n + 1) |^ 3 = (n + 1) * (n + 1) * (n + 1) by POLYEQ_3:27 .= n * n * n + 3 * n * n + 3 * n + 1; A3: (n + 1) * (n + 1) = (n + 1) |^ 2 by NEWTON:81; (Triangle (n + 1)) |^ 2 - (Triangle n) |^ 2 = ((n + 1) * (n + 2) / 2) |^ 2 - (n * (n + 1) / 2) |^ 2 by Th19,A1 .= ((n + 1) * (n + 2) / 2) * ((n + 1) * (n + 2) / 2) - (n * (n + 1) / 2) |^ 2 by NEWTON:81 .= (n + 1) * (n + 1) * (n + 2) * (n + 2) / 4 - (n * (n + 1) / 2) |^ 2 .= (n + 1) |^ 2 * (n + 2) * (n + 2) / 4 - (n * (n + 1) / 2) |^ 2 by NEWTON:81 .= (n + 1) |^ 2 * (n + 2) * (n + 2) / 4 - (n * (n + 1) / 2) * (n * (n + 1) / 2) by NEWTON:81 .= (n + 1) |^ 2 * (n + 2) * (n + 2) / 4 - n * n * (n + 1) * (n + 1) / 4 .= (n + 1) |^ 2 * (n + 2) * (n + 2) / 4 - n |^ 2 * (n + 1) * (n + 1) / 4 by NEWTON:81 .= (n + 1) |^ 2 * (n * n + 2 * n + 2 * n + 4 - n |^ 2) / 4 by A3 .= (n + 1) |^ 2 * (n |^ 2 + 2 * n + 2 * n + 4 - n |^ 2) / 4 by NEWTON:81 .= (n + 1) |^ 2 * (n + 1) .= (n + 1) * (n + 1) * (n + 1) by NEWTON:81 .= (n + 1) |^ 3 by A2; hence thesis; end; theorem for n being non zero Nat holds 3 * (Triangle n) + (Triangle (n -' 1)) = Triangle (2 * n) proof let n be non zero Nat; A1: n -' 1 = n - 1 by XREAL_1:233,NAT_1:14; A2: Triangle (n -' 1) = (n - 1) * (n - 1 + 1) / 2 by A1,Th19; 3 * (Triangle n) + (Triangle (n -' 1)) = 3 * (n * (n + 1) / 2) + (n - 1) * (n - 1 + 1) / 2 by A2,Th19 .= 2 * n * (2 * n + 1) / 2 .= Triangle (2 * n) by Th19; hence thesis; end; theorem 3 * (Triangle n) + Triangle (n + 1) = Triangle (2 * n + 1) proof A1: Triangle n = n * (n + 1) / 2 by Th19; A2: Triangle (n + 1) = (n + 1) * (n + 1 + 1) / 2 by Th19 .= (n + 1) * (n + 2) / 2; Triangle (2 * n + 1) = (2 * n + 1) * (2 * n + 1 + 1) / 2 by Th19 .= (2 * n + 1) * (2 * n + 2) / 2; hence thesis by A1,A2; end; theorem for n being non zero Nat holds Triangle (n -' 1) + 6 * (Triangle n) + Triangle (n + 1) = 8 * (Triangle n) + 1 proof let n be non zero Nat; A1: n -' 1 = n - 1 by XREAL_1:233,NAT_1:14; A2: Triangle (n -' 1) = (n - 1) * (n - 1 + 1) / 2 by A1,Th19; A3: Triangle n = n * (n + 1) / 2 by Th19; Triangle (n + 1) = (n + 1) * (n + 1 + 1) / 2 by Th19 .= (n + 1) * (n + 2) / 2; hence thesis by A3,A2; end; theorem for n being non zero Nat holds Triangle n + Triangle (n -' 1) = (1 + 2 * n - 1) * n / 2 proof let n be non zero Nat; A1: n-'1 = n-1 by XREAL_1:233,NAT_1:14; A2: Triangle (n -' 1) = (n - 1) * (n - 1 + 1) / 2 by A1,Th19; Triangle n + Triangle (n -' 1) = n * (n + 1) / 2 + Triangle (n-'1) by Th19 .= (1 + 2 * n - 1) * n / 2 by A2; hence thesis; end; theorem Th67: 1 + 9 * Triangle n = Triangle (3 * n + 1) proof A1: Triangle n = n * (n + 1) / 2 by Th19; Triangle (3 * n + 1) = (3 * n + 1) * (3 * n + 1 + 1) / 2 by Th19 .= 1 + 9 * Triangle n by A1; hence thesis; end; theorem for m being Nat holds Triangle (n + m) = Triangle n + Triangle m + n * m proof let m be Nat; Triangle (n + m) = (n + m) * (n + m + 1) / 2 by Th19 .= n * (n + 1) / 2 + m * (m + 1) / 2 + n * m .= Triangle n + m * (m + 1) / 2 + n * m by Th19 .= Triangle n + Triangle m + n * m by Th19; hence thesis; end; theorem for n,m being non trivial Nat holds (Triangle n) * (Triangle m) + (Triangle (n -' 1)) * (Triangle (m -' 1)) = Triangle (n * m) proof let n, m be non trivial Nat; 0+1 <= n by NAT_1:13; then A1: n -' 1 = n - 1 by XREAL_1:233; 0 + 1 <= m by NAT_1:13; then A2: m -' 1 = m - 1 by XREAL_1:233; A3: Triangle (n -' 1) = (n - 1) * (n - 1 + 1) / 2 by A1,Th19; A4: Triangle (m -' 1) = (m - 1) * (m - 1 + 1) / 2 by A2,Th19; A5: Triangle (n * m) = n * m * (n * m + 1) / 2 by Th19; (Triangle n) * (Triangle m) + (Triangle (n -' 1)) * (Triangle (m -' 1)) = (n * (n + 1) / 2) * (Triangle m) + (Triangle (n -' 1)) * (Triangle (m -' 1)) by Th19 .= (n * (n + 1) / 2) * (m * (m + 1) / 2) + ((n - 1) * (n - 1 + 1) / 2) * ((m - 1) * (m - 1 + 1) / 2) by A4,A3,Th19 .= ((n * n + n) / 2) * ((m * m + m) / 2) + ((n * n - n) / 2) * ((m * m - m) / 2) .= ((n |^ 2 + n) / 2) * ((m * m + m) / 2) + ((n * n - n) / 2) * ((m * m - m) / 2) by NEWTON:81 .= ((n |^ 2 + n) / 2) * ((m |^ 2 + m) / 2) + ((n * n - n) / 2) * ((m * m - m) / 2) by NEWTON:81 .= ((n |^ 2 + n) / 2) * ((m |^ 2 + m) / 2) + ((n |^ 2 - n) / 2) * ((m * m - m) / 2) by NEWTON:81 .= ((n |^ 2 + n) / 2) * ((m |^ 2 + m) / 2) + ((n |^ 2 - n) / 2) * ((m |^ 2 - m) / 2) by NEWTON:81 .= (n |^ 2 * m |^ 2 + n * m) / 2 .= (n * n * (m |^ 2) + n * m) / 2 by NEWTON:81 .= (n * n * (m * m) + n * m) / 2 by NEWTON:81 .= Triangle (n * m) by A5; hence thesis; end; begin :: Sets of Polygonal Numbers definition let s be Nat; func PolygonalNumbers s -> set equals the set of all Polygon (s,n) where n is Nat; coherence; end; definition let s be non trivial Nat; redefine func PolygonalNumbers s -> Subset of NAT; coherence proof the set of all Polygon (s,n) where n is Nat c= NAT proof let x be object; assume x in the set of all Polygon (s,n) where n is Nat ; then ex n being Nat st x = Polygon (s,n); hence thesis by ORDINAL1:def 12; end; hence thesis; end; end; Lm4: for s being non trivial Nat holds PolygonalNumbers s is Subset of NAT; definition func TriangularNumbers -> Subset of NAT equals PolygonalNumbers 3; coherence proof 3 is non trivial by NAT_2:def 1; hence thesis by Lm4; end; func SquareNumbers -> Subset of NAT equals PolygonalNumbers 4; coherence proof 4 is non trivial by NAT_2:def 1; hence thesis by Lm4; end; end; registration let s be non trivial Nat; cluster PolygonalNumbers s -> non empty; coherence proof A1: Polygon (s,0) is set; Polygon (s,n) in PolygonalNumbers s; hence thesis by A1,XBOOLE_0:def 1; end; end; registration cluster TriangularNumbers -> non empty; coherence proof 3 is non trivial by NAT_2:def 1; hence thesis; end; cluster SquareNumbers -> non empty; coherence proof 4 is non trivial by NAT_2:def 1; hence thesis; end; end; registration cluster -> triangular for Element of TriangularNumbers; coherence proof let x be Element of TriangularNumbers; x in TriangularNumbers by SUBSET_1:def 1; then ex n being Nat st x = Polygon (3,n); hence thesis; end; cluster -> square for Element of SquareNumbers; coherence proof let x be Element of SquareNumbers; x in SquareNumbers by SUBSET_1:def 1; then ex n being Nat st x = Polygon (4,n); hence thesis; end; end; theorem Th70: for x being number holds x in TriangularNumbers iff x is triangular proof let x be number; thus x in TriangularNumbers implies x is triangular; assume x is triangular; then consider n being Nat such that A1: x = Triangle n; x = Polygon (3,n) by A1,Th40; hence thesis; end; theorem Th71: for x being number holds x in SquareNumbers iff x is square proof let x be number; thus x in SquareNumbers implies x is square; assume x is square; then consider n being Nat such that A1: x = n ^2 by PYTHTRIP:def 3; x = Polygon (4,n) by A1; hence thesis; end; begin :: Some Well-known Properties theorem Th72: (n + 1) choose 2 = n * (n + 1) / 2 proof per cases; suppose A1: n <> 0; then A2: n = n -' 1 + 1 by XREAL_1:235,NAT_1:14; A3: n + 1 >= 1 + 1 by NAT_1:14,A1,XREAL_1:6; n -' 1 = n - 1 by XREAL_1:233,NAT_1:14,A1 .= (n + 1) - 2; then (n + 1) choose 2 = ((n + 1)!) / (2! * ((n -' 1)!)) by NEWTON:def 3,A3 .= (n! * (n + 1)) / (2 * ((n -' 1)!)) by NEWTON:15,14 .= ((n -' 1)! * n * (n + 1)) / (2 * ((n -' 1)!)) by NEWTON:15,A2 .= ((n -' 1)! * (n * (n + 1))) / (2 * ((n -' 1)!)) .= (n * (n + 1)) / 2 by XCMPLX_1:91; hence thesis; end; suppose n = 0; hence thesis by NEWTON:def 3; end; end; theorem Triangle n = (n + 1) choose 2 proof (n + 1) choose 2 = n * (n + 1) / 2 by Th72; hence thesis by Th19; end; theorem Th74: for n being non zero Nat st n is even perfect holds n is triangular proof let n be non zero Nat; assume n is even perfect; then consider p being Nat such that A1: 2 |^ p -' 1 is prime & n = 2 |^ (p -' 1) * (2 |^ p -' 1) by NAT_5:39; set p1 = Mersenne p; A2: p <> 0 proof assume p = 0; then 2 |^ p -' 1 = 1 -' 1 by NEWTON:4 .= 0 by XREAL_1:232; hence thesis by A1; end; A3: n = 2 |^ (p -' 1) * p1 by A1,XREAL_0:def 2; A4: p -' 1 = p - 1 by XREAL_1:233,A2,NAT_1:14; (2 to_power p) / (2 to_power 1) = (p1 + 1) / 2; then A5: (2 to_power (p -' 1)) = (p1 + 1) / 2 by A4,POWER:29; (p1 * (p1 + 1)) / 2 = Triangle p1 by Th19; hence thesis by A3,A5; end; registration let n be non zero Nat; cluster Mersenne n -> non zero; coherence proof assume Mersenne n = 0; then log (2, 2 to_power n) = 0 by POWER:51; then n * log (2, 2) = 0 by POWER:55; then n * 1 = 0 by POWER:52; hence thesis; end; end; definition let n be number; attr n is mersenne means :Def12: ex p being Nat st n = Mersenne p; end; registration cluster mersenne for Prime; existence proof reconsider p = Mersenne 2 as Prime by PEPIN:41,GR_CY_3:18; p is mersenne; hence thesis; end; cluster non prime for Nat; existence by INT_2:29; end; registration cluster mersenne non prime for Nat; existence proof set p = Mersenne 11; reconsider p as non prime Nat by INT_2:def 4,GR_CY_3:22,NAT_D:9; p is mersenne; hence thesis; end; end; registration cluster -> non zero for Prime; coherence by INT_2:def 4; end; registration let n be mersenne Prime; cluster Triangle n -> perfect; coherence proof reconsider n0 = Triangle n as non zero Nat by TARSKI:1; consider p being Nat such that A1: n = Mersenne p by Def12; 2 to_power p > 0 by POWER:34; then 2 |^ p >= 0 + 1 by NAT_1:13; then A2: 2 |^ p -' 1 = 2 |^ p - 1 by XREAL_0:def 2,XREAL_1:19; A3: p -' 1 = p - 1 by XREAL_1:233,A1,GR_CY_3:16,NAT_1:14; reconsider p1 = Mersenne p as Nat; (2 to_power p) / (2 to_power 1) = (p1 + 1) / 2; then 2 to_power (p -' 1) = (p1 + 1) / 2 by A3,POWER:29; then p1 * 2|^ (p -' 1) = (p1 * (p1 + 1)) / 2; then n0 is perfect by NAT_5:38,A2,A1,Th19; hence thesis; end; end; registration cluster even perfect -> triangular for non zero Nat; coherence by Th74; end; theorem Th75: 8 * (Triangle n) + 1 = (2 * n + 1) ^2 proof 8 * Triangle n = 8 * (n * (n + 1) / 2) by Th19 .= 4 * (n^2 + n); hence thesis; end; theorem Th76: n is triangular implies 8 * n + 1 is square proof assume n is triangular; then consider k being Nat such that A1: n = Triangle k; 8 * (Triangle k) + 1 = (2 * k + 1) ^2 by Th75; hence 8 * n + 1 is square by A1; end; theorem Th77: n is triangular implies 9 * n + 1 is triangular proof assume n is triangular; then consider k being Nat such that A1: n = Triangle k; 1 + 9 * Triangle k = Triangle (3 * k + 1) by Th67; hence thesis by A1; end; theorem Th78: Triangle n is triangular square implies Triangle (4 * n * (n + 1)) is triangular square proof assume Triangle n is triangular square; then n * (n + 1) / 2 is triangular square by Th19; then consider k being Nat such that A1: n * (n + 1) / 2 = k ^2 by PYTHTRIP:def 3; Triangle (4 * n * (n + 1)) = (8 * k ^2) * (8 * k^2 + 1) / 2 by Th19,A1 .= (4 * k ^2) * (4 * n * (n + 1) + 1) by A1 .= ((2 * k) * (2 * n + 1)) ^2; hence thesis; end; registration cluster TriangularNumbers -> infinite; coherence proof set T = TriangularNumbers; for m being Element of NAT ex n being Element of NAT st n >= m & n in T proof let m be Element of NAT; reconsider w = Triangle m as Nat by TARSKI:1; A1: w is triangular; reconsider n = 9 * w + 1 as Element of NAT by ORDINAL1:def 12; take n; A2: w >= m by Th44; 9 * w >= 1 * w by XREAL_1:64; then 9 * w + 1 > w by NAT_1:13; hence n >= m by A2,XXREAL_0:2; thus thesis by Th70,A1,Th77; end; hence thesis by PYTHTRIP:9; end; cluster SquareNumbers -> infinite; coherence proof set T = SquareNumbers; for m being Element of NAT ex n being Element of NAT st n >= m & n in T proof let m be Element of NAT; reconsider w = Triangle m as Nat by TARSKI:1; A3: w is triangular; reconsider n = 8 * w + 1 as Element of NAT by ORDINAL1:def 12; take n; A4: w >= m by Th44; 8 * w >= 1 * w by XREAL_1:64; then 8 * w + 1 > w by NAT_1:13; hence n >= m by A4,XXREAL_0:2; thus thesis by Th71,A3,Th76; end; hence thesis by PYTHTRIP:9; end; end; registration cluster triangular square non zero for Nat; existence proof reconsider a = Triangle 1 as Nat by TARSKI:1; take a; 1 = 1 ^2; then Triangle 1 is triangular square by FINSEQ_2:50,RVSUM_1:73; hence thesis; end; end; theorem Th79: 0 is triangular square proof 0 = 0 ^2; then Triangle 0 is triangular square; hence thesis; end; registration cluster zero -> triangular square for number; coherence by Th79; end; theorem Th80: 1 is triangular square proof 1 = 1 ^2; hence thesis by Th11; end; ::\$N Square triangular number theorem 36 is triangular square proof Triangle (4 * 1 * (1 + 1)) is triangular square by Th11,Th80,Th78; hence thesis by Th18; end; theorem 1225 is triangular square proof A1: 35 ^2 = 1225; Triangle 49 = 49 * (49 + 1) / 2 by Th19 .= 1225; hence thesis by A1; end; registration let n be triangular Nat; cluster 9 * n + 1 -> triangular; coherence by Th77; end; registration let n be triangular Nat; cluster 8 * n + 1 -> square; coherence by Th76; end; begin :: Reciprocals of Triangular Numbers registration let a be Real; reduce lim seq_const a to a; reducibility proof (seq_const a).1 = a by SEQ_1:57; hence thesis by SEQ_4:25; end; end; definition func ReciTriangRS -> Real_Sequence means :Def13: for i being Nat holds it.i = 1 / Triangle i; correctness proof deffunc F(Nat) = 1 / Triangle \$1; thus (ex seq being Real_Sequence st for n being Nat holds seq.n = F(n)) & (for seq1, seq2 being Real_Sequence st (for n being Nat holds seq1.n = F(n)) & (for n being Nat holds seq2.n = F(n)) holds seq1 = seq2) from LNatRealSeq; end; end; registration reduce ReciTriangRS.0 to 0; reducibility proof thus ReciTriangRS.0 = 1 / Triangle 0 by Def13 .= 0; end; end; theorem Th83: 1 / (Triangle n) = 2 / (n * (n + 1)) proof 1 / (Triangle n) = 1 / ((n * (n + 1)) / 2) by Th19 .= 2 / (n * (n + 1)) by XCMPLX_1:57; hence thesis; end; theorem Th84: Partial_Sums ReciTriangRS.n = 2 - 2 / (n + 1) proof defpred P[Nat] means Partial_Sums ReciTriangRS.\$1 = 2 - 2/(\$1+1); A1: P[0] proof ReciTriangRS.0 = 0; hence thesis by SERIES_1:def 1; end; A2: for k being Nat st P[k] holds P[k+1] proof let k be Nat such that A3: P[k]; A4: ReciTriangRS.(k+1) = 1 / Triangle (k+1) by Def13 .= 2 / ((k + 1) * (k + 1 + 1)) by Th83 .= 2 / (k * k + 3 * k + 2); A5: (k + 2) / (k + 2) = 1 by XCMPLX_1:60; A6: (k + 1) / (k + 1) = 1 by XCMPLX_1:60; Partial_Sums ReciTriangRS.(k+1) = 2 * ((k + 2) / (k + 2)) - (2 / (k + 1)) * 1 + 2 / ((k + 1) * (k + 2)) by A5,A3,A4,SERIES_1:def 1 .= (2 * (k + 2)) / (k + 2) - (2 / (k + 1)) * ((k + 2) / (k + 2)) + 2 / ((k + 1) * (k + 2)) by XCMPLX_1:74,A5 .= ((2 * (k + 2)) / (k + 2)) * ((k + 1) / (k + 1)) - (2 * (k + 2)) / ((k + 1) * (k + 2)) + 2 / ((k + 1) * (k + 2)) by A6,XCMPLX_1:76 .= (2 * (k + 2) * (k + 1)) / ((k + 2) * (k + 1)) - (2 * (k + 2)) / ((k + 1) * (k + 2)) + 2 / ((k + 1) * (k + 2)) by XCMPLX_1:76 .= (2 * k * k + 6 * k + 4 - (2 * k + 4)) / ((k + 2) * (k + 1)) + 2 / ((k + 1) * (k + 2)) by XCMPLX_1:120 .= (2 * k * k + 6 * k + 4 - (2 * k + 4) + 2) / ((k + 2) * (k + 1)) by XCMPLX_1:62 .= (2 * (k + 1)) * (k + 1) / ((k + 2) * (k + 1)) .= (2 * (k + 2) - 2) / (k + 2) by XCMPLX_1:91 .= 2 * (k + 2) / (k + 2) - 2 / (k + 2) by XCMPLX_1:120 .= 2 - 2 / (k + 2) by XCMPLX_1:89; hence thesis; end; for k being Nat holds P[k] from NAT_1:sch 2(A1,A2); hence thesis; end; definition func SumsReciTriang -> Real_Sequence means :Def14: for n being Nat holds it.n = 2 - 2 / (n + 1); correctness proof deffunc F(Nat) = 2 - 2 / (\$1 + 1); thus (ex seq being Real_Sequence st for n being Nat holds seq.n = F(n)) & (for seq1, seq2 being Real_Sequence st (for n being Nat holds seq1.n = F(n)) & (for n being Nat holds seq2.n = F(n)) holds seq1 = seq2) from LNatRealSeq; end; let a, b be Real; func geo-seq (a,b) -> Real_Sequence means :Def15: for n being Nat holds it.n = a / (n + b); correctness proof deffunc F(Nat) = a / (\$1 + b); thus (ex seq being Real_Sequence st for n being Nat holds seq.n = F(n)) & (for seq1, seq2 being Real_Sequence st (for n being Nat holds seq1.n = F(n)) & (for n being Nat holds seq2.n = F(n)) holds seq1 = seq2) from LNatRealSeq; end; end; theorem Th85: for a, b being Real st b > 0 holds geo-seq (a,b) is convergent & lim geo-seq (a,b) = 0 proof let a, b be Real; assume A1: b > 0; for k being Nat holds geo-seq (a,b).k = a / (k + b) by Def15; hence thesis by A1,SEQ_4:31; end; theorem Th86: SumsReciTriang = seq_const 2 + - geo-seq (2,1) proof for k being Nat holds SumsReciTriang.k = (seq_const 2).k + (- geo-seq (2,1)).k proof let k be Nat; A1: SumsReciTriang.k = 2 - 2 / (k + 1) by Def14; A2: (seq_const 2).k = 2 by SEQ_1:57; - (geo-seq(2,1)).k = (- geo-seq(2,1)).k by VALUED_1:8; then (- geo-seq(2,1)).k = - 2 / (k + 1) by Def15; hence thesis by A1,A2; end; hence thesis by SEQ_1:7; end; theorem Th87: SumsReciTriang is convergent & lim SumsReciTriang = 2 proof A1: seq_const 2 is convergent & lim seq_const 2 = 2; A2:geo-seq (2,1) is convergent by Th85; A3:lim geo-seq (2,1) = 0 by Th85; A4: lim - geo-seq (2,1) = - (lim geo-seq(2,1)) by SEQ_2:10,Th85 .= 0 by A3; lim SumsReciTriang = 2 + 0 by SEQ_2:6,A1,A2,Th86,A4; hence thesis by Th86,A2; end; theorem Partial_Sums ReciTriangRS = SumsReciTriang by Th84,Def14; ::\$N Reciprocals of triangular numbers theorem Sum ReciTriangRS = 2 by Th84,Def14,Th87;