:: Basel Problem -- Preliminaries
:: by Artur Korni{\l}owicz and Karol P\kak
::
:: Received June 27, 2017
:: Copyright (c) 2017-2021 Association of Mizar Users


set p = (PI ^2) / 6;

theorem Th1: :: BASEL_1:1
for a, b being Real st 0 < a holds
ex m being Nat st 0 < (a * m) + b
proof end;

Lm1: for f being FinSequence
for h being Function st dom h = dom f holds
h is FinSequence
proof end;

Lm2: for f being FinSequence
for y being object st y in rng f holds
ex n being Nat st
( 1 <= n & n <= len f & y = f . n )
proof end;

Lm3: for f being complex-valued FinSequence holds len (f ") = len f
proof end;

registration
let f be real-valued FinSequence;
let n be Nat;
cluster f | n -> REAL -valued ;
coherence
f | n is REAL -valued ;
end;

registration
let f be complex-valued FinSequence;
cluster f ^2 -> len f -element ;
coherence
f ^2 is len f -element
proof end;
cluster f " -> len f -element ;
coherence
f " is len f -element
proof end;
end;

registration
let f be complex-valued FinSequence;
let c be Complex;
cluster c + f -> len f -element ;
coherence
c + f is len f -element
proof end;
end;

theorem Th2: :: BASEL_1:2
for c, z being Complex holds c + <*z*> = <*(c + z)*>
proof end;

theorem Th3: :: BASEL_1:3
for f, g being complex-valued FinSequence
for c being Complex holds c + (f ^ g) = (c + f) ^ (c + g)
proof end;

theorem :: BASEL_1:4
for f being complex-valued FinSequence
for c being Complex holds Sum (c + f) = (c * (len f)) + (Sum f)
proof end;

definition
let a, b, c, d be Complex;
deffunc H1( Nat) -> set = (Polynom (a,b,$1)) / (Polynom (c,d,$1));
func Rat_Exp_Seq (a,b,c,d) -> Complex_Sequence means :Def1: :: BASEL_1:def 1
 for n being Nat holds it . n = (Polynom (a,b,n)) / (Polynom (c,d,n));
existence
ex b1 being Complex_Sequence st
for n being Nat holds b1 . n = (Polynom (a,b,n)) / (Polynom (c,d,n))
proof end;
uniqueness
for b1, b2 being Complex_Sequence st ( for n being Nat holds b1 . n = (Polynom (a,b,n)) / (Polynom (c,d,n)) ) & ( for n being Nat holds b2 . n = (Polynom (a,b,n)) / (Polynom (c,d,n)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines Rat_Exp_Seq BASEL_1:def 1 :
for a, b, c, d being Complex
for b5 being Complex_Sequence holds
( b5 = Rat_Exp_Seq (a,b,c,d) iff for n being Nat holds b5 . n = (Polynom (a,b,n)) / (Polynom (c,d,n)) );

definition
let a, b, c, d be Real;
func rseq (a,b,c,d) -> Real_Sequence equals :: BASEL_1:def 2
 Re (Rat_Exp_Seq (a,b,c,d));
coherence
Re (Rat_Exp_Seq (a,b,c,d)) is Real_Sequence ;
end;

:: deftheorem defines rseq BASEL_1:def 2 :
for a, b, c, d being Real holds rseq (a,b,c,d) = Re (Rat_Exp_Seq (a,b,c,d));

theorem Th5: :: BASEL_1:5
for n being Nat
for a, b, c, d being Real holds (rseq (a,b,c,d)) . n = ((a * n) + b) / ((c * n) + d)
proof end;

theorem Th6: :: BASEL_1:6
for n being Nat
for b, d being Real holds (rseq (0,b,0,d)) . n = b / d
proof end;

registration
let a, b be Real;
cluster rseq (a,b,0,0) -> constant ;
coherence
rseq (a,b,0,0) is constant
proof end;
end;

registration
let b, d be Real;
cluster rseq (0,b,0,d) -> constant ;
coherence
rseq (0,b,0,d) is constant
proof end;
end;

theorem Th7: :: BASEL_1:7
for b, c, d being Real holds
( rseq (0,b,c,d) = b (#) (rseq (0,1,c,d)) & rseq (0,b,c,d) = (- b) (#) (rseq (0,1,(- c),(- d))) )
proof end;

theorem Th8: :: BASEL_1:8
for a, c, d being Real holds
( rseq (a,0,c,d) = a (#) (rseq (1,0,c,d)) & rseq (a,0,c,d) = (- a) (#) (rseq (1,0,(- c),(- d))) )
proof end;

Lm4: for c, d being Real st 0 < c holds
for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((rseq (0,1,c,d)) . m) - 0).| < p
proof end;

Lm5: for c, d being Real st 0 < c holds
rseq (0,1,c,d) is convergent
proof end;

Lm6: for c, d being Real holds rseq (0,1,c,d) is convergent
proof end;

Lm7: for c, d being Real st 0 < c holds
lim (rseq (0,1,c,d)) = 0
proof end;

Lm8: for c, d being Real st c < 0 holds
lim (rseq (0,1,c,d)) = 0
proof end;

registration
let b, c, d be Real;
cluster rseq (0,b,c,d) -> convergent ;
coherence
rseq (0,b,c,d) is convergent
proof end;
end;

theorem :: BASEL_1:9
for b, d being Real holds lim (rseq (0,b,0,d)) = b / d
proof end;

theorem Th10: :: BASEL_1:10
for b, d being Real
for c being non zero Real holds lim (rseq (0,b,c,d)) = 0
proof end;

Lm9: for c, d being Real st 0 < c holds
for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((rseq (1,0,c,d)) . m) - (1 / c)).| < p
proof end;

Lm10: for c, d being Real st 0 < c holds
rseq (1,0,c,d) is convergent
proof end;

Lm11: for c, d being Real st 0 < c holds
lim (rseq (1,0,c,d)) = 1 / c
proof end;

Lm12: for d being Real
for c being non zero Real holds rseq (1,0,c,d) is convergent
proof end;

Lm13: for d being Real
for c being non zero Real holds lim (rseq (1,0,c,d)) = 1 / c
proof end;

registration
let c be non zero Real;
let a, b, d be Real;
cluster rseq (a,b,c,d) -> convergent ;
coherence
rseq (a,b,c,d) is convergent
proof end;
end;

registration
let a, d be positive Real;
let b be Real;
cluster rseq (a,b,0,d) -> non bounded_above ;
coherence
not rseq (a,b,0,d) is bounded_above
proof end;
end;

registration
let a, d be negative Real;
let b be Real;
cluster rseq (a,b,0,d) -> non bounded_above ;
coherence
not rseq (a,b,0,d) is bounded_above
proof end;
end;

registration
let a be positive Real;
let b be Real;
let d be negative Real;
cluster rseq (a,b,0,d) -> non bounded_below ;
coherence
not rseq (a,b,0,d) is bounded_below
proof end;
end;

registration
let a be negative Real;
let b be Real;
let d be positive Real;
cluster rseq (a,b,0,d) -> non bounded_below ;
coherence
not rseq (a,b,0,d) is bounded_below
proof end;
end;

registration
let a, d be non zero Real;
let b be Real;
cluster rseq (a,b,0,d) -> non bounded ;
coherence
not rseq (a,b,0,d) is bounded
proof end;
end;

registration
let a, d be non zero Real;
let b be Real;
cluster rseq (a,b,0,d) -> non convergent ;
coherence
not rseq (a,b,0,d) is convergent ;
end;

theorem Th11: :: BASEL_1:11
for a, b, d being Real
for c being non zero Real holds lim (rseq (a,b,c,d)) = a / c
proof end;

theorem Th12: :: BASEL_1:12
for b, d being Real
for a being non zero Real holds lim (rseq (a,b,a,d)) = 1
proof end;

theorem :: BASEL_1:13
for i being Integer holds sin (PI * i) = 0
proof end;

theorem Th14: :: BASEL_1:14
for i being Integer holds cos ((PI / 2) + (PI * i)) = 0
proof end;

theorem Th15: :: BASEL_1:15
for r being Real holds
( tan r = (cot r) " & cot r = (tan r) " )
proof end;

theorem Th16: :: BASEL_1:16
dom tan = union { ].((- (PI / 2)) + (PI * i)),((PI / 2) + (PI * i)).[ where i is Integer : verum }
proof end;

registration
cluster dom tan -> open for Subset of REAL;
coherence
for b1 being Subset of REAL st b1 = dom tan holds
b1 is open
proof end;
end;

theorem Th17: :: BASEL_1:17
for r being Real st 0 <= r holds
sin . r <= r
proof end;

theorem Th18: :: BASEL_1:18
for r being Real st 0 <= r & r < PI / 2 holds
r <= tan . r
proof end;

definition
let f be real-valued Function;
func cot f -> Function means :Def3: :: BASEL_1:def 3
( dom it = dom f & ( for x being object st x in dom f holds
it . x = cot (f . x) ) );
existence
ex b1 being Function st
( dom b1 = dom f & ( for x being object st x in dom f holds
b1 . x = cot (f . x) ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = dom f & ( for x being object st x in dom f holds
b1 . x = cot (f . x) ) & dom b2 = dom f & ( for x being object st x in dom f holds
b2 . x = cot (f . x) ) holds
b1 = b2
proof end;
func cosec f -> Function means :Def4: :: BASEL_1:def 4
( dom it = dom f & ( for x being object st x in dom f holds
it . x = cosec (f . x) ) );
existence
ex b1 being Function st
( dom b1 = dom f & ( for x being object st x in dom f holds
b1 . x = cosec (f . x) ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = dom f & ( for x being object st x in dom f holds
b1 . x = cosec (f . x) ) & dom b2 = dom f & ( for x being object st x in dom f holds
b2 . x = cosec (f . x) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines cot BASEL_1:def 3 :
for f being real-valued Function
for b2 being Function holds
( b2 = cot f iff ( dom b2 = dom f & ( for x being object st x in dom f holds
b2 . x = cot (f . x) ) ) );

:: deftheorem Def4 defines cosec BASEL_1:def 4 :
for f being real-valued Function
for b2 being Function holds
( b2 = cosec f iff ( dom b2 = dom f & ( for x being object st x in dom f holds
b2 . x = cosec (f . x) ) ) );

registration
let f be real-valued Function;
cluster cot f -> REAL -valued ;
coherence
cot f is REAL -valued
proof end;
cluster cosec f -> REAL -valued ;
coherence
cosec f is REAL -valued
proof end;
end;

registration
let f be real-valued FinSequence;
cluster cot f -> FinSequence-like ;
coherence
cot f is FinSequence-like
proof end;
cluster cosec f -> FinSequence-like ;
coherence
cosec f is FinSequence-like
proof end;
end;

theorem Lm14: :: BASEL_1:19
for f being real-valued FinSequence holds len (cot f) = len f
proof end;

theorem Lm15: :: BASEL_1:20
for f being real-valued FinSequence holds len (cosec f) = len f
proof end;

registration
let f be real-valued FinSequence;
cluster cot f -> len f -element ;
coherence
cot f is len f -element
proof end;
cluster cosec f -> len f -element ;
coherence
cosec f is len f -element
proof end;
end;

Lm16: for n being Nat holds (rseq (0,1,1,0)) . n = 1 / n
proof end;

Lm17: lim (rseq (2,0,2,1)) = 1
by Th12;

Lm18: lim (rseq (2,(- 1),2,1)) = 1
by Th12;

Lm19: lim (rseq (2,2,2,1)) = 1
by Th12;

definition
let m be Nat;
func x_r-seq m -> FinSequence equals :: BASEL_1:def 5
(PI / ((2 * m) + 1)) (#) (idseq m);
coherence
(PI / ((2 * m) + 1)) (#) (idseq m) is FinSequence ;
end;

:: deftheorem defines x_r-seq BASEL_1:def 5 :
for m being Nat holds x_r-seq m = (PI / ((2 * m) + 1)) (#) (idseq m);

theorem Th19: :: BASEL_1:21
for m being Nat holds
( len (x_r-seq m) = m & ( for k being Nat st 1 <= k & k <= m holds
(x_r-seq m) . k = (k * PI) / ((2 * m) + 1) ) )
proof end;

theorem Th20: :: BASEL_1:22
for m being Nat holds rng (x_r-seq m) c= ].0,(PI / 2).[
proof end;

registration
let m be Nat;
cluster x_r-seq m -> REAL -valued ;
coherence
x_r-seq m is REAL -valued ;
end;

theorem Th21: :: BASEL_1:23
for k, m being Nat st 1 <= k & k <= m holds
( 0 < (x_r-seq m) . k & (x_r-seq m) . k < PI / 2 )
proof end;

registration
cluster x_r-seq 0 -> empty ;
coherence
x_r-seq 0 is empty ;
end;

theorem :: BASEL_1:24
for k, m being Nat st 1 <= k & k <= m holds
(2 / (k * PI)) + (((x_r-seq m) ") . k) = ((x_r-seq (m + 1)) ") . k
proof end;

theorem :: BASEL_1:25
for k, m being Nat st 1 <= k & k <= m holds
((2 * m) + 1) * ((x_r-seq m) . k) = k * PI
proof end;

theorem :: BASEL_1:26
for m being Nat holds sqr (cosec (x_r-seq m)) = 1 + (sqr (cot (x_r-seq m)))
proof end;

theorem Th25: :: BASEL_1:27
for n being Nat holds x_r-seq n is one-to-one
proof end;

theorem :: BASEL_1:28
for n being Nat holds sqr (cot (x_r-seq n)) is one-to-one
proof end;

theorem :: BASEL_1:29
for m being Nat holds Sum (sqr (cot (x_r-seq m))) <= Sum ((sqr (x_r-seq m)) ")
proof end;

theorem :: BASEL_1:30
for m being Nat holds Sum ((sqr (x_r-seq m)) ") <= Sum (sqr (cosec (x_r-seq m)))
proof end;

definition
func Basel-seq -> Real_Sequence equals :: BASEL_1:def 6
(rseq (0,1,1,0)) (#) (rseq (0,1,1,0));
coherence
(rseq (0,1,1,0)) (#) (rseq (0,1,1,0)) is Real_Sequence ;
func Basel-seq1 -> Real_Sequence equals :: BASEL_1:def 7
(((PI ^2) / 6) (#) (rseq (2,0,2,1))) (#) (rseq (2,(- 1),2,1));
coherence
(((PI ^2) / 6) (#) (rseq (2,0,2,1))) (#) (rseq (2,(- 1),2,1)) is Real_Sequence ;
func Basel-seq2 -> Real_Sequence equals :: BASEL_1:def 8
(((PI ^2) / 6) (#) (rseq (2,0,2,1))) (#) (rseq (2,2,2,1));
coherence
(((PI ^2) / 6) (#) (rseq (2,0,2,1))) (#) (rseq (2,2,2,1)) is Real_Sequence ;
end;

:: deftheorem defines Basel-seq BASEL_1:def 6 :
Basel-seq = (rseq (0,1,1,0)) (#) (rseq (0,1,1,0));

:: deftheorem defines Basel-seq1 BASEL_1:def 7 :
Basel-seq1 = (((PI ^2) / 6) (#) (rseq (2,0,2,1))) (#) (rseq (2,(- 1),2,1));

:: deftheorem defines Basel-seq2 BASEL_1:def 8 :
Basel-seq2 = (((PI ^2) / 6) (#) (rseq (2,0,2,1))) (#) (rseq (2,2,2,1));

theorem Th29: :: BASEL_1:31
for n being Nat holds Basel-seq . n = 1 / (n ^2)
proof end;

theorem :: BASEL_1:32
for n being Nat holds Basel-seq1 . n = (((PI ^2) / 6) * ((2 * n) / ((2 * n) + 1))) * (((2 * n) - 1) / ((2 * n) + 1))
proof end;

theorem :: BASEL_1:33
for n being Nat holds Basel-seq2 . n = (((PI ^2) / 6) * ((2 * n) / ((2 * n) + 1))) * (((2 * n) + 2) / ((2 * n) + 1))
proof end;

registration
cluster Basel-seq -> convergent ;
coherence
Basel-seq is convergent ;
cluster Basel-seq1 -> convergent ;
coherence
Basel-seq1 is convergent ;
cluster Basel-seq2 -> convergent ;
coherence
Basel-seq2 is convergent ;
end;

theorem :: BASEL_1:34
( lim Basel-seq1 = (PI ^2) / 6 & (PI ^2) / 6 = lim Basel-seq2 )
proof end;

theorem :: BASEL_1:35
for m being Nat holds Sum ((sqr (x_r-seq m)) ") = ((((2 * m) + 1) ^2) / (PI ^2)) * (Sum (Basel-seq,m))
proof end;