:: Polygonal Numbers
:: by Adam Grabowski
::
:: Received May 19, 2013
:: Copyright (c) 2013-2026 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, NEWTON, SEQ_1, XCMPLX_0, NUMBERS, SEQ_2, POWER, ABIAN,
PYTHTRIP, SQUARE_1, ORDINAL1, XBOOLE_0, FUNCT_2, VALUED_0, VALUED_1,
NAT_2, WSIERP_1;
requirements REAL, NUMERALS, SUBSET, ARITHM;
definitions ORDINAL1, TARSKI, FUNCT_2;
equalities SERIES_1, SQUARE_1, GR_CY_3;
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;
ex j being Integer st n = 2 * j by ABIAN:11;
hence thesis;
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
let n be Real;
cluster n_or_greater for Real;
existence by EC_PF_2:def 1;
end;
registration
let n be Nat;
cluster n_or_greater for Nat;
existence
proof
take n;
thus thesis by EC_PF_2:def 1;
end;
end;
begin :: Triangular Numbers
definition let n be natural Number;
func Triangle n -> Nat equals
Sum idseq n;
coherence
proof
Sum idseq n is natural;
hence thesis;
end;
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
Triangle n >= 0;
registration let n be Nat;
cluster Triangle n -> non negative;
coherence;
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;
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
take Triangle 1;
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 natural Number;
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;
registration
let s, n be natural Number;
cluster Polygon(s,n) -> s-gonal;
coherence
proof
reconsider n as Nat by TARSKI:1;
take n;
thus thesis;
end;
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 n be positive Nat;
cluster n_or_greater non zero for Nat;
existence
proof
take n;
thus thesis by EC_PF_2:def 1;
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 holds
Polygon (s, IndexPoly (s,x)) = x
proof
let s be 4_or_greater Nat,
x be non zero s-gonal number;
A1: s - 2 <> 0 by EC_PF_2:def 1;
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
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;
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; :: redefines PolygonalNumbers (NUMPOLY1, definition)
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
set n0 = Triangle n;
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;
set p1 = Mersenne p;
(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;
hence thesis by NAT_5:38,A2,A1,Th19;
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 Nat
ex n being Nat st n >= m & n in T
proof
let m be Nat;
set w = Triangle m;
A1: w is triangular;
take n = 9 * w + 1;
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 Nat
ex n being Nat st n >= m & n in T
proof
let m be Nat;
set w = Triangle m;
A3: w is triangular;
take n = 8 * w + 1;
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
take Triangle 1;
1 = 1 ^2;
hence thesis by FINSEQ_2:50,RVSUM_1:73;
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 holds
geo-seq (a,b) is convergent & lim geo-seq (a,b) = 0
proof
let a, b be Real;
for k being Nat holds geo-seq (a,b).k = a / (k + b) by Def15;
hence thesis by 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
::$L https://en.wikipedia.org/wiki/List_of_sums_of_reciprocals Sum of the Reciprocals of the Triangular Numbers
theorem
Sum ReciTriangRS = 2 by Th84,Def14,Th87;