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

set FC = F_Complex ;

registration

let L be non empty right_zeroed doubleLoopStr ;
let n be Nat;

reduce n * (0. L) to 0. L;

reducibility
n * (0. L) = 0. L

proof end;

end;

theorem Th1: :: BASEL_2:1

for n being Nat
for z being Complex
for e being Element of F_Complex st z = e holds
n * z = n * e

proof end;

registration

let e be Element of F_Complex;
let z be Complex;
let n be Nat;

identify n * e with n * z when e = z;

correctness
compatibility
( e = z implies n * e = n * z );
by Th1;

end;

theorem Th2: :: BASEL_2:2

for Z being complex-valued FinSequence
for E being FinSequence of F_Complex st E = Z holds
Sum Z = Sum E

proof end;

theorem Th3: :: BASEL_2:3

for n being Nat holds (1_ F_Complex) |^ n = 1_ F_Complex

proof end;

theorem Th4: :: BASEL_2:4

for L being non empty right_zeroed left_zeroed addLoopStr
for z0, z1 being Element of L holds <%z0,z1%> = <%z0%> + <%(0. L),z1%>

proof end;

theorem Th5: :: BASEL_2:5

for L being non empty right_complementable add-associative right_zeroed distributive doubleLoopStr
for a, b, c, d being Element of L holds <%a,b%> *' <%c,d%> = <%(a * c),((a * d) + (b * c)),(b * d)%>

proof end;

theorem Th6: :: BASEL_2:6

for L being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive commutative doubleLoopStr holds <%(0. L),(0. L),(1. L)%> = <%(0. L),(1. L)%> `^ 2

proof end;

theorem Th7: :: BASEL_2:7

for n being Nat
for L being non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr
for z being Element of L
for p being Polynomial of L holds (p *' <%z%>) . n = (p . n) * z

proof end;

theorem Th8: :: BASEL_2:8

for n being Nat
for L being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative commutative doubleLoopStr
for x being Element of L holds <%x%> `^ n = <%(x |^ n)%>

proof end;

theorem Th9: :: BASEL_2:9

for k, n being Nat
for R being commutative Ring
for z0, z1 being Element of R holds
( (<%z0,z1%> `^ 0) . 0 = 1. R & ( n > 0 implies (<%(0. R),z1%> `^ n) . n = z1 |^ n ) & ( k <> n implies (<%(0. R),z1%> `^ n) . k = 0. R ) )

proof end;

theorem Th10: :: BASEL_2:10

for n being Nat
for R being commutative Ring holds
( (<%(0. R),(0. R),(1_ R)%> `^ n) . (2 * n) = 1_ R & ( for k being Nat st k <> 2 * n holds
(<%(0. R),(0. R),(1_ R)%> `^ n) . k = 0. R ) )

proof end;

theorem Th11: :: BASEL_2:11

for L being domRing
for p being non-zero Polynomial of L holds card (Roots p) < len p

proof end;

definition

let L be non empty right_complementable add-associative right_zeroed distributive doubleLoopStr ;
let a be Polynomial of L;

func @ a -> Element of (Polynom-Ring L) equals :: BASEL_2:def 1
a;

coherence
a is Element of (Polynom-Ring L) by POLYNOM3:def 10;

end;

:: deftheorem defines @ BASEL_2:def 1 :
for L being non empty right_complementable add-associative right_zeroed distributive doubleLoopStr
for a being Polynomial of L holds @ a = a;

definition

let L be non empty right_complementable add-associative right_zeroed distributive doubleLoopStr ;
let a be Polynomial of L;
let n be Nat;

func n * a -> Polynomial of L equals :: BASEL_2:def 2
n * (@ a);

coherence
n * (@ a) is Polynomial of L by POLYNOM3:def 10;

end;

:: deftheorem defines * BASEL_2:def 2 :
for L being non empty right_complementable add-associative right_zeroed distributive doubleLoopStr
for a being Polynomial of L
for n being Nat holds n * a = n * (@ a);

Lm1: for n being Nat
for R being commutative Ring
for p, q being Polynomial of R ex F being FinSequence of (Polynom-Ring R) st
( (p + q) `^ n = Sum F & len F = n + 1 & ( for k being Nat st k <= n holds
F . (k + 1) = (n choose k) * ((p `^ k) *' (q `^ (n -' k))) ) )

proof end;

theorem Th12: :: BASEL_2:12

for k, n being Nat
for L being non empty right_complementable add-associative right_zeroed distributive doubleLoopStr
for a being Polynomial of L holds (n * a) . k = n * (a . k)

proof end;

theorem Th13: :: BASEL_2:13

for k, n being Nat
for R being commutative Ring
for z0, z1 being Element of R holds (<%z0,z1%> `^ n) . k = (n choose k) * ((z1 |^ k) * (z0 |^ (n -' k)))

proof end;

definition

let z be Complex;

attr z is imaginary means :Def3: :: BASEL_2:def 3
Re z = 0 ;

end;

:: deftheorem Def3 defines imaginary BASEL_2:def 3 :
for z being Complex holds
( z is imaginary iff Re z = 0 );

registration

cluster <i> -> imaginary ;

coherence
<i> is imaginary by COMPLEX1:7;

cluster complex real imaginary -> zero for object ;

coherence
for b₁ being Complex st b₁ is real & b₁ is imaginary holds
b₁ is zero ;

cluster zero complex -> imaginary for object ;

coherence
for b₁ being Complex st b₁ is zero holds
b₁ is imaginary ;

end;

registration

let z1, z2 be imaginary Complex;

cluster z1 * z2 -> real ;

coherence
z1 * z2 is real

proof end;

cluster z1 + z2 -> imaginary ;

coherence
z1 + z2 is imaginary

proof end;

end;

registration

let z be imaginary Complex;
let r be real Complex;

cluster z * r -> imaginary ;

coherence
z * r is imaginary

proof end;

end;

registration

cluster 0. F_Complex -> real imaginary ;

coherence
( 0. F_Complex is real & 0. F_Complex is imaginary ) by COMPLFLD:7;

end;

registration

cluster complex real left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable imaginary for Element of the carrier of F_Complex;

existence
ex b₁ being Element of F_Complex st
( b₁ is real & b₁ is imaginary )

proof end;

end;

registration

let z be real Element of F_Complex;
let n be Nat;

cluster n * z -> real ;

coherence
n * z is real ;

end;

registration

let z be imaginary Element of F_Complex;
let n be Nat;

cluster n * z -> imaginary ;

coherence
n * z is imaginary ;

end;

registration

let z be imaginary Complex;
let n be even Nat;

cluster (power F_Complex) . (z,n) -> real ;

coherence
(power F_Complex) . (z,n) is real

proof end;

end;

registration

let z be imaginary Complex;
let n be odd Nat;

cluster (power F_Complex) . (z,n) -> imaginary for Complex;

coherence
for b₁ being Complex st b₁ = (power F_Complex) . (z,n) holds
b₁ is imaginary

proof end;

end;

registration

let r be real Element of F_Complex;
let n be Nat;

cluster (power F_Complex) . (r,n) -> real ;

coherence
(power F_Complex) . (r,n) is real

proof end;

end;

registration

cluster zero -> real imaginary for Element of the carrier of F_Complex;

coherence
for b₁ being Element of F_Complex st b₁ is zero holds
( b₁ is imaginary & b₁ is real ) by MATRIX_5:2, STRUCT_0:def 12;

end;

definition

let p be sequence of F_Complex;

attr p is imaginary means :Def4: :: BASEL_2:def 4
for i being Nat holds p . i is imaginary ;

end;

:: deftheorem Def4 defines imaginary BASEL_2:def 4 :
for p being sequence of F_Complex holds
( p is imaginary iff for i being Nat holds p . i is imaginary );

registration

let im1 be imaginary Element of F_Complex;

cluster <%im1%> -> imaginary ;

coherence
<%im1%> is imaginary

proof end;

let im2 be imaginary Element of F_Complex;

cluster <%im1,im2%> -> imaginary ;

coherence
<%im1,im2%> is imaginary

proof end;

end;

registration

cluster V4() V7( NAT ) V8( the carrier of F_Complex) Function-like V32( NAT , the carrier of F_Complex) complex-valued finite-Support imaginary for Element of K21(K22(NAT, the carrier of F_Complex));

existence
ex b₁ being Polynomial of F_Complex st b₁ is imaginary

proof end;

end;

theorem Th14: :: BASEL_2:14

for I being imaginary Polynomial of F_Complex
for r being real Element of F_Complex holds eval (I,r) is imaginary

proof end;

theorem Th15: :: BASEL_2:15

for R being real Polynomial of F_Complex
for r being real Element of F_Complex holds eval (R,r) is real

proof end;

theorem :: BASEL_2:16

for n being Nat
for im being imaginary Element of F_Complex
for r being real Element of F_Complex st n is even holds
( even_part (<%im,r%> `^ n) is real & odd_part (<%im,r%> `^ n) is imaginary )

proof end;

theorem Th17: :: BASEL_2:17

for n being Nat
for im being imaginary Element of F_Complex
for r being real Element of F_Complex st n is odd holds
( even_part (<%im,r%> `^ n) is imaginary & odd_part (<%im,r%> `^ n) is real )

proof end;

theorem Th18: :: BASEL_2:18

for L being non empty ZeroStr
for p being Polynomial of L st len (even_part p) <> 0 holds
len (even_part p) is odd

proof end;

definition

let L be non empty set ;
let p be sequence of L;
let m be Nat;

func sieve (p,m) -> sequence of L means :Def5: :: BASEL_2:def 5
for i being Nat holds it . i = p . (m * i);

existence
ex b₁ being sequence of L st
for i being Nat holds b₁ . i = p . (m * i)

proof end;

uniqueness
for b₁, b₂ being sequence of L st ( for i being Nat holds b₁ . i = p . (m * i) ) & ( for i being Nat holds b₂ . i = p . (m * i) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines sieve BASEL_2:def 5 :
for L being non empty set
for p being sequence of L
for m being Nat
for b₄ being sequence of L holds
( b₄ = sieve (p,m) iff for i being Nat holds b₄ . i = p . (m * i) );

registration

let L be non empty ZeroStr ;
let p be finite-Support sequence of L;
let m be non zero Nat;

cluster sieve (p,m) -> finite-Support ;

coherence
sieve (p,m) is finite-Support

proof end;

end;

theorem Th19: :: BASEL_2:19

for k being Nat
for L being non empty ZeroStr
for p being sequence of L holds sieve (p,(2 * k)) = sieve ((even_part p),(2 * k))

proof end;

theorem Th20: :: BASEL_2:20

for L being non empty ZeroStr
for p being Polynomial of L st len (even_part p) is odd holds
2 * (len (sieve (p,2))) = (len (even_part p)) + 1

proof end;

theorem Th21: :: BASEL_2:21

for L being non empty ZeroStr
for p being Polynomial of L st len (even_part p) = 0 holds
for n being non zero Nat holds len (sieve (p,(2 * n))) = 0

proof end;

theorem Th22: :: BASEL_2:22

for L being Field
for p being Polynomial of L holds even_part p = Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>)

proof end;

set PP = <%i_FC,(1. F_Complex)%>;

theorem Th23: :: BASEL_2:23

for n being Nat holds (sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1)),2)) . n = (((2 * n) + 1) choose 1) * i_FC

proof end;

theorem Th24: :: BASEL_2:24

for n being Nat st n >= 1 holds
(sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1)),2)) . (n - 1) = (((2 * n) + 1) choose 3) * (- i_FC)

proof end;

theorem Th25: :: BASEL_2:25

for n being Nat holds len (sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1)),2)) = n + 1

proof end;

registration

let n be Nat;

cluster sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1)),2) -> non-zero ;

coherence
sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1)),2) is non-zero

proof end;

end;

theorem Th26: :: BASEL_2:26

for n being Nat holds rng (sqr (cot (x_r-seq n))) c= Roots (sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1)),2))

proof end;

theorem Th27: :: BASEL_2:27

for n being Nat holds Roots (sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1)),2)) = rng (sqr (cot (x_r-seq n)))

proof end;

theorem Th28: :: BASEL_2:28

for m being Nat holds Sum (sqr (cot (x_r-seq m))) = ((2 * m) * ((2 * m) - 1)) / 6

proof end;

theorem Th29: :: BASEL_2:29

for m being Nat holds Sum (sqr (cosec (x_r-seq m))) = ((2 * m) * ((2 * m) + 2)) / 6

proof end;

theorem Th30: :: BASEL_2:30

for m being Nat holds Basel-seq1 . m <= Sum (Basel-seq,m)

proof end;

theorem Th31: :: BASEL_2:31

for m being Nat holds Sum (Basel-seq,m) <= Basel-seq2 . m

proof end;

:: Basel problem

theorem Th32: :: BASEL_2:32

Sum Basel-seq = (PI ^2) / 6

proof end;

registration

cluster Partial_Sums Basel-seq -> non summable for Real_Sequence;

coherence
for b₁ being Real_Sequence st b₁ = Partial_Sums Basel-seq holds
not b₁ is summable by Th32, SERIES_1:4;

end;