let n be Nat; for fp being FinSequence of INT st len fp = n + 2 holds
for a being Integer ex fr being FinSequence of INT ex r being Integer st
( len fr = n + 1 & ( for x being Element of INT holds (Poly-INT fp) . x = ((x - a) * ((Poly-INT fr) . x)) + r ) & fp . (n + 2) = fr . (n + 1) )
let fp be FinSequence of INT ; ( len fp = n + 2 implies for a being Integer ex fr being FinSequence of INT ex r being Integer st
( len fr = n + 1 & ( for x being Element of INT holds (Poly-INT fp) . x = ((x - a) * ((Poly-INT fr) . x)) + r ) & fp . (n + 2) = fr . (n + 1) ) )
assume A1:
len fp = n + 2
; for a being Integer ex fr being FinSequence of INT ex r being Integer st
( len fr = n + 1 & ( for x being Element of INT holds (Poly-INT fp) . x = ((x - a) * ((Poly-INT fr) . x)) + r ) & fp . (n + 2) = fr . (n + 1) )
(n + 1) + 1 in Seg ((n + 1) + 1)
by FINSEQ_1:4;
then
n + 2 in dom fp
by A1, FINSEQ_1:def 3;
then reconsider A = fp . (n + 2) as Element of INT by FINSEQ_2:11;
reconsider n1 = n + 1 as Element of NAT ;
let a be Integer; ex fr being FinSequence of INT ex r being Integer st
( len fr = n + 1 & ( for x being Element of INT holds (Poly-INT fp) . x = ((x - a) * ((Poly-INT fr) . x)) + r ) & fp . (n + 2) = fr . (n + 1) )
defpred S1[ Nat, Integer, set ] means $3 = (fp . ((n + 2) - $1)) + (a * $2);
A2:
for d being Nat st 1 <= d & d < n1 holds
for x being Element of INT ex y being Element of INT st S1[d,x,y]
proof
let d be
Nat;
( 1 <= d & d < n1 implies for x being Element of INT ex y being Element of INT st S1[d,x,y] )
assume that
1
<= d
and
d < n1
;
for x being Element of INT ex y being Element of INT st S1[d,x,y]
let x be
Element of
INT ;
ex y being Element of INT st S1[d,x,y]
set y =
(fp . ((n + 2) - d)) + (a * x);
reconsider y =
(fp . ((n + 2) - d)) + (a * x) as
Element of
INT by INT_1:def 2;
take
y
;
S1[d,x,y]
thus
S1[
d,
x,
y]
;
verum
end;
consider p being FinSequence of INT such that
A3:
( len p = n1 & ( p . 1 = A or n1 = 0 ) & ( for d being Nat st 1 <= d & d < n1 holds
S1[d,p . d,p . (d + 1)] ) )
from RECDEF_1:sch 4(A2);
take fr = Rev p; ex r being Integer st
( len fr = n + 1 & ( for x being Element of INT holds (Poly-INT fp) . x = ((x - a) * ((Poly-INT fr) . x)) + r ) & fp . (n + 2) = fr . (n + 1) )
take r = (fp . 1) + (a * (fr . 1)); ( len fr = n + 1 & ( for x being Element of INT holds (Poly-INT fp) . x = ((x - a) * ((Poly-INT fr) . x)) + r ) & fp . (n + 2) = fr . (n + 1) )
A4:
len fr = n + 1
by A3, FINSEQ_5:def 3;
for x being Element of INT holds (Poly-INT fp) . x = ((x - a) * ((Poly-INT fr) . x)) + r
proof
let x be
Element of
INT ;
(Poly-INT fp) . x = ((x - a) * ((Poly-INT fr) . x)) + r
deffunc H1(
Nat)
-> set =
(fr . $1) * (x |^ $1);
deffunc H2(
Nat)
-> set =
(a * (fr . $1)) * (x |^ ($1 -' 1));
consider f1 being
FinSequence of
INT such that A5:
len f1 = len fp
and A6:
for
d being
Nat st
d in dom f1 holds
f1 . d = (fp . d) * (x |^ (d -' 1))
and A7:
(Poly-INT fp) . x = Sum f1
by Def1;
A8:
f1 <> {}
by A1, A5;
then
n + 2
in dom f1
by A1, A5, FINSEQ_5:6;
then
f1 . (n + 2) = (fp . (n + 2)) * (x |^ (((n + 1) + 1) -' 1))
by A6;
then A9:
f1 . (n + 2) = (fp . (n + 2)) * (x |^ (n + 1))
by NAT_D:34;
f1 . 1
= (fp . 1) * (x |^ (1 -' 1))
by A6, A8, FINSEQ_5:6;
then
f1 . 1
= (fp . 1) * (x |^ 0)
by XREAL_1:232;
then A10:
f1 . 1
= (fp . 1) * 1
by NEWTON:4;
reconsider n =
n as
Element of
NAT by ORDINAL1:def 12;
consider f4 being
FinSequence such that A11:
(
len f4 = n + 1 & ( for
d being
Nat st
d in dom f4 holds
f4 . d = H1(
d) ) )
from FINSEQ_1:sch 2();
A12:
for
d being
Nat st
d in dom f4 holds
f4 . d in INT
f4 <> {}
by A11;
then
n + 1
in dom f4
by A11, FINSEQ_5:6;
then
f4 . (n + 1) = (fr . (n + 1)) * (x |^ (n + 1))
by A11;
then A13:
f4 . (n + 1) = (fp . (n + 2)) * (x |^ (n + 1))
by A3, FINSEQ_5:62;
reconsider f4 =
f4 as
FinSequence of
INT by A12, FINSEQ_2:12;
consider f5 being
FinSequence such that A14:
(
len f5 = n + 1 & ( for
d being
Nat st
d in dom f5 holds
f5 . d = H2(
d) ) )
from FINSEQ_1:sch 2();
A15:
for
d being
Nat st
d in dom f5 holds
f5 . d in INT
f5 <> {}
by A14;
then
1
in dom f5
by FINSEQ_5:6;
then
f5 . 1
= (a * (fr . 1)) * (x |^ (1 -' 1))
by A14;
then
f5 . 1
= (a * (fr . 1)) * (x |^ 0)
by XREAL_1:232;
then A16:
f5 . 1
= (a * (fr . 1)) * 1
by NEWTON:4;
reconsider f5 =
f5 as
FinSequence of
INT by A15, FINSEQ_2:12;
A17:
f4 is
FinSequence of
REAL
by FINSEQ_3:117;
consider f2 being
FinSequence of
INT such that A18:
len f2 = len fr
and A19:
for
d being
Nat st
d in dom f2 holds
f2 . d = (fr . d) * (x |^ (d -' 1))
and A20:
(Poly-INT fr) . x = Sum f2
by Def1;
set f3 =
(x - a) * f2;
A21:
dom ((x - a) * f2) = dom f2
by VALUED_1:def 5;
then A22:
len ((x - a) * f2) = len f2
by FINSEQ_3:29;
A23:
dom ((x - a) * f2) = dom f4
by A4, A18, A11, A21, FINSEQ_3:29;
A24:
for
k being
Element of
NAT st
k in dom ((x - a) * f2) holds
((x - a) * f2) . k = ((fr . k) * (x |^ k)) - ((a * (fr . k)) * (x |^ (k -' 1)))
A28:
dom ((x - a) * f2) = dom f5
by A4, A18, A14, A21, FINSEQ_3:29;
A29:
for
d being
Nat st
d in dom ((x - a) * f2) holds
((x - a) * f2) . d = (f4 . d) - (f5 . d)
f5 is
FinSequence of
REAL
by FINSEQ_3:117;
then consider f6 being
FinSequence of
REAL such that A32:
len f6 = (len ((x - a) * f2)) - 1
and A33:
for
d being
Nat st
d in dom f6 holds
f6 . d = (f4 . d) - (f5 . (d + 1))
and A34:
Sum ((x - a) * f2) = ((Sum f6) + (f4 . (n + 1))) - (f5 . 1)
by A4, A18, A11, A14, A22, A29, A17, Th5;
A35:
len f6 <= len ((x - a) * f2)
by A4, A18, A22, A32, XREAL_1:145;
then A36:
dom f6 c= dom ((x - a) * f2)
by FINSEQ_3:30;
A37:
for
d being
Element of
NAT st
d in dom f6 holds
f6 . d = f1 . (d + 1)
proof
let d be
Element of
NAT ;
( d in dom f6 implies f6 . d = f1 . (d + 1) )
A38:
dom f6 c= dom p
by A3, A4, A18, A22, A35, FINSEQ_3:30;
assume A39:
d in dom f6
;
f6 . d = f1 . (d + 1)
then A40:
d in Seg n
by A4, A18, A22, A32, FINSEQ_1:def 3;
then A41:
d <= n
by FINSEQ_1:1;
then A42:
n - d >= 0
by XREAL_1:48;
then reconsider d9 =
(n - d) + 1 as
Element of
NAT by INT_1:3;
d >= 1
by A40, FINSEQ_1:1;
then
n - d <= n - 1
by XREAL_1:10;
then
d9 <= (n - 1) + 1
by XREAL_1:6;
then A43:
d9 < n + 1
by XREAL_1:145;
d9 >= 0 + 1
by A42, XREAL_1:6;
then A44:
p . (d9 + 1) = (fp . ((n + 2) - d9)) + (a * (p . d9))
by A3, A43;
d < n + 1
by A41, XREAL_1:145;
then A45:
d + 1
in Seg (n + 1)
by FINSEQ_3:11;
then A46:
d + 1
in dom f5
by A14, FINSEQ_1:def 3;
d + 0 < n + 2
by A41, XREAL_1:8;
then
d + 1
in Seg (n + 2)
by FINSEQ_3:11;
then A47:
d + 1
in dom f1
by A1, A5, FINSEQ_1:def 3;
A48:
d + 1
in dom p
by A3, A45, FINSEQ_1:def 3;
thus f6 . d =
(f4 . d) - (f5 . (d + 1))
by A33, A39
.=
((fr . d) * (x |^ d)) - (f5 . (d + 1))
by A11, A23, A36, A39
.=
((fr . d) * (x |^ d)) - ((a * (fr . (d + 1))) * (x |^ ((d + 1) -' 1)))
by A14, A46
.=
((fr . d) * (x |^ d)) - ((a * (fr . (d + 1))) * (x |^ d))
by NAT_D:34
.=
((fr . d) - (a * (fr . (d + 1)))) * (x |^ d)
.=
((p . (((n + 1) - d) + 1)) - (a * (fr . (d + 1)))) * (x |^ d)
by A3, A39, A38, FINSEQ_5:58
.=
((p . (((n - d) + 1) + 1)) - (a * (p . (((n + 1) - (d + 1)) + 1)))) * (x |^ d)
by A3, A48, FINSEQ_5:58
.=
(fp . (d + 1)) * (x |^ ((d + 1) -' 1))
by A44, NAT_D:34
.=
f1 . (d + 1)
by A6, A47
;
verum
end;
f1 = (<*(f1 . 1)*> ^ f6) ^ <*(f1 . (n + 2))*>
proof
set K =
(<*(f1 . 1)*> ^ f6) ^ <*(f1 . (n + 2))*>;
A49:
for
d being
Nat st
d in dom f1 holds
f1 . d = ((<*(f1 . 1)*> ^ f6) ^ <*(f1 . (n + 2))*>) . d
proof
let d be
Nat;
( d in dom f1 implies f1 . d = ((<*(f1 . 1)*> ^ f6) ^ <*(f1 . (n + 2))*>) . d )
assume A50:
d in dom f1
;
f1 . d = ((<*(f1 . 1)*> ^ f6) ^ <*(f1 . (n + 2))*>) . d
then A51:
d >= 1
by FINSEQ_3:25;
A52:
d <= n + 2
by A1, A5, A50, FINSEQ_3:25;
per cases
( d = 1 or ( d > 1 & d < n + 2 ) or d = n + 2 )
by A51, A52, XXREAL_0:1;
suppose A54:
(
d > 1 &
d < n + 2 )
;
f1 . d = ((<*(f1 . 1)*> ^ f6) ^ <*(f1 . (n + 2))*>) . dthen reconsider w =
d - 1 as
Element of
NAT by INT_1:3;
d - 1
< (n + 2) - 1
by A54, XREAL_1:9;
then A55:
d - 1
<= (n + 1) - 1
by INT_1:7;
d - 1
>= 0 + 1
by A54, INT_1:7, XREAL_1:50;
then
w in Seg n
by A55, FINSEQ_1:1;
then A56:
w in dom f6
by A4, A18, A22, A32, FINSEQ_1:def 3;
then A57:
w in dom (f6 ^ <*(f1 . (n + 2))*>)
by FINSEQ_2:15;
thus ((<*(f1 . 1)*> ^ f6) ^ <*(f1 . (n + 2))*>) . d =
(<*(f1 . 1)*> ^ (f6 ^ <*(f1 . (n + 2))*>)) . (w + 1)
by FINSEQ_1:32
.=
(f6 ^ <*(f1 . (n + 2))*>) . w
by A57, FINSEQ_3:103
.=
f6 . w
by A56, FINSEQ_1:def 7
.=
f1 . (w + 1)
by A37, A56
.=
f1 . d
;
verum end; end;
end;
len ((<*(f1 . 1)*> ^ f6) ^ <*(f1 . (n + 2))*>) =
len (<*(f1 . 1)*> ^ (f6 ^ <*(f1 . (n + 2))*>))
by FINSEQ_1:32
.=
1
+ (len (f6 ^ <*(f1 . (n + 2))*>))
by FINSEQ_5:8
.=
(1 + (len f6)) + 1
by FINSEQ_2:16
.=
len f1
by A1, A4, A5, A18, A22, A32
;
hence
f1 = (<*(f1 . 1)*> ^ f6) ^ <*(f1 . (n + 2))*>
by A49, FINSEQ_3:29;
verum
end;
then Sum f1 =
Sum (<*(f1 . 1)*> ^ (f6 ^ <*(f1 . (n + 2))*>))
by FINSEQ_1:32
.=
(f1 . 1) + (Sum (f6 ^ <*(f1 . (n + 2))*>))
by RVSUM_1:76
.=
(f1 . 1) + ((Sum f6) + (f1 . (n + 2)))
by RVSUM_1:74
.=
(Sum ((x - a) * f2)) + r
by A10, A9, A13, A16, A34
.=
((x - a) * ((Poly-INT fr) . x)) + r
by A20, RVSUM_1:87
;
hence
(Poly-INT fp) . x = ((x - a) * ((Poly-INT fr) . x)) + r
by A7;
verum
end;
hence
( len fr = n + 1 & ( for x being Element of INT holds (Poly-INT fp) . x = ((x - a) * ((Poly-INT fr) . x)) + r ) & fp . (n + 2) = fr . (n + 1) )
by A3, FINSEQ_5:62, FINSEQ_5:def 3; verum