:: Basel Problem
:: by Karol P\kak and Artur Korni{\l}owicz
::
:: Received June 27, 2017
:: Copyright (c) 2017-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XCMPLX_0, SUBSET_1, FUNCT_1, ARYTM_3, ORDINAL4, COMPLEX1,
NUMBERS, RELAT_1, NEWTON, NAT_1, CARD_3, SQUARE_1, SIN_COS, CARD_1,
XXREAL_0, SEQ_1, VALUED_0, SERIES_1, PARTFUN1, XBOOLE_0, ARYTM_1,
FINSEQ_1, RVSUM_1, TARSKI, XXREAL_1, SIN_COS4, ABIAN, ALGSTR_1, ALGSTR_0,
VECTSP_1, SUPINF_2, BINOP_1, MESFUNC1, STRUCT_0, RLVECT_1, LATTICES,
GROUP_1, POLYNOM3, ALGSEQ_1, POLYNOM1, POLYNOM2, QC_LANG1, FUNCSDOM,
HAHNBAN1, COMPLFLD, AFINSQ_1, CQC_LANG, POLYNOM5, HURWITZ2, XREAL_0,
UPROOTS, VECTSP_2, POLYVIE1, BASEL_1, BASEL_2;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, FUNCT_1, RELSET_1, PARTFUN1,
FUNCT_2, BINOP_1, NUMBERS, XXREAL_0, XCMPLX_0, COMPLEX1, XREAL_0, NAT_1,
NAT_D, SQUARE_1, CARD_1, FINSEQ_1, VALUED_0, VALUED_1, RVSUM_1, SEQ_1,
STRUCT_0, ALGSTR_0, RLVECT_1, GROUP_1, VECTSP_1, NORMSP_1, ALGSTR_1,
ALGSEQ_1, COMPLFLD, HAHNBAN1, RCOMP_1, SERIES_1, NEWTON, ABIAN, SIN_COS,
SIN_COS4, BINOM, HURWITZ2, POLYNOM3, POLYNOM4, POLYNOM5, UPROOTS,
VECTSP_2, NIVEN, POLYVIE1, BASEL_1;
constructors SEQ_2, REAL_1, SIN_COS, SQUARE_1, COMSEQ_2, RELSET_1, COMSEQ_3,
SIN_COS4, ABIAN, INTEGRA1, NAT_D, ALGSEQ_1, ALGSTR_1, HAHNBAN1, POLYNOM4,
POLYNOM5, BINOM, BINOP_2, HURWITZ2, NIVEN, WSIERP_1, REALSET2, POLYVIE1,
BASEL_1;
registrations XCMPLX_0, NEWTON, XREAL_0, NAT_1, ORDINAL1, SQUARE_1, VALUED_0,
RELSET_1, VALUED_1, MEMBERED, INT_1, SIN_COS, SIN_COS6, ABIAN, XBOOLE_0,
XXREAL_0, FINSEQ_1, CARD_1, RVSUM_1, STRUCT_0, VECTSP_1, ALGSTR_1,
POLYNOM3, ALGSTR_0, NEWTON01, COMPLEX1, COMPLFLD, POLYNOM5, HURWITZ2,
NIVEN, ALGSEQ_1, RLVECT_1, UPROOTS, INT_6, FINSET_1, POLYNOM4, NEWTON04,
BASEL_1;
requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
definitions TARSKI, FUNCT_2, HURWITZ2, ALGSEQ_1;
equalities SERIES_1, SIN_COS, SIN_COS4, XCMPLX_0, SQUARE_1, FINSEQ_1,
POLYNOM3, HAHNBAN1, POLYNOM5, BINOM;
theorems SEQ_2, ORDINAL1, PREPOWER, XCMPLX_1, VALUED_1, XREAL_1, XXREAL_0,
SERIES_1, FUNCT_1, FINSEQ_3, XXREAL_1, NAT_1, XREAL_0, FINSEQ_1, RVSUM_1,
ABIAN, COMPTRIG, FUNCT_2, XBOOLE_0, PARTFUN1, CARD_1, RVSUM_2, FUNCOP_1,
RLVECT_1, NORMSP_1, ALGSEQ_1, GROUP_1, POLYNOM2, POLYNOM3, ALGSTR_1,
XCMPLX_0, POLYNOM5, BINOM, NEWTON, UPROOTS, HURWITZ2, COMPLEX1, MATRIX_5,
STRUCT_0, COMPLFLD, POLYNOM4, NIVEN, CARD_2, HAHNBAN1, POLYVIE1,
VECTSP_1, NAT_D, STIRL2_1, FINSEQ_5, BASEL_1;
schemes NAT_1, FUNCT_2;
begin :: Preliminaries
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 being 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 being Nat holds P[i] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
end;
theorem Th1:
for z being Complex, e being 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 being 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 being 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*e with n*z when e = z;
correctness by Th1;
end;
theorem Th2:
for Z being complex-valued FinSequence, E being 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 being 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 Th3:
(1_F_Complex) |^ n = 1_F_Complex
proof
thus (1_FC) |^ n = 1r|^n by COMPLFLD:8,74
.= 1_FC by COMPLFLD:8,COMPLEX1:def 4;
end;
theorem Th4:
for L being left_zeroed right_zeroed non empty addLoopStr
for z0,z1 being 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,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,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,38;
then (<%z0%> + <%0.L,z1%>).n = 0.L by A1, ALGSTR_1:def 2;
hence thesis by A4,POLYNOM5:38;
end;
end;
theorem Th5:
for L being add-associative right_zeroed right_complementable
distributive non empty doubleLoopStr
for a,b,c,d being 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;
then 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 being 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 Th6:
for L being 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 Th7:
for L being right_zeroed add-associative right_complementable
right-distributive non empty doubleLoopStr
for z being Element of L, p being 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,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 Th8:
for L being Abelian add-associative right_zeroed right_complementable
well-unital associative commutative distributive non empty doubleLoopStr
for x being 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 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 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 Th11:
for L being domRing, p being 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 being 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 being 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 being 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 being 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;
func @a -> Element of the carrier 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;
:: func n * a -> Polynomial of L equals
:: n * @a;
:: coherence by POLYNOM3:def 10;
::end;
definition
let L be add-associative right_zeroed right_complementable distributive
non empty doubleLoopStr;
let a be Element of the carrier of Polynom-Ring L;
func ~a -> Polynomial of L equals
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,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 Th12:
for L being add-associative right_zeroed right_complementable distributive
non empty doubleLoopStr
for a being 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 being 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 being Nat holds P[i] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem 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 being 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 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 being sequence of the carrier of PRR such that
A10:Sum F = f.(len F) and
A11:f.0 = 0.PRR & for j being Nat for v being 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 being 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 being Polynomial of R st
p = f.$1 holds p.k = 0.R;
A14:P[0] by A12;
A15:for i being 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 being 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 being Polynomial of R st p = f.$1 holds p.k = 0.R;
A24:P[0] by A12;
A25:for i being 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 being Nat holds P[i] from NAT_1:sch 2(A24,A25);
defpred R[Nat] means $1 <= n implies for p being 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 being 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 being Nat st k <= i holds R[i] from NAT_1:sch 8(A34,A39);
hence thesis by A10,A1,A23,A2;
end;
end;
begin :: Imaginary complex numbers
definition
let z be Complex;
attr z is imaginary means :Def3:
Re z = 0;
end;
registration
cluster <i> -> 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 for Complex;
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;
attr p is imaginary means:Def4:
for i being 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 Th14:
for I being imaginary Polynomial of F_Complex
for r being 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 being sequence of the carrier of FC such that
A3:Sum H = h.(len H) and
A4:h.0 = 0.FC & for j being Nat for v being 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 Th15:
for R being real Polynomial of F_Complex
for r being 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 being sequence of the carrier of FC such that
A3:Sum H = h.(len H) and
A4:h.0 = 0.FC & for j being Nat for v being 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
for im being imaginary Element of F_Complex,
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
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 Th17:
for im being imaginary Element of F_Complex,
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
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 Th18:
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
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 :: Main facts
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:
for i being Nat holds it.i = p.(m*i);
existence
proof
defpred P[object,object] means
for i being Nat st i = $1 holds $2 = p.(m*i);
A1:for x be object st x in NAT ex y being 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 being Function of NAT,L such that
A2: for x being 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 being Nat holds s1.i = p.(m*i) and
A4: for i being 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 Th19:
for L being non empty ZeroStr
for p being 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 Th20:
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
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 Th21:
for L being non empty ZeroStr
for p being Polynomial of L st len even_part p = 0
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 Th22:
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
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 being sequence of Polynom-Ring L such that
A3:Sum F = f.(len F) and
A4:f.0 = 0.Polynom-Ring L & for j being Nat
for v being 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 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 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
.= -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 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,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 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)+<i>) |^ 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 <i>*sin(f.x)/sin(f.x) = <i> by XCMPLX_1:89;
then (cot(f.x)+<i>) |^ N = ((cos(f.x)+<i>*sin(f.x))/sin(f.x)) |^ N
.= ( (cos(f.x) + <i>*sin(f.x)) |^ N) / ((sin(f.x)) |^ N) by PREPOWER:8
.= (cos(N*f.x) + <i>*sin(N*f.x)) / ((sin(f.x)) |^ N) by COMPTRIG:53
.= (cos(N*f.x) + <i>*sin(x*PI)) / ((sin(f.x)) |^ N) by A8,BASEL_1:25
.= (cos(N*f.x) + <i>*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)+<i>) |^ 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)+<i>) |^ 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*<i> 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 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 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) * <i>;
then
A11: C.m <>0.FC;
C.(m-1)=((2*m+1) choose 3) * (-i_FC) by Th24,A3
.= ((2*m+1) choose 3) * (- <i>);
then
A12: C.(len C-'2) / C.m = ((2*m+1) choose 3) * (- <i>) / ((2*m+1) * <i>)
by A5,A6,A11,A10,COMPLFLD:6
.= -(((2*m+1) choose 3) * <i>) / ((2*m+1) * <i>)
.= -((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;
end;
end;
theorem 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 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 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;
::$N Basel problem
::$L https://en.wikipedia.org/wiki/Basel_problem Basel problem
theorem 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 for Real_Sequence;
coherence by Th32,SERIES_1:4;
end;