defpred S_{1}[ Nat] means for p being Polynomial of L st len p = L holds

odd_part p is odd ;

_{1}[k]
from NAT_1:sch 4(A12);

consider k being Nat such that

A23: len p = k ;

thus odd_part p is odd by A23, A22; :: thesis: verum

odd_part p is odd ;

A12: now :: thesis: for k being Nat st ( for n being Nat st n < k holds

S_{1}[n] ) holds

S_{1}[k]

A22:
for k being Nat holds SS

S

let k be Nat; :: thesis: ( ( for n being Nat st n < k holds

S_{1}[n] ) implies S_{1}[k] )

assume A13: for n being Nat st n < k holds

S_{1}[n]
; :: thesis: S_{1}[k]

_{1}[k]
; :: thesis: verum

end;S

assume A13: for n being Nat st n < k holds

S

now :: thesis: for p being Polynomial of L st len p = k holds

odd_part p is odd

hence
Sodd_part p is odd

let p be Polynomial of L; :: thesis: ( len p = k implies odd_part p is odd )

assume A14: len p = k ; :: thesis: odd_part p is odd

end;assume A14: len p = k ; :: thesis: odd_part p is odd

now :: thesis: ( ( k = 0 & odd_part p is odd ) or ( k <> 0 & odd_part p is odd ) )end;

hence
odd_part p is odd
; :: thesis: verumper cases
( k = 0 or k <> 0 )
;

end;

case A15:
k <> 0
; :: thesis: odd_part p is odd

set LMp = Leading-Monomial p;

set g = Polynomial-Function (L,(Leading-Monomial p));

(Leading-Monomial p) + (p - (Leading-Monomial p)) = ((Leading-Monomial p) + (- (Leading-Monomial p))) + p by POLYNOM3:26

.= ((Leading-Monomial p) - (Leading-Monomial p)) + p

.= (0_. L) + p by POLYNOM3:29

.= p by POLYNOM3:28 ;

then A16: odd_part p = (odd_part (Leading-Monomial p)) + (odd_part (p - (Leading-Monomial p))) by Th16;

consider t being Polynomial of L such that

A17: ( len t < len p & p = t + (Leading-Monomial p) & ( for n being Element of NAT st n < (len p) - 1 holds

t . n = p . n ) ) by A15, A14, POLYNOM4:16;

p - (Leading-Monomial p) = t + ((Leading-Monomial p) - (Leading-Monomial p)) by A17, POLYNOM3:26

.= t + (0_. L) by POLYNOM3:29

.= t by POLYNOM3:28 ;

then A18: odd_part (p - (Leading-Monomial p)) is odd by A17, A13, A14;

end;set g = Polynomial-Function (L,(Leading-Monomial p));

(Leading-Monomial p) + (p - (Leading-Monomial p)) = ((Leading-Monomial p) + (- (Leading-Monomial p))) + p by POLYNOM3:26

.= ((Leading-Monomial p) - (Leading-Monomial p)) + p

.= (0_. L) + p by POLYNOM3:29

.= p by POLYNOM3:28 ;

then A16: odd_part p = (odd_part (Leading-Monomial p)) + (odd_part (p - (Leading-Monomial p))) by Th16;

consider t being Polynomial of L such that

A17: ( len t < len p & p = t + (Leading-Monomial p) & ( for n being Element of NAT st n < (len p) - 1 holds

t . n = p . n ) ) by A15, A14, POLYNOM4:16;

p - (Leading-Monomial p) = t + ((Leading-Monomial p) - (Leading-Monomial p)) by A17, POLYNOM3:26

.= t + (0_. L) by POLYNOM3:29

.= t by POLYNOM3:28 ;

then A18: odd_part (p - (Leading-Monomial p)) is odd by A17, A13, A14;

now :: thesis: ( ( deg p is odd & odd_part (Leading-Monomial p) is odd ) or ( deg p is even & odd_part (Leading-Monomial p) is odd ) )end;

hence
odd_part p is odd
by A18, A16; :: thesis: verumper cases
( deg p is odd or deg p is even )
;

end;

case A19:
deg p is odd
; :: thesis: odd_part (Leading-Monomial p) is odd

then A20:
odd_part (Leading-Monomial p) = Leading-Monomial p
by Th20;

end;now :: thesis: for x being Element of L holds - ((Polynomial-Function (L,(Leading-Monomial p))) . x) = (Polynomial-Function (L,(Leading-Monomial p))) . (- x)

hence
odd_part (Leading-Monomial p) is odd
by A20, Def4; :: thesis: verumlet x be Element of L; :: thesis: - ((Polynomial-Function (L,(Leading-Monomial p))) . x) = (Polynomial-Function (L,(Leading-Monomial p))) . (- x)

(len p) + 1 > 0 + 1 by A14, A15, XREAL_1:8;

then len p >= 1 by NAT_1:13;

then A21: (len p) -' 1 = deg p by XREAL_1:233;

thus - ((Polynomial-Function (L,(Leading-Monomial p))) . x) = - (eval ((Leading-Monomial p),x)) by POLYNOM5:def 13

.= - ((p . ((len p) -' 1)) * ((power L) . (x,((len p) -' 1)))) by POLYNOM4:22

.= (p . ((len p) -' 1)) * (- ((power L) . (x,((len p) -' 1)))) by VECTSP_1:8

.= (p . ((len p) -' 1)) * ((power L) . ((- x),((len p) -' 1))) by A21, A19, Th4

.= eval ((Leading-Monomial p),(- x)) by POLYNOM4:22

.= (Polynomial-Function (L,(Leading-Monomial p))) . (- x) by POLYNOM5:def 13 ; :: thesis: verum

end;(len p) + 1 > 0 + 1 by A14, A15, XREAL_1:8;

then len p >= 1 by NAT_1:13;

then A21: (len p) -' 1 = deg p by XREAL_1:233;

thus - ((Polynomial-Function (L,(Leading-Monomial p))) . x) = - (eval ((Leading-Monomial p),x)) by POLYNOM5:def 13

.= - ((p . ((len p) -' 1)) * ((power L) . (x,((len p) -' 1)))) by POLYNOM4:22

.= (p . ((len p) -' 1)) * (- ((power L) . (x,((len p) -' 1)))) by VECTSP_1:8

.= (p . ((len p) -' 1)) * ((power L) . ((- x),((len p) -' 1))) by A21, A19, Th4

.= eval ((Leading-Monomial p),(- x)) by POLYNOM4:22

.= (Polynomial-Function (L,(Leading-Monomial p))) . (- x) by POLYNOM5:def 13 ; :: thesis: verum

case
deg p is even
; :: thesis: odd_part (Leading-Monomial p) is odd

then
odd_part (Leading-Monomial p) = 0_. L
by Th19;

hence odd_part (Leading-Monomial p) is odd ; :: thesis: verum

end;hence odd_part (Leading-Monomial p) is odd ; :: thesis: verum

consider k being Nat such that

A23: len p = k ;

thus odd_part p is odd by A23, A22; :: thesis: verum