Metamath Proof Explorer

Theorem fveecn

Description: The function value of a point is a complex. (Contributed by Scott Fenton, 10-Jun-2013)

Ref Expression
Assertion fveecn 
|- ( ( A e. ( EE ` N ) /\ I e. ( 1 ... N ) ) -> ( A ` I ) e. CC )

Proof

Step Hyp Ref Expression
1 fveere 
 |-  ( ( A e. ( EE ` N ) /\ I e. ( 1 ... N ) ) -> ( A ` I ) e. RR )
2 1 recnd 
 |-  ( ( A e. ( EE ` N ) /\ I e. ( 1 ... N ) ) -> ( A ` I ) e. CC )