:: 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 H₁( 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 b₁ being Complex_Sequence st
for n being Nat holds b₁ . n = (Polynom (a,b,n)) / (Polynom (c,d,n))

proof end;

uniqueness
for b₁, b₂ being Complex_Sequence st ( for n being Nat holds b₁ . n = (Polynom (a,b,n)) / (Polynom (c,d,n)) ) & ( for n being Nat holds b₂ . n = (Polynom (a,b,n)) / (Polynom (c,d,n)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines Rat_Exp_Seq BASEL_1:def 1 :
for a, b, c, d being Complex
for b₅ being Complex_Sequence holds
( b₅ = Rat_Exp_Seq (a,b,c,d) iff for n being Nat holds b₅ . 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 b₁ being Subset of REAL st b₁ = dom tan holds
b₁ 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 b₁ being Function st
( dom b₁ = dom f & ( for x being object st x in dom f holds
b₁ . x = cot (f . x) ) )

proof end;

uniqueness
for b₁, b₂ being Function st dom b₁ = dom f & ( for x being object st x in dom f holds
b₁ . x = cot (f . x) ) & dom b₂ = dom f & ( for x being object st x in dom f holds
b₂ . x = cot (f . x) ) holds
b₁ = b₂

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 b₁ being Function st
( dom b₁ = dom f & ( for x being object st x in dom f holds
b₁ . x = cosec (f . x) ) )

proof end;

uniqueness
for b₁, b₂ being Function st dom b₁ = dom f & ( for x being object st x in dom f holds
b₁ . x = cosec (f . x) ) & dom b₂ = dom f & ( for x being object st x in dom f holds
b₂ . x = cosec (f . x) ) holds
b₁ = b₂

proof end;

end;

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

:: deftheorem Def4 defines cosec BASEL_1:def 4 :
for f being real-valued Function
for b₂ being Function holds
( b₂ = cosec f iff ( dom b₂ = dom f & ( for x being object st x in dom f holds
b₂ . 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;