let L be Field; :: thesis: for p being Polynomial of L holds even_part p = Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>)
let p be Polynomial of L; :: thesis: even_part p = Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>)
set C = sieve (p,2);
set x2 = <%(0. L),(0. L),(1_ L)%>;
set Cx = Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>);
set E = even_part p;
consider F being FinSequence of (Polynom-Ring L) such that
A1: ( Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>) = Sum F & len F = len (sieve (p,2)) ) and
A2: for n being Element of NAT st n in dom F holds
F . n = ((sieve (p,2)) . (n -' 1)) * (<%(0. L),(0. L),(1_ L)%> `^ (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 ; :: according to FUNCT_2:def 8 :: thesis: (even_part p) . n = (Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>)) . n
per cases ( n is odd or n is even ) ;
suppose A5: n is odd ; :: thesis: (even_part p) . n = (Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>)) . n
defpred S1[ Nat] means ( $1 <= len F implies for P being Polynomial of L st P = f . $1 holds
P . n = 0. L );
A6: S1[ 0 ]
proof
assume 0 <= len F ; :: thesis: for P being Polynomial of L st P = f . 0 holds
P . n = 0. L
let P be Polynomial of L; :: thesis: ( P = f . 0 implies P . n = 0. L )
assume P = f . 0 ; :: thesis: P . n = 0. L
then P = 0_. L by A4, POLYNOM3:def 10;
hence P . n = 0. L by FUNCOP_1:7; :: thesis: verum
end;
A7: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A8: S1[k] ; :: thesis: S1[k + 1]
set k1 = k + 1;
assume A9: k + 1 <= len F ; :: thesis: for P being Polynomial of L st P = f . (k + 1) holds
P . n = 0. L
let P be Polynomial of L; :: thesis: ( P = f . (k + 1) implies P . n = 0. L )
assume A10: P = f . (k + 1) ; :: thesis: P . n = 0. L
A11: (k + 1) -' 1 = (k + 1) - 1 by NAT_1:11, XREAL_1:233;
k + 1 in dom F by A9, NAT_1:11, FINSEQ_3:25;
then A12: F . (k + 1) = ((sieve (p,2)) . k) * (<%(0. L),(0. L),(1_ L)%> `^ k) by A11, A2;
then reconsider Fk1 = F . (k + 1) 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 + (((sieve (p,2)) . k) * (<%(0. L),(0. L),(1_ L)%> `^ k)) by A12, POLYNOM3:def 10 ;
A14: fk . n = 0. L by A9, NAT_1:13, A8;
n <> 2 * k by A5;
then (<%(0. L),(0. L),(1_ L)%> `^ k) . n = 0. L by Th10;
then (((sieve (p,2)) . k) * (<%(0. L),(0. L),(1_ L)%> `^ k)) . n = ((sieve (p,2)) . k) * (0. L) by POLYNOM5:def 4
.= 0. L ;
then P . n = (0. L) + (0. L) by A13, A14, NORMSP_1:def 2;
hence P . n = 0. L ; :: thesis: verum
end;
for k being Nat holds S1[k] from NAT_1:sch 2(A6, A7);
then (Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>)) . n = 0. L by A1, A3;
hence (even_part p) . n = (Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>)) . n by A5, HURWITZ2:def 1; :: thesis: verum
end;
suppose A15: n is even ; :: thesis: (even_part p) . n = (Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>)) . n
then consider m being Nat such that
A16: 2 * m = n by ABIAN:def 2;
set m1 = m + 1;
per cases ( m < len F or m >= len F ) ;
suppose A17: m < len F ; :: thesis: (even_part p) . n = (Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>)) . n
defpred S1[ Nat] means ( $1 <= len F implies for P being Polynomial of L st P = f . $1 holds
P . n = p . n );
defpred S2[ Nat] means ( $1 <= m implies for P being Polynomial of L st P = f . $1 holds
P . n = 0. L );
A18: S2[ 0 ]
proof
assume 0 <= m ; :: thesis: for P being Polynomial of L st P = f . 0 holds
P . n = 0. L
let P be Polynomial of L; :: thesis: ( P = f . 0 implies P . n = 0. L )
assume P = f . 0 ; :: thesis: P . n = 0. L
then P = 0_. L by A4, POLYNOM3:def 10;
hence P . n = 0. L by FUNCOP_1:7; :: thesis: verum
end;
A19: for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
assume A20: S2[k] ; :: thesis: S2[k + 1]
set k1 = k + 1;
assume A21: k + 1 <= m ; :: thesis: for P being Polynomial of L st P = f . (k + 1) holds
P . n = 0. L
then A22: k < m by NAT_1:13;
let P be Polynomial of L; :: thesis: ( P = f . (k + 1) implies P . n = 0. L )
assume A23: P = f . (k + 1) ; :: thesis: P . n = 0. L
A24: (k + 1) -' 1 = (k + 1) - 1 by NAT_1:11, XREAL_1:233;
A25: ( k < len F & k + 1 <= len F ) by A22, A17, A21, XXREAL_0:2;
then k + 1 in dom F by NAT_1:11, FINSEQ_3:25;
then A26: F . (k + 1) = ((sieve (p,2)) . k) * (<%(0. L),(0. L),(1_ L)%> `^ k) by A24, A2;
then reconsider Fk1 = F . (k + 1) 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 + (((sieve (p,2)) . k) * (<%(0. L),(0. L),(1_ L)%> `^ 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 (<%(0. L),(0. L),(1_ L)%> `^ k) . n = 0. L by Th10;
then (((sieve (p,2)) . k) * (<%(0. L),(0. L),(1_ L)%> `^ k)) . n = ((sieve (p,2)) . k) * (0. L) by POLYNOM5:def 4
.= 0. L ;
then P . n = (0. L) + (0. L) by A27, A28, NORMSP_1:def 2;
hence P . n = 0. L ; :: thesis: verum
end;
A29: for k being Nat holds S2[k] from NAT_1:sch 2(A18, A19);
A30: S1[m + 1]
proof
assume A31: m + 1 <= len F ; :: thesis: for P being Polynomial of L st P = f . (m + 1) holds
P . n = p . n
let P be Polynomial of L; :: thesis: ( P = f . (m + 1) implies P . n = p . n )
assume A32: P = f . (m + 1) ; :: thesis: P . n = p . n
reconsider fm = f . m as Polynomial of L by POLYNOM3:def 10;
A33: 1 <= m + 1 by NAT_1:11;
A34: (m + 1) -' 1 = (m + 1) - 1 by NAT_1:11, XREAL_1:233;
A35: F . (m + 1) = ((sieve (p,2)) . m) * (<%(0. L),(0. L),(1_ L)%> `^ m) by A34, A2, A33, A31, FINSEQ_3:25;
then reconsider Fm1 = F . (m + 1) as Element of (Polynom-Ring L) by POLYNOM3:def 10;
A36: P = (f . m) + Fm1 by A32, A31, NAT_1:13, A4
.= fm + (((sieve (p,2)) . m) * (<%(0. L),(0. L),(1_ L)%> `^ m)) by A35, POLYNOM3:def 10 ;
A37: fm . n = 0. L by A29;
(<%(0. L),(0. L),(1_ L)%> `^ m) . n = 1_ L by A16, Th10;
then (((sieve (p,2)) . m) * (<%(0. L),(0. L),(1_ L)%> `^ m)) . n = ((sieve (p,2)) . m) * (1_ L) by POLYNOM5:def 4
.= (sieve (p,2)) . m ;
then P . n = (0. L) + ((sieve (p,2)) . m) by A36, A37, NORMSP_1:def 2;
hence P . n = p . n by Def5, A16; :: thesis: verum
end;
A38: for k being Nat st m + 1 <= k & S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( m + 1 <= k & S1[k] implies S1[k + 1] )
set k1 = k + 1;
assume A39: ( m + 1 <= k & S1[k] ) ; :: thesis: S1[k + 1]
assume A40: k + 1 <= len F ; :: thesis: for P being Polynomial of L st P = f . (k + 1) holds
P . n = p . n
let P be Polynomial of L; :: thesis: ( P = f . (k + 1) implies P . n = p . n )
assume A41: P = f . (k + 1) ; :: thesis: P . n = p . n
A42: (k + 1) -' 1 = (k + 1) - 1 by NAT_1:11, XREAL_1:233;
k + 1 in dom F by A40, NAT_1:11, FINSEQ_3:25;
then A43: F . (k + 1) = ((sieve (p,2)) . k) * (<%(0. L),(0. L),(1_ L)%> `^ k) by A42, A2;
then reconsider Fk1 = F . (k + 1) 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 + (((sieve (p,2)) . k) * (<%(0. L),(0. L),(1_ L)%> `^ 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 (<%(0. L),(0. L),(1_ L)%> `^ k) . n = 0. L by Th10;
then (((sieve (p,2)) . k) * (<%(0. L),(0. L),(1_ L)%> `^ k)) . n = ((sieve (p,2)) . k) * (0. L) by POLYNOM5:def 4
.= 0. L ;
then P . n = (p . n) + (0. L) by A44, A45, NORMSP_1:def 2;
hence P . n = p . n ; :: thesis: verum
end;
A46: for k being Nat st m + 1 <= k holds
S1[k] from NAT_1:sch 8(A30, A38);
 m + 1 <= len F by A17, NAT_1:13;
then (Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>)) . n = p . n by A1, A3, A46;
hence (even_part p) . n = (Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>)) . n by A15, HURWITZ2:def 1; :: thesis: verum
end;
suppose A47: m >= len F ; :: thesis: (even_part p) . n = (Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>)) . n
then A48: 2 * m >= 2 * (len (sieve (p,2))) by A1, XREAL_1:64;
A49: len (even_part p) is_at_least_length_of even_part p by ALGSEQ_1:def 3;
2 * m >= len (even_part p) then A50: (even_part p) . n = 0. L by A16, ALGSEQ_1:def 2, A49;
A51: len (Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>)) is_at_least_length_of Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>) by ALGSEQ_1:def 3;
D: 2 = 2 * 1 ;
2 * m >= len (Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>))
proof
per cases ( len (even_part p) = 0 or len (even_part p) > 0 ) ;
suppose len (even_part p) = 0 ; :: thesis: 2 * m >= len (Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>))
then len (sieve (p,2)) = 0 by D, Th21;
then sieve (p,2) = 0_. L by POLYNOM4:5;
then Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>) = 0_. L by POLYNOM5:49;
hence 2 * m >= len (Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>)) by POLYNOM4:3; :: thesis: verum
end;
suppose len (even_part p) > 0 ; :: thesis: 2 * m >= len (Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>))
then 2 * (len (sieve (p,2))) = (len (even_part p)) + 1 by Th18, Th20;
then A52: len (sieve (p,2)) <> 0 ;
len <%(0. L),(0. L),(1_ L)%> = 3 by NIVEN:28;
then len (Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>)) = ((((len (sieve (p,2))) * 3) - (len (sieve (p,2)))) - 3) + 2 by A52, POLYNOM5:52
.= ((len (sieve (p,2))) * 2) - 1 ;
then 2 * m >= (len (Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>))) + 1 by A47, A1, XREAL_1:64;
hence 2 * m >= len (Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>)) by NAT_1:13; :: thesis: verum
end;
end;
end;
hence (even_part p) . n = (Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>)) . n by A16, A50, ALGSEQ_1:def 2, A51; :: thesis: verum
end;
end;
end;
end;