:: 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 b1 being Complex st b1 is real & b1 is imaginary holds
b1 is zero ;
cluster zero complex -> imaginary for object ;
coherence
for b1 being Complex st b1 is zero holds
b1 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 b1 being Element of F_Complex st
( b1 is real & b1 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 b1 being Complex st b1 = (power F_Complex) . (z,n) holds
b1 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 b1 being Element of F_Complex st b1 is zero holds
( b1 is imaginary & b1 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 b1 being Polynomial of F_Complex st b1 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 b1 being sequence of L st
for i being Nat holds b1 . i = p . (m * i)
proof end;
uniqueness
for b1, b2 being sequence of L st ( for i being Nat holds b1 . i = p . (m * i) ) & ( for i being Nat holds b2 . i = p . (m * i) ) holds
b1 = b2
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 b4 being sequence of L holds
( b4 = sieve (p,m) iff for i being Nat holds b4 . 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;

:: WP: 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 b1 being Real_Sequence st b1 = Partial_Sums Basel-seq holds
not b1 is summable by Th32, SERIES_1:4;
end;