1 - 1 = 0 ;
then A1: 1 -' 1 = 0 by XREAL_1:233;
reconsider z2 = 1_ F_Complex as Element of COMPLEX by COMPLFLD:def 1;
let n be non zero Element of NAT ; :: thesis: for x being Element of F_Complex holds eval ((),x) = ( . (x,n)) - 1
let x be Element of F_Complex; :: thesis: eval ((),x) = ( . (x,n)) - 1
set p = unital_poly (F_Complex,n);
consider F being FinSequence of F_Complex such that
A2: eval ((),x) = Sum F and
A3: len F = len () and
A4: for i being Element of NAT st i in dom F holds
F . i = (() . (i -' 1)) * ( . (x,(i -' 1))) by POLYNOM4:def 2;
A5: 0 + 1 < n + 1 by XREAL_1:8;
then A6: 1 < len F by ;
A7: len F = n + 1 by ;
then (len F) - 1 = n ;
then A8: (len F) -' 1 = n by ;
((len F) - 1) + 1 = len F ;
then A9: ((len F) -' 1) + 1 = len F by ;
A10: (unital_poly (F_Complex,n)) . 0 = - () by Th38;
set xn = . (x,n);
set null = ((len F) -' 1) |-> ();
A11: len (((len F) -' 1) |-> ()) = (len F) -' 1 by CARD_1:def 7;
set tR2 = (((len F) -' 1) |-> ()) ^ <*( . (x,n))*>;
set tR1 = <*(- ())*> ^ (((len F) -' 1) |-> ());
A12: dom F = Seg (len F) by FINSEQ_1:def 3;
reconsider R1 = <*(- ())*> ^ (((len F) -' 1) |-> ()) as Tuple of len F, the carrier of F_Complex by A9;
reconsider R1 = R1 as Element of (len F) -tuples_on the carrier of F_Complex by FINSEQ_2:131;
reconsider R2 = (((len F) -' 1) |-> ()) ^ <*( . (x,n))*> as Tuple of len F, the carrier of F_Complex by A9;
reconsider R2 = R2 as Element of (len F) -tuples_on the carrier of F_Complex by FINSEQ_2:131;
A13: for i being Element of NAT st i in dom (((len F) -' 1) |-> ()) holds
(((len F) -' 1) |-> ()) . i = 0. F_Complex
proof
let i be Element of NAT ; :: thesis: ( i in dom (((len F) -' 1) |-> ()) implies (((len F) -' 1) |-> ()) . i = 0. F_Complex )
assume i in dom (((len F) -' 1) |-> ()) ; :: thesis: (((len F) -' 1) |-> ()) . i = 0. F_Complex
then i in Seg ((len F) -' 1) by FUNCOP_1:13;
hence (((len F) -' 1) |-> ()) . i = 0. F_Complex by FUNCOP_1:7; :: thesis: verum
end;
A14: for i being Nat st i <> 1 & i in dom R1 holds
R1 . i = 0. F_Complex
proof
let i be Nat; :: thesis: ( i <> 1 & i in dom R1 implies R1 . i = 0. F_Complex )
assume that
A15: i <> 1 and
A16: i in dom R1 ; :: thesis:
A17: dom <*(- ())*> = Seg 1 by FINSEQ_1:def 8;
now :: thesis: not i in dom <*(- ())*>
assume i in dom <*(- ())*> ; :: thesis: contradiction
then ( 1 <= i & i <= 1 ) by ;
hence contradiction by A15, XXREAL_0:1; :: thesis: verum
end;
then consider j being Nat such that
A18: j in dom (((len F) -' 1) |-> ()) and
A19: i = (len <*(- ())*>) + j by ;
(((len F) -' 1) |-> ()) . j = 0. F_Complex by ;
hence R1 . i = 0. F_Complex by ; :: thesis: verum
end;
len ((((len F) -' 1) |-> ()) ^ <*( . (x,n))*>) = (len (((len F) -' 1) |-> ())) + (len <*( . (x,n))*>) by FINSEQ_1:22;
then A20: len ((((len F) -' 1) |-> ()) ^ <*( . (x,n))*>) = len F by ;
A21: for i being Element of NAT st i in dom R2 & i <> len F holds
R2 . i = 0. F_Complex
proof
let i be Element of NAT ; :: thesis: ( i in dom R2 & i <> len F implies R2 . i = 0. F_Complex )
assume that
A22: i in dom R2 and
A23: i <> len F ; :: thesis:
A24: dom R2 = Seg (len F) by ;
then i <= len F by ;
then i < ((len F) -' 1) + 1 by ;
then A25: i <= (len F) -' 1 by NAT_1:13;
1 <= i by ;
then i in Seg ((len F) -' 1) by ;
then A26: i in dom (((len F) -' 1) |-> ()) by ;
then R2 . i = (((len F) -' 1) |-> ()) . i by FINSEQ_1:def 7;
hence R2 . i = 0. F_Complex by ; :: thesis: verum
end;
len R1 = len F by CARD_1:def 7;
then A27: dom R1 = Seg (len F) by FINSEQ_1:def 3;
len R2 = len F by CARD_1:def 7;
then A28: dom R2 = Seg (len F) by FINSEQ_1:def 3;
A29: R1 . 1 = - () by FINSEQ_1:41;
A30: len (R1 + R2) = len F by CARD_1:def 7;
then A31: dom (R1 + R2) = Seg (len F) by FINSEQ_1:def 3;
A32: R2 . (len F) = . (x,n) by ;
for k being Nat st k in dom (R1 + R2) holds
(R1 + R2) . k = F . k
proof
let k be Nat; :: thesis: ( k in dom (R1 + R2) implies (R1 + R2) . k = F . k )
assume A33: k in dom (R1 + R2) ; :: thesis: (R1 + R2) . k = F . k
A34: k in Seg (len F) by ;
A35: k in dom F by ;
A36: 1 <= k by ;
A37: (- ()) * () = - () ;
now :: thesis: (R1 + R2) . k = F . k
per cases ( k = 1 or k <> 1 ) ;
suppose A38: k = 1 ; :: thesis: (R1 + R2) . k = F . k
then R2 . k = 0. F_Complex by A6, A21, A28, A34;
then A39: (R1 + R2) . 1 = (- ()) + () by ;
F . 1 = (() . 0) * ( . (x,0)) by A4, A1, A35, A38
.= - () by ;
hence (R1 + R2) . k = F . k by ; :: thesis: verum
end;
suppose A40: k <> 1 ; :: thesis: (R1 + R2) . k = F . k
now :: thesis: (R1 + R2) . k = F . k
per cases ( k = len F or k <> len F ) ;
suppose A41: k = len F ; :: thesis: (R1 + R2) . k = F . k
len F <> 0 by A3, A5, Th40;
then A42: F . (len F) = (() . ((len F) -' 1)) * ( . (x,((len F) -' 1))) by
.= () * ( . (x,n)) by
.= . (x,n) ;
R1 . (len F) = 0. F_Complex by A6, A14, A27, A34, A41;
then (R1 + R2) . (len F) = () + ( . (x,n)) by
.= . (x,n) by COMPLFLD:7 ;
hence (R1 + R2) . k = F . k by ; :: thesis: verum
end;
suppose A43: k <> len F ; :: thesis: (R1 + R2) . k = F . k
A44: now :: thesis: not k -' 1 = n
assume k -' 1 = n ; :: thesis: contradiction
then k - 1 = n by ;
hence contradiction by A7, A43; :: thesis: verum
end;
1 < k by ;
then 1 + (- 1) < k + (- 1) by XREAL_1:8;
then 1 - 1 < k - 1 ;
then 0 < k -' 1 by ;
then (unital_poly (F_Complex,n)) . (k -' 1) = 0. F_Complex by ;
then A45: F . k = () * ( . (x,(k -' 1))) by ;
A46: R2 . k = 0. F_Complex by A21, A28, A34, A43;
R1 . k = 0. F_Complex by A14, A27, A34, A40;
then (R1 + R2) . k = () + () by ;
hence (R1 + R2) . k = F . k by ; :: thesis: verum
end;
end;
end;
hence (R1 + R2) . k = F . k ; :: thesis: verum
end;
end;
end;
hence (R1 + R2) . k = F . k ; :: thesis: verum
end;
then A47: R1 + R2 = F by ;
Sum (((len F) -' 1) |-> ()) = 0. F_Complex by MATRIX_3:11;
then ( Sum R1 = (- ()) + () & Sum R2 = () + ( . (x,n)) ) by ;
then ( - z2 = - () & Sum F = (- ()) + ( . (x,n)) ) by ;
hence eval ((),x) = ( . (x,n)) - 1 by ; :: thesis: verum