let n, k be Nat; :: thesis: ( 1 <= k & k <= n implies for z being FinSequence of INT.Ring st z = idseq n holds
( eval ((LagIPoly (z,k)),(In (k,INT.Ring))) = (((- 1) |^ (n -' k)) * ((n -' k) !)) * ((k -' 1) !) & ( for i being Nat st 1 <= i & i <= n & i <> k holds
In (i,INT.Ring) is_a_root_of LagIPoly (z,k) ) ) )
assume A1: ( 1 <= k & k <= n ) ; :: thesis: for z being FinSequence of INT.Ring st z = idseq n holds
( eval ((LagIPoly (z,k)),(In (k,INT.Ring))) = (((- 1) |^ (n -' k)) * ((n -' k) !)) * ((k -' 1) !) & ( for i being Nat st 1 <= i & i <= n & i <> k holds
In (i,INT.Ring) is_a_root_of LagIPoly (z,k) ) )
let z be FinSequence of INT.Ring; :: thesis: ( z = idseq n implies ( eval ((LagIPoly (z,k)),(In (k,INT.Ring))) = (((- 1) |^ (n -' k)) * ((n -' k) !)) * ((k -' 1) !) & ( for i being Nat st 1 <= i & i <= n & i <> k holds
In (i,INT.Ring) is_a_root_of LagIPoly (z,k) ) ) )
assume A2: z = idseq n ; :: thesis: ( eval ((LagIPoly (z,k)),(In (k,INT.Ring))) = (((- 1) |^ (n -' k)) * ((n -' k) !)) * ((k -' 1) !) & ( for i being Nat st 1 <= i & i <= n & i <> k holds
In (i,INT.Ring) is_a_root_of LagIPoly (z,k) ) )
set D = Del (z,k);
A3: len z = n by A2;
then A4: k in dom z by A1, FINSEQ_3:25;
then A5: (len (Del (z,k))) + 1 = n by A3, WSIERP_1:def 1;
A6: len ((len (Del (z,k))) |-> 1) = len (Del (z,k)) ;
eval ((LagIPoly (z,k)),(In (k,INT.Ring))) = eval ((~ (Product (rpoly (((len (Del (z,k))) |-> 1),(Del (z,k)))))),(In (k,INT.Ring))) ;
then consider e being FinSequence of the carrier of INT.Ring such that
A7: eval ((LagIPoly (z,k)),(In (k,INT.Ring))) = Product e and
A8: len e = len ((len (Del (z,k))) |-> 1) and
A9: for i being Nat st 1 <= i & i <= len e holds
e . i = eval ((rpoly ((((len (Del (z,k))) |-> 1) /. i),((Del (z,k)) /. i))),(In (k,INT.Ring))) by Th50;
defpred S1[ Nat] means ( $1 < k implies Product (e | $1) = ((k -' 1) !) / (((k -' 1) -' $1) !) );
e | 0 = <*> the carrier of INT.Ring ;
then A10: Product (e | 0) = 1_ INT.Ring by GROUP_4:8;
A11: k -' 1 = k - 1 by A1, XREAL_1:233;
(k -' 1) -' 0 = (k -' 1) - 0 ;
then A12: S1[ 0 ] by A10, XCMPLX_1:60;
A13: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
assume A14: S1[i] ; :: thesis: S1[i + 1]
set i1 = i + 1;
assume A15: i + 1 < k ; :: thesis: Product (e | (i + 1)) = ((k -' 1) !) / (((k -' 1) -' (i + 1)) !)
then A16: i + 1 < n by A1, XXREAL_0:2;
then A17: i + 1 <= len (Del (z,k)) by A5, NAT_1:13;
A18: i + 1 <= len e by A16, A8, A5, NAT_1:13;
A19: 1 <= i + 1 by NAT_1:11;
then A20: ( i + 1 in dom ((len (Del (z,k))) |-> 1) & i + 1 in dom (Del (z,k)) & i + 1 in Seg (len (Del (z,k))) ) by A17, A6, FINSEQ_3:25;
then A21: ( ((len (Del (z,k))) |-> 1) /. (i + 1) = ((len (Del (z,k))) |-> 1) . (i + 1) & ((len (Del (z,k))) |-> 1) . (i + 1) = 1 & (Del (z,k)) /. (i + 1) = (Del (z,k)) . (i + 1) ) by PARTFUN1:def 6, FINSEQ_2:57;
A22: i + 1 in Seg n by A19, A16;
(Del (z,k)) . (i + 1) = z . (i + 1) by A4, A15, WSIERP_1:def 1;
then A23: (Del (z,k)) . (i + 1) = i + 1 by A2, A22, FINSEQ_2:49;
A24: e . (i + 1) = eval ((rpoly ((((len (Del (z,k))) |-> 1) /. (i + 1)),((Del (z,k)) /. (i + 1)))),(In (k,INT.Ring))) by NAT_1:11, A17, A8, A9
.= (In (k,INT.Ring)) - ((Del (z,k)) /. (i + 1)) by A21, HURWITZ:29 ;
k = (k -' 1) + 1 by A11;
then A25: i + 1 <= k -' 1 by A15, NAT_1:13;
then i < k -' 1 by NAT_1:13;
then A26: (k -' 1) -' i = (k -' 1) - i by XREAL_1:233;
A27: k - (i + 1) <> 0 by A15;
(k -' 1) -' (i + 1) = (k -' 1) - (i + 1) by A25, XREAL_1:233;
then ((k -' 1) -' (i + 1)) + 1 = (k -' 1) -' i by A26;
then A28: ((k -' 1) -' i) ! = (((k -' 1) -' (i + 1)) !) * (k - (i + 1)) by A26, A11, NEWTON:15;
i + 1 in dom e by A18, NAT_1:11, FINSEQ_3:25;
then e | (i + 1) = (e | i) ^ <*(e . (i + 1))*> by FINSEQ_5:10;
hence Product (e | (i + 1)) = (Product (e | i)) * ((In (k,INT.Ring)) - ((Del (z,k)) /. (i + 1))) by A24, GROUP_4:6
.= (((k -' 1) !) / (((k -' 1) -' i) !)) * (k - (i + 1)) by A15, NAT_1:13, A14, A23, A20, PARTFUN1:def 6
.= ((k -' 1) !) / (((k -' 1) -' (i + 1)) !) by A28, A27, XCMPLX_1:92 ;
:: thesis: verum
end;
A29: for i being Nat holds S1[i] from NAT_1:sch 2(A12, A13);
 k = (k -' 1) + 1 by A11;
then A30: k -' 1 < k by NAT_1:13;
A31: Product (e | (k -' 1)) = ((k -' 1) !) / (((k -' 1) -' (k -' 1)) !) by A29, A30;
A32: ((k -' 1) -' (k -' 1)) ! = 1 by NEWTON:12, XREAL_1:232;
then A33: Product (e | (k -' 1)) = (k -' 1) ! by A31;
defpred S2[ Nat] means ( k <= $1 & $1 < n implies Product (e | $1) = (((- 1) |^ (($1 + 1) -' k)) * ((($1 + 1) -' k) !)) * ((k -' 1) !) );
A34: S2[ 0 ] by A1;
A35: for i being Nat st S2[i] holds
S2[i + 1]
proof
let i be Nat; :: thesis: ( S2[i] implies S2[i + 1] )
assume A36: S2[i] ; :: thesis: S2[i + 1]
set i1 = i + 1;
assume A37: ( k <= i + 1 & i + 1 < n ) ; :: thesis: Product (e | (i + 1)) = (((- 1) |^ (((i + 1) + 1) -' k)) * ((((i + 1) + 1) -' k) !)) * ((k -' 1) !)
then A38: i + 1 <= len (Del (z,k)) by A5, NAT_1:13;
A39: i + 1 <= len e by A8, A37, A5, NAT_1:13;
1 <= i + 1 by NAT_1:11;
then ( i + 1 in dom ((len (Del (z,k))) |-> 1) & i + 1 in dom (Del (z,k)) & i + 1 in Seg (len (Del (z,k))) ) by A38, A6, FINSEQ_3:25;
then A40: ( ((len (Del (z,k))) |-> 1) /. (i + 1) = ((len (Del (z,k))) |-> 1) . (i + 1) & ((len (Del (z,k))) |-> 1) . (i + 1) = 1 & (Del (z,k)) /. (i + 1) = (Del (z,k)) . (i + 1) ) by PARTFUN1:def 6, FINSEQ_2:57;
( 1 <= (i + 1) + 1 & (i + 1) + 1 <= n ) by A37, NAT_1:11, NAT_1:13;
then A41: (i + 1) + 1 in Seg n ;
A42: (Del (z,k)) . (i + 1) = z . ((i + 1) + 1) by A4, A37, WSIERP_1:def 1;
A43: e . (i + 1) = eval ((rpoly ((((len (Del (z,k))) |-> 1) /. (i + 1)),((Del (z,k)) /. (i + 1)))),(In (k,INT.Ring))) by NAT_1:11, A38, A8, A9
.= (In (k,INT.Ring)) - ((Del (z,k)) /. (i + 1)) by A40, HURWITZ:29 ;
i + 1 in dom e by A38, A8, NAT_1:11, FINSEQ_3:25;
then e | (i + 1) = (e | i) ^ <*(e . (i + 1))*> by FINSEQ_5:10;
then A44: Product (e | (i + 1)) = (Product (e | i)) * ((In (k,INT.Ring)) - ((Del (z,k)) /. (i + 1))) by A43, GROUP_4:6;
per cases ( i + 1 = k or k < i + 1 ) by A37, XXREAL_0:1;
suppose A45: i + 1 = k ; :: thesis: Product (e | (i + 1)) = (((- 1) |^ (((i + 1) + 1) -' k)) * ((((i + 1) + 1) -' k) !)) * ((k -' 1) !)
(In (k,INT.Ring)) - ((Del (z,k)) /. (i + 1)) = k - ((i + 1) + 1) by A42, A2, A41, FINSEQ_2:49, A40
.= ((- 1) |^ (((i + 1) + 1) -' k)) * ((((i + 1) + 1) -' k) !) by A45, NEWTON:13 ;
hence Product (e | (i + 1)) = (((- 1) |^ (((i + 1) + 1) -' k)) * ((((i + 1) + 1) -' k) !)) * ((k -' 1) !) by A44, A32, A45, A31; :: thesis: verum
end;
suppose A46: k < i + 1 ; :: thesis: Product (e | (i + 1)) = (((- 1) |^ (((i + 1) + 1) -' k)) * ((((i + 1) + 1) -' k) !)) * ((k -' 1) !)
k < (i + 1) + 1 by A46, NAT_1:13;
then A47: ( ((i + 1) + 1) -' k = ((i + 1) + 1) - k & (i + 1) -' k = (i + 1) - k ) by A46, XREAL_1:233;
then ((i + 1) + 1) -' k = ((i + 1) -' k) + 1 ;
then A48: (((i + 1) -' k) !) * (((i + 1) + 1) -' k) = (((i + 1) + 1) -' k) ! by NEWTON:15;
A49: (In (k,INT.Ring)) - ((Del (z,k)) /. (i + 1)) = k - ((i + 1) + 1) by A42, A2, A41, FINSEQ_2:49, A40
.= - (((i + 1) + 1) -' k) by A47 ;
i + 1 in dom e by A39, NAT_1:11, FINSEQ_3:25;
then e | (i + 1) = (e | i) ^ <*(e . (i + 1))*> by FINSEQ_5:10;
then A50: Product (e | (i + 1)) = (Product (e | i)) * ((In (k,INT.Ring)) - ((Del (z,k)) /. (i + 1))) by A43, GROUP_4:6;
A51: - ((- 1) |^ ((i + 1) -' k)) = (- 1) * ((- 1) |^ ((i + 1) -' k))
.= (- 1) |^ (((i + 1) -' k) + 1) by NEWTON:6
.= (- 1) |^ (((i + 1) + 1) -' k) by A47 ;
Product (e | (i + 1)) = (((- 1) |^ (((i + 1) + 1) -' k)) * ((((i + 1) + 1) -' k) !)) * ((k -' 1) !) by A51, A48, A50, A36, A46, A37, NAT_1:13, A49;
hence Product (e | (i + 1)) = (((- 1) |^ (((i + 1) + 1) -' k)) * ((((i + 1) + 1) -' k) !)) * ((k -' 1) !) ; :: thesis: verum
end;
end;
end;
A52: for i being Nat holds S2[i] from NAT_1:sch 2(A34, A35);
 thus eval ((LagIPoly (z,k)),(In (k,INT.Ring))) = (((- 1) |^ (n -' k)) * ((n -' k) !)) * ((k -' 1) !) :: thesis: for i being Nat st 1 <= i & i <= n & i <> k holds
In (i,INT.Ring) is_a_root_of LagIPoly (z,k)
proof
per cases ( k < n or k = n ) by A1, XXREAL_0:1;
suppose k < n ; :: thesis: eval ((LagIPoly (z,k)),(In (k,INT.Ring))) = (((- 1) |^ (n -' k)) * ((n -' k) !)) * ((k -' 1) !)
then ( k <= len e & len e < n ) by A5, A8, NAT_1:13;
then Product (e | (len e)) = (((- 1) |^ (n -' k)) * ((n -' k) !)) * ((k -' 1) !) by A52, A5, A8;
hence eval ((LagIPoly (z,k)),(In (k,INT.Ring))) = (((- 1) |^ (n -' k)) * ((n -' k) !)) * ((k -' 1) !) by A7; :: thesis: verum
end;
suppose A53: k = n ; :: thesis: eval ((LagIPoly (z,k)),(In (k,INT.Ring))) = (((- 1) |^ (n -' k)) * ((n -' k) !)) * ((k -' 1) !)
n -' k = 0 by A53, XREAL_1:232;
then ( (- 1) |^ (n -' k) = 1 & (n -' k) ! = 1 ) by NEWTON:4, NEWTON:12;
hence eval ((LagIPoly (z,k)),(In (k,INT.Ring))) = (((- 1) |^ (n -' k)) * ((n -' k) !)) * ((k -' 1) !) by A7, A53, A33, A5, A8; :: thesis: verum
end;
end;
end;
let i be Nat; :: thesis: ( 1 <= i & i <= n & i <> k implies In (i,INT.Ring) is_a_root_of LagIPoly (z,k) )
assume A54: ( 1 <= i & i <= n & i <> k ) ; :: thesis: In (i,INT.Ring) is_a_root_of LagIPoly (z,k)
per cases ( i < k or i >= k ) ;
suppose A55: i < k ; :: thesis: In (i,INT.Ring) is_a_root_of LagIPoly (z,k)
then i < n by A1, A54, XXREAL_0:1;
then i <= len (Del (z,k)) by A5, NAT_1:13;
then A56: ( i in dom (Del (z,k)) & i in dom ((len (Del (z,k))) |-> 1) & i in Seg (len (Del (z,k))) & i in Seg n ) by A6, A54, FINSEQ_3:25;
then ((len (Del (z,k))) |-> 1) . i = 1 by FINSEQ_2:57;
then A57: ( (Del (z,k)) . i = (Del (z,k)) /. i & (Del (z,k)) /. i is_a_root_of ~ (Product (rpoly (((len (Del (z,k))) |-> 1),(Del (z,k))))) ) by A56, Th51, PARTFUN1:def 6;
(Del (z,k)) . i = z . i by A4, A55, WSIERP_1:def 1
.= In (i,INT.Ring) by A2, A56, FINSEQ_2:49 ;
hence In (i,INT.Ring) is_a_root_of LagIPoly (z,k) by A57; :: thesis: verum
end;
suppose A58: i >= k ; :: thesis: In (i,INT.Ring) is_a_root_of LagIPoly (z,k)
then reconsider i1 = i - 1 as Nat by A1;
i1 + 1 > k by A54, A58, XXREAL_0:1;
then A59: i1 >= k by NAT_1:13;
then A60: i1 >= 1 by A1, XXREAL_0:2;
i1 <= n - 1 by A54, XREAL_1:9;
then A61: ( i1 in dom (Del (z,k)) & i1 in dom ((len (Del (z,k))) |-> 1) & i1 in Seg (len (Del (z,k))) & i in Seg n ) by A5, A60, A6, A54, FINSEQ_3:25;
then ((len (Del (z,k))) |-> 1) . i1 = 1 by FINSEQ_2:57;
then A62: ( (Del (z,k)) . i1 = (Del (z,k)) /. i1 & (Del (z,k)) /. i1 is_a_root_of ~ (Product (rpoly (((len (Del (z,k))) |-> 1),(Del (z,k))))) ) by A61, Th51, PARTFUN1:def 6;
(Del (z,k)) . i1 = z . (i1 + 1) by A59, A4, WSIERP_1:def 1
.= In (i,INT.Ring) by A2, A61, FINSEQ_2:49 ;
hence In (i,INT.Ring) is_a_root_of LagIPoly (z,k) by A62; :: thesis: verum
end;
end;