:: by Adam Grabowski

::

:: Received May 19, 2013

:: Copyright (c) 2013-2016 Association of Mizar Users

scheme :: NUMPOLY1:sch 1

LNatRealSeq{ F_{1}( set ) -> Real } :

LNatRealSeq{ F

( ex seq being Real_Sequence st

for n being Nat holds seq . n = F_{1}(n) & ( for seq1, seq2 being Real_Sequence st ( for n being Nat holds seq1 . n = F_{1}(n) ) & ( for n being Nat holds seq2 . n = F_{1}(n) ) holds

seq1 = seq2 ) )

for n being Nat holds seq . n = F

seq1 = seq2 ) )

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
end;

registration
end;

registration
end;

registration

coherence

for b_{1} being Nat st not b_{1} is trivial holds

b_{1} is 2 _or_greater
by EC_PF_2:def 1, NAT_2:29;

coherence

for b_{1} being Nat st b_{1} is 2 _or_greater holds

not b_{1} is trivial

end;
for b

b

coherence

for b

not b

proof end;

registration

coherence

for b_{1} being Nat st b_{1} is 4 _or_greater holds

( b_{1} is 3 _or_greater & not b_{1} is zero )

end;
for b

( b

proof end;

registration
end;

registration

ex b_{1} being Nat st b_{1} is 4 _or_greater
by EC_PF_2:def 1;

ex b_{1} being Nat st b_{1} is 3 _or_greater
by EC_PF_2:def 1;

end;

cluster epsilon-transitive epsilon-connected ordinal natural real complex ext-real non negative integer dim-like 4 _or_greater for set ;

existence ex b

cluster epsilon-transitive epsilon-connected ordinal natural real complex ext-real non negative integer dim-like 3 _or_greater for set ;

existence ex b

:: deftheorem Def2 defines triangular NUMPOLY1:def 2 :

for n being object holds

( n is triangular iff ex k being Nat st n = Triangle k );

for n being object holds

( n is triangular iff ex k being Nat st n = Triangle k );

registration
end;

registration
end;

registration
end;

registration
end;

Lm3: 0 - 1 < 0

;

registration
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 )

( 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 ;

coherence

(((n ^2) * (s - 2)) - (n * (s - 4))) / 2 is Integer

end;
coherence

(((n ^2) * (s - 2)) - (n * (s - 4))) / 2 is Integer

proof 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;

for s, n being natural Number holds Polygon (s,n) = (((n ^2) * (s - 2)) - (n * (s - 4))) / 2;

theorem :: NUMPOLY1:28

:: 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) );

for s being Nat

for x being object holds

( x is s -gonal iff ex n being Nat st x = Polygon (s,n) );

definition
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 );

for x being object holds

( x is polygonal iff ex s being Nat st x is s -gonal );

registration

let s be non zero Nat;

existence

ex b_{1} being number st

( not b_{1} is zero & b_{1} is s -gonal )

end;
existence

ex b

( not b

proof end;

registration
end;

registration

let s be non trivial Nat;

coherence

for b_{1} being number st b_{1} is s -gonal holds

b_{1} is natural
by EC_PF_2:def 1, Th27;

end;
coherence

for b

b

theorem :: NUMPOLY1:31

definition

let s be Nat;

let x be s -gonal number ;

(((sqrt ((((8 * s) - 16) * x) + ((s - 4) ^2))) + s) - 4) / ((2 * s) - 4) is Real ;

end;
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);

(((sqrt ((((8 * s) - 16) * x) + ((s - 4) ^2))) + s) - 4) / ((2 * s) - 4) is Real ;

:: deftheorem defines IndexPoly NUMPOLY1:def 6 :

for s being Nat

for x being b_{1} -gonal number holds IndexPoly (s,x) = (((sqrt ((((8 * s) - 16) * x) + ((s - 4) ^2))) + s) - 4) / ((2 * s) - 4);

for s being Nat

for x being b

theorem :: NUMPOLY1:32

theorem :: NUMPOLY1:33

for s being non zero Nat

for x being non zero b_{1} -gonal number st s >= 4 holds

(((8 * s) - 16) * x) + ((s - 4) ^2) is square

for x being non zero b

(((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_{1} -gonal number st s >= 4 holds

IndexPoly (s,x) in NAT

for x being non zero b

IndexPoly (s,x) in NAT

proof end;

theorem Th35: :: NUMPOLY1:35

for s being non trivial Nat

for x being b_{1} -gonal number holds 0 <= (((8 * s) - 16) * x) + ((s - 4) ^2)

for x being b

proof end;

:: Centered polygonal number

:: deftheorem defines CenterPolygon NUMPOLY1:def 7 :

for s, n being Nat holds CenterPolygon (s,n) = (((s * n) / 2) * (n - 1)) + 1;

for s, n being Nat holds CenterPolygon (s,n) = (((s * n) / 2) * (n - 1)) + 1;

registration
end;

registration

coherence

for b_{1} being 4 _or_greater Nat st b_{1} is triangular holds

not b_{1} is prime

end;
for b

not b

proof end;

registration

let s be non zero 4 _or_greater Nat;

let x be non zero s -gonal number ;

coherence

IndexPoly (s,x) is natural by Th34, EC_PF_2:def 1;

end;
let x be non zero s -gonal number ;

coherence

IndexPoly (s,x) is natural by Th34, EC_PF_2:def 1;

theorem :: NUMPOLY1:47

for s being 4 _or_greater Nat

for x being non zero b_{1} -gonal number st s <> 2 holds

Polygon (s,(IndexPoly (s,x))) = x

for x being non zero b

Polygon (s,(IndexPoly (s,x))) = x

proof end;

registration
end;

registration
end;

registration
end;

registration

coherence

for b_{1} being Nat st b_{1} is 3 -gonal holds

b_{1} is triangular
;

coherence

for b_{1} being Nat st b_{1} is triangular holds

b_{1} is 3 -gonal

for b_{1} being Nat st b_{1} is 4 -gonal holds

b_{1} is square
;

coherence

for b_{1} being Nat st b_{1} is square holds

b_{1} is 4 -gonal

end;
for b

b

coherence

for b

b

proof end;

coherence for b

b

coherence

for b

b

proof end;

definition

let n, k be Nat;

ex b_{1} being FinSequence of REAL st

( dom b_{1} = Seg k & ( for i being Nat st i in dom b_{1} holds

b_{1} . i = i |^ n ) )

for b_{1}, b_{2} being FinSequence of REAL st dom b_{1} = Seg k & ( for i being Nat st i in dom b_{1} holds

b_{1} . i = i |^ n ) & dom b_{2} = Seg k & ( for i being Nat st i in dom b_{2} holds

b_{2} . i = i |^ n ) holds

b_{1} = b_{2}

end;
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 ( dom it = Seg k & ( for i being Nat st i in dom it holds

it . i = i |^ n ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def8 defines NPower NUMPOLY1:def 8 :

for n, k being Nat

for b_{3} being FinSequence of REAL holds

( b_{3} = NPower (n,k) iff ( dom b_{3} = Seg k & ( for i being Nat st i in dom b_{3} holds

b_{3} . i = i |^ n ) ) );

for n, k being Nat

for b

( b

b

registration
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: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: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;

{ (Polygon (s,n)) where n is Nat : verum } is set ;

end;
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 } ;

{ (Polygon (s,n)) where n is Nat : verum } is set ;

:: deftheorem defines PolygonalNumbers NUMPOLY1:def 9 :

for s being Nat holds PolygonalNumbers s = { (Polygon (s,n)) where n is Nat : verum } ;

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

end;
:: original: PolygonalNumbers

redefine func PolygonalNumbers s -> Subset of NAT;

coherence

PolygonalNumbers s is Subset of NAT

proof end;

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

;

definition

coherence

PolygonalNumbers 3 is Subset of NAT

PolygonalNumbers 4 is Subset of NAT

end;
PolygonalNumbers 3 is Subset of NAT

proof end;

coherence PolygonalNumbers 4 is Subset of NAT

proof end;

registration
end;

registration

coherence

for b_{1} being Element of TriangularNumbers holds b_{1} is triangular

for b_{1} being Element of SquareNumbers holds b_{1} is square

end;
for b

proof end;

coherence for b

proof end;

registration
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 );

for n being number holds

( n is mersenne iff ex p being Nat st n = Mersenne p );

registration

ex b_{1} being Prime st b_{1} is mersenne

not for b_{1} being Nat holds b_{1} is prime
by INT_2:29;

end;

cluster epsilon-transitive epsilon-connected ordinal natural real complex ext-real non negative integer dim-like prime mersenne for set ;

existence ex b

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

registration

ex b_{1} being Nat st

( b_{1} is mersenne & not b_{1} is prime )
end;

cluster epsilon-transitive epsilon-connected ordinal natural real complex ext-real non negative integer dim-like non prime mersenne for set ;

existence ex b

( b

proof end;

registration
end;

registration

coherence

for b_{1} being non zero Nat st b_{1} is even & b_{1} is perfect holds

b_{1} is triangular
by Th74;

end;
for b

b

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 )

( Triangle ((4 * n) * (n + 1)) is triangular & Triangle ((4 * n) * (n + 1)) is square )

proof end;

registration

coherence

not TriangularNumbers is finite

not SquareNumbers is finite

end;
not TriangularNumbers is finite

proof end;

coherence not SquareNumbers is finite

proof end;

registration

ex b_{1} being Nat st

( b_{1} is triangular & b_{1} is square & not b_{1} is zero )
end;

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

( b

proof end;

registration

coherence

for b_{1} being number st b_{1} is zero holds

( b_{1} is triangular & b_{1} is square )
by Th79;

end;
for b

( b

registration
end;

registration
end;

definition

existence

ex b_{1} being Real_Sequence st

for i being Nat holds b_{1} . i = 1 / (Triangle i);

uniqueness

for b_{1}, b_{2} being Real_Sequence st ( for i being Nat holds b_{1} . i = 1 / (Triangle i) ) & ( for i being Nat holds b_{2} . i = 1 / (Triangle i) ) holds

b_{1} = b_{2};

end;

func ReciTriangRS -> Real_Sequence means :Def13: :: NUMPOLY1:def 13

for i being Nat holds it . i = 1 / (Triangle i);

correctness for i being Nat holds it . i = 1 / (Triangle i);

existence

ex b

for i being Nat holds b

uniqueness

for b

b

proof end;

:: deftheorem Def13 defines ReciTriangRS NUMPOLY1:def 13 :

for b_{1} being Real_Sequence holds

( b_{1} = ReciTriangRS iff for i being Nat holds b_{1} . i = 1 / (Triangle i) );

for b

( b

definition

existence

ex b_{1} being Real_Sequence st

for n being Nat holds b_{1} . n = 2 - (2 / (n + 1));

uniqueness

for b_{1}, b_{2} being Real_Sequence st ( for n being Nat holds b_{1} . n = 2 - (2 / (n + 1)) ) & ( for n being Nat holds b_{2} . n = 2 - (2 / (n + 1)) ) holds

b_{1} = b_{2};

existence

ex b_{1} being Real_Sequence st

for n being Nat holds b_{1} . n = a / (n + b);

uniqueness

for b_{1}, b_{2} being Real_Sequence st ( for n being Nat holds b_{1} . n = a / (n + b) ) & ( for n being Nat holds b_{2} . n = a / (n + b) ) holds

b_{1} = b_{2};

end;

func SumsReciTriang -> Real_Sequence means :Def14: :: NUMPOLY1:def 14

for n being Nat holds it . n = 2 - (2 / (n + 1));

correctness for n being Nat holds it . n = 2 - (2 / (n + 1));

existence

ex b

for n being Nat holds b

uniqueness

for 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 for n being Nat holds it . n = a / (n + b);

existence

ex b

for n being Nat holds b

uniqueness

for b

b

proof end;

:: deftheorem Def14 defines SumsReciTriang NUMPOLY1:def 14 :

for b_{1} being Real_Sequence holds

( b_{1} = SumsReciTriang iff for n being Nat holds b_{1} . n = 2 - (2 / (n + 1)) );

for b

( b

:: deftheorem Def15 defines geo-seq NUMPOLY1:def 15 :

for a, b being Real

for b_{3} being Real_Sequence holds

( b_{3} = geo-seq (a,b) iff for n being Nat holds b_{3} . n = a / (n + b) );

for a, b being Real

for b

( b