Theorem fveecn

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

	Ref	Expression
Assertion	fveecn	$$⊢\left(A\in 𝔼\left(N\right)\wedge I\in \left(1\dots N\right)\right)\to A\left(I\right)\in ℂ$$

Proof

Step	Hyp	Ref	Expression
1		fveere	$$⊢\left(A\in 𝔼\left(N\right)\wedge I\in \left(1\dots N\right)\right)\to A\left(I\right)\in ℝ$$
2	1	recnd	$$⊢\left(A\in 𝔼\left(N\right)\wedge I\in \left(1\dots N\right)\right)\to A\left(I\right)\in ℂ$$