defpred S1[ Nat] means for p being Polynomial of L st len p = L holds
odd_part p is odd ;
A12:
now for k being Nat st ( for n being Nat st n < k holds
S1[n] ) holds
S1[k]let k be
Nat;
( ( for n being Nat st n < k holds
S1[n] ) implies S1[k] )assume A13:
for
n being
Nat st
n < k holds
S1[
n]
;
S1[k]now for p being Polynomial of L st len p = k holds
odd_part p is odd let p be
Polynomial of
L;
( len p = k implies odd_part p is odd )assume A14:
len p = k
;
odd_part p is odd now ( ( k = 0 & odd_part p is odd ) or ( k <> 0 & odd_part p is odd ) )per cases
( k = 0 or k <> 0 )
;
case A15:
k <> 0
;
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;
now ( ( deg p is odd & odd_part (Leading-Monomial p) is odd ) or ( deg p is even & odd_part (Leading-Monomial p) is odd ) )per cases
( deg p is odd or deg p is even )
;
case A19:
deg p is
odd
;
odd_part (Leading-Monomial p) is odd then A20:
odd_part (Leading-Monomial p) = Leading-Monomial p
by Th20;
now for x being Element of L holds - ((Polynomial-Function (L,(Leading-Monomial p))) . x) = (Polynomial-Function (L,(Leading-Monomial p))) . (- x)let x be
Element of
L;
- ((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
;
verum end; hence
odd_part (Leading-Monomial p) is
odd
by A20, Def4;
verum end; end; end; hence
odd_part p is
odd
by A18, A16;
verum end; end; end; hence
odd_part p is
odd
;
verum end; hence
S1[
k]
;
verum end;
A22:
for k being Nat holds S1[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; verum