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

scheme :: NUMPOLY1:sch 1
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 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 b₁ being Nat st not b₁ is trivial holds
b₁ is 2 _or_greater by EC_PF_2:def 1, NAT_2:29;

cluster natural 2 _or_greater -> non trivial for set ;

coherence
for b₁ being Nat st b₁ is 2 _or_greater holds
not b₁ is trivial

proof end;

end;

registration

cluster natural 4 _or_greater -> non zero 3 _or_greater for set ;

coherence
for b₁ being Nat st b₁ is 4 _or_greater holds
( b₁ is 3 _or_greater & not b₁ is zero )

proof end;

end;

registration

cluster natural 4 _or_greater -> non trivial for set ;

coherence
for b₁ being Nat st b₁ is 4 _or_greater holds
not b₁ 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 b₁ being Nat st b₁ 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 b₁ being Nat st b₁ 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 b₁ being number st b₁ is triangular holds
b₁ is natural ;

end;

registration

cluster non zero triangular for set ;

existence
ex b₁ being number st
( b₁ is triangular & not b₁ 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 b₁ being number st b₁ is s -gonal

proof end;

end;

registration

let s be non zero Nat;

cluster non zero s -gonal for set ;

existence
ex b₁ being number st
( not b₁ is zero & b₁ is s -gonal )

proof end;

end;

registration

let s be Nat;

cluster s -gonal -> real for set ;

coherence
for b₁ being number st b₁ is s -gonal holds
b₁ is real ;

end;

registration

let s be non trivial Nat;

cluster s -gonal -> natural for set ;

coherence
for b₁ being number st b₁ is s -gonal holds
b₁ 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 b₁ -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 b₂ -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 b₁ -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 b₁ -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 b₁ -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;

:: 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 b₁ being 4 _or_greater Nat st b₁ is triangular holds
not b₁ 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 b₁ -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 b₁ being Nat st b₁ is 3 -gonal holds
b₁ is triangular ;

cluster natural triangular -> 3 -gonal for set ;

coherence
for b₁ being Nat st b₁ is triangular holds
b₁ is 3 -gonal

proof end;

cluster natural 4 -gonal -> square for set ;

coherence
for b₁ being Nat st b₁ is 4 -gonal holds
b₁ is square ;

cluster natural square -> 4 -gonal for set ;

coherence
for b₁ being Nat st b₁ is square holds
b₁ 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 b₁ being FinSequence of REAL st
( dom b₁ = Seg k & ( for i being Nat st i in dom b₁ holds
b₁ . i = i |^ n ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of REAL st dom b₁ = Seg k & ( for i being Nat st i in dom b₁ holds
b₁ . i = i |^ n ) & dom b₂ = Seg k & ( for i being Nat st i in dom b₂ holds
b₂ . i = i |^ n ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def8 defines NPower NUMPOLY1:def 8 :
for n, k being Nat
for b₃ being FinSequence of REAL holds
( b₃ = NPower (n,k) iff ( dom b₃ = Seg k & ( for i being Nat st i in dom b₃ holds
b₃ . 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 b₁ being Element of TriangularNumbers holds b₁ is triangular

proof end;

cluster -> square for Element of SquareNumbers ;

coherence
for b₁ being Element of SquareNumbers holds b₁ 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 b₁ being Prime st b₁ 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 b₁ being Nat holds b₁ 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 b₁ being Nat st
( b₁ is mersenne & not b₁ is prime )

proof end;

end;

registration

cluster natural prime -> non zero for set ;

coherence
for b₁ being Prime holds not b₁ 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 b₁ being non zero Nat st b₁ is even & b₁ is perfect holds
b₁ 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 b₁ being Nat st
( b₁ is triangular & b₁ is square & not b₁ 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 b₁ being number st b₁ is zero holds
( b₁ is triangular & b₁ is square ) by Th79;

end;

theorem Th80: :: NUMPOLY1:80

( 1 is triangular & 1 is square )

proof end;

:: 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 b₁ being Real_Sequence st
for i being Nat holds b₁ . i = 1 / (Triangle i);
uniqueness
for b₁, b₂ being Real_Sequence st ( for i being Nat holds b₁ . i = 1 / (Triangle i) ) & ( for i being Nat holds b₂ . i = 1 / (Triangle i) ) holds
b₁ = b₂;

proof end;

end;

:: deftheorem Def13 defines ReciTriangRS NUMPOLY1:def 13 :
for b₁ being Real_Sequence holds
( b₁ = ReciTriangRS iff for i being Nat holds b₁ . 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 b₁ being Real_Sequence st
for n being Nat holds b₁ . n = 2 - (2 / (n + 1));
uniqueness
for b₁, b₂ being Real_Sequence st ( for n being Nat holds b₁ . n = 2 - (2 / (n + 1)) ) & ( for n being Nat holds b₂ . n = 2 - (2 / (n + 1)) ) holds
b₁ = b₂;

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 b₁ being Real_Sequence st
for n being Nat holds b₁ . n = a / (n + b);
uniqueness
for b₁, b₂ being Real_Sequence st ( for n being Nat holds b₁ . n = a / (n + b) ) & ( for n being Nat holds b₂ . n = a / (n + b) ) holds
b₁ = b₂;

proof end;

end;

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

:: deftheorem Def15 defines geo-seq NUMPOLY1:def 15 :
for a, b being Real
for b₃ being Real_Sequence holds
( b₃ = geo-seq (a,b) iff for n being Nat holds b₃ . 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;

:: Reciprocals of triangular numbers

theorem :: NUMPOLY1:89

Sum ReciTriangRS = 2 by Th84, Def14, Th87;