let I be imaginary Polynomial of F_Complex; :: thesis: for r being real Element of F_Complex holds eval (I,r) is imaginary
let r be real Element of F_Complex; :: thesis: eval (I,r) is imaginary
consider H being FinSequence of F_Complex such that
A1: ( eval (I,r) = Sum H & len H = len I ) and
A2: for n being Element of NAT st n in dom H holds
H . n = (I . (n -' 1)) * ( . (r,(n -' 1))) by POLYNOM4:def 2;
consider h being sequence of the carrier of F_Complex such that
A3: Sum H = h . (len H) and
A4: ( h . 0 = 0. F_Complex & ( for j being Nat
for v being Element of F_Complex st j < len H & v = H . (j + 1) holds
h . (j + 1) = (h . j) + v ) ) by RLVECT_1:def 12;
defpred S1[ Nat] means ( \$1 <= len H implies h . \$1 is imaginary );
A5: S1[ 0 ] by A4;
A6: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A7: S1[n] ; :: thesis: S1[n + 1]
set n1 = n + 1;
assume A8: n + 1 <= len H ; :: thesis: h . (n + 1) is imaginary
n + 1 in dom H by ;
then A9: H . (n + 1) = (I . ((n + 1) -' 1)) * ( . (r,((n + 1) -' 1))) by A2;
A10: I . ((n + 1) -' 1) is imaginary by Def4;
reconsider Hn1 = H . (n + 1) as imaginary Element of F_Complex by ;
h . (n + 1) = (h . n) + Hn1 by ;
hence h . (n + 1) is imaginary by ; :: thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch 2(A5, A6);
hence eval (I,r) is imaginary by A1, A3; :: thesis: verum