basel_2.miz

begin

 reserve k,m,n for Nat;

 reserve R for commutative Ring,

p,q for Polynomial of R,

z0,z1 for Element of R;

 set FC = F_Complex ;

 registration

 let L be right_zeroed non empty doubleLoopStr;

 let n;

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

 reducibility

 proof

 defpred P[ Nat] means ($1 * ( 0. L)) = ( 0. L);



 A1: P[ 0 ] by BINOM: 12;



 A2: for i be Nat st P[i] holds P[(i + 1)]

 proof

 let i be Nat such that

 A3: P[i];



 thus ((i + 1) * ( 0. L)) = (( 0. L) + (i * ( 0. L))) by BINOM:def 3

 .= ( 0. L) by A3, RLVECT_1:def 4;

 end;

 for i be Nat holds P[i] from NAT_1:sch 2( A1, A2);

 hence thesis;

 end;

 end

 theorem :: BASEL_2:1



 Th1: for z be Complex, e be Element of F_Complex st z = e holds (n * z) = (n * e)

 proof

 let z be Complex, e be Element of F_Complex such that

 A1: z = e;

 defpred P[ Nat] means ($1 * z) = ($1 * e);



 A2: P[ 0 ] by COMPLFLD: 7, BINOM: 12;



 A3: for i be Nat st P[i] holds P[(i + 1)]

 proof

 let i be Nat such that

 A4: P[i];

 ((i + 1) * e) = (e + (i * e)) by BINOM:def 3

 .= (z + (i * z)) by A1, A4;

 hence thesis;

 end;

 for i be Nat holds P[i] from NAT_1:sch 2( A2, A3);

 hence thesis;

 end;

 registration

 let e be Element of F_Complex , z be Complex;

 let n;

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

 correctness by Th1;

 end

 theorem :: BASEL_2:2



 Th2: for Z be complex-valued FinSequence, E be FinSequence of F_Complex st E = Z holds ( Sum Z) = ( Sum E)

 proof

 let Z be complex-valued FinSequence, E be FinSequence of FC such that

 A1: E = Z;

 consider f be sequence of FC such that

 A2: ( Sum E) = (f . ( len E)) & (f . 0 ) = ( 0. FC) and

 A3: for j be Nat, v be Element of FC st j < ( len E) & v = (E . (j + 1)) holds (f . (j + 1)) = ((f . j) + v) by RLVECT_1:def 12;

 reconsider E1 = E as FinSequence of FC;

 defpred P[ Nat] means $1 <= ( len Z) implies ( Sum (Z | $1)) = (f . $1);



 A4: P[ 0 ] by A2, RVSUM_2: 29, COMPLFLD: 7;



 A5: P[n] implies P[(n + 1)]

 proof

 set n1 = (n + 1);

 assume

 A6: P[n] & n1 <= ( len Z);



 A7: n1 in ( dom Z) by A6, NAT_1: 11, FINSEQ_3: 25;

 then

 A8: (Z | n1) = ((Z | n) ^ <*(Z . n1)*>) by FINSEQ_5: 10;

 (E1 . n1) in ( rng E1) & ( rng E1) c= the carrier of FC by A7, A1, FUNCT_1:def 3;

 then

 reconsider E1n1 = (E1 . n1) as Element of FC;

 (f . n1) = ((f . n) + E1n1) by A1, A3, A6, NAT_1: 13;

 hence thesis by A8, A1, NAT_1: 13, A6, RVSUM_2: 31;

 end;

 P[n] from NAT_1:sch 2( A4, A5);

 then P[( len Z)] & (Z | ( len Z)) = Z;

 hence thesis by A2, A1;

 end;

 theorem :: BASEL_2:3



 Th3: (( 1_ F_Complex ) |^ n) = ( 1_ F_Complex )

 proof



 thus (( 1_ FC) |^ n) = ( 1r |^ n) by COMPLFLD: 8, COMPLFLD: 74

 .= ( 1_ FC) by COMPLFLD: 8, COMPLEX1:def 4;

 end;

 theorem :: BASEL_2:4



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

 proof

 let L be left_zeroed right_zeroed non empty addLoopStr;

 let z0,z1 be Element of L;

 let n be Element of NAT ;



 A1: (( <%z0%> + <%( 0. L), z1%>) . n) = (( <%z0%> . n) + ( <%( 0. L), z1%> . n)) by NORMSP_1:def 2;

 per cases by NAT_1: 23;

 suppose

 A2: n = 0 ;

 then ( <%z0%> . n) = z0 & ( <%( 0. L), z1%> . n) = ( 0. L) by POLYNOM5: 32, POLYNOM5: 38;

 then (( <%z0%> + <%( 0. L), z1%>) . n) = z0 by A1, RLVECT_1:def 4;

 hence thesis by A2, POLYNOM5: 38;

 end;

 suppose

 A3: n = 1;

 then ( <%z0%> . n) = ( 0. L) & ( <%( 0. L), z1%> . n) = z1 by POLYNOM5: 32, POLYNOM5: 38;

 then (( <%z0%> + <%( 0. L), z1%>) . n) = z1 by A1, ALGSTR_1:def 2;

 hence thesis by A3, POLYNOM5: 38;

 end;

 suppose

 A4: n >= 2;

 then ( <%z0%> . n) = ( 0. L) & ( <%( 0. L), z1%> . n) = ( 0. L) by XXREAL_0: 2, POLYNOM5: 32, POLYNOM5: 38;

 then (( <%z0%> + <%( 0. L), z1%>) . n) = ( 0. L) by A1, ALGSTR_1:def 2;

 hence thesis by A4, POLYNOM5: 38;

 end;

 end;

 theorem :: BASEL_2:5



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

 proof

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

 let a,b,c,d be Element of L;

 let n be Element of NAT ;



 A1: ( <%c, d%> . 0 ) = c by POLYNOM5: 38;



 A2: ( <%c, d%> . 1) = d by POLYNOM5: 38;

 (n = 0 or ... or n = 2) or n > 2;

 per cases ;

 suppose

 A3: n = 0 ;



 hence (( <%a, b%> *' <%c, d%>) . n) = (a * ( <%c, d%> . 0 )) by UPROOTS: 37

 .= ( <%(a * c), ((a * d) + (b * c)), (b * d)%> . n) by A1, A3, NIVEN: 23;

 end;

 suppose

 A4: n = 1;



 hence (( <%a, b%> *' <%c, d%>) . n) = ((a * ( <%c, d%> . ( 0 + 1))) + (b * ( <%c, d%> . 0 ))) by UPROOTS: 37

 .= ( <%(a * c), ((a * d) + (b * c)), (b * d)%> . n) by A1, A2, A4, NIVEN: 24;

 end;

 suppose

 A5: n = 2;

 ( <%c, d%> . 2) = ( 0. L) by POLYNOM5: 38;



 hence ( <%(a * c), ((a * d) + (b * c)), (b * d)%> . n) = ((a * ( <%c, d%> . (1 + 1))) + (b * ( <%c, d%> . 1))) by A2, A5, NIVEN: 25

 .= (( <%a, b%> *' <%c, d%>) . n) by A5, UPROOTS: 37;

 end;

 suppose

 A6: n > 2;

 then

 A7: n >= (2 + 1) by NAT_1: 13;

 consider k be Nat such that

 A8: n = (k + 1) by A6, NAT_1: 6;



 A9: ( len <%c, d%>) <= 2 by POLYNOM5: 39;

 ((k + 1) - 1) >= (3 - 1) by A6, A8, NAT_1: 13;

 then ( <%c, d%> . (k + 1)) = ( 0. L) & ( <%c, d%> . k) = ( 0. L) by A6, A8, A9, XXREAL_0: 2, ALGSEQ_1: 8;



 hence ( <%(a * c), ((a * d) + (b * c)), (b * d)%> . n) = ((a * ( <%c, d%> . (k + 1))) + (b * ( <%c, d%> . k))) by A7, NIVEN: 26

 .= (( <%a, b%> *' <%c, d%>) . n) by A8, UPROOTS: 37;

 end;

 end;

 theorem :: BASEL_2:6



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

 proof

 let L be Abelian add-associative right_zeroed right_complementable well-unital commutative distributive non empty doubleLoopStr;



 thus <%( 0. L), ( 0. L), ( 1. L)%> = <%(( 0. L) * ( 0. L)), ((( 0. L) * ( 1. L)) + (( 1. L) * ( 0. L))), (( 1. L) * ( 1. L))%>

 .= ( <%( 0. L), ( 1. L)%> *' <%( 0. L), ( 1. L)%>) by Th5

 .= ( <%( 0. L), ( 1. L)%> `^ 2) by POLYNOM5: 17;

 end;

 theorem :: BASEL_2:7



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

 proof

 let L be right_zeroed add-associative right_complementable right-distributive non empty doubleLoopStr, z be Element of L, p be Polynomial of L;

 set Z = <%z%>;

 n in NAT by ORDINAL1:def 12;

 then

 consider r be FinSequence of the carrier of L such that

 A1: ( len r) = (n + 1) and

 A2: ((p *' <%z%>) . n) = ( Sum r) and

 A3: for k be Element of NAT st k in ( dom r) holds (r . k) = ((p . (k -' 1)) * (Z . ((n + 1) -' k))) by POLYNOM3:def 9;

 set l = ( len r);



 A4: 1 <= l by A1, NAT_1: 11;

 then

 A5: l in ( dom r) & (l -' 1) = (l - 1) & ((n + 1) -' l) = 0 by A1, FINSEQ_3: 25, XREAL_1: 233, XREAL_1: 232;

 then

 A6: (r . l) = ((p . n) * (Z . ((n + 1) -' l))) & (Z . ((n + 1) -' l)) = z by A1, A3, POLYNOM5: 32;

 for k be Element of NAT st k in ( dom r) & k <> l holds (r /. k) = ( 0. L)

 proof

 let k be Element of NAT such that

 A7: k in ( dom r) & k <> l;



 A8: (r /. k) = (r . k) by PARTFUN1:def 6, A7;

 k <= l by A7, FINSEQ_3: 25;

 then (l -' k) = (l - k) by XREAL_1: 233;

 then (l -' k) <> 0 by A7;

 then (Z . (l -' k)) = ( 0. L) by NAT_1: 14, POLYNOM5: 32;

 then ((p . (k -' 1)) * (Z . (l -' k))) = ( 0. L);

 hence thesis by A1, A8, A7, A3;

 end;

 then ( Sum r) = (r /. l) by A4, FINSEQ_3: 25, POLYNOM2: 3;

 hence thesis by A6, A2, A5, PARTFUN1:def 6;

 end;

 theorem :: BASEL_2:8



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

 proof

 let L be Abelian add-associative right_zeroed right_complementable well-unital associative commutative distributive non empty doubleLoopStr;

 let x be Element of L;

 set X = <%x%>;

 defpred P[ Nat] means (X `^ $1) = <%(x |^ $1)%>;



 A1: P[ 0 ]

 proof



 A2: <%(x |^ 0 )%> = <%( 1_ L)%> by BINOM: 8;

 ( 1_. L) = <%( 1_ L)%>

 proof

 let n be Element of NAT ;

 per cases by NAT_1: 14;

 suppose n = 0 ;

 then ( <%( 1_ L)%> . n) = ( 1_ L) & (( 1_. L) . n) = ( 1. L) by POLYNOM5: 32, POLYNOM3: 30;

 hence thesis;

 end;

 suppose n >= 1;

 then ( <%( 1_ L)%> . n) = ( 0. L) & (( 1_. L) . n) = ( 0. L) by POLYNOM5: 32, POLYNOM3: 30;

 hence thesis;

 end;

 end;

 hence thesis by POLYNOM5: 15, A2;

 end;



 A3: for n holds P[n] implies P[(n + 1)]

 proof

 let n;

 set n1 = (n + 1);

 assume

 A4: P[n];



 A5: (X `^ n1) = ((X `^ n) *' X) by POLYNOM5: 19;

 let k be Element of NAT ;

 per cases by NAT_1: 14;

 suppose k = 0 ;

 then

 A6: ((X `^ n) . k) = (x |^ n) & ( <%(x |^ n1)%> . k) = (x |^ n1) & (x |^ 1) = x by A4, POLYNOM5: 32, BINOM: 8;

 then ((X `^ n1) . k) = ((x |^ n) * (x |^ 1)) by A5, Th7;

 hence thesis by A6, BINOM: 10;

 end;

 suppose

 A7: k >= 1;

 then ((X `^ n) . k) = ( 0. L) by A4, POLYNOM5: 32;

 then ((X `^ n1) . k) = (( 0. L) * x) by A5, Th7;

 hence thesis by A7, POLYNOM5: 32;

 end;

 end;

 for n holds P[n] from NAT_1:sch 2( A1, A3);

 hence thesis;

 end;

 theorem :: BASEL_2:9



 Th9: (( <%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

 ( <%z0, z1%> `^ 0 ) = ( 1_. R) by POLYNOM5: 15;

 hence (( <%z0, z1%> `^ 0 ) . 0 ) = ( 1. R) by POLYNOM3: 30;

 set P = <%( 0. R), z1%>;

 defpred P[ Nat] means ($1 > 0 implies ((P `^ $1) . $1) = (z1 |^ $1)) & for k st k <> $1 holds ((P `^ $1) . k) = ( 0. R);



 A1: P[ 0 ]

 proof

 thus 0 > 0 implies (( <%( 0. R), z1%> `^ 0 ) . 0 ) = (z1 |^ 0 );

 let k;

 assume

 A2: k <> 0 ;

 (P `^ 0 ) = ( 1_. R) by POLYNOM5: 15;

 hence thesis by A2, POLYNOM3: 30;

 end;



 A3: for i be Nat st P[i] holds P[(i + 1)]

 proof

 let i be Nat;

 set i1 = (i + 1);

 assume

 A4: P[i];



 A5: (P `^ i1) = ((P `^ i) *' P) by POLYNOM5: 19;

 thus (i + 1) > 0 implies ((P `^ i1) . i1) = (z1 |^ i1)

 proof

 assume (i + 1) > 0 ;

 per cases ;

 suppose

 A6: i = 0 ;

 then (P `^ i1) = P by POLYNOM5: 16;



 hence ((P `^ i1) . i1) = z1 by A6, POLYNOM5: 38

 .= (z1 |^ i1) by A6, BINOM: 8;

 end;

 suppose

 A7: i > 0 ;

 consider r be FinSequence of the carrier of R such that

 A8: ( len r) = (i1 + 1) & ((P `^ i1) . i1) = ( Sum r) and

 A9: for k be Element of NAT st k in ( dom r) holds (r . k) = (((P `^ i) . (k -' 1)) * (P . ((i1 + 1) -' k))) by A5, POLYNOM3:def 9;



 A10: 1 <= i1 & i1 <= ( len r) by A8, NAT_1: 11;

 then

 A11: i1 in ( dom r) by FINSEQ_3: 25;

 for k be Element of NAT st k in ( dom r) & k <> i1 holds (r /. k) = ( 0. R)

 proof

 let k be Element of NAT such that

 A12: k in ( dom r) & k <> i1;



 A13: k <= (i1 + 1) by A8, A12, FINSEQ_3: 25;



 A14: (r /. k) = (r . k) by PARTFUN1:def 6, A12;

 per cases by A12, XXREAL_0: 1;

 suppose k > i1;

 then k >= (i1 + 1) by NAT_1: 13;

 then k = (i1 + 1) by A13, XXREAL_0: 1;

 then ((i1 + 1) -' k) = 0 by XREAL_1: 232;

 then (P . ((i1 + 1) -' k)) = ( 0. R) by POLYNOM5: 38;

 then (((P `^ i) . (k -' 1)) * (P . ((i1 + 1) -' k))) = ( 0. R);

 hence thesis by A14, A12, A9;

 end;

 suppose

 A15: k < i1;

 then k < (i1 + 1) by NAT_1: 13;

 then

 A16: ((i1 + 1) -' k) = ((i1 + 1) - k) by XREAL_1: 233;

 k <= i by A15, NAT_1: 13;

 then (i - k) >= 0 by XREAL_1: 48;

 then ((i - k) + 2) >= ( 0 + 2) by XREAL_1: 6;

 then (P . ((i1 + 1) -' k)) = ( 0. R) by A16, POLYNOM5: 38;

 then (((P `^ i) . (k -' 1)) * (P . ((i1 + 1) -' k))) = ( 0. R);

 hence thesis by A14, A12, A9;

 end;

 end;

 then

 A17: ( Sum r) = (r /. i1) by A10, FINSEQ_3: 25, POLYNOM2: 3;

 (i1 -' 1) = (i1 - 1) & ((i1 + 1) -' i1) = ((i1 + 1) - i1) by NAT_1: 11, XREAL_1: 233;

 then ((P `^ i) . (i1 -' 1)) = (z1 |^ i) & (P . ((i1 + 1) -' i1)) = z1 by A7, A4, POLYNOM5: 38;

 then (r . i1) = ((z1 |^ i) * z1) & z1 = (z1 |^ 1) by A9, A10, FINSEQ_3: 25, BINOM: 8;

 then (r . i1) = (z1 |^ i1) by BINOM: 10;

 hence thesis by A17, A8, A11, PARTFUN1:def 6;

 end;

 end;

 let j be Nat such that

 A18: j <> i1;

 set j1 = (j + 1);

 j in NAT by ORDINAL1:def 12;

 then

 consider r be FinSequence of the carrier of R such that

 A19: ( len r) = (j + 1) & ((P `^ i1) . j) = ( Sum r) and

 A20: for k be Element of NAT st k in ( dom r) holds (r . k) = (((P `^ i) . (k -' 1)) * (P . (j1 -' k))) by A5, POLYNOM3:def 9;

 for k be Element of NAT st k in ( dom r) holds (r . k) = ( 0. R)

 proof

 let k be Element of NAT such that

 A21: k in ( dom r);



 A22: 1 <= k <= j1 by A19, A21, FINSEQ_3: 25;

 per cases by XXREAL_0: 1;

 suppose k = j;

 then (k -' 1) = (j - 1) by A22, XREAL_1: 233;

 then (k -' 1) <> i by A18;

 then ((P `^ i) . (k -' 1)) = ( 0. R) by A4;

 then (((P `^ i) . (k -' 1)) * (P . ((j + 1) -' k))) = ( 0. R);

 hence thesis by A21, A20;

 end;

 suppose k > j;

 then k >= (j + 1) by NAT_1: 13;

 then k = (j + 1) by A22, XXREAL_0: 1;

 then ((j + 1) -' k) = 0 by XREAL_1: 232;

 then (P . ((j + 1) -' k)) = ( 0. R) by POLYNOM5: 38;

 then (((P `^ i) . (k -' 1)) * (P . ((j + 1) -' k))) = ( 0. R);

 hence thesis by A21, A20;

 end;

 suppose

 A23: k < j;

 then k < (j + 1) by NAT_1: 13;

 then

 A24: ((j + 1) -' k) = ((j + 1) - k) by XREAL_1: 233;

 (j - k) > 0 by A23, XREAL_1: 50;

 then ((j - k) + 1) > ( 0 + 1) by XREAL_1: 6;

 then ((j + 1) -' k) >= (1 + 1) by NAT_1: 13, A24;

 then (P . ((j + 1) -' k)) = ( 0. R) by POLYNOM5: 38;

 then (((P `^ i) . (k -' 1)) * (P . ((j + 1) -' k))) = ( 0. R);

 hence thesis by A21, A20;

 end;

 end;

 hence thesis by A19, POLYNOM3: 1;

 end;

 for i be Nat holds P[i] from NAT_1:sch 2( A1, A3);

 hence thesis;

 end;

 theorem :: BASEL_2:10



 Th10: (( <%( 0. R), ( 0. R), ( 1_ R)%> `^ n) . (2 * n)) = ( 1_ R) & for k st k <> (2 * n) holds (( <%( 0. R), ( 0. R), ( 1_ R)%> `^ n) . k) = ( 0. R)

 proof

 set x1 = <%( 0. R), ( 1_ R)%>;

 set x2 = <%( 0. R), ( 0. R), ( 1_ R)%>;

 set 2n = (2 * n);

 defpred P[ Nat] means (x2 `^ $1) = (x1 `^ (2 * $1));

 (x2 `^ 0 ) = ( 1_. R) = (x1 `^ 0 ) by POLYNOM5: 15;

 then

 A1: P[ 0 ];



 A2: P[k] implies P[(k + 1)]

 proof



 A3: x2 = (x1 `^ 2) by Th6

 .= (x1 *' x1) by POLYNOM5: 17;

 assume P[k];



 hence (x2 `^ (k + 1)) = ((x1 `^ (2 * k)) *' x2) by POLYNOM5: 19

 .= (((x1 `^ (2 * k)) *' x1) *' x1) by A3, POLYNOM3: 33

 .= ((x1 `^ ((2 * k) + 1)) *' x1) by POLYNOM5: 19

 .= (x1 `^ (((2 * k) + 1) + 1)) by POLYNOM5: 19

 .= (x1 `^ (2 * (k + 1)));

 end;

 P[k] from NAT_1:sch 2( A1, A2);

 then

 A4: (x2 `^ n) = (x1 `^ (2 * n));

 defpred Q[ Nat] means (( 1_ R) |^ $1) = ( 1_ R);



 A5: Q[ 0 ] by BINOM: 8;



 A6: Q[k] implies Q[(k + 1)]

 proof

 assume Q[k];



 hence (( 1_ R) |^ (k + 1)) = (( 1_ R) * ( 1_ R)) by GROUP_1:def 7

 .= ( 1_ R);

 end;

 Q[k] from NAT_1:sch 2( A5, A6);

 then

 A7: Q[2n];

 n = 0 or n > 0 ;

 hence ((x2 `^ n) . 2n) = ( 1_ R) by A4, Th9, A7;

 let k;

 thus k <> (2 * n) implies ((x2 `^ n) . k) = ( 0. R) by A4, Th9;

 end;

 theorem :: BASEL_2:11



 Th11: for L be domRing, p be non-zero Polynomial of L holds ( card ( Roots p)) < ( len p)

 proof

 let L be domRing, p be non-zero Polynomial of L;

 defpred P[ Nat] means for p be non-zero Polynomial of L st ( len p) = $1 holds ( card ( Roots p)) < ( len p);



 A1: P[1] by UPROOTS: 46, CARD_1: 27;



 A2: for n be Nat st n >= 1 & P[n] holds P[(n + 1)]

 proof

 let n be Nat such that n >= 1 and

 A3: P[n];

 let p be non-zero Polynomial of L;

 assume

 A4: ( len p) = (n + 1);

 per cases ;

 suppose p is with_roots;

 then

 consider x be Element of L such that

 A5: x is_a_root_of p by POLYNOM5:def 8;

 set r = <%( - x), ( 1. L)%>, pq = ( poly_quotient (p,x));

 ( len pq) > 0 by A5, UPROOTS: 47;

 then pq <> ( 0_. L) by POLYNOM4: 3;

 then

 reconsider pq as non-zero Polynomial of L by UPROOTS:def 5;

 set Rr = ( Roots r), Rpq = ( Roots pq);

 p = ( <%( - x), ( 1. L)%> *' ( poly_quotient (p,x))) by A5, UPROOTS: 50;

 then

 A6: ( Roots p) = (Rr \/ Rpq) by UPROOTS: 23;



 A7: Rr = {x} by UPROOTS: 48;



 A8: (( len pq) + 1) = ( len p) by A4, A5, UPROOTS:def 7;

 ( card Rr) = 1 by A7, CARD_1: 30;

 then

 A9: ( card (Rr \/ Rpq)) <= (( card Rpq) + 1) by CARD_2: 43;

 (( card Rpq) + 1) < (n + 1) by A8, A3, A4, XREAL_1: 8;

 hence thesis by A4, A6, A9, XXREAL_0: 2;

 end;

 suppose

 A10: not p is with_roots;

 now

 assume ( Roots p) <> {} ;

 then

 consider x be object such that

 A11: x in ( Roots p) by XBOOLE_0:def 1;

 reconsider x as Element of L by A11;

 x is_a_root_of p by A11, POLYNOM5:def 10;

 hence contradiction by A10, POLYNOM5:def 8;

 end;

 hence thesis by A4;

 end;

 end;

 p <> ( 0_. L) by UPROOTS:def 5;

 then

 A12: ( len p) >= 1 by NAT_1: 14, POLYNOM4: 5;

 for n be Nat st n >= 1 holds P[n] from NAT_1:sch 8( A1, A2);

 hence thesis by A12;

 end;

 definition

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

 :: BASEL_2:def1

 func @ a -> Element of ( Polynom-Ring L) equals a;

 coherence by POLYNOM3:def 10;

 end

 definition

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

 let n be Nat;

 :: BASEL_2:def2

 func n * a -> Polynomial of L equals (n * ( @ a));

 coherence by POLYNOM3:def 10;

 end



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

 proof

 let p, q;



 A1: n in NAT by ORDINAL1:def 12;

 take F = ((( @ q),( @ p)) In_Power n);

 ((p + q) `^ n) = ((( @ p) + ( @ q)) |^ n) by POLYNOM3:def 10;

 hence

 A2: ((p + q) `^ n) = ( Sum F) & ( len F) = (n + 1) by A1, BINOM: 25, BINOM:def 7;

 let k be Nat such that

 A3: k <= n;

 set k1 = (k + 1);

 1 <= k1 <= ( len F) by A2, A3, NAT_1: 11, XREAL_1: 6;

 then

 A4: k1 in ( dom F) by FINSEQ_3: 25;

 then

 A5: (F /. k1) = (F . k1) by PARTFUN1:def 6;



 A6: (k1 - 1) = k;



 A7: ((( @ q) |^ (n -' k)) * (( @ p) |^ k)) = ( @ ((p `^ k) *' (q `^ (n -' k)))) by POLYNOM3:def 10;

 (n -' k) = (n - k) by A3, XREAL_1: 233;



 hence (F . k1) = (((n choose k) * (( @ q) |^ (n -' k))) * (( @ p) |^ k)) by A4, A6, A5, BINOM:def 7

 .= ((n choose k) * ((p `^ k) *' (q `^ (n -' k)))) by A7, BINOM: 19;

 end;

 theorem :: BASEL_2:12



 Th12: for L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr holds for a be Polynomial of L holds ((n * a) . k) = (n * (a . k))

 proof

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

 set PRR = ( Polynom-Ring L);

 defpred P[ Nat] means (($1 * a) . k) = ($1 * (a . k));

 ( 0 * a) = ( 0. PRR) by BINOM: 12

 .= ( 0_. L) by POLYNOM3:def 10;



 then (( 0 * a) . k) = ( 0. L) by ORDINAL1:def 12, FUNCOP_1: 7

 .= ( 0 * (a . k)) by BINOM: 12;

 then

 A1: P[ 0 ];



 A2: for i be Nat st P[i] holds P[(i + 1)]

 proof

 let i be Nat such that

 A3: P[i];

 ((i + 1) * a) = (( @ a) + (i * ( @ a))) by BINOM:def 3

 .= (a + (i * a)) by POLYNOM3:def 10;



 hence (((i + 1) * a) . k) = ((a . k) + ((i * a) . k)) by NORMSP_1:def 2

 .= ((i + 1) * (a . k)) by A3, BINOM:def 3;

 end;

 for i be Nat holds P[i] from NAT_1:sch 2( A1, A2);

 hence thesis;

 end;

 theorem :: BASEL_2:13



 Th13: (( <%z0, z1%> `^ n) . k) = ((n choose k) * ((z1 |^ k) * (z0 |^ (n -' k))))

 proof

 set Z0 = <%z0%>, Z1 = <%( 0. R), z1%>, C = ((n choose k) * ((z1 |^ k) * (z0 |^ (n -' k))));

 set PRR = ( Polynom-Ring R);

 <%z0, z1%> = (Z0 + Z1) by Th4;

 then

 consider F be FinSequence of ( Polynom-Ring R) such that

 A1: ( <%z0, z1%> `^ n) = ( Sum F) and

 A2: ( len F) = (n + 1) and

 A3: for k be Nat st k <= n holds (F . (k + 1)) = ((n choose k) * ((Z1 `^ k) *' (Z0 `^ (n -' k)))) by Lm1;



 A4: for i be Nat st i <= n holds for Fi1 be Polynomial of R st Fi1 = (F . (i + 1)) holds (k <> i implies (Fi1 . k) = ( 0. R)) & (k = i implies (Fi1 . k) = C)

 proof

 let i be Nat such that

 A5: i <= n;

 let Fi1 be Polynomial of R such that

 A6: Fi1 = (F . (i + 1));

 Fi1 = ((n choose i) * ((Z1 `^ i) *' (Z0 `^ (n -' i)))) by A5, A6, A3;

 then

 A7: (Fi1 . k) = ((n choose i) * (((Z1 `^ i) *' (Z0 `^ (n -' i))) . k)) by Th12;

 <%(z0 |^ (n -' i))%> = (Z0 `^ (n -' i)) by Th8;

 then

 A8: (((Z1 `^ i) *' (Z0 `^ (n -' i))) . k) = (((Z1 `^ i) . k) * (z0 |^ (n -' i))) by Th7;

 thus k <> i implies (Fi1 . k) = ( 0. R)

 proof

 assume k <> i;

 then ((Z1 `^ i) . k) = ( 0. R) by Th9;

 hence thesis by A7, A8;

 end;

 assume

 A9: k = i;

 then i = 0 implies ((Z1 `^ i) . k) = ( 1_ R) by Th9;

 then i = 0 implies ((Z1 `^ i) . k) = (z1 |^ k) by A9, BINOM: 8;

 hence thesis by A9, Th9, A7, A8;

 end;

 consider f be sequence of the carrier of PRR such that

 A10: ( Sum F) = (f . ( len F)) and

 A11: (f . 0 ) = ( 0. PRR) & for j be Nat holds for v be Element of PRR st j < ( len F) & v = (F . (j + 1)) holds (f . (j + 1)) = ((f . j) + v) by RLVECT_1:def 12;

 set L = ( len F);

 reconsider fL = (f . L) as Polynomial of R by POLYNOM3:def 10;



 A12: for p be Polynomial of R st p = (f . 0 ) holds (p . k) = ( 0. R)

 proof

 let p be Polynomial of R;

 assume p = (f . 0 );

 then p = ( 0_. R) & k in NAT by A11, POLYNOM3:def 10, ORDINAL1:def 12;

 hence thesis by FUNCOP_1: 7;

 end;

 per cases ;

 suppose

 A13: k > n;

 defpred P[ Nat] means $1 <= L implies for p be Polynomial of R st p = (f . $1) holds (p . k) = ( 0. R);



 A14: P[ 0 ] by A12;



 A15: for i be Nat st P[i] holds P[(i + 1)]

 proof

 let i be Nat such that

 A16: P[i];

 set i1 = (i + 1);

 reconsider fi = (f . i) as Polynomial of R by POLYNOM3:def 10;

 assume

 A17: i1 <= L;

 then

 A18: i < L by NAT_1: 13;



 A19: (fi . k) = ( 0. R) by A16, A17, NAT_1: 13;

 i1 in ( dom F) by NAT_1: 11, A17, FINSEQ_3: 25;

 then

 A20: (F /. i1) = (F . i1) by PARTFUN1:def 6;

 then

 reconsider Fi1 = (F . i1) as Polynomial of R by POLYNOM3:def 10;

 let p be Polynomial of R such that

 A21: p = (f . i1);



 A22: i <= n by A2, A18, NAT_1: 13;

 p = ((f . i) + (F /. i1)) by A20, A17, NAT_1: 13, A11, A21

 .= (fi + Fi1) by A20, POLYNOM3:def 10;



 hence (p . k) = ((fi . k) + (Fi1 . k)) by NORMSP_1:def 2

 .= ( 0. R) by A4, A13, A19, A22;

 end;

 for i be Nat holds P[i] from NAT_1:sch 2( A14, A15);



 hence (( <%z0, z1%> `^ n) . k) = ( 0. R) by A10, A1

 .= ( 0 * ((z1 |^ k) * (z0 |^ (n -' k)))) by BINOM: 12

 .= C by A13, NEWTON:def 3;

 end;

 suppose

 A23: k <= n;

 defpred P[ Nat] means $1 <= k & $1 <= L implies for p be Polynomial of R st p = (f . $1) holds (p . k) = ( 0. R);



 A24: P[ 0 ] by A12;



 A25: for i be Nat st P[i] holds P[(i + 1)]

 proof

 let i be Nat such that

 A26: P[i];

 set i1 = (i + 1);

 reconsider fi = (f . i) as Polynomial of R by POLYNOM3:def 10;

 assume

 A27: i1 <= k & i1 <= L;

 then

 A28: i < k & i < L by NAT_1: 13;



 A29: (fi . k) = ( 0. R) by A26, A27, NAT_1: 13;

 i1 in ( dom F) by A27, NAT_1: 11, FINSEQ_3: 25;

 then

 A30: (F /. i1) = (F . i1) by PARTFUN1:def 6;

 then

 reconsider Fi1 = (F . i1) as Polynomial of R by POLYNOM3:def 10;

 let p be Polynomial of R such that

 A31: p = (f . i1);



 A32: i <= n by A2, A28, NAT_1: 13;

 p = ((f . i) + (F /. i1)) by A30, A27, NAT_1: 13, A11, A31

 .= (fi + Fi1) by A30, POLYNOM3:def 10;



 hence (p . k) = ((fi . k) + (Fi1 . k)) by NORMSP_1:def 2

 .= ( 0. R) by A32, A28, A4, A29;

 end;



 A33: for i be Nat holds P[i] from NAT_1:sch 2( A24, A25);

 defpred R[ Nat] means $1 <= n implies for p be Polynomial of R st p = (f . ($1 + 1)) holds (p . k) = C;



 A34: R[k]

 proof

 assume

 A35: k <= n;

 set k1 = (k + 1);

 let p be Polynomial of R such that

 A36: p = (f . k1);

 reconsider fk = (f . k) as Polynomial of R by POLYNOM3:def 10;

 1 <= k1 & k1 <= L by A2, A35, NAT_1: 11, XREAL_1: 6;

 then k1 in ( dom F) by FINSEQ_3: 25;

 then

 A37: (F /. k1) = (F . k1) by PARTFUN1:def 6;

 then

 reconsider Fk1 = (F . k1) as Polynomial of R by POLYNOM3:def 10;



 A38: k < L by A35, A2, NAT_1: 13;



 then p = ((f . k) + (F /. k1)) by A37, A11, A36

 .= (fk + Fk1) by A37, POLYNOM3:def 10;



 hence (p . k) = ((fk . k) + (Fk1 . k)) by NORMSP_1:def 2

 .= (( 0. R) + (Fk1 . k)) by A38, A33

 .= C by A4, A35;

 end;



 A39: for i be Nat st k <= i holds R[i] implies R[(i + 1)]

 proof

 let i be Nat such that

 A40: k <= i & R[i];

 set i1 = (i + 1), i2 = (i1 + 1);

 reconsider fi1 = (f . i1) as Polynomial of R by POLYNOM3:def 10;

 assume

 A41: i1 <= n;

 1 <= i2 & i2 <= L by A41, A2, NAT_1: 11, XREAL_1: 6;

 then i2 in ( dom F) by FINSEQ_3: 25;

 then

 A42: (F /. i2) = (F . i2) by PARTFUN1:def 6;

 then

 reconsider Fi2 = (F . i2) as Polynomial of R by POLYNOM3:def 10;

 let p be Polynomial of R such that

 A43: p = (f . i2);



 A44: i1 < L by A41, NAT_1: 13, A2;



 A45: i1 <> k by A40, NAT_1: 13;



 A46: (Fi2 . k) = ( 0. R) by A45, A41, A4;

 p = ((f . i1) + (F /. i2)) by A44, A42, A11, A43

 .= (fi1 + Fi2) by A42, POLYNOM3:def 10;



 hence (p . k) = ((fi1 . k) + (Fi2 . k)) by NORMSP_1:def 2

 .= C by A40, A41, A46, NAT_1: 13;

 end;

 for i be Nat st k <= i holds R[i] from NAT_1:sch 8( A34, A39);

 hence thesis by A10, A1, A23, A2;

 end;

 end;

 begin

 definition

 let z be Complex;

 :: BASEL_2:def3

 attr z is imaginary means

 : Def3: ( Re z) = 0 ;

 end

 registration

 cluster -> imaginary;

 coherence by COMPLEX1: 7;

 cluster real imaginary -> zero for Complex;

 coherence ;

 cluster zero -> imaginary for Complex;

 coherence ;

 end

 registration

 let z1,z2 be imaginary Complex;

 cluster (z1 * z2) -> real;

 coherence

 proof

 ( Im (z1 * z2)) = ((( Re z1) * ( Im z2)) + (( Re z2) * ( Im z1))) & ( Re z2) = 0 & ( Re z1) = 0 by Def3, COMPLEX1: 9;

 hence thesis;

 end;

 cluster (z1 + z2) -> imaginary;

 coherence

 proof

 ( Re (z1 + z2)) = (( Re z1) + ( Re z2)) & ( Re z2) = 0 by Def3, COMPLEX1: 8;

 hence thesis by Def3;

 end;

 end

 registration

 let z be imaginary Complex;

 let r be real Complex;

 cluster (z * r) -> imaginary;

 coherence

 proof

 ( Re (z * r)) = ((( Re z) * ( Re r)) - (( Im r) * ( Im z))) & ( Re z) = 0 & ( Im r) = 0 by Def3, COMPLEX1: 9;

 hence thesis;

 end;

 end

 registration

 cluster ( 0. F_Complex ) -> real imaginary;

 coherence by COMPLFLD: 7;

 end

 registration

 cluster real imaginary for Element of F_Complex ;

 existence

 proof

 take ( 0. FC);

 thus thesis;

 end;

 end

 registration

 let z be real Element of F_Complex ;

 let n be Nat;

 cluster (n * z) -> real;

 coherence ;

 end

 registration

 let z be imaginary Element of F_Complex ;

 let n be Nat;

 cluster (n * z) -> imaginary;

 coherence ;

 end

 registration

 let z be imaginary Complex;

 let n be even Nat;

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

 coherence

 proof

 z in COMPLEX by XCMPLX_0:def 2;

 then

 reconsider Z = z as Element of FC by COMPLFLD:def 1;

 n in NAT & ( Re z) = 0 by Def3, ORDINAL1:def 12;

 then ( Im (( power FC) . (Z,n))) = 0 by HURWITZ2: 5;

 hence thesis;

 end;

 end

 registration

 let z be imaginary Complex;

 let n be odd Nat;

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

 coherence

 proof

 z in COMPLEX by XCMPLX_0:def 2;

 then

 reconsider Z = z as Element of FC by COMPLFLD:def 1;

 n in NAT & ( Re z) = 0 by Def3, ORDINAL1:def 12;

 then ( Re (( power FC) . (Z,n))) = 0 by HURWITZ2: 6;

 hence thesis;

 end;

 end

 registration

 let r be real Element of F_Complex ;

 let n be Nat;

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

 coherence

 proof

 defpred P[ Nat] means (( power FC) . (r,$1)) is real;

 (( power FC) . (r, 0 )) = ( 1_ FC) by GROUP_1:def 7;

 then

 A1: P[ 0 ] by COMPLFLD: 8, COMPLEX1: 6;



 A2: P[k] implies P[(k + 1)]

 proof

 (( power FC) . (r,(k + 1))) = ((( power FC) . (r,k)) * r) by GROUP_1:def 7;

 hence thesis;

 end;

 P[k] from NAT_1:sch 2( A1, A2);

 hence thesis;

 end;

 end

 registration

 cluster zero -> imaginary real for Element of F_Complex ;

 coherence by MATRIX_5: 2, STRUCT_0:def 12;

 end

 definition

 let p be sequence of F_Complex ;

 :: BASEL_2:def4

 attr p is imaginary means

 : Def4: for i be Nat holds (p . i) is imaginary;

 end

 registration

 let im1 be imaginary Element of F_Complex ;

 cluster <%im1%> -> imaginary;

 coherence

 proof

 let i be Nat;



 A1: i in NAT by ORDINAL1:def 12;

 i = 0 or i >= 1 by NAT_1: 14;

 then ( <%im1%> . i) = im1 or ( <%im1%> . i) = ( 0. FC) by POLYNOM5: 32, A1;

 hence thesis;

 end;

 let im2 be imaginary Element of F_Complex ;

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

 coherence

 proof

 let i be Nat;

 i = 0 or i = 1 or i >= 2 by NAT_1: 23;

 hence thesis by POLYNOM5: 38;

 end;

 end

 registration

 cluster imaginary for Polynomial of F_Complex ;

 existence

 proof

 <% i_FC %> is imaginary;

 hence thesis;

 end;

 end

 theorem :: BASEL_2:14



 Th14: for I be imaginary Polynomial of F_Complex holds for r be real Element of F_Complex holds ( eval (I,r)) is imaginary

 proof

 let I be imaginary Polynomial of FC;

 let r be real Element of FC;

 consider H be FinSequence of FC such that

 A1: ( eval (I,r)) = ( Sum H) & ( len H) = ( len I) and

 A2: for n be Element of NAT st n in ( dom H) holds (H . n) = ((I . (n -' 1)) * (( power FC) . (r,(n -' 1)))) by POLYNOM4:def 2;

 consider h be sequence of the carrier of FC such that

 A3: ( Sum H) = (h . ( len H)) and

 A4: (h . 0 ) = ( 0. FC) & for j be Nat holds for v be Element of FC st j < ( len H) & v = (H . (j + 1)) holds (h . (j + 1)) = ((h . j) + v) by RLVECT_1:def 12;

 defpred P[ Nat] means $1 <= ( len H) implies (h . $1) is imaginary;



 A5: P[ 0 ] by A4;



 A6: P[n] implies P[(n + 1)]

 proof

 assume

 A7: P[n];

 set n1 = (n + 1);

 assume

 A8: n1 <= ( len H);

 n1 in ( dom H) by NAT_1: 11, A8, FINSEQ_3: 25;

 then

 A9: (H . n1) = ((I . (n1 -' 1)) * (( power FC) . (r,(n1 -' 1)))) by A2;



 A10: (I . (n1 -' 1)) is imaginary by Def4;

 reconsider Hn1 = (H . n1) as imaginary Element of FC by A10, A9;

 (h . n1) = ((h . n) + Hn1) by A4, A8, NAT_1: 13;

 hence thesis by A8, A7, NAT_1: 13;

 end;

 P[n] from NAT_1:sch 2( A5, A6);

 hence thesis by A1, A3;

 end;

 theorem :: BASEL_2:15



 Th15: for R be real Polynomial of F_Complex holds for r be real Element of F_Complex holds ( eval (R,r)) is real

 proof

 let I be real Polynomial of FC;

 let r be real Element of FC;

 consider H be FinSequence of FC such that

 A1: ( eval (I,r)) = ( Sum H) & ( len H) = ( len I) and

 A2: for n be Element of NAT st n in ( dom H) holds (H . n) = ((I . (n -' 1)) * (( power FC) . (r,(n -' 1)))) by POLYNOM4:def 2;

 consider h be sequence of the carrier of FC such that

 A3: ( Sum H) = (h . ( len H)) and

 A4: (h . 0 ) = ( 0. FC) & for j be Nat holds for v be Element of FC st j < ( len H) & v = (H . (j + 1)) holds (h . (j + 1)) = ((h . j) + v) by RLVECT_1:def 12;

 defpred P[ Nat] means $1 <= ( len H) implies (h . $1) is real;



 A5: P[ 0 ] by A4;



 A6: P[n] implies P[(n + 1)]

 proof

 assume

 A7: P[n];

 set n1 = (n + 1);

 assume

 A8: n1 <= ( len H);

 n1 in ( dom H) by NAT_1: 11, A8, FINSEQ_3: 25;

 then

 A9: (H . n1) = ((I . (n1 -' 1)) * (( power FC) . (r,(n1 -' 1)))) by A2;

 reconsider Hn1 = (H . n1) as real Element of FC by A9;

 (h . n1) = ((h . n) + Hn1) by A4, A8, NAT_1: 13;

 hence thesis by A8, A7, NAT_1: 13;

 end;

 P[n] from NAT_1:sch 2( A5, A6);

 hence thesis by A1, A3;

 end;

 theorem :: BASEL_2:16

 for im be imaginary Element of F_Complex , r be 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

 let im be imaginary Element of FC, r be real Element of FC;

 assume

 A1: n is even;

 set pC = ( power FC);

 set IRn = ( <%im, r%> `^ n);

 thus ( even_part IRn) is real

 proof

 let k be Nat;

 per cases ;

 suppose k is odd;

 hence thesis by HURWITZ2:def 1;

 end;

 suppose

 A2: k is even;



 A3: (IRn . k) = ((n choose k) * ((r |^ k) * (im |^ (n -' k)))) by Th13;

 (n -' k) = (n - k) or (n -' k) = 0 by XREAL_0:def 2;

 hence thesis by HURWITZ2:def 1, A3, A1, A2;

 end;

 end;

 thus ( odd_part IRn) is imaginary

 proof

 let k be Nat;

 per cases ;

 suppose k is even;

 hence thesis by HURWITZ2:def 2;

 end;

 suppose

 A4: k is odd;



 A5: (IRn . k) = ((n choose k) * ((r |^ k) * (im |^ (n -' k)))) by Th13;

 per cases ;

 suppose k <= n;

 then (n -' k) = (n - k) by XREAL_1: 233;

 hence thesis by HURWITZ2:def 2, A5, A1, A4;

 end;

 suppose k > n;

 then (n choose k) = 0 by NEWTON:def 3;

 hence thesis by A4, A5, HURWITZ2:def 2;

 end;

 end;

 end;

 end;

 theorem :: BASEL_2:17



 Th17: for im be imaginary Element of F_Complex , r be 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

 let im be imaginary Element of FC, r be real Element of FC;

 assume

 A1: n is odd;

 set pC = ( power FC);

 set IRn = ( <%im, r%> `^ n);

 thus ( even_part IRn) is imaginary

 proof

 let k be Nat;

 per cases ;

 suppose k is odd;

 hence thesis by HURWITZ2:def 1;

 end;

 suppose

 A2: k is even;



 A3: (IRn . k) = ((n choose k) * ((r |^ k) * (im |^ (n -' k)))) by Th13;

 per cases ;

 suppose k <= n;

 then (n -' k) = (n - k) by XREAL_1: 233;

 hence thesis by HURWITZ2:def 1, A3, A1, A2;

 end;

 suppose k > n;

 then (n choose k) = 0 by NEWTON:def 3;

 hence thesis by A2, A3, HURWITZ2:def 1;

 end;

 end;

 end;

 thus ( odd_part IRn) is real

 proof

 let k be Nat;

 per cases ;

 suppose k is even;

 hence thesis by HURWITZ2:def 2;

 end;

 suppose

 A4: k is odd;



 A5: (IRn . k) = ((n choose k) * ((r |^ k) * (im |^ (n -' k)))) by Th13;

 per cases ;

 suppose k <= n;

 then (n -' k) = (n - k) by XREAL_1: 233;

 hence thesis by HURWITZ2:def 2, A5, A1, A4;

 end;

 suppose k > n;

 then (n choose k) = 0 by NEWTON:def 3;

 hence thesis by A4, A5, HURWITZ2:def 2;

 end;

 end;

 end;

 end;

 theorem :: BASEL_2:18



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

 proof

 let L be non empty ZeroStr;

 let p be Polynomial of L such that

 A1: ( len ( even_part p)) <> 0 ;

 set E = ( even_part p);

 assume ( len E) is even;

 then

 consider n such that

 A2: (2 * n) = ( len E) by ABIAN:def 2;



 A3: ( len E) is_at_least_length_of E by ALGSEQ_1:def 3;

 n <> 0 by A1, A2;

 then

 reconsider n1 = (n - 1) as Nat;

 (n + n1) is_at_least_length_of E

 proof

 let k such that

 A4: k >= (n + n1);

 assume

 A5: (E . k) <> ( 0. L);

 then k is even & (n + n1) = ((2 * n) - 1) by HURWITZ2:def 1;

 then k > (n + n1) by A4, XXREAL_0: 1;

 then k >= ((n + n1) + 1) by NAT_1: 13;

 hence thesis by A5, A2, A3, ALGSEQ_1:def 2;

 end;

 then (n + n) <= (n + n1) by ALGSEQ_1:def 3, A2;

 then (n1 + 1) <= n1 by XREAL_1: 8;

 hence thesis by NAT_1: 13;

 end;

 begin

 definition

 let L be non empty set;

 let p be sequence of L;

 let m be Nat;

 :: BASEL_2:def5

 func sieve (p,m) -> sequence of L means

 : Def5: for i be Nat holds (it . i) = (p . (m * i));

 existence

 proof

 defpred P[ object, object] means for i be Nat st i = $1 holds $2 = (p . (m * i));



 A1: for x be object st x in NAT holds ex y be object st y in L & P[x, y]

 proof

 let x be object;

 assume x in NAT ;

 then

 reconsider i = x as Nat;

 take (p . (m * i));

 thus thesis;

 end;

 consider f be Function of NAT , L such that

 A2: for x be object st x in NAT holds P[x, (f . x)] from FUNCT_2:sch 1( A1);

 take f;

 thus thesis by A2, ORDINAL1:def 12;

 end;

 uniqueness

 proof

 let s1,s2 be sequence of L such that

 A3: for i be Nat holds (s1 . i) = (p . (m * i)) and

 A4: for i be Nat holds (s2 . i) = (p . (m * i));



 A5: ( dom s1) = NAT = ( dom s2) by FUNCT_2:def 1;

 for x be object st x in ( dom s1) holds (s1 . x) = (s2 . x)

 proof

 let x be object;

 assume x in ( dom s1);

 then

 reconsider i = x as Element of NAT ;



 thus (s1 . x) = (p . (m * i)) by A3

 .= (s2 . x) by A4;

 end;

 hence s1 = s2 by A5, FUNCT_1: 2;

 end;

 end

 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

 proof



 A1: 1 <= m by NAT_1: 14;

 consider n such that

 A2: k >= n implies (p . k) = ( 0. L) by ALGSEQ_1:def 1;

 take n;

 let k;

 assume k >= n;

 then

 A3: (m * k) >= (1 * n) by A1, XREAL_1: 66;



 thus (( sieve (p,m)) . k) = (p . (m * k)) by Def5

 .= ( 0. L) by A2, A3;

 end;

 end

 theorem :: BASEL_2:19



 Th19: for L be non empty ZeroStr holds for p be sequence of L holds ( sieve (p,(2 * k))) = ( sieve (( even_part p),(2 * k)))

 proof

 let L be non empty ZeroStr;

 let p be sequence of L;

 let n be Element of NAT ;



 thus (( sieve (( even_part p),(2 * k))) . n) = (( even_part p) . ((2 * k) * n)) by Def5

 .= (p . ((2 * k) * n)) by HURWITZ2:def 1

 .= (( sieve (p,(2 * k))) . n) by Def5;

 end;

 theorem :: BASEL_2:20



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

 proof

 let L be non empty ZeroStr, p be Polynomial of L;

 set E = ( even_part p), CE = ( sieve (E,2));

 assume ( len E) is odd;

 then

 consider n such that

 A1: ( len E) = ((2 * n) + 1) by ABIAN: 9;



 A2: ( len E) is_at_least_length_of E by ALGSEQ_1:def 3;

 set n1 = (n + 1);



 A3: n1 is_at_least_length_of CE

 proof

 let k such that

 A4: k >= n1;

 (k + k) >= (n1 + n1) & (n1 + n1) = (( len E) + 1) by A1, A4, XREAL_1: 7;

 then (k + k) > ( len E) by NAT_1: 13;



 hence ( 0. L) = (E . (2 * k)) by A2, ALGSEQ_1:def 2

 .= (CE . k) by Def5;

 end;

 for m be Nat st m is_at_least_length_of CE holds n1 <= m

 proof

 let m be Nat such that

 A5: m is_at_least_length_of CE;

 m > 0

 proof

 assume

 A6: m <= 0 ;

 (2 * n) is_at_least_length_of E

 proof

 let k such that

 A7: k >= (2 * n);

 per cases by A7, XXREAL_0: 1;

 suppose k > (2 * n);

 then k >= ((2 * n) + 1) by NAT_1: 13;

 hence thesis by A1, A2, ALGSEQ_1:def 2;

 end;

 suppose k = (2 * n);



 hence (E . k) = (CE . n) by Def5

 .= ( 0. L) by A5, A6, ALGSEQ_1:def 2;

 end;

 end;

 then ((2 * n) + 1) <= (2 * n) by A1, ALGSEQ_1:def 3;

 hence thesis by NAT_1: 13;

 end;

 then

 reconsider mm = (m - 1) as Nat;

 (m + mm) is_at_least_length_of E

 proof

 let k such that

 A8: k >= (m + mm);

 assume

 A9: (E . k) <> ( 0. L);

 then

 A10: k is even by HURWITZ2:def 1;

 then

 consider i be Nat such that

 A11: k = (2 * i) by ABIAN:def 2;

 (m + mm) = ((2 * m) - 1);

 then k > (m + mm) by A10, A8, XXREAL_0: 1;

 then k >= ((m + mm) + 1) by NAT_1: 13;

 then (2 * i) >= (2 * m) by A11;

 then i >= m by XREAL_1: 68;

 then (CE . i) = ( 0. L) by A5, ALGSEQ_1:def 2;

 hence thesis by A9, Def5, A11;

 end;

 then ( len E) <= (m + mm) by ALGSEQ_1:def 3;

 then (((2 * n) + 1) + 1) <= (((2 * m) - 1) + 1) by A1, XREAL_1: 7;

 then (2 * n1) <= (2 * m);

 hence n1 <= m by XREAL_1: 68;

 end;

 then

 A12: ( len CE) = n1 by A3, ALGSEQ_1:def 3;

 CE = ( sieve (p,(2 * 1))) by Th19;

 hence thesis by A1, A12;

 end;

 theorem :: BASEL_2:21



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

 proof

 let L be non empty ZeroStr;

 let p be Polynomial of L such that

 A1: ( len ( even_part p)) = 0 ;

 let n be non zero Nat;



 A2: 0 is_at_least_length_of ( even_part p) by A1, ALGSEQ_1:def 3;

 0 is_at_least_length_of ( sieve (p,(2 * n)))

 proof

 let k such that k >= 0 ;



 thus (( sieve (p,(2 * n))) . k) = (p . ((2 * n) * k)) by Def5

 .= (( even_part p) . ((2 * n) * k)) by HURWITZ2:def 1

 .= ( 0. L) by A2, ALGSEQ_1:def 2;

 end;

 hence thesis by ALGSEQ_1:def 3;

 end;

 theorem :: BASEL_2:22



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

 proof

 let L be Field;

 let p be Polynomial of L;

 set C = ( sieve (p,2)), x2 = <%( 0. L), ( 0. L), ( 1_ L)%>, Cx = ( Subst (C,x2)), E = ( even_part p);

 consider F be FinSequence of ( Polynom-Ring L) such that

 A1: Cx = ( Sum F) & ( len F) = ( len C) and

 A2: for n be Element of NAT st n in ( dom F) holds (F . n) = ((C . (n -' 1)) * (x2 `^ (n -' 1))) by POLYNOM5:def 6;

 consider f be sequence of ( Polynom-Ring L) such that

 A3: ( Sum F) = (f . ( len F)) and

 A4: (f . 0 ) = ( 0. ( Polynom-Ring L)) & for j be Nat holds for v be Element of ( Polynom-Ring L) st j < ( len F) & v = (F . (j + 1)) holds (f . (j + 1)) = ((f . j) + v) by RLVECT_1:def 12;

 let n be Element of NAT ;

 per cases ;

 suppose

 A5: n is odd;

 defpred P[ Nat] means $1 <= ( len F) implies for P be Polynomial of L st P = (f . $1) holds (P . n) = ( 0. L);



 A6: P[ 0 ]

 proof

 assume 0 <= ( len F);

 let P be Polynomial of L;

 assume P = (f . 0 );

 then P = ( 0_. L) by A4, POLYNOM3:def 10;

 hence (P . n) = ( 0. L) by FUNCOP_1: 7;

 end;



 A7: P[k] implies P[(k + 1)]

 proof

 assume

 A8: P[k];

 set k1 = (k + 1);

 assume

 A9: k1 <= ( len F);

 let P be Polynomial of L such that

 A10: P = (f . k1);



 A11: (k1 -' 1) = (k1 - 1) by NAT_1: 11, XREAL_1: 233;

 k1 in ( dom F) by A9, NAT_1: 11, FINSEQ_3: 25;

 then

 A12: (F . k1) = ((C . k) * (x2 `^ k)) by A11, A2;

 then

 reconsider Fk1 = (F . k1) as Element of ( Polynom-Ring L) by POLYNOM3:def 10;

 reconsider fk = (f . k) as Polynomial of L by POLYNOM3:def 10;



 A13: P = ((f . k) + Fk1) by A10, A9, NAT_1: 13, A4

 .= (fk + ((C . k) * (x2 `^ k))) by A12, POLYNOM3:def 10;



 A14: (fk . n) = ( 0. L) by A9, NAT_1: 13, A8;

 n <> (2 * k) by A5;

 then ((x2 `^ k) . n) = ( 0. L) by Th10;



 then (((C . k) * (x2 `^ k)) . n) = ((C . k) * ( 0. L)) by POLYNOM5:def 4

 .= ( 0. L);

 then (P . n) = (( 0. L) + ( 0. L)) by A13, A14, NORMSP_1:def 2;

 hence thesis;

 end;

 P[k] from NAT_1:sch 2( A6, A7);

 then (Cx . n) = ( 0. L) by A1, A3;

 hence thesis by A5, HURWITZ2:def 1;

 end;

 suppose

 A15: n is even;

 then

 consider m be Nat such that

 A16: (2 * m) = n by ABIAN:def 2;

 set m1 = (m + 1);

 per cases ;

 suppose

 A17: m < ( len F);

 defpred R[ Nat] means $1 <= ( len F) implies for P be Polynomial of L st P = (f . $1) holds (P . n) = (p . n);

 defpred P[ Nat] means $1 <= m implies for P be Polynomial of L st P = (f . $1) holds (P . n) = ( 0. L);



 A18: P[ 0 ]

 proof

 assume 0 <= m;

 let P be Polynomial of L;

 assume P = (f . 0 );

 then P = ( 0_. L) by A4, POLYNOM3:def 10;

 hence (P . n) = ( 0. L) by FUNCOP_1: 7;

 end;



 A19: P[k] implies P[(k + 1)]

 proof

 assume

 A20: P[k];

 set k1 = (k + 1);

 assume

 A21: k1 <= m;

 then

 A22: k < m by NAT_1: 13;

 let P be Polynomial of L such that

 A23: P = (f . k1);



 A24: (k1 -' 1) = (k1 - 1) by NAT_1: 11, XREAL_1: 233;



 A25: k < ( len F) & k1 <= ( len F) by A22, A17, A21, XXREAL_0: 2;

 then k1 in ( dom F) by NAT_1: 11, FINSEQ_3: 25;

 then

 A26: (F . k1) = ((C . k) * (x2 `^ k)) by A24, A2;

 then

 reconsider Fk1 = (F . k1) as Element of ( Polynom-Ring L) by POLYNOM3:def 10;

 reconsider fk = (f . k) as Polynomial of L by POLYNOM3:def 10;



 A27: P = ((f . k) + Fk1) by A23, A4, A25

 .= (fk + ((C . k) * (x2 `^ k))) by A26, POLYNOM3:def 10;



 A28: (fk . n) = ( 0. L) by NAT_1: 13, A20, A21;

 n <> (2 * k) by A16, A21, NAT_1: 13;

 then ((x2 `^ k) . n) = ( 0. L) by Th10;



 then (((C . k) * (x2 `^ k)) . n) = ((C . k) * ( 0. L)) by POLYNOM5:def 4

 .= ( 0. L);

 then (P . n) = (( 0. L) + ( 0. L)) by A27, A28, NORMSP_1:def 2;

 hence thesis;

 end;



 A29: P[k] from NAT_1:sch 2( A18, A19);



 A30: R[m1]

 proof

 assume

 A31: m1 <= ( len F);

 let P be Polynomial of L such that

 A32: P = (f . m1);

 reconsider fm = (f . m) as Polynomial of L by POLYNOM3:def 10;



 A33: 1 <= m1 by NAT_1: 11;



 A34: (m1 -' 1) = (m1 - 1) by NAT_1: 11, XREAL_1: 233;



 A35: (F . m1) = ((C . m) * (x2 `^ m)) by A34, A2, A33, A31, FINSEQ_3: 25;

 then

 reconsider Fm1 = (F . m1) as Element of ( Polynom-Ring L) by POLYNOM3:def 10;



 A36: P = ((f . m) + Fm1) by A32, A31, NAT_1: 13, A4

 .= (fm + ((C . m) * (x2 `^ m))) by A35, POLYNOM3:def 10;



 A37: (fm . n) = ( 0. L) by A29;

 ((x2 `^ m) . n) = ( 1_ L) by A16, Th10;



 then (((C . m) * (x2 `^ m)) . n) = ((C . m) * ( 1_ L)) by POLYNOM5:def 4

 .= (C . m);

 then (P . n) = (( 0. L) + (C . m)) by A36, A37, NORMSP_1:def 2;

 hence thesis by Def5, A16;

 end;



 A38: m1 <= k & R[k] implies R[(k + 1)]

 proof

 set k1 = (k + 1);

 assume

 A39: m1 <= k & R[k];

 assume

 A40: k1 <= ( len F);

 let P be Polynomial of L such that

 A41: P = (f . k1);



 A42: (k1 -' 1) = (k1 - 1) by NAT_1: 11, XREAL_1: 233;

 k1 in ( dom F) by A40, NAT_1: 11, FINSEQ_3: 25;

 then

 A43: (F . k1) = ((C . k) * (x2 `^ k)) by A42, A2;

 then

 reconsider Fk1 = (F . k1) as Element of ( Polynom-Ring L) by POLYNOM3:def 10;

 reconsider fk = (f . k) as Polynomial of L by POLYNOM3:def 10;



 A44: P = ((f . k) + Fk1) by A41, A4, A40, NAT_1: 13

 .= (fk + ((C . k) * (x2 `^ k))) by A43, POLYNOM3:def 10;



 A45: (fk . n) = (p . n) by A40, NAT_1: 13, A39;

 n <> (2 * k) by A16, A39, NAT_1: 13;

 then ((x2 `^ k) . n) = ( 0. L) by Th10;



 then (((C . k) * (x2 `^ k)) . n) = ((C . k) * ( 0. L)) by POLYNOM5:def 4

 .= ( 0. L);

 then (P . n) = ((p . n) + ( 0. L)) by A44, A45, NORMSP_1:def 2;

 hence thesis;

 end;



 A46: m1 <= k implies R[k] from NAT_1:sch 8( A30, A38);

 m1 <= ( len F) by A17, NAT_1: 13;

 then (Cx . n) = (p . n) by A1, A3, A46;

 hence thesis by A15, HURWITZ2:def 1;

 end;

 suppose

 A47: m >= ( len F);

 then

 A48: (2 * m) >= (2 * ( len C)) by A1, XREAL_1: 64;



 A49: ( len E) is_at_least_length_of E by ALGSEQ_1:def 3;

 (2 * m) >= ( len E)

 proof

 per cases ;

 suppose ( len E) = 0 ;

 hence thesis;

 end;

 suppose ( len E) > 0 ;

 then (2 * ( len C)) = (( len E) + 1) by Th18, Th20;

 hence thesis by A48, NAT_1: 13;

 end;

 end;

 then

 A50: (E . n) = ( 0. L) by A16, ALGSEQ_1:def 2, A49;



 A51: ( len Cx) is_at_least_length_of Cx by ALGSEQ_1:def 3;



 D: 2 = (2 * 1);

 (2 * m) >= ( len Cx)

 proof

 per cases ;

 suppose ( len E) = 0 ;

 then ( len C) = 0 by D, Th21;

 then C = ( 0_. L) by POLYNOM4: 5;

 then Cx = ( 0_. L) by POLYNOM5: 49;

 hence thesis by POLYNOM4: 3;

 end;

 suppose ( len E) > 0 ;

 then (2 * ( len C)) = (( len E) + 1) by Th18, Th20;

 then

 A52: ( len C) <> 0 ;

 ( len x2) = 3 by NIVEN: 28;



 then ( len Cx) = ((((( len C) * 3) - ( len C)) - 3) + 2) by A52, POLYNOM5: 52

 .= ((( len C) * 2) - 1);

 then (2 * m) >= (( len Cx) + 1) by A47, A1, XREAL_1: 64;

 hence thesis by NAT_1: 13;

 end;

 end;

 hence thesis by A16, A50, ALGSEQ_1:def 2, A51;

 end;

 end;

 end;

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

 theorem :: BASEL_2:23



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

 proof

 (((2 * n) + 1) -' (2 * n)) = (((2 * n) + 1) - (2 * n)) by NAT_1: 11, XREAL_1: 233;

 then

 A1: ( i_FC |^ (((2 * n) + 1) -' (2 * n))) = i_FC by BINOM: 8;

 (( 1. FC) |^ (2 * n)) = ( 1_ FC) by Th3;

 then

 A2: ((( 1. FC) |^ (2 * n)) * i_FC ) = i_FC ;

 (((2 * n) + 1) - (2 * n)) = 1;

 then

 A3: (((2 * n) + 1) choose (2 * n)) = (((2 * n) + 1) choose 1) by NAT_1: 11, NEWTON: 20;

 (( sieve ((PP `^ ((2 * n) + 1)),2)) . n) = ((PP `^ ((2 * n) + 1)) . (2 * n)) by Def5;

 hence thesis by A1, A2, A3, Th13;

 end;

 theorem :: BASEL_2:24



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

 proof



 A1: ( i_FC |^ 1) = i_FC by BINOM: 8;

 assume n >= 1;

 then

 reconsider n1 = (n - 1) as Nat;

 n1 <= (n1 + 1) by NAT_1: 11;

 then

 A2: (2 * n1) < ((2 * n) + 1) by NAT_1: 13, XREAL_1: 64;

 then (((2 * n) + 1) -' (2 * n1)) = (((2 * n) + 1) - (2 * n1)) by XREAL_1: 233;



 then

 A3: ( i_FC |^ (((2 * n) + 1) -' (2 * n1))) = ( i_FC |^ (2 + 1))

 .= (( i_FC |^ (1 + 1)) * ( i_FC |^ 1)) by BINOM: 10

 .= (( i_FC * i_FC ) * i_FC ) by A1, BINOM: 10

 .= ( - (( 1_ FC) * i_FC )) by HAHNBAN1: 4, VECTSP_1: 9

 .= ( - i_FC );



 A4: (( 1. FC) |^ (2 * n1)) = ( 1_ FC) by Th3;

 (((2 * n) + 1) - (2 * n1)) = 3;

 then

 A5: (((2 * n) + 1) choose (2 * n1)) = (((2 * n) + 1) choose 3) by A2, NEWTON: 20;

 (( sieve ((PP `^ ((2 * n) + 1)),2)) . n1) = ((PP `^ ((2 * n) + 1)) . (2 * n1)) by Def5

 .= ((((2 * n) + 1) choose 3) * ((( 1. FC) |^ (2 * n1)) * ( - i_FC ))) by A3, A5, Th13

 .= ((((2 * n) + 1) choose 3) * ( - i_FC )) by A4;

 hence thesis;

 end;

 theorem :: BASEL_2:25



 Th25: ( len ( sieve (( <% i_FC , ( 1. F_Complex )%> `^ ((2 * n) + 1)),2))) = (n + 1)

 proof

 set PPn = (PP `^ ((2 * n) + 1));



 A1: (n + 1) is_at_least_length_of ( sieve (PPn,2))

 proof

 let i be Nat;

 assume i >= (n + 1);

 then (i + i) >= ((n + 1) + (n + 1)) & (((2 * n) + 1) + 1) > (((2 * n) + 1) + 0 ) by XREAL_1: 7, XREAL_1: 8;

 then (2 * i) > ((2 * n) + 1) by XXREAL_0: 2;

 then

 A2: (((2 * n) + 1) choose (2 * i)) = 0 by NEWTON:def 3;



 thus (( sieve (PPn,2)) . i) = (PPn . (2 * i)) by Def5

 .= ( 0 * ((( 1. FC) |^ (2 * i)) * ( i_FC |^ (((2 * n) + 1) -' (2 * i))))) by A2, Th13

 .= ( 0. FC);

 end;

 for m st m is_at_least_length_of ( sieve (PPn,2)) holds (n + 1) <= m

 proof

 let m such that

 A3: m is_at_least_length_of ( sieve (PPn,2));

 assume m < (n + 1);

 then m <= n by NAT_1: 13;

 then (( sieve (PPn,2)) . n) = ( 0. FC) by A3, ALGSEQ_1:def 2;

 then ((((2 * n) + 1) choose 1) * i_FC ) = ( 0. FC) by Th23;

 hence thesis;

 end;

 hence thesis by A1, ALGSEQ_1:def 3;

 end;

 registration

 let n be Nat;

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

 coherence

 proof

 ( len ( sieve (( <% i_FC , ( 1. FC)%> `^ ((2 * n) + 1)),2))) = (n + 1) by Th25;

 then ( sieve (( <% i_FC , ( 1. FC)%> `^ ((2 * n) + 1)),2)) <> ( 0_. FC) by POLYNOM4: 3;

 hence thesis by UPROOTS:def 5;

 end;

 end

 theorem :: BASEL_2:26



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

 proof

 set f = ( x_r-seq n);

 set f1 = ( sqr ( cot f));

 set PPn = (PP `^ ((2 * n) + 1));

 let y be object;

 assume y in ( rng f1);

 then

 consider x be object such that

 A1: x in ( dom f1) & (f1 . x) = y by FUNCT_1:def 3;



 A2: ( len f1) = ( len ( cot f)) by CARD_1:def 7;

 then

 A3: ( dom f1) = ( dom ( cot f)) by FINSEQ_3: 29;



 A4: ( dom ( cot f)) = ( dom f) by BASEL_1:def 3;

 reconsider x as Nat by A1;



 A5: (( cot f) . x) = ( cot (f . x)) by BASEL_1:def 3, A1, A3, A4;

 ( cot (f . x)) is Element of COMPLEX by XCMPLX_0:def 2;

 then

 reconsider c = ( cot (f . x)) as Element of FC by COMPLFLD:def 1;



 A6: (c * c) = ((( cot f) . x) ^2 ) by A5

 .= y by VALUED_1: 11, A1;

 set N = ((2 * n) + 1);



 A7: ((( cot (f . x)) + ) |^ N) is real

 proof

 x in ( dom f) & ( len f) = n by BASEL_1: 21, A2, FINSEQ_3: 29, A4, A1;

 then

 A8: 1 <= x <= n by FINSEQ_3: 25;

 then 0 < (f . x) < ( PI / 2) & ( PI / 2) < PI by BASEL_1: 23, COMPTRIG: 5;

 then 0 < (f . x) < PI by XXREAL_0: 2;

 then (f . x) in ]. 0 , PI .[ by XXREAL_1: 4;

 then ( sin . (f . x)) > 0 by COMPTRIG: 7;

 then (( * ( sin (f . x))) / ( sin (f . x))) = by XCMPLX_1: 89;



 then ((( cot (f . x)) + ) |^ N) = (((( cos (f . x)) + ( * ( sin (f . x)))) / ( sin (f . x))) |^ N)

 .= (((( cos (f . x)) + ( * ( sin (f . x)))) |^ N) / (( sin (f . x)) |^ N)) by PREPOWER: 8

 .= ((( cos (N * (f . x))) + ( * ( sin (N * (f . x))))) / (( sin (f . x)) |^ N)) by COMPTRIG: 53

 .= ((( cos (N * (f . x))) + ( * ( sin (x * PI )))) / (( sin (f . x)) |^ N)) by A8, BASEL_1: 25

 .= ((( cos (N * (f . x))) + ( * 0 )) / (( sin (f . x)) |^ N)) by BASEL_1: 13;

 hence thesis;

 end;



 A9: ( eval (( even_part PPn),c)) = 0

 proof



 A10: (( power FC) . ((c + i_FC ),N)) = ((( cot (f . x)) + ) |^ N) by COMPLFLD: 74;



 A11: ( 1. FC) is real by COMPLEX1: 6, COMPLFLD: 8;

 ( even_part PPn) is imaginary by A11, Th17;

 then

 A12: ( eval (( even_part PPn),c)) is imaginary by Th14;

 ( odd_part PPn) is real by Th17, A11;

 then ( eval (( odd_part PPn),c)) is real by Th15;

 then

 A13: ( Im ( eval (( odd_part PPn),c))) = 0 ;



 A14: ( eval (PP,c)) = ( i_FC + (( 1. FC) * c)) by POLYNOM5: 44

 .= (c + i_FC );



 A15: ( Im ( eval (PPn,c))) = ( Im ((( cot (f . x)) + ) |^ N)) by A14, A10, POLYNOM5: 22

 .= 0 by A7;

 ( Im ( eval (PPn,c))) = (( Im ( eval (( odd_part PPn),c))) + ( Im ( eval (( even_part PPn),c))))

 proof

 reconsider ppn = PPn as Polynomial of FC;

 PPn = (( odd_part ppn) + ( even_part ppn)) by HURWITZ2: 10;

 then ( eval (PPn,c)) = (( eval (( odd_part PPn),c)) + ( eval (( even_part PPn),c))) by POLYNOM4: 19;

 hence thesis by COMPLEX1: 8;

 end;



 hence ( eval (( even_part PPn),c)) = ( 0 + ( 0 * )) by A15, A13, A12, COMPLEX1: 13

 .= 0 ;

 end;

 set X2 = <%( 0. FC), ( 0. FC), ( 1_ FC)%>;

 reconsider z1 = ( 0. FC) as Element of FC;



 A16: ( eval (X2,c)) = ((( 0. FC) + (z1 * c)) + ((( 1_ FC) * c) * c)) by NIVEN: 38

 .= (c * c);

 ( even_part PPn) = ( Subst (( sieve (PPn,2)),X2)) by Th22;

 then ( eval (( sieve (PPn,2)),(c * c))) = ( 0. FC) by A9, A16, POLYNOM5: 53;

 then (c * c) is_a_root_of ( sieve (PPn,2)) by POLYNOM5:def 7;

 hence thesis by A6, POLYNOM5:def 10;

 end;

 theorem :: BASEL_2:27



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

 proof

 set f = ( x_r-seq n), F = ( sqr ( cot f)), C = ( sieve ((PP `^ ((2 * n) + 1)),2));



 A1: ( len F) = ( len ( cot f)) = ( len f) = n by CARD_1:def 7, BASEL_1: 21;

 F is one-to-one by BASEL_1: 28;

 then

 A2: ( card ( dom F)) = ( card ( rng F)) & ( dom F) = ( Seg n) by A1, CARD_1: 70, FINSEQ_1:def 3;



 A3: ( rng F) c= ( Roots C) by Th26;



 A4: n <= ( card ( Roots C)) by A2, NAT_1: 43, Th26;

 ( card ( Roots C)) < ( len C) by Th11;

 then ( card ( Roots C)) < (n + 1) by Th25;

 then ( card ( Roots C)) <= n by NAT_1: 13;

 hence thesis by A3, CARD_2: 102, A2, A4, XXREAL_0: 1;

 end;

 theorem :: BASEL_2:28



 Th28: ( Sum ( sqr ( cot ( x_r-seq m)))) = (((2 * m) * ((2 * m) - 1)) / 6)

 proof

 set C = ( sieve ((PP `^ ((2 * m) + 1)),2));

 set f = ( x_r-seq m);



 A1: ( sqr ( cot f)) is one-to-one by BASEL_1: 28;



 A2: ( len ( sqr ( cot f))) = ( len ( cot f)) = ( len f) = m by CARD_1:def 7, BASEL_1: 21;

 per cases by NAT_1: 14;

 suppose m = 0 ;

 hence thesis by A2, RVSUM_1: 72;

 end;

 suppose

 A3: m >= 1;

 then

 A4: (m + 1) >= (1 + 1) by XREAL_1: 7;

 then

 A5: ((m + 1) -' 2) = ((m + 1) - 2) by XREAL_1: 233;



 A6: ( len C) = (m + 1) by Th25;



 A7: ( len ( sqr ( cot f))) = (( len C) -' 1) by A6, A2, NAT_D: 34;



 A8: ( Roots C) = ( rng ( sqr ( cot ( x_r-seq m)))) by Th27;

 then

 reconsider S = ( sqr ( cot f)) as FinSequence of FC by FINSEQ_1:def 4;



 A9: (( len C) -' 1) = m & (( len C) -' 2) = (m - 1) by A6, NAT_D: 34, A5;

 (((2 * m) + 1) choose 1) = ((2 * m) + 1) by STIRL2_1: 51;



 then

 A10: (C . m) = (((2 * m) + 1) * i_FC ) by Th23

 .= (((2 * m) + 1) * );

 then

 A11: (C . m) <> ( 0. FC);

 (C . (m - 1)) = ((((2 * m) + 1) choose 3) * ( - i_FC )) by Th24, A3

 .= ((((2 * m) + 1) choose 3) * ( - )) by COMPLFLD: 2;



 then

 A12: ((C . (( len C) -' 2)) / (C . m)) = (((((2 * m) + 1) choose 3) * ( - )) / (((2 * m) + 1) * )) by A5, A6, A11, A10, COMPLFLD: 6

 .= ( - (((((2 * m) + 1) choose 3) * ) / (((2 * m) + 1) * )))

 .= ( - ((((2 * m) + 1) choose 3) / ((2 * m) + 1))) by XCMPLX_1: 91

 .= ( - ((((((2 * m) + 1) * (((2 * m) + 1) - 1)) * (((2 * m) + 1) - 2)) / 6) / ((2 * m) + 1))) by STIRL2_1: 51

 .= ( - (((((2 * m) * ((2 * m) - 1)) / ((2 * m) + 1)) / 6) * ((2 * m) + 1)))

 .= ( - (((2 * m) * ((2 * m) - 1)) / 6)) by XCMPLX_1: 97;



 thus ( Sum ( sqr ( cot f))) = ( Sum S) by Th2

 .= ( SumRoots C) by A1, A7, A8, POLYVIE1: 31

 .= ( - ((C . (( len C) -' 2)) / (C . m))) by A4, A6, A9, POLYVIE1: 32

 .= ( - ( - (((2 * m) * ((2 * m) - 1)) / 6))) by A12, COMPLFLD: 2

 .= (((2 * m) * ((2 * m) - 1)) / 6);

 end;

 end;

 theorem :: BASEL_2:29



 Th29: ( Sum ( sqr ( cosec ( x_r-seq m)))) = (((2 * m) * ((2 * m) + 2)) / 6)

 proof

 set f = ( x_r-seq m);



 A1: ( len ( sqr ( cot f))) = ( len ( cot f)) by CARD_1:def 7

 .= ( len f) by CARD_1:def 7

 .= m by BASEL_1: 21;



 A2: ( Sum (1 + ( sqr ( cot f)))) = ((1 * ( len ( sqr ( cot f)))) + ( Sum ( sqr ( cot f)))) by BASEL_1: 4;

 ( Sum ( sqr ( cot f))) = (((2 * m) * ((2 * m) - 1)) / 6) by Th28;

 hence thesis by A1, A2, BASEL_1: 26;

 end;

 theorem :: BASEL_2:30



 Th30: ( Basel-seq1 . m) <= ( Sum ( Basel-seq ,m))

 proof

 set 2m1 = ((2 * m) + 1), 2mI = ((2 * m) - 1);



 A1: (((((2 * m) * 2mI) / 6) / (2m1 ^2 )) / (( PI ^2 ) " )) = (((((2 * m) * 2mI) / (2m1 * 2m1)) * ( PI ^2 )) * (6 " ))

 .= (((((2 * m) / 2m1) * (2mI / 2m1)) * ( PI ^2 )) * (6 " )) by XCMPLX_1: 76

 .= (((( PI ^2 ) / 6) * ((2 * m) / 2m1)) * (2mI / 2m1))

 .= ( Basel-seq1 . m) by BASEL_1: 32;

 ( Sum ( sqr ( cot ( x_r-seq m)))) <= ( Sum (( sqr ( x_r-seq m)) " )) by BASEL_1: 29;

 then (((2 * m) * 2mI) / 6) <= ( Sum (( sqr ( x_r-seq m)) " )) by Th28;

 then (((2 * m) * 2mI) / 6) <= (((2m1 ^2 ) / ( PI ^2 )) * ( Sum ( Basel-seq ,m))) by BASEL_1: 35;

 then (((2 * m) * 2mI) / 6) <= ((2m1 ^2 ) * ((( PI ^2 ) " ) * ( Sum ( Basel-seq ,m))));

 then ((((2 * m) * 2mI) / 6) / (2m1 ^2 )) <= ((( PI ^2 ) " ) * ( Sum ( Basel-seq ,m))) by XREAL_1: 79;

 hence thesis by A1, XREAL_1: 79;

 end;

 theorem :: BASEL_2:31



 Th31: ( Sum ( Basel-seq ,m)) <= ( Basel-seq2 . m)

 proof

 set 2m1 = ((2 * m) + 1), 2m2 = ((2 * m) + 2);



 A1: (((((2 * m) * 2m2) / 6) / (2m1 ^2 )) / (( PI ^2 ) " )) = (((((2 * m) * 2m2) / (2m1 * 2m1)) * ( PI ^2 )) * (6 " ))

 .= (((((2 * m) / 2m1) * (2m2 / 2m1)) * ( PI ^2 )) * (6 " )) by XCMPLX_1: 76

 .= (((( PI ^2 ) / 6) * ((2 * m) / 2m1)) * (2m2 / 2m1))

 .= ( Basel-seq2 . m) by BASEL_1: 33;

 ( Sum ( sqr ( cosec ( x_r-seq m)))) >= ( Sum (( sqr ( x_r-seq m)) " )) by BASEL_1: 30;

 then (((2 * m) * 2m2) / 6) >= ( Sum (( sqr ( x_r-seq m)) " )) by Th29;

 then (((2 * m) * 2m2) / 6) >= (((2m1 ^2 ) / ( PI ^2 )) * ( Sum ( Basel-seq ,m))) by BASEL_1: 35;

 then (((2 * m) * 2m2) / 6) >= ((2m1 ^2 ) * ((( PI ^2 ) " ) * ( Sum ( Basel-seq ,m))));

 then ((((2 * m) * 2m2) / 6) / (2m1 ^2 )) >= ((( PI ^2 ) " ) * ( Sum ( Basel-seq ,m))) by XREAL_1: 77;

 hence thesis by A1, XREAL_1: 77;

 end;

 ::$Notion-Name

 theorem :: BASEL_2:32



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

 proof

 for n holds ( Basel-seq1 . n) <= (( Partial_Sums Basel-seq ) . n) & (( Partial_Sums Basel-seq ) . n) <= ( Basel-seq2 . n)

 proof

 let n;

 ( Sum ( Basel-seq ,n)) = ( Sum ( Basel-seq ,n));

 hence thesis by Th30, Th31;

 end;

 hence thesis by SEQ_2: 20, BASEL_1: 34;

 end;

 registration

 cluster ( Partial_Sums Basel-seq ) -> non summable;

 coherence by Th32, SERIES_1: 4;

 end