:: Polygonal Numbers
:: by Adam Grabowski
::
:: Received May 19, 2013
:: Copyright (c) 2013-2021 Association of Mizar Users


scheme :: NUMPOLY1:sch 1
LNatRealSeq{ F1( set ) -> Real } :
( ex seq being Real_Sequence st
for n being Nat holds seq . n = F1(n) & ( for seq1, seq2 being Real_Sequence st ( for n being Nat holds seq1 . n = F1(n) ) & ( for n being Nat holds seq2 . n = F1(n) ) holds
seq1 = seq2 ) )
proof end;

theorem Th1: :: NUMPOLY1:1
for n, a being non zero Nat holds 1 <= a * n
proof end;

Lm1: for n being Integer holds n * (n - 1) is even
proof end;

Lm2: for n being Integer holds n * (n + 1) is even
proof end;

registration
let n be Integer;
cluster n * (n - 1) -> even ;
coherence
n * (n - 1) is even by Lm1;
cluster n * (n + 1) -> even ;
coherence
n * (n + 1) is even by Lm2;
end;

theorem Th2: :: NUMPOLY1:2
for n being even Integer holds n / 2 is Integer
proof end;

registration
let n be even Nat;
cluster n / 2 -> natural ;
coherence
n / 2 is natural
proof end;
end;

registration
let n be odd Nat;
cluster n - 1 -> natural ;
coherence
n - 1 is natural by CHORD:2;
end;

registration
let n be odd Nat;
cluster n - 1 -> even ;
coherence
n - 1 is even ;
end;

theorem Th3: :: NUMPOLY1:3
for n being Nat holds
not not n mod 5 = 0 & ... & not n mod 5 = 4
proof end;

theorem Th4: :: NUMPOLY1:4
for n, k being Nat st k <> 0 holds
n,n mod k are_congruent_mod k
proof end;

theorem Th5: :: NUMPOLY1:5
for n being Nat holds
not not n, 0 are_congruent_mod 5 & ... & not n,4 are_congruent_mod 5
proof end;

theorem Th6: :: NUMPOLY1:6
for n being Nat holds not (n * n) + n,4 are_congruent_mod 5
proof end;

theorem Th7: :: NUMPOLY1:7
for n being Nat holds not (n * n) + n,3 are_congruent_mod 5
proof end;

theorem Th8: :: NUMPOLY1:8
for n being Nat holds
not not n mod 10 = 0 & ... & not n mod 10 = 9
proof end;

theorem Th9: :: NUMPOLY1:9
for n being Nat holds
not not n, 0 are_congruent_mod 10 & ... & not n,9 are_congruent_mod 10
proof end;

registration
cluster non trivial natural -> 2 _or_greater for set ;
coherence
for b1 being Nat st not b1 is trivial holds
b1 is 2 _or_greater by EC_PF_2:def 1, NAT_2:29;
cluster natural 2 _or_greater -> non trivial for set ;
coherence
for b1 being Nat st b1 is 2 _or_greater holds
not b1 is trivial
proof end;
end;

registration
cluster natural 4 _or_greater -> non zero 3 _or_greater for set ;
coherence
for b1 being Nat st b1 is 4 _or_greater holds
( b1 is 3 _or_greater & not b1 is zero )
proof end;
end;

registration
cluster natural 4 _or_greater -> non trivial for set ;
coherence
for b1 being Nat st b1 is 4 _or_greater holds
not b1 is trivial
proof end;
end;

registration
cluster epsilon-transitive epsilon-connected ordinal natural real complex ext-real non negative integer dim-like 4 _or_greater for set ;
existence
ex b1 being Nat st b1 is 4 _or_greater by EC_PF_2:def 1;
cluster epsilon-transitive epsilon-connected ordinal natural real complex ext-real non negative integer dim-like 3 _or_greater for set ;
existence
ex b1 being Nat st b1 is 3 _or_greater by EC_PF_2:def 1;
end;

definition
let n be Nat;
func Triangle n -> Real equals :: NUMPOLY1:def 1
 Sum (idseq n);
coherence
Sum (idseq n) is Real ;
end;

:: deftheorem defines Triangle NUMPOLY1:def 1 :
for n being Nat holds Triangle n = Sum (idseq n);

definition
let n be object ;
attr n is triangular means :Def2: :: NUMPOLY1:def 2
 ex k being Nat st n = Triangle k;
end;

:: deftheorem Def2 defines triangular NUMPOLY1:def 2 :
for n being object holds
( n is triangular iff ex k being Nat st n = Triangle k );

registration
let n be zero number ;
cluster Triangle n -> zero ;
coherence
Triangle n is zero by RVSUM_1:72;
end;

theorem Th10: :: NUMPOLY1:10
for n being Nat holds Triangle (n + 1) = (Triangle n) + (n + 1)
proof end;

theorem Th11: :: NUMPOLY1:11
Triangle 1 = 1 by FINSEQ_2:50, RVSUM_1:73;

theorem Th12: :: NUMPOLY1:12
Triangle 2 = 3
proof end;

theorem Th13: :: NUMPOLY1:13
Triangle 3 = 6
proof end;

theorem Th14: :: NUMPOLY1:14
Triangle 4 = 10
proof end;

theorem Th15: :: NUMPOLY1:15
Triangle 5 = 15
proof end;

theorem Th16: :: NUMPOLY1:16
Triangle 6 = 21
proof end;

theorem Th17: :: NUMPOLY1:17
Triangle 7 = 28
proof end;

theorem Th18: :: NUMPOLY1:18
Triangle 8 = 36
proof end;

theorem Th19: :: NUMPOLY1:19
for n being Nat holds Triangle n = (n * (n + 1)) / 2
proof end;

theorem Th20: :: NUMPOLY1:20
for n being Nat holds Triangle n >= 0
proof end;

registration
let n be Nat;
cluster Triangle n -> non negative ;
coherence
not Triangle n is negative by Th20;
end;

registration
let n be non zero Nat;
cluster Triangle n -> positive ;
coherence
Triangle n is positive
proof end;
end;

registration
let n be Nat;
cluster Triangle n -> natural ;
coherence
Triangle n is natural
proof end;
end;

Lm3: 0 - 1 < 0
;

theorem Th21: :: NUMPOLY1:21
for n being Nat holds Triangle (n -' 1) = (n * (n - 1)) / 2
proof end;

registration
cluster triangular -> natural for set ;
coherence
for b1 being number st b1 is triangular holds
b1 is natural ;
end;

registration
cluster non zero triangular for set ;
existence
ex b1 being number st
( b1 is triangular & not b1 is zero )
proof end;
end;

theorem Th22: :: NUMPOLY1:22
for n being triangular number holds not n,7 are_congruent_mod 10
proof end;

theorem Th23: :: NUMPOLY1:23
for n being triangular number holds not n,9 are_congruent_mod 10
proof end;

theorem Th24: :: NUMPOLY1:24
for n being triangular number holds not n,2 are_congruent_mod 10
proof end;

theorem Th25: :: NUMPOLY1:25
for n being triangular number holds not n,4 are_congruent_mod 10
proof end;

theorem :: NUMPOLY1:26
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 end;

definition
let s, n be natural Number ;
func Polygon (s,n) -> Integer equals :: NUMPOLY1:def 3
(((n ^2) * (s - 2)) - (n * (s - 4))) / 2;
coherence
(((n ^2) * (s - 2)) - (n * (s - 4))) / 2 is Integer
proof end;
end;

:: deftheorem defines Polygon NUMPOLY1:def 3 :
for s, n being natural Number holds Polygon (s,n) = (((n ^2) * (s - 2)) - (n * (s - 4))) / 2;

theorem Th27: :: NUMPOLY1:27
for n, s being Nat st s >= 2 holds
Polygon (s,n) is natural
proof end;

theorem :: NUMPOLY1:28
for n, s being Nat holds Polygon (s,n) = (((n * (s - 2)) * (n - 1)) / 2) + n ;

definition
let s be Nat;
let x be object ;
attr x is s -gonal means :Def4: :: NUMPOLY1:def 4
 ex n being Nat st x = Polygon (s,n);
end;

:: deftheorem Def4 defines -gonal NUMPOLY1:def 4 :
for s being Nat
for x being object holds
( x is s -gonal iff ex n being Nat st x = Polygon (s,n) );

definition
let x be object ;
attr x is polygonal means :: NUMPOLY1:def 5
 ex s being Nat st x is s -gonal ;
end;

:: deftheorem defines polygonal NUMPOLY1:def 5 :
for x being object holds
( x is polygonal iff ex s being Nat st x is s -gonal );

theorem :: NUMPOLY1:29
for s being Nat holds Polygon (s,1) = 1 ;

theorem :: NUMPOLY1:30
for s being Nat holds Polygon (s,2) = s ;

registration
let s be Nat;
cluster s -gonal for set ;
existence
ex b1 being number st b1 is s -gonal
proof end;
end;

registration
let s be non zero Nat;
cluster non zero s -gonal for set ;
existence
ex b1 being number st
( not b1 is zero & b1 is s -gonal )
proof end;
end;

registration
let s be Nat;
cluster s -gonal -> real for set ;
coherence
for b1 being number st b1 is s -gonal holds
b1 is real ;
end;

registration
let s be non trivial Nat;
cluster s -gonal -> natural for set ;
coherence
for b1 being number st b1 is s -gonal holds
b1 is natural by EC_PF_2:def 1, Th27;
end;

theorem :: NUMPOLY1:31
for n, s being Nat holds (Polygon (s,(n + 1))) - (Polygon (s,n)) = ((s - 2) * n) + 1 ;

definition
let s be Nat;
let x be s -gonal number ;
func IndexPoly (s,x) -> Real equals :: NUMPOLY1:def 6
(((sqrt ((((8 * s) - 16) * x) + ((s - 4) ^2))) + s) - 4) / ((2 * s) - 4);
coherence
(((sqrt ((((8 * s) - 16) * x) + ((s - 4) ^2))) + s) - 4) / ((2 * s) - 4) is Real ;
end;

:: deftheorem defines IndexPoly NUMPOLY1:def 6 :
for s being Nat
for x being b1 -gonal number holds IndexPoly (s,x) = (((sqrt ((((8 * s) - 16) * x) + ((s - 4) ^2))) + s) - 4) / ((2 * s) - 4);

theorem :: NUMPOLY1:32
for n being Nat
for s being non zero Nat
for x being non zero b2 -gonal number st x = Polygon (s,n) holds
(((8 * s) - 16) * x) + ((s - 4) ^2) = (((2 * n) * (s - 2)) - (s - 4)) ^2 ;

theorem :: NUMPOLY1:33
for s being non zero Nat
for x being non zero b1 -gonal number st s >= 4 holds
(((8 * s) - 16) * x) + ((s - 4) ^2) is square
proof end;

theorem Th34: :: NUMPOLY1:34
for s being non zero Nat
for x being non zero b1 -gonal number st s >= 4 holds
IndexPoly (s,x) in NAT
proof end;

theorem Th35: :: NUMPOLY1:35
for s being non trivial Nat
for x being b1 -gonal number holds 0 <= (((8 * s) - 16) * x) + ((s - 4) ^2)
proof end;

theorem Th36: :: NUMPOLY1:36
for s being Nat
for n being odd Nat st s >= 2 holds
n divides Polygon (s,n)
proof end;

:: WP: Centered polygonal number
definition
let s, n be Nat;
func CenterPolygon (s,n) -> Integer equals :: NUMPOLY1:def 7
(((s * n) / 2) * (n - 1)) + 1;
coherence
(((s * n) / 2) * (n - 1)) + 1 is Integer
proof end;
end;

:: deftheorem defines CenterPolygon NUMPOLY1:def 7 :
for s, n being Nat holds CenterPolygon (s,n) = (((s * n) / 2) * (n - 1)) + 1;

registration
let s be Nat;
let n be non zero Nat;
cluster CenterPolygon (s,n) -> natural ;
coherence
CenterPolygon (s,n) is natural
proof end;
end;

theorem :: NUMPOLY1:37
for n being Nat holds CenterPolygon (0,n) = 1 ;

theorem :: NUMPOLY1:38
for s being Nat holds CenterPolygon (s,0) = 1 ;

theorem :: NUMPOLY1:39
for n, s being Nat holds CenterPolygon (s,n) = (s * (Triangle (n -' 1))) + 1
proof end;

theorem Th40: :: NUMPOLY1:40
for n being Nat holds Triangle n = Polygon (3,n)
proof end;

theorem Th41: :: NUMPOLY1:41
for n being odd Nat holds n divides Triangle n
proof end;

theorem Th42: :: NUMPOLY1:42
for n being Nat holds Triangle n <= Triangle (n + 1)
proof end;

theorem :: NUMPOLY1:43
for n, k being Nat st k <= n holds
Triangle k <= Triangle n
proof end;

theorem Th44: :: NUMPOLY1:44
for n being Nat holds n <= Triangle n
proof end;

theorem Th45: :: NUMPOLY1:45
for n being non trivial Nat holds n < Triangle n
proof end;

theorem Th46: :: NUMPOLY1:46
for n being Nat st n <> 2 holds
not Triangle n is prime
proof end;

registration
let n be 3 _or_greater Nat;
cluster Triangle n -> non prime ;
coherence
not Triangle n is prime
proof end;
end;

registration
cluster natural 4 _or_greater triangular -> non prime 4 _or_greater for set ;
coherence
for b1 being 4 _or_greater Nat st b1 is triangular holds
not b1 is prime
proof end;
end;

registration
let s be non zero 4 _or_greater Nat;
let x be non zero s -gonal number ;
cluster IndexPoly (s,x) -> natural ;
coherence
IndexPoly (s,x) is natural by Th34, EC_PF_2:def 1;
end;

theorem :: NUMPOLY1:47
for s being 4 _or_greater Nat
for x being non zero b1 -gonal number st s <> 2 holds
Polygon (s,(IndexPoly (s,x))) = x
proof end;

theorem :: NUMPOLY1:48
( 36 is square & 36 is triangular )
proof end;

registration
let n be Nat;
cluster Polygon (3,n) -> natural ;
coherence
Polygon (3,n) is natural
proof end;
end;

registration
let n be Nat;
cluster Polygon (3,n) -> triangular ;
coherence
Polygon (3,n) is triangular
proof end;
end;

theorem Th49: :: NUMPOLY1:49
for n, s being Nat holds Polygon (s,n) = ((s - 2) * (Triangle (n -' 1))) + n
proof end;

theorem :: NUMPOLY1:50
for n, s being Nat holds Polygon (s,n) = ((s - 3) * (Triangle (n -' 1))) + (Triangle n)
proof end;

theorem :: NUMPOLY1:51
for n being Nat holds Polygon (0,n) = n * (2 - n) ;

theorem :: NUMPOLY1:52
for n being Nat holds Polygon (1,n) = (n * (3 - n)) / 2 ;

theorem :: NUMPOLY1:53
for n being Nat holds Polygon (2,n) = n ;

registration
let s be non trivial Nat;
let n be Nat;
cluster Polygon (s,n) -> natural ;
coherence
Polygon (s,n) is natural
proof end;
end;

registration
let n be Nat;
cluster Polygon (4,n) -> square ;
coherence
Polygon (4,n) is square ;
end;

registration
cluster natural 3 -gonal -> triangular for set ;
coherence
for b1 being Nat st b1 is 3 -gonal holds
b1 is triangular ;
cluster natural triangular -> 3 -gonal for set ;
coherence
for b1 being Nat st b1 is triangular holds
b1 is 3 -gonal
proof end;
cluster natural 4 -gonal -> square for set ;
coherence
for b1 being Nat st b1 is 4 -gonal holds
b1 is square ;
cluster natural square -> 4 -gonal for set ;
coherence
for b1 being Nat st b1 is square holds
b1 is 4 -gonal
proof end;
end;

theorem :: NUMPOLY1:54
for n being Nat holds (Triangle (n -' 1)) + (Triangle n) = n ^2
proof end;

theorem Th55: :: NUMPOLY1:55
for n being Nat holds (Triangle n) + (Triangle (n + 1)) = (n + 1) ^2
proof end;

registration
let n be Nat;
cluster (Triangle n) + (Triangle (n + 1)) -> square ;
coherence
(Triangle n) + (Triangle (n + 1)) is square
proof end;
end;

theorem :: NUMPOLY1:56
for n being non trivial Nat holds (1 / 3) * (Triangle ((3 * n) -' 1)) = (n * ((3 * n) - 1)) / 2
proof end;

theorem :: NUMPOLY1:57
for n being non zero Nat holds Triangle ((2 * n) -' 1) = (n * ((4 * n) - 2)) / 2
proof end;

definition
let n, k be Nat;
func NPower (n,k) -> FinSequence of REAL means :Def8: :: NUMPOLY1:def 8
( dom it = Seg k & ( for i being Nat st i in dom it holds
it . i = i |^ n ) );
existence
ex b1 being FinSequence of REAL st
( dom b1 = Seg k & ( for i being Nat st i in dom b1 holds
b1 . i = i |^ n ) )
proof end;
uniqueness
for b1, b2 being FinSequence of REAL st dom b1 = Seg k & ( for i being Nat st i in dom b1 holds
b1 . i = i |^ n ) & dom b2 = Seg k & ( for i being Nat st i in dom b2 holds
b2 . i = i |^ n ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines NPower NUMPOLY1:def 8 :
for n, k being Nat
for b3 being FinSequence of REAL holds
( b3 = NPower (n,k) iff ( dom b3 = Seg k & ( for i being Nat st i in dom b3 holds
b3 . i = i |^ n ) ) );

theorem Th58: :: NUMPOLY1:58
for n, k being Nat holds NPower (n,(k + 1)) = (NPower (n,k)) ^ <*((k + 1) |^ n)*>
proof end;

registration
let n be Nat;
reduce Sum (NPower (n,0)) to 0 ;
reducibility
Sum (NPower (n,0)) = 0
proof end;
end;

theorem :: NUMPOLY1:59
for n being Nat holds (Triangle n) |^ 2 = Sum (NPower (3,n))
proof end;

theorem :: NUMPOLY1:60
for n being non trivial Nat holds (Triangle n) + ((Triangle (n -' 1)) * (Triangle (n + 1))) = (Triangle n) |^ 2
proof end;

theorem :: NUMPOLY1:61
for n being Nat holds ((Triangle n) |^ 2) + ((Triangle (n + 1)) |^ 2) = Triangle ((n + 1) |^ 2)
proof end;

theorem :: NUMPOLY1:62
for n being Nat holds ((Triangle (n + 1)) |^ 2) - ((Triangle n) |^ 2) = (n + 1) |^ 3
proof end;

theorem :: NUMPOLY1:63
for n being non zero Nat holds (3 * (Triangle n)) + (Triangle (n -' 1)) = Triangle (2 * n)
proof end;

theorem :: NUMPOLY1:64
for n being Nat holds (3 * (Triangle n)) + (Triangle (n + 1)) = Triangle ((2 * n) + 1)
proof end;

theorem :: NUMPOLY1:65
for n being non zero Nat holds ((Triangle (n -' 1)) + (6 * (Triangle n))) + (Triangle (n + 1)) = (8 * (Triangle n)) + 1
proof end;

theorem :: NUMPOLY1:66
for n being non zero Nat holds (Triangle n) + (Triangle (n -' 1)) = (((1 + (2 * n)) - 1) * n) / 2
proof end;

theorem Th67: :: NUMPOLY1:67
for n being Nat holds 1 + (9 * (Triangle n)) = Triangle ((3 * n) + 1)
proof end;

theorem :: NUMPOLY1:68
for n, m being Nat holds Triangle (n + m) = ((Triangle n) + (Triangle m)) + (n * m)
proof end;

theorem :: NUMPOLY1:69
for n, m being non trivial Nat holds ((Triangle n) * (Triangle m)) + ((Triangle (n -' 1)) * (Triangle (m -' 1))) = Triangle (n * m)
proof end;

definition
let s be Nat;
func PolygonalNumbers s -> set equals :: NUMPOLY1:def 9
 { (Polygon (s,n)) where n is Nat : verum } ;
coherence
{ (Polygon (s,n)) where n is Nat : verum } is set ;
end;

:: deftheorem defines PolygonalNumbers NUMPOLY1:def 9 :
for s being Nat holds PolygonalNumbers s = { (Polygon (s,n)) where n is Nat : verum } ;

definition
let s be non trivial Nat;
:: original: PolygonalNumbers
redefine func PolygonalNumbers s -> Subset of NAT;
coherence
PolygonalNumbers s is Subset of NAT
proof end;
end;

Lm4: for s being non trivial Nat holds PolygonalNumbers s is Subset of NAT
;

definition
func TriangularNumbers -> Subset of NAT equals :: NUMPOLY1:def 10
 PolygonalNumbers 3;
coherence
PolygonalNumbers 3 is Subset of NAT
proof end;
func SquareNumbers -> Subset of NAT equals :: NUMPOLY1:def 11
 PolygonalNumbers 4;
coherence
PolygonalNumbers 4 is Subset of NAT
proof end;
end;

:: deftheorem defines TriangularNumbers NUMPOLY1:def 10 :
TriangularNumbers = PolygonalNumbers 3;

:: deftheorem defines SquareNumbers NUMPOLY1:def 11 :
SquareNumbers = PolygonalNumbers 4;

registration
let s be non trivial Nat;
cluster PolygonalNumbers s -> non empty ;
coherence
not PolygonalNumbers s is empty
proof end;
end;

registration
cluster TriangularNumbers -> non empty ;
coherence
not TriangularNumbers is empty
proof end;
cluster SquareNumbers -> non empty ;
coherence
not SquareNumbers is empty
proof end;
end;

registration
cluster -> triangular for Element of TriangularNumbers ;
coherence
for b1 being Element of TriangularNumbers holds b1 is triangular
proof end;
cluster -> square for Element of SquareNumbers ;
coherence
for b1 being Element of SquareNumbers holds b1 is square
proof end;
end;

theorem Th70: :: NUMPOLY1:70
for x being number holds
( x in TriangularNumbers iff x is triangular )
proof end;

theorem Th71: :: NUMPOLY1:71
for x being number holds
( x in SquareNumbers iff x is square )
proof end;

theorem Th72: :: NUMPOLY1:72
for n being Nat holds (n + 1) choose 2 = (n * (n + 1)) / 2
proof end;

theorem :: NUMPOLY1:73
for n being Nat holds Triangle n = (n + 1) choose 2
proof end;

theorem Th74: :: NUMPOLY1:74
for n being non zero Nat st n is even & n is perfect holds
n is triangular
proof end;

registration
let n be non zero Nat;
cluster Mersenne n -> non zero ;
coherence
not Mersenne n is zero
proof end;
end;

definition
let n be number ;
attr n is mersenne means :Def12: :: NUMPOLY1:def 12
 ex p being Nat st n = Mersenne p;
end;

:: deftheorem Def12 defines mersenne NUMPOLY1:def 12 :
for n being number holds
( n is mersenne iff ex p being Nat st n = Mersenne p );

registration
cluster epsilon-transitive epsilon-connected ordinal natural real complex ext-real non negative integer dim-like prime mersenne for set ;
existence
ex b1 being Prime st b1 is mersenne
proof end;
cluster epsilon-transitive epsilon-connected ordinal natural real complex ext-real non negative integer dim-like non prime for set ;
existence
not for b1 being Nat holds b1 is prime by INT_2:29;
end;

registration
cluster epsilon-transitive epsilon-connected ordinal natural real complex ext-real non negative integer dim-like non prime mersenne for set ;
existence
ex b1 being Nat st
( b1 is mersenne & not b1 is prime )
proof end;
end;

registration
cluster natural prime -> non zero for set ;
coherence
for b1 being Prime holds not b1 is zero by INT_2:def 4;
end;

registration
let n be mersenne Prime;
cluster Triangle n -> perfect ;
coherence
Triangle n is perfect
proof end;
end;

registration
cluster natural non zero perfect even -> non zero triangular for set ;
coherence
for b1 being non zero Nat st b1 is even & b1 is perfect holds
b1 is triangular by Th74;
end;

theorem Th75: :: NUMPOLY1:75
for n being Nat holds (8 * (Triangle n)) + 1 = ((2 * n) + 1) ^2
proof end;

theorem Th76: :: NUMPOLY1:76
for n being Nat st n is triangular holds
(8 * n) + 1 is square
proof end;

theorem Th77: :: NUMPOLY1:77
for n being Nat st n is triangular holds
(9 * n) + 1 is triangular
proof end;

theorem Th78: :: NUMPOLY1:78
for n being Nat st Triangle n is triangular & Triangle n is square holds
( Triangle ((4 * n) * (n + 1)) is triangular & Triangle ((4 * n) * (n + 1)) is square )
proof end;

registration
cluster TriangularNumbers -> infinite ;
coherence
not TriangularNumbers is finite
proof end;
cluster SquareNumbers -> infinite ;
coherence
not SquareNumbers is finite
proof end;
end;

registration
cluster epsilon-transitive epsilon-connected ordinal natural non zero real complex ext-real non negative integer dim-like square triangular for set ;
existence
ex b1 being Nat st
( b1 is triangular & b1 is square & not b1 is zero )
proof end;
end;

theorem Th79: :: NUMPOLY1:79
( 0 is triangular & 0 is square )
proof end;

registration
cluster zero -> square triangular for set ;
coherence
for b1 being number st b1 is zero holds
( b1 is triangular & b1 is square ) by Th79;
end;

theorem Th80: :: NUMPOLY1:80
( 1 is triangular & 1 is square )
proof end;

:: WP: Square triangular number
theorem :: NUMPOLY1:81
( 36 is triangular & 36 is square )
proof end;

theorem :: NUMPOLY1:82
( 1225 is triangular & 1225 is square )
proof end;

registration
let n be triangular Nat;
cluster (9 * n) + 1 -> triangular ;
coherence
(9 * n) + 1 is triangular by Th77;
end;

registration
let n be triangular Nat;
cluster (8 * n) + 1 -> square ;
coherence
(8 * n) + 1 is square by Th76;
end;

registration
let a be Real;
reduce lim (seq_const a) to a;
reducibility
lim (seq_const a) = a
proof end;
end;

definition
func ReciTriangRS -> Real_Sequence means :Def13: :: NUMPOLY1:def 13
 for i being Nat holds it . i = 1 / (Triangle i);
correctness
existence
ex b1 being Real_Sequence st
for i being Nat holds b1 . i = 1 / (Triangle i);
uniqueness
for b1, b2 being Real_Sequence st ( for i being Nat holds b1 . i = 1 / (Triangle i) ) & ( for i being Nat holds b2 . i = 1 / (Triangle i) ) holds
b1 = b2;
proof end;
end;

:: deftheorem Def13 defines ReciTriangRS NUMPOLY1:def 13 :
for b1 being Real_Sequence holds
( b1 = ReciTriangRS iff for i being Nat holds b1 . i = 1 / (Triangle i) );

registration
reduce ReciTriangRS . 0 to 0 ;
reducibility
ReciTriangRS . 0 = 0
proof end;
end;

theorem Th83: :: NUMPOLY1:83
for n being Nat holds 1 / (Triangle n) = 2 / (n * (n + 1))
proof end;

theorem Th84: :: NUMPOLY1:84
for n being Nat holds (Partial_Sums ReciTriangRS) . n = 2 - (2 / (n + 1))
proof end;

definition
func SumsReciTriang -> Real_Sequence means :Def14: :: NUMPOLY1:def 14
 for n being Nat holds it . n = 2 - (2 / (n + 1));
correctness
existence
ex b1 being Real_Sequence st
for n being Nat holds b1 . n = 2 - (2 / (n + 1));
uniqueness
for b1, b2 being Real_Sequence st ( for n being Nat holds b1 . n = 2 - (2 / (n + 1)) ) & ( for n being Nat holds b2 . n = 2 - (2 / (n + 1)) ) holds
b1 = b2;
proof end;
let a, b be Real;
func geo-seq (a,b) -> Real_Sequence means :Def15: :: NUMPOLY1:def 15
 for n being Nat holds it . n = a / (n + b);
correctness
existence
ex b1 being Real_Sequence st
for n being Nat holds b1 . n = a / (n + b);
uniqueness
for b1, b2 being Real_Sequence st ( for n being Nat holds b1 . n = a / (n + b) ) & ( for n being Nat holds b2 . n = a / (n + b) ) holds
b1 = b2;
proof end;
end;

:: deftheorem Def14 defines SumsReciTriang NUMPOLY1:def 14 :
for b1 being Real_Sequence holds
( b1 = SumsReciTriang iff for n being Nat holds b1 . n = 2 - (2 / (n + 1)) );

:: deftheorem Def15 defines geo-seq NUMPOLY1:def 15 :
for a, b being Real
for b3 being Real_Sequence holds
( b3 = geo-seq (a,b) iff for n being Nat holds b3 . n = a / (n + b) );

theorem Th85: :: NUMPOLY1:85
for a, b being Real holds
( geo-seq (a,b) is convergent & lim (geo-seq (a,b)) = 0 )
proof end;

theorem Th86: :: NUMPOLY1:86
SumsReciTriang = (seq_const 2) + (- (geo-seq (2,1)))
proof end;

theorem Th87: :: NUMPOLY1:87
( SumsReciTriang is convergent & lim SumsReciTriang = 2 )
proof end;

theorem :: NUMPOLY1:88
Partial_Sums ReciTriangRS = SumsReciTriang by Th84, Def14;

:: WP: Reciprocals of triangular numbers
theorem :: NUMPOLY1:89
Sum ReciTriangRS = 2 by Th84, Def14, Th87;