:: by Karol P\kak and Artur Korni{\l}owicz

::

:: Received June 27, 2017

:: Copyright (c) 2017-2018 Association of Mizar Users

set FC = F_Complex ;

registration

let L be non empty right_zeroed doubleLoopStr ;

let n be Nat;

reducibility

n * (0. L) = 0. L

end;
let n be Nat;

reducibility

n * (0. L) = 0. L

proof end;

registration

let e be Element of F_Complex;

let z be Complex;

let n be Nat;

correctness

compatibility

( e = z implies n * e = n * z );

by Th1;

end;
let z be Complex;

let n be Nat;

correctness

compatibility

( e = z implies n * e = n * z );

by Th1;

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

for E being FinSequence of F_Complex st E = Z holds

Sum Z = Sum E

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%>

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

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

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

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

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

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;

definition

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

let a be Polynomial of L;

coherence

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

end;
let a be Polynomial of L;

coherence

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

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

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;

coherence

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

end;
let a be Polynomial of L;

let n be Nat;

coherence

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

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

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)

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

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;

:: deftheorem Def3 defines imaginary BASEL_2:def 3 :

for z being Complex holds

( z is imaginary iff Re z = 0 );

for z being Complex holds

( z is imaginary iff Re z = 0 );

registration

coherence

<i> is imaginary by COMPLEX1:7;

coherence

for b_{1} being Complex st b_{1} is real & b_{1} is imaginary holds

b_{1} is zero
;

coherence

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

b_{1} is imaginary
;

end;
<i> is imaginary by COMPLEX1:7;

coherence

for b

b

coherence

for b

b

registration

let z1, z2 be imaginary Complex;

coherence

z1 * z2 is real

z1 + z2 is imaginary

end;
coherence

z1 * z2 is real

proof end;

coherence z1 + z2 is imaginary

proof end;

registration
end;

registration

ex b_{1} being Element of F_Complex st

( b_{1} is real & b_{1} is imaginary )
end;

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

existence ex b

( b

proof end;

registration
end;

registration
end;

registration

let z be imaginary Complex;

let n be even Nat;

coherence

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

end;
let n be even Nat;

coherence

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

proof end;

registration

let z be imaginary Complex;

let n be odd Nat;

coherence

for b_{1} being Complex st b_{1} = (power F_Complex) . (z,n) holds

b_{1} is imaginary

end;
let n be odd Nat;

coherence

for b

b

proof end;

registration

let r be real Element of F_Complex;

let n be Nat;

coherence

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

end;
let n be Nat;

coherence

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

proof end;

registration

coherence

for b_{1} being Element of F_Complex st b_{1} is zero holds

( b_{1} is imaginary & b_{1} is real )
by MATRIX_5:2, STRUCT_0:def 12;

end;
for b

( b

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

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;

coherence

<%im1%> is imaginary

coherence

<%im1,im2%> is imaginary

end;
coherence

<%im1%> is imaginary

proof end;

let im2 be imaginary Element of F_Complex;coherence

<%im1,im2%> is imaginary

proof end;

registration

ex b_{1} being Polynomial of F_Complex st b_{1} is imaginary
end;

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 Polynomial of ;

existence ex b

proof 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

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

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 )

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 )

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

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;

ex b_{1} being sequence of L st

for i being Nat holds b_{1} . i = p . (m * i)

for b_{1}, b_{2} being sequence of L st ( for i being Nat holds b_{1} . i = p . (m * i) ) & ( for i being Nat holds b_{2} . i = p . (m * i) ) holds

b_{1} = b_{2}

end;
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 for i being Nat holds it . i = p . (m * i);

ex b

for i being Nat holds b

proof end;

uniqueness for b

b

proof 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_{4} being sequence of L holds

( b_{4} = sieve (p,m) iff for i being Nat holds b_{4} . i = p . (m * i) );

for L being non empty set

for p being sequence of L

for m being Nat

for b

( b

registration

let L be non empty ZeroStr ;

let p be finite-Support sequence of L;

let m be non zero Nat;

coherence

sieve (p,m) is finite-Support

end;
let p be finite-Support sequence of L;

let m be non zero Nat;

coherence

sieve (p,m) is finite-Support

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

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

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

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

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)

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

proof end;

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

:: Basel problem

registration

coherence

for b_{1} being Real_Sequence st b_{1} = Partial_Sums Basel-seq holds

not b_{1} is summable
by Th32, SERIES_1:4;

end;
for b

not b