let n be Nat; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: 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:6;
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:13;
let a be Integer; :: thesis: 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, set , set ] means ex i being Integer st
( i = $2 & $3 = (fp . ((n + 2) - $1)) + (a * i) );
reconsider n1 = n + 1 as Element of NAT ;
A2: for d being Element of 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 Element of NAT ; :: thesis: ( 1 <= d & d < n1 implies for x being Element of INT ex y being Element of INT st S1[d,x,y] )
assume ( 1 <= d & d < n1 ) ; :: thesis: for x being Element of INT ex y being Element of INT st S1[d,x,y]
let x be Element of INT ; :: thesis: 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 ; :: thesis: S1[d,x,y]
thus S1[d,x,y] ; :: thesis: verum
end;
consider p being FinSequence of INT such that
A3: ( len p = n1 & ( p . 1 = A or n1 = 0 ) & ( for d being Element of NAT st 1 <= d & d < n1 holds
S1[d,p . d,p . (d + 1)] ) ) from RECDEF_1:sch 4(A2);
 take fr = Rev p; :: thesis: 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)); :: thesis: ( 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 ; :: thesis: (Poly-INT fp) . x = ((x - a) * ((Poly-INT fr) . x)) + r
consider f1 being FinSequence of INT such that
A5: ( len f1 = len fp & ( for d being Nat st d in dom f1 holds
f1 . d = (fp . d) * (x |^ (d -' 1)) ) & (Poly-INT fp) . x = Sum f1 ) by Def1;
f1 <> {} by A1, A5;
then ( 1 in dom f1 & n + 2 in dom f1 ) by A1, A5, FINSEQ_5:6;
then ( f1 . 1 = (fp . 1) * (x |^ (1 -' 1)) & f1 . (n + 2) = (fp . (n + 2)) * (x |^ ((n + 2) -' 1)) ) by A5;
then ( f1 . 1 = (fp . 1) * (x |^ 0 ) & f1 . (n + 2) = (fp . (n + 2)) * (x |^ (((n + 1) + 1) -' 1)) ) by XREAL_1:234;
then A6: ( f1 . 1 = (fp . 1) * 1 & f1 . (n + 2) = (fp . (n + 2)) * (x |^ (n + 1)) ) by NAT_D:34, NEWTON:9;
consider f2 being FinSequence of INT such that
A7: ( len f2 = len fr & ( for d being Nat st d in dom f2 holds
f2 . d = (fr . d) * (x |^ (d -' 1)) ) & (Poly-INT fr) . x = Sum f2 ) by Def1;
set f3 = (x - a) * f2;
A8: 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)))
proof
let k be Element of NAT ; :: thesis: ( k in dom ((x - a) * f2) implies ((x - a) * f2) . k = ((fr . k) * (x |^ k)) - ((a * (fr . k)) * (x |^ (k -' 1))) )
assume A9: k in dom ((x - a) * f2) ; :: thesis: ((x - a) * f2) . k = ((fr . k) * (x |^ k)) - ((a * (fr . k)) * (x |^ (k -' 1)))
then A10: k >= 1 by FINSEQ_3:27;
A11: k in dom f2 by A9, VALUED_1:def 5;
thus ((x - a) * f2) . k = (x - a) * (f2 . k) by A9, VALUED_1:def 5
.= (x - a) * ((fr . k) * (x |^ (k -' 1))) by A7, A11
.= ((fr . k) * ((x |^ (k -' 1)) * x)) - ((a * (fr . k)) * (x |^ (k -' 1)))
.= ((fr . k) * (x |^ ((k -' 1) + 1))) - ((a * (fr . k)) * (x |^ (k -' 1))) by NEWTON:11
.= ((fr . k) * (x |^ k)) - ((a * (fr . k)) * (x |^ (k -' 1))) by A10, XREAL_1:237 ; :: thesis: verum
end;
deffunc H1( Nat) -> set = (fr . $1) * (x |^ $1);
deffunc H2( Nat) -> set = (a * (fr . $1)) * (x |^ ($1 -' 1));
reconsider n = n as Element of NAT by ORDINAL1:def 13;
consider f4 being FinSequence such that
A12: ( len f4 = n + 1 & ( for d being Nat st d in dom f4 holds
f4 . d = H1(d) ) ) from FINSEQ_1:sch 2();
 consider f5 being FinSequence such that
A13: ( len f5 = n + 1 & ( for d being Nat st d in dom f5 holds
f5 . d = H2(d) ) ) from FINSEQ_1:sch 2();
 ( f4 <> {} & f5 <> {} ) by A12, A13;
then ( 1 in dom f5 & n + 1 in dom f4 ) by A12, FINSEQ_5:6;
then ( f4 . (n + 1) = (fr . (n + 1)) * (x |^ (n + 1)) & f5 . 1 = (a * (fr . 1)) * (x |^ (1 -' 1)) ) by A12, A13;
then ( f4 . (n + 1) = (fp . (n + 2)) * (x |^ (n + 1)) & f5 . 1 = (a * (fr . 1)) * (x |^ 0 ) ) by A3, FINSEQ_5:65, XREAL_1:234;
then A14: ( f4 . (n + 1) = (fp . (n + 2)) * (x |^ (n + 1)) & f5 . 1 = (a * (fr . 1)) * 1 ) by NEWTON:9;
for d being Nat st d in dom f4 holds
f4 . d in INT
proof
let d be Nat; :: thesis: ( d in dom f4 implies f4 . d in INT )
reconsider d1 = d as Element of NAT by ORDINAL1:def 13;
assume d in dom f4 ; :: thesis: f4 . d in INT
then f4 . d1 = (fr . d1) * (x |^ d1) by A12;
hence f4 . d in INT by INT_1:def 2; :: thesis: verum
end;
then reconsider f4 = f4 as FinSequence of INT by FINSEQ_2:14;
for d being Nat st d in dom f5 holds
f5 . d in INT
proof
let d be Nat; :: thesis: ( d in dom f5 implies f5 . d in INT )
assume d in dom f5 ; :: thesis: f5 . d in INT
then f5 . d = (a * (fr . d)) * (x |^ (d -' 1)) by A13;
hence f5 . d in INT by INT_1:def 2; :: thesis: verum
end;
then reconsider f5 = f5 as FinSequence of INT by FINSEQ_2:14;
A15: dom ((x - a) * f2) = dom f2 by VALUED_1:def 5;
then A16: ( dom ((x - a) * f2) = dom f4 & dom ((x - a) * f2) = dom f5 ) by A4, A7, A12, A13, FINSEQ_3:31;
A17: len ((x - a) * f2) = len f2 by A15, FINSEQ_3:31;
A18: for d being Nat st d in dom ((x - a) * f2) holds
((x - a) * f2) . d = (f4 . d) - (f5 . d)
proof
let d be Nat; :: thesis: ( d in dom ((x - a) * f2) implies ((x - a) * f2) . d = (f4 . d) - (f5 . d) )
assume A19: d in dom ((x - a) * f2) ; :: thesis: ((x - a) * f2) . d = (f4 . d) - (f5 . d)
then ( f4 . d = (fr . d) * (x |^ d) & f5 . d = (a * (fr . d)) * (x |^ (d -' 1)) ) by A12, A13, A16;
hence ((x - a) * f2) . d = (f4 . d) - (f5 . d) by A8, A19; :: thesis: verum
end;
( f4 is FinSequence of REAL & f5 is FinSequence of REAL ) by FINSEQ_3:126;
then consider f6 being FinSequence of REAL such that
A20: ( len f6 = (len ((x - a) * f2)) - 1 & ( for d being Nat st d in dom f6 holds
f6 . d = (f4 . d) - (f5 . (d + 1)) ) & Sum ((x - a) * f2) = ((Sum f6) + (f4 . (n + 1))) - (f5 . 1) ) by A4, A7, A12, A13, A17, A18, Th5;
A21: len f6 <= len ((x - a) * f2) by A4, A7, A17, A20, XREAL_1:147;
then A22: dom f6 c= dom ((x - a) * f2) by FINSEQ_3:32;
A23: for d being Element of NAT st d in dom f6 holds
f6 . d = f1 . (d + 1)
proof
let d be Element of NAT ; :: thesis: ( d in dom f6 implies f6 . d = f1 . (d + 1) )
assume A24: d in dom f6 ; :: thesis: f6 . d = f1 . (d + 1)
then d in Seg n by A4, A7, A17, A20, FINSEQ_1:def 3;
then A25: ( d <= n & d >= 1 ) by FINSEQ_1:3;
then d < n + 1 by XREAL_1:147;
then d + 1 in Seg (n + 1) by FINSEQ_3:12;
then A26: ( d + 1 in dom f5 & d + 1 in dom p ) by A3, A13, FINSEQ_1:def 3;
A27: dom f6 c= dom p by A3, A4, A7, A17, A21, FINSEQ_3:32;
A28: ( n - d >= 0 & n - d <= n - 1 ) by A25, XREAL_1:12, XREAL_1:50;
then (n - d) + 1 >= 0 + 1 by XREAL_1:8;
then reconsider d' = (n - d) + 1 as Element of NAT by INT_1:16;
( d' >= 0 + 1 & d' <= (n - 1) + 1 ) by A28, XREAL_1:8;
then ( d' >= 1 & d' < n + 1 ) by XREAL_1:147;
then consider i being Integer such that
A29: ( i = p . d' & p . (d' + 1) = (fp . ((n + 2) - d')) + (a * i) ) by A3;
d + 0 < n + 2 by A25, XREAL_1:10;
then d + 1 in Seg (n + 2) by FINSEQ_3:12;
then A30: d + 1 in dom f1 by A1, A5, FINSEQ_1:def 3;
thus f6 . d = (f4 . d) - (f5 . (d + 1)) by A20, A24
.= ((fr . d) * (x |^ d)) - (f5 . (d + 1)) by A12, A16, A22, A24
.= ((fr . d) * (x |^ d)) - ((a * (fr . (d + 1))) * (x |^ ((d + 1) -' 1))) by A13, A26
.= ((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, A24, A27, FINSEQ_5:61
.= ((p . (((n - d) + 1) + 1)) - (a * (p . (((n + 1) - (d + 1)) + 1)))) * (x |^ d) by A3, A26, FINSEQ_5:61
.= (fp . (d + 1)) * (x |^ ((d + 1) -' 1)) by A29, NAT_D:34
.= f1 . (d + 1) by A5, A30 ; :: thesis: verum
end;
f1 = (<*(f1 . 1)*> ^ f6) ^ <*(f1 . (n + 2))*>
proof
set K = (<*(f1 . 1)*> ^ f6) ^ <*(f1 . (n + 2))*>;
len ((<*(f1 . 1)*> ^ f6) ^ <*(f1 . (n + 2))*>) = len (<*(f1 . 1)*> ^ (f6 ^ <*(f1 . (n + 2))*>)) by FINSEQ_1:45
.= 1 + (len (f6 ^ <*(f1 . (n + 2))*>)) by FINSEQ_5:8
.= (1 + (len f6)) + 1 by FINSEQ_2:19
.= len f1 by A1, A4, A5, A7, A17, A20 ;
then A31: dom f1 = dom ((<*(f1 . 1)*> ^ f6) ^ <*(f1 . (n + 2))*>) by FINSEQ_3:31;
for d being Nat st d in dom f1 holds
f1 . d = ((<*(f1 . 1)*> ^ f6) ^ <*(f1 . (n + 2))*>) . d
proof
let d be Nat; :: thesis: ( d in dom f1 implies f1 . d = ((<*(f1 . 1)*> ^ f6) ^ <*(f1 . (n + 2))*>) . d )
assume d in dom f1 ; :: thesis: f1 . d = ((<*(f1 . 1)*> ^ f6) ^ <*(f1 . (n + 2))*>) . d
then A32: ( d >= 1 & d <= n + 2 ) by A1, A5, FINSEQ_3:27;
per cases ( d = 1 or ( d > 1 & d < n + 2 ) or d = n + 2 ) by A32, XXREAL_0:1;
suppose A33: d = 1 ; :: thesis: f1 . d = ((<*(f1 . 1)*> ^ f6) ^ <*(f1 . (n + 2))*>) . d
hence ((<*(f1 . 1)*> ^ f6) ^ <*(f1 . (n + 2))*>) . d = (<*(f1 . 1)*> ^ (f6 ^ <*(f1 . (n + 2))*>)) . 1 by FINSEQ_1:45
.= f1 . d by A33, FINSEQ_1:58 ;
:: thesis: verum
end;
suppose ( d > 1 & d < n + 2 ) ; :: thesis: f1 . d = ((<*(f1 . 1)*> ^ f6) ^ <*(f1 . (n + 2))*>) . d
then A34: ( d - 1 > 0 & d - 1 < (n + 2) - 1 ) by XREAL_1:11, XREAL_1:52;
then reconsider w = d - 1 as Element of NAT by INT_1:16;
( d - 1 >= 0 + 1 & d - 1 <= (n + 1) - 1 ) by A34, INT_1:20;
then w in Seg n by FINSEQ_1:3;
then A35: w in dom f6 by A4, A7, A17, A20, FINSEQ_1:def 3;
then A36: w in dom (f6 ^ <*(f1 . (n + 2))*>) by FINSEQ_2:18;
thus ((<*(f1 . 1)*> ^ f6) ^ <*(f1 . (n + 2))*>) . d = (<*(f1 . 1)*> ^ (f6 ^ <*(f1 . (n + 2))*>)) . (w + 1) by FINSEQ_1:45
.= (f6 ^ <*(f1 . (n + 2))*>) . w by A36, FINSEQ_3:112
.= f6 . w by A35, FINSEQ_1:def 7
.= f1 . (w + 1) by A23, A35
.= f1 . d ; :: thesis: verum
end;
suppose A37: d = n + 2 ; :: thesis: f1 . d = ((<*(f1 . 1)*> ^ f6) ^ <*(f1 . (n + 2))*>) . d
set K1 = <*(f1 . 1)*> ^ f6;
thus ((<*(f1 . 1)*> ^ f6) ^ <*(f1 . (n + 2))*>) . d = ((<*(f1 . 1)*> ^ f6) ^ <*(f1 . (n + 2))*>) . ((n + 1) + 1) by A37
.= ((<*(f1 . 1)*> ^ f6) ^ <*(f1 . (n + 2))*>) . ((len (<*(f1 . 1)*> ^ f6)) + 1) by A4, A7, A17, A20, FINSEQ_5:8
.= f1 . d by A37, FINSEQ_1:59 ; :: thesis: verum
end;
end;
end;
hence f1 = (<*(f1 . 1)*> ^ f6) ^ <*(f1 . (n + 2))*> by A31, FINSEQ_1:17; :: thesis: verum
end;
then Sum f1 = Sum (<*(f1 . 1)*> ^ (f6 ^ <*(f1 . (n + 2))*>)) by FINSEQ_1:45
.= (f1 . 1) + (Sum (f6 ^ <*(f1 . (n + 2))*>)) by RVSUM_1:106
.= (f1 . 1) + ((Sum f6) + (f1 . (n + 2))) by RVSUM_1:104
.= (Sum ((x - a) * f2)) + r by A6, A14, A20
.= ((x - a) * ((Poly-INT fr) . x)) + r by A7, RVSUM_1:117 ;
hence (Poly-INT fp) . x = ((x - a) * ((Poly-INT fr) . x)) + r by A5; :: thesis: 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:65, FINSEQ_5:def 3; :: thesis: verum