:: Polygonal Numbers
:: by Adam Grabowski
::
:: Received May 19, 2013
:: Copyright (c) 2013 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;
schemes NAT_1, SEQ_1, FINSEQ_2, NAT_2;
begin :: Preliminaries
scheme LNatRealSeq {F(set) -> real number}:
(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
A0: 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 A0;
let seq1, seq2 be Real_Sequence;
assume that
A1: for n being Nat holds seq1.n = F(n) and
A2: for n being Nat holds seq2.n = F(n);
let n be Element of NAT;
thus seq1.n = F(n) by A1
.= seq2.n by A2;
end;
theorem ThX:
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;
LemI1:
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;
LemI3:
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 LemI1;
cluster n * (n + 1) -> even;
coherence by LemI3;
end;
theorem LemI2:
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 NMod5:
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 NTA18: ::: 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 Kit10:
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 NMod5;
hence thesis by NTA18;
end;
theorem Kit1:
not n * n + n, 4 are_congruent_mod 5
proof
assume n * n + n, 4 are_congruent_mod 5; then
A2: 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 Kit10; then
per cases;
suppose
B1: 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 B1,INT_1:16; then
5 divides 4 - 0 by INT_1:def 4,A2,INT_1:15;
hence thesis by NAT_D:7;
end;
suppose
B1: 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 B1,INT_1:16; then
5 divides 4 - 2 by INT_1:def 4,A2,INT_1:15;
hence thesis by NAT_D:7;
end;
suppose
B1: 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 B1,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,A2,INT_1:15; then
5 <= 3 by NAT_D:7;
hence thesis;
end;
suppose
B1: 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 B1,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,A2,INT_1:15;
hence thesis by NAT_D:7;
end;
suppose
B1: 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 B1,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,A2,INT_1:15;
hence thesis by NAT_D:7;
end;
end;
theorem Kit2:
not n * n + n, 3 are_congruent_mod 5
proof
assume n * n + n, 3 are_congruent_mod 5; then
A2: 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 Kit10; then
per cases;
suppose
B1: 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 B1,INT_1:16; then
5 divides 3 - 0 by INT_1:def 4,A2,INT_1:15;
hence thesis by NAT_D:7;
end;
suppose
B1: 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 B1,INT_1:16; then
5 divides 3 - 2 by INT_1:def 4,A2,INT_1:15; then
5 <= 1 by NAT_D:7;
hence thesis;
end;
suppose
B1: 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 B1,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,A2,INT_1:15; then
5 <= 2 by NAT_D:7;
hence thesis;
end;
suppose
B1: 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 B1,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,A2,INT_1:15; then
5 <= 1 by NAT_D:7;
hence thesis;
end;
suppose
B1: 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 B1,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,A2,INT_1:15;
hence thesis by NAT_D:7;
end;
end;
theorem Mod10:
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 Mod10C:
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 Mod10;
hence thesis by NTA18;
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 number;
attr n is triangular means :TriDef:
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 Th3:
Triangle (n + 1) = (Triangle n) + (n + 1)
proof
defpred P[Nat] means
(Triangle $1) + ($1 + 1) = Triangle($1+1);
AA: 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(AA,A2);
hence thesis;
end;
theorem Th2:
Triangle 1 = 1 by FINSEQ_2:50,RVSUM_1:73;
theorem Th23:
Triangle 2 = 3
proof
thus Triangle 2 = 1 + 2 by RVSUM_1:77,FINSEQ_2:52
.= 3;
end;
theorem Tri3:
Triangle 3 = 6
proof
thus Triangle 3 = 1 + 2 + 3 by RVSUM_1:78,FINSEQ_2:53
.= 6;
end;
theorem Tri4:
Triangle 4 = 10
proof
thus Triangle 4 = Triangle 3 + (3 + 1) by Th3
.= 10 by Tri3;
end;
theorem Tri5:
Triangle 5 = 15
proof
thus Triangle 5 = Triangle 4 + (4 + 1) by Th3
.= 15 by Tri4;
end;
theorem Tri6:
Triangle 6 = 21
proof
thus Triangle 6 = Triangle 5 + (5 + 1) by Th3
.= 21 by Tri5;
end;
theorem Tri7:
Triangle 7 = 28
proof
thus Triangle 7 = Triangle 6 + (6 + 1) by Th3
.= 28 by Tri6;
end;
theorem Tri8:
Triangle 8 = 36
proof
thus Triangle 8 = Triangle 7 + (7 + 1) by Th3
.= 36 by Tri7;
end;
theorem Th1:
Triangle n = n * (n + 1) / 2
proof
defpred P[Nat] means
Triangle $1 = $1 * ($1 + 1) / 2;
AA: P[0];
A2: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A0: P[k];
Triangle (k + 1) = (Triangle k) + (k + 1) by Th3
.= (k + 1) * (k + 2) / 2 by A0;
hence thesis;
end;
for n being Nat holds P[n] from NAT_1:sch 2(AA,A2);
hence thesis;
end;
theorem PosTh:
Triangle n >= 0
proof
A1: Triangle n = n * (n + 1) / 2 by Th1;
thus thesis by A1;
end;
registration let n be Nat;
cluster Triangle n -> non negative;
coherence by PosTh;
end;
registration let n be non zero Nat;
cluster Triangle n -> positive;
coherence
proof
n * (n + 1) / 2 > 0;
hence thesis by Th1;
end;
end;
registration let n be Nat;
cluster Triangle n -> natural;
coherence
proof
Triangle n = n * (n + 1) / 2 by Th1;
hence thesis;
end;
end;
A: 0 - 1 < 0;
theorem TriangleRes:
Triangle (n -' 1) = n * (n - 1) / 2
proof
per cases;
suppose n <> 0; then
A1: 1 <= 1 * n by ThX;
Triangle (n -' 1) = (n -' 1) * (n -' 1 + 1) / 2 by Th1
.= (n -' 1) * n / 2 by XREAL_1:235,A1;
hence thesis by XREAL_1:233,A1;
end;
suppose
Z1: n = 0; then
Triangle (n -' 1) = Triangle 0 by XREAL_0:def 2,A
.= n * (n - 1) / 2 by Z1;
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 Nie7:
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 TriDef;
A0: 4 * 5 = 20;
A2: n = k * (k + 1) / 2 by A1,Th1;
assume n, 7 are_congruent_mod 10; then
k * (k + 1) / 2 * 2, 7 * 2 are_congruent_mod (10 * 2)
by A2,INT_4:10; then
k * (k + 1), 14 are_congruent_mod 5 by A0,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 Kit1,INT_1:14;
end;
theorem Nie9:
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 TriDef;
A0: 4 * 5 = 20;
A2: n = k * (k + 1) / 2 by A1,Th1;
assume n, 9 are_congruent_mod 10; then
k * (k + 1) / 2 * 2, 9 * 2 are_congruent_mod (10 * 2)
by A2,INT_4:10; then
k * (k + 1), 18 are_congruent_mod 5 by A0,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 Kit2,INT_1:14;
end;
theorem Nie2:
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 TriDef;
A0: 4 * 5 = 20;
A2: n = k * (k + 1) / 2 by A1,Th1;
assume n, 2 are_congruent_mod 10; then
k * (k + 1) / 2 * 2, 2 * 2 are_congruent_mod (10 * 2)
by A2,INT_4:10; then
k * (k + 1), 4 are_congruent_mod 5 by A0,INT_1:20; then
4, k * k + k are_congruent_mod 5 by INT_1:14;
hence thesis by Kit1,INT_1:14;
end;
theorem Nie4:
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 TriDef;
A0: 4 * 5 = 20;
A2: n = k * (k + 1) / 2 by A1,Th1;
assume n, 4 are_congruent_mod 10; then
k * (k + 1) / 2 * 2, 4 * 2 are_congruent_mod (10 * 2) by A2,INT_4:10; then
k * (k + 1), 8 are_congruent_mod 5 by A0,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 Kit2,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 Mod10C;
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 Nie2;
end;
suppose
n, 3 are_congruent_mod 10;
hence thesis;
end;
suppose
n, 4 are_congruent_mod 10;
hence thesis by Nie4;
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 Nie7;
end;
suppose
n, 8 are_congruent_mod 10;
hence thesis;
end;
suppose
n, 9 are_congruent_mod 10;
hence thesis by Nie9;
end;
end;
begin :: Polygonal Numbers
definition let s, n be Nat;
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 LemI2; then
(n * (s - 2) * (n - 1)) / 2 + n is Integer;
hence thesis;
end;
end;
theorem PolNat:
s >= 2 implies Polygon (s,n) is natural
proof
assume s >= 2; then
A2: 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 A2;
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 element;
attr x is s-gonal means :GonalDef:
ex n being Nat st x = Polygon (s,n);
end;
definition let x be element;
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
take Polygon (s,2);
thus thesis;
end;
end;
registration let s be non zero Nat;
cluster non zero s-gonal for number;
existence
proof
take Polygon (s,2);
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,PolNat;
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
FF: s >= 4;
consider n being Nat such that
A1: x = Polygon (s,n) by GonalDef;
A2: ((8 * s - 16) * x) + (s - 4) ^2 = (2 * n * (s - 2) - (s - 4)) ^2 by A1;
n <> 0 by A1; then
X1: 2 * n >= 1 by ThX;
s >= 0 + 4 by FF; then
X2: 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 X1,X2,XREAL_1:66; then
2 * n * (s - 2) - (s - 4) in NAT by INT_1:3,XREAL_1:19;
hence thesis by A2;
end;
theorem Pom2:
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
FF: s >= 4;
consider n being Nat such that
A1: x = Polygon (s,n) by GonalDef;
A2: ((8*s - 16) * x) + (s - 4) ^2 = (2 * n * (s - 2) - (s - 4)) ^2 by A1;
A3: s - 2 <> 0 by FF;
n <> 0 by A1; then
X1: 2 * n >= 1 by ThX;
s >= 0 + 4 by FF; then
X2: s - 4 >= 0 by XREAL_1:19;
s - 2 >= s - 4 by XREAL_1:13; then
a4: 2 * n * (s - 2) >= 0 + 1 * (s - 4) by X1,X2,XREAL_1:66;
IndexPoly (s,x) = ((2 * n * (s - 2) - (s - 4)) + s - 4) / (2 * s - 4)
by SQUARE_1:22,a4,A2,XREAL_1:19
.= (2 * n * (s - 2)) / (2 * (s - 2))
.= (2 * n) / 2 by A3,XCMPLX_1:91
.= n;
hence thesis by ORDINAL1:def 12;
end;
theorem IndPol1:
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 DivPoly:
for n being odd Nat st s >= 2 holds
n divides Polygon (s,n)
proof
let n be odd Nat;
assume
A0: s >= 2;
A1: Polygon (s,n) = (n * (s - 2) * (n - 1)) / 2 + n;
ss: s - 0 >= 2 by A0; 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,ss,XREAL_1:11;
k = n * ((s - 2) * ((n - 1) / 2)); then
n divides k by NAT_D:def 3,a5;
hence thesis by A1,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 LemI2; 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 TriangleRes;
hence thesis;
end;
begin :: On the Connection between Triangular and Other Polygonal Numbers
theorem TriPol:
Triangle n = Polygon (3, n)
proof
Polygon (3, n) = n * (n + 1) / 2;
hence thesis by Th1;
end;
theorem ndivT:
for n being odd Nat holds
n divides Triangle n
proof
let n be odd Nat;
n divides Polygon (3,n) by DivPoly;
hence thesis by TriPol;
end;
theorem StepA:
Triangle n <= Triangle (n + 1)
proof
Triangle (n + 1) = Triangle (n) + (n + 1) by Th3;
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
A0: n = k + i by NAT_1:10;
defpred P[Nat] means
for n being Nat holds Triangle n <= Triangle (n + $1);
A1: P[0];
A2: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
Z1: P[k];
let n be Nat;
A4: Triangle n <= Triangle (n + k) by Z1;
Triangle (n + k) <= Triangle (n + k + 1) by StepA;
hence thesis by A4,XXREAL_0:2;
end;
for n being Nat holds P[n] from NAT_1:sch 2(A1,A2);
hence thesis by A0;
end;
theorem TriMono:
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 Th3;
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 Ble1:
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 Th23;
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 Th3;
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 Pomoc1:
n <> 2 implies Triangle n is non prime
proof
assume
AA: n <> 2;
assume
A1: Triangle n is prime; then
A2: n <> 1 by Th2,INT_2:def 4;
n <> 0 by A1,INT_2:def 4; then
A3: n is non trivial by NAT_2:def 1,A2;
per cases;
suppose n is odd; then
n = 1 or n = Triangle n by INT_2:def 4,A1,ndivT;
hence thesis by Ble1,A3,Th2;
end;
suppose n is even; then
consider k being Nat such that
B2: n = 2 * k by ABIAN:def 2;
BB: k <> 0 by A1,INT_2:def 4,B2;
B3: Triangle n = n * (n + 1) / 2 by Th1
.= k * (n + 1) by B2; then
k divides Triangle n by NAT_D:def 3; then
per cases by INT_2:def 4,A1;
suppose k = 1;
hence thesis by AA,B2;
end;
suppose
B4: k = Triangle n;
1 = k / k by BB,XCMPLX_1:60
.= n + 1 by BB,XCMPLX_1:89,B3,B4; then
n = 0;
hence thesis by INT_2:def 4,A1;
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 Pomoc1;
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,Th23;
hence thesis by A1,Pomoc1;
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 Pom2,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
Y4: s - 2 <> 0;
X1: 0 <= (((8 * s - 16) * x) + (s - 4) ^2) by IndPol1;
set qq = sqrt (((8*s - 16) * x) + (s - 4) ^2);
set w = IndexPoly (s,x);
Y1: 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,Y4;
Y2: 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));
Y3: qq^2 = ((8 * s - 16) * x) + (s - 4) ^2 by SQUARE_1:def 2,X1;
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,Y1,Y2
.= ( (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 Y4,XCMPLX_1:89,Y3;
hence thesis;
end;
theorem
36 is square triangular
proof
A1: 6 ^2 = 36;
Triangle 8 = (8 + 1) * 8 / 2 by Th1 .= 36;
hence thesis by A1;
end;
registration let n be Nat;
cluster Polygon (3,n) -> natural;
coherence
proof
Triangle n = Polygon (3, n) by TriPol;
hence thesis;
end;
end;
registration let n be Nat;
cluster Polygon (3,n) -> triangular;
coherence
proof
Triangle n = Polygon (3, n) by TriPol;
hence thesis;
end;
end;
theorem AA:
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 TriangleRes;
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 TriangleRes
.= (s - 3) * (n * (n - 1) / 2) + n * (n+1) / 2 by Th1;
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
B2: s - 2 >= 0 by XREAL_1:19;
Polygon (s,n) = (s - 2) * Triangle (n -' 1) + n by AA;
hence thesis by INT_1:3,B2;
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,TriPol;
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
A1: x = n^2 by PYTHTRIP:def 3;
x = Polygon (4,n) by A1;
hence thesis;
end;
end;
theorem
Triangle (n -' 1) + Triangle (n) = n^2
proof
per cases;
suppose n <> 0; then
B0: n -' 1 = n - 1 by XREAL_1:233,NAT_1:14;
Triangle (n -' 1) =
(n - 1) * (n - 1 + 1) / 2 by Th1,B0; then
Triangle (n -' 1) + Triangle (n)
= (n - 1) * (n + 1 - 1) / 2 + n * (n + 1) / 2 by Th1
.= n ^2;
hence thesis;
end;
suppose
Z1: n = 0; then
Triangle (n -' 1) + Triangle (n) = Triangle (0 -' 1) + Triangle 0
.= n^2 by Z1,XREAL_0:def 2,A;
hence thesis;
end;
end;
theorem TriSq:
Triangle (n) + Triangle (n + 1) = (n + 1) ^2
proof
Triangle n = n * (n + 1) / 2 by Th1; then
Triangle n + Triangle (n + 1)
= n * (n + 1) / 2 + (n + 1) * (n + 1 + 1) / 2 by Th1
.= (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 TriSq;
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;
B0: (3*n)-'1 = (3*n)-1 by XREAL_1:233,ThX;
Triangle (3*n-'1) = ((3*n-1) * (3*n-1+1)) / 2 by B0,Th1;
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;
B0: (2 * n) -' 1 = (2 * n) - 1 by XREAL_1:233,ThX;
Triangle (2 * n -' 1) = ((2 * n - 1) * (2 * n - 1 + 1)) / 2 by B0,Th1;
hence thesis;
end;
definition let n, k be Nat;
func NPower (n, k) -> FinSequence of REAL means :D1:
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
K1: i in dom e;
f(i) = i |^ n;
hence thesis by K1,a1;
end;
uniqueness
proof
deffunc f(Nat) = $1 |^ n;
let e1,e2 be FinSequence of REAL such that
b1: dom e1 = Seg k &
for i being Nat st i in dom e1 holds e1.i = f(i) and
b2: 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
c1: i in dom e1;
hence e1.i = f(i) by b1
.= e2.i by c1,b1,b2;
end;
hence thesis by b1,b2,FINSEQ_1:13;
end;
end;
theorem Dodane1:
for k being Nat holds
NPower (n,k+1) = NPower (n,k) ^ <*(k+1) |^ n*>
proof
let k be Nat;
XX: 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 D1; then
c1: len NPower (n,k) = k by FINSEQ_1:6;
c2: 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 D1,c2,c1;
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
b1: l in dom NPower (n,k+1); then
l in Seg (k+1) by D1; then
b5: 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 b5,NAT_1:8;
suppose l <= k; then
l in Seg k by b5,FINSEQ_1:1; then
Aa: l in dom NPower (n,k) by D1; then
NP = (NPower (n,k)).l by FINSEQ_1:def 7 .= l |^ n by D1,Aa;
hence thesis;
end;
suppose
Z1: l = k + 1;
Seg k = dom NPower (n,k) by D1
.= Seg len NPower (n,k) by FINSEQ_1:def 3; then
k = len NPower (n,k) by FINSEQ_1:6;
hence thesis by Z1,FINSEQ_1:42;
end;
end;
hence thesis by D1,b1;
end;
hence thesis by XX,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 D1 .= {};
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 Th1
.= ((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 Th1
.= (Triangle k) * (Triangle k) + ((k + 1) |^ 2 * 4 * k) / 4 +
((k + 1) |^ 2 * 4) / 4 by Th1
.= (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 Dodane1;
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;
B00:Triangle n = n * (n + 1) / 2 by Th1;
0 + 1 <= n by NAT_1:13; then
B0: n -' 1 = n - 1 by XREAL_1:233;
B1: Triangle (n -' 1) = (n -' 1) * (n -' 1 + 1) / 2 by Th1
.= (n - 1) * n / 2 by B0;
Triangle (n + 1) = (n + 1) * (n + 1 + 1) / 2 by Th1
.= (n + 1) * (n + 2) / 2;then
Triangle n + Triangle (n -' 1) * Triangle (n + 1) =
Triangle n * Triangle n by B00,B1
.= (Triangle n) |^ 2 by NEWTON:81;
hence thesis;
end;
theorem
(Triangle n) |^ 2 + (Triangle (n + 1)) |^ 2 = Triangle ((n + 1) |^ 2)
proof
B1: Triangle (n + 1) = (n + 1) * (n + 1 + 1) / 2 by Th1
.= (n + 1) * (n + 2) / 2;
B6: (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 Th1
.= (n * (n + 1) / 2) * (n * (n + 1) / 2) + ((n + 1) * (n + 2) / 2) |^ 2
by NEWTON:81,B1
.= (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 B6
.= Triangle (n + 1) |^ 2 by Th1;
hence thesis;
end;
theorem
(Triangle (n + 1)) |^ 2 - (Triangle n) |^ 2 = (n + 1) |^ 3
proof
B1: Triangle (n + 1) = (n + 1) * (n + 1 + 1) / 2 by Th1
.= (n + 1) * (n + 2) / 2;
B4: (n + 1) |^ 3 = (n + 1) * (n + 1) * (n + 1) by POLYEQ_3:27
.= n * n * n + 3 * n * n + 3 * n + 1;
B5: (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 Th1,B1
.= ((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 B5
.= (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 B4;
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;
B0: n -' 1 = n - 1 by XREAL_1:233,NAT_1:14;
B1: Triangle (n -' 1) = (n - 1) * (n - 1 + 1) / 2 by B0,Th1;
3 * (Triangle n) + (Triangle (n -' 1)) =
3 * (n * (n + 1) / 2) + (n - 1) * (n - 1 + 1) / 2 by B1,Th1
.= 2 * n * (2 * n + 1) / 2
.= Triangle (2 * n) by Th1;
hence thesis;
end;
theorem
3 * (Triangle n) + Triangle (n + 1) = Triangle (2 * n + 1)
proof
B1: Triangle n = n * (n + 1) / 2 by Th1;
B2: Triangle (n + 1) = (n + 1) * (n + 1 + 1) / 2 by Th1
.= (n + 1) * (n + 2) / 2;
Triangle (2 * n + 1) = (2 * n + 1) * (2 * n + 1 + 1) / 2 by Th1
.= (2 * n + 1) * (2 * n + 2) / 2;
hence thesis by B1,B2;
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;
B0: n -' 1 = n - 1 by XREAL_1:233,NAT_1:14;
B1: Triangle (n -' 1) = (n - 1) * (n - 1 + 1) / 2 by B0,Th1;
B2: Triangle n = n * (n + 1) / 2 by Th1;
Triangle (n + 1) = (n + 1) * (n + 1 + 1) / 2 by Th1
.= (n + 1) * (n + 2) / 2;
hence thesis by B2,B1;
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;
B0: n-'1 = n-1 by XREAL_1:233,NAT_1:14;
B1: Triangle (n -' 1) = (n - 1) * (n - 1 + 1) / 2 by B0,Th1;
Triangle n + Triangle (n -' 1)
= n * (n + 1) / 2 + Triangle (n-'1) by Th1
.= (1 + 2 * n - 1) * n / 2 by B1;
hence thesis;
end;
theorem Wazny1:
1 + 9 * Triangle n = Triangle (3 * n + 1)
proof
B1: Triangle n = n * (n + 1) / 2 by Th1;
Triangle (3 * n + 1) = (3 * n + 1) * (3 * n + 1 + 1) / 2 by Th1
.= 1 + 9 * Triangle n by B1;
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 Th1
.= n * (n + 1) / 2 + m * (m + 1) / 2 + n * m
.= Triangle n + m * (m + 1) / 2 + n * m by Th1
.= Triangle n + Triangle m + n * m by Th1;
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
B0: n -' 1 = n - 1 by XREAL_1:233;
0 + 1 <= m by NAT_1:13; then
B1: m -' 1 = m - 1 by XREAL_1:233;
B2: Triangle (n -' 1) = (n - 1) * (n - 1 + 1) / 2 by B0,Th1;
B3: Triangle (m -' 1) = (m - 1) * (m - 1 + 1) / 2 by B1,Th1;
B6: Triangle (n * m) = n * m * (n * m + 1) / 2 by Th1;
(Triangle n) * (Triangle m) + (Triangle (n -' 1)) * (Triangle (m -' 1))
= (n * (n + 1) / 2) * (Triangle m) +
(Triangle (n -' 1)) * (Triangle (m -' 1)) by Th1
.= (n * (n + 1) / 2) * (m * (m + 1) / 2) +
((n - 1) * (n - 1 + 1) / 2) * ((m - 1) * (m - 1 + 1) / 2)
by B3,B2,Th1
.= ((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 B6;
hence thesis;
end;
begin :: Sets of Polygonal Numbers
definition let s be Nat;
func PolygonalNumbers s -> set equals
{ Polygon (s,n) where n is Nat : not contradiction };
coherence;
end;
definition let s be non trivial Nat;
redefine func PolygonalNumbers s -> Subset of NAT;
coherence
proof
{ Polygon (s,n) where n is Nat : not contradiction } c= NAT
proof
let x be element;
assume x in { Polygon (s,n) where n is Nat : not contradiction }; then
consider n being Nat such that
A1: x = Polygon (s,n) & not contradiction;
thus thesis by A1,ORDINAL1:def 12;
end;
hence thesis;
end;
end;
KK:
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 KK;
end;
func SquareNumbers -> Subset of NAT equals
PolygonalNumbers 4;
coherence
proof
4 is non trivial by NAT_2:def 1;
hence thesis by KK;
end;
end;
registration let s be non trivial Nat;
cluster PolygonalNumbers s -> non empty;
coherence
proof
set n = 0;
Polygon (s,n) in
{ Polygon (s,n) where n is Nat : not contradiction }; then
PolygonalNumbers s <> {};
hence thesis;
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
consider n being Nat such that
A1: x = Polygon (3,n) & not contradiction;
thus thesis by A1;
end;
cluster -> square for Element of SquareNumbers;
coherence
proof
let x be Element of SquareNumbers;
x in SquareNumbers by SUBSET_1:def 1; then
consider n being Nat such that
A1: x = Polygon (4,n) & not contradiction;
thus thesis by A1;
end;
end;
theorem TriSet:
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,TriPol;
hence thesis;
end;
theorem SqSet:
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 Lemacik2:
(n + 1) choose 2 = n * (n + 1) / 2
proof
per cases;
suppose
Z1: n <> 0; then
A0: n = n -' 1 + 1 by XREAL_1:235,NAT_1:14;
A1: n + 1 >= 1 + 1 by NAT_1:14,Z1,XREAL_1:6;
n -' 1 = n - 1 by XREAL_1:233,NAT_1:14,Z1
.= (n + 1) - 2; then
(n + 1) choose 2 = ((n + 1)!) / (2! * ((n -' 1)!)) by NEWTON:def 3,A1
.= (n! * (n + 1)) / (2 * ((n -' 1)!)) by NEWTON:15,14
.= ((n -' 1)! * n * (n + 1)) / (2 * ((n -' 1)!)) by NEWTON:15,A0
.= ((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 Lemacik2;
hence thesis by Th1;
end;
theorem ThY:
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;
Z0: 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;
A2: n = 2 |^ (p -' 1) * p1 by A1,XREAL_0:def 2;
Z1: p -' 1 = p - 1 by XREAL_1:233,Z0,NAT_1:14;
(2 to_power p) / (2 to_power 1) = (p1 + 1) / 2 by NEWTON:5; then
A3: (2 to_power (p -' 1)) = (p1 + 1) / 2 by Z1,POWER:29;
(p1 * (p1 + 1)) / 2 = Triangle p1 by Th1;
hence thesis by A2,A3;
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 :MerDef:
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 MerDef;
2 to_power p > 0 by POWER:34; then
2 |^ p >= 0 + 1 by NAT_1:13; then
Z2: 2 |^ p -' 1 = 2 |^ p - 1 by XREAL_0:def 2,XREAL_1:19;
Z1: 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 by NEWTON:5; then
2 to_power (p -' 1) = (p1 + 1) / 2 by Z1,POWER:29; then
p1 * 2|^ (p -' 1) = (p1 * (p1 + 1)) / 2;
hence thesis by NAT_5:38,Z2,A1,Th1;
end;
end;
registration
cluster even perfect -> triangular for non zero Nat;
coherence by ThY;
end;
theorem EightA:
8 * (Triangle n) + 1 = (2 * n + 1) ^2
proof
8 * Triangle n = 8 * (n * (n + 1) / 2) by Th1
.= 4 * (n^2 + n);
hence thesis;
end;
theorem TriSq:
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 EightA;
hence 8 * n + 1 is square by A1;
end;
theorem TriTri:
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 Wazny1;
hence thesis by A1;
end;
theorem TriSq1:
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 Th1; 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 Th1,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;
set w = Triangle m;
A1: w is triangular;
reconsider n = 9 * w + 1 as Element of NAT by ORDINAL1:def 12;
take n;
A3: w >= m by TriMono;
9 * w >= 1 * w by XREAL_1:64; then
9 * w + 1 > w by NAT_1:13;
hence n >= m by A3,XXREAL_0:2;
thus thesis by TriSet,A1,TriTri;
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;
set w = Triangle m;
A1: w is triangular;
reconsider n = 8 * w + 1 as Element of NAT by ORDINAL1:def 12;
take n;
A3: w >= m by TriMono;
8 * w >= 1 * w by XREAL_1:64; then
8 * w + 1 > w by NAT_1:13;
hence n >= m by A3,XXREAL_0:2;
thus thesis by SqSet,A1,TriSq;
end;
hence thesis by PYTHTRIP:9;
end;
end;
registration
cluster triangular square non zero for Nat;
existence
proof
1 = 1 ^2; then
Triangle 1 is triangular square by FINSEQ_2:50,RVSUM_1:73;
hence thesis;
end;
end;
theorem ZeroTriSq:
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 ZeroTriSq;
end;
theorem TriSquare1:
1 is triangular square
proof
1 = 1 ^2;
hence thesis by Th2;
end;
::$N Square triangular number
theorem
36 is triangular square
proof
Triangle (4 * 1 * (1 + 1)) is triangular square
by Th2,TriSquare1,TriSq1;
hence thesis by Tri8;
end;
theorem
1225 is triangular square
proof
A1: 35 ^2 = 1225;
Triangle 49 = 49 * (49 + 1) / 2 by Th1 .= 1225;
hence thesis by A1;
end;
registration let n be triangular Nat;
cluster 9 * n + 1 -> triangular;
coherence by TriTri;
end;
registration let n be triangular Nat;
cluster 8 * n + 1 -> square;
coherence by TriSq;
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 :def71:
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 def71
.= 0;
end;
end;
theorem E3:
1 / (Triangle n) = 2 / (n * (n + 1))
proof
1 / (Triangle n) = 1 / ((n * (n + 1)) / 2) by Th1
.= 2 / (n * (n + 1)) by XCMPLX_1:57;
hence thesis;
end;
theorem Tw999:
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;
K2: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A2: P[k];
A2a: ReciTriangRS.(k+1) = 1 / Triangle (k+1) by def71
.= 2 / ((k + 1) * (k + 1 + 1)) by E3
.= 2 / (k * k + 3 * k + 2);
A2d: (k + 2) / (k + 2) = 1 by XCMPLX_1:60;
A2e: (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 A2d,A2,A2a,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,A2d
.= ((2 * (k + 2)) / (k + 2)) * ((k + 1) / (k + 1)) -
(2 * (k + 2)) / ((k + 1) * (k + 2)) + 2 / ((k + 1) * (k + 2))
by A2e,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,K2);
hence thesis;
end;
definition
func SumsReciTriang -> Real_Sequence means :defsek:
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 number;
func geo-seq (a,b) -> Real_Sequence means :defseka:
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 CiagPom:
for a, b being real number st b > 0 holds
geo-seq (a,b) is convergent & lim geo-seq (a,b) = 0
proof
let a, b be real number;
assume
A1: b > 0;
for k being Nat holds geo-seq (a,b).k = a / (k + b) by defseka;
hence thesis by A1,SEQ_4:31;
end;
theorem SumyCiagow:
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 defsek;
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 defseka;
hence thesis by a1,a2;
end;
hence thesis by SEQ_1:7;
end;
theorem GranicaFseq:
SumsReciTriang is convergent & lim SumsReciTriang = 2
proof
C1: seq_const 2 is convergent & lim seq_const 2 = 2;
C1a:geo-seq (2,1) is convergent by CiagPom;
C2a:lim geo-seq (2,1) = 0 by CiagPom;
C3: lim - geo-seq (2,1) = - (lim geo-seq(2,1)) by SEQ_2:10,CiagPom
.= 0 by C2a;
lim SumsReciTriang = 2 + 0 by SEQ_2:6,C1,C1a,SumyCiagow,C3;
hence thesis by SumyCiagow,C1a;
end;
theorem
Partial_Sums ReciTriangRS = SumsReciTriang by Tw999,defsek;
::$N Reciprocals of triangular numbers
theorem
Sum ReciTriangRS = 2 by Tw999,defsek,GranicaFseq;