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)) * ((power F_Complex) . (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 S_{1}[ Nat] means ( $1 <= len H implies h . $1 is imaginary );

A5: S_{1}[ 0 ]
by A4;

A6: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]
_{1}[n]
from NAT_1:sch 2(A5, A6);

hence eval (I,r) is imaginary by A1, A3; :: thesis: verum

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)) * ((power F_Complex) . (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 S

A5: S

A6: for n being Nat st S

S

proof

for n being Nat holds S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A7: S_{1}[n]
; :: thesis: S_{1}[n + 1]

set n1 = n + 1;

assume A8: n + 1 <= len H ; :: thesis: h . (n + 1) is imaginary

n + 1 in dom H by NAT_1:11, A8, FINSEQ_3:25;

then A9: H . (n + 1) = (I . ((n + 1) -' 1)) * ((power F_Complex) . (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 A10, A9;

h . (n + 1) = (h . n) + Hn1 by A4, A8, NAT_1:13;

hence h . (n + 1) is imaginary by A8, A7, NAT_1:13; :: thesis: verum

end;assume A7: S

set n1 = n + 1;

assume A8: n + 1 <= len H ; :: thesis: h . (n + 1) is imaginary

n + 1 in dom H by NAT_1:11, A8, FINSEQ_3:25;

then A9: H . (n + 1) = (I . ((n + 1) -' 1)) * ((power F_Complex) . (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 A10, A9;

h . (n + 1) = (h . n) + Hn1 by A4, A8, NAT_1:13;

hence h . (n + 1) is imaginary by A8, A7, NAT_1:13; :: thesis: verum

hence eval (I,r) is imaginary by A1, A3; :: thesis: verum