let R be non degenerated Ring; for n being non zero Nat
for a, x being Element of R holds eval ((anpoly (a,n)),x) = a * (x |^ n)
let n be non zero Nat; for a, x being Element of R holds eval ((anpoly (a,n)),x) = a * (x |^ n)
let a, x be Element of R; eval ((anpoly (a,n)),x) = a * (x |^ n)
set q = anpoly (a,n);
per cases
( a = 0. R or a <> 0. R )
;
suppose
a <> 0. R
;
eval ((anpoly (a,n)),x) = a * (x |^ n)then A2:
not
a is
zero
;
consider F being
FinSequence of
R such that A3:
eval (
(anpoly (a,n)),
x)
= Sum F
and A4:
len F = len (anpoly (a,n))
and A5:
for
j being
Element of
NAT st
j in dom F holds
F . j = ((anpoly (a,n)) . (j -' 1)) * ((power R) . (x,(j -' 1)))
by POLYNOM4:def 2;
n =
deg (anpoly (a,n))
by A2, Lm1
.=
(len (anpoly (a,n))) - 1
;
then A7:
dom F = Seg (n + 1)
by A4, FINSEQ_1:def 3;
A8:
1
<= n + 1
by NAT_1:11;
A9:
(n + 1) -' 1
= (n + 1) - 1
by NAT_1:11, XREAL_1:233;
A10:
F /. (n + 1) =
F . (n + 1)
by A7, FINSEQ_1:3, PARTFUN1:def 6
.=
((anpoly (a,n)) . n) * ((power R) . (x,((n + 1) -' 1)))
by A9, A5, A8, A7, FINSEQ_1:1
.=
a * ((power R) . (x,((n + 1) -' 1)))
by POLYDIFF:24
.=
a * (x |^ n)
by A9, BINOM:def 2
;
now for j being Element of NAT st j in dom F & j <> n + 1 holds
F /. j = 0. Rlet j be
Element of
NAT ;
( j in dom F & j <> n + 1 implies F /. j = 0. R )assume A11:
(
j in dom F &
j <> n + 1 )
;
F /. j = 0. Rthen A12:
( 1
<= j &
j <= n + 1 )
by A7, FINSEQ_1:1;
then
j < n + 1
by A11, XXREAL_0:1;
then A13:
( 1
<= j &
j <= n )
by A11, NAT_1:13, A7, FINSEQ_1:1;
A14:
j -' 1
= j - 1
by A12, XREAL_0:def 2;
A15:
j - 1
< j - 0
by XREAL_1:15;
thus F /. j =
F . j
by A11, PARTFUN1:def 6
.=
((anpoly (a,n)) . (j -' 1)) * ((power R) . (x,(j -' 1)))
by A5, A11
.=
(0. R) * ((power R) . (x,(j -' 1)))
by A15, A13, A14, POLYDIFF:25
.=
0. R
;
verum end; hence
eval (
(anpoly (a,n)),
x)
= a * (x |^ n)
by A3, A10, A7, FINSEQ_1:3, POLYNOM2:3;
verum end;