Theorem fveecn

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

	Ref	Expression
Assertion	fveecn	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐼 ∈ ( 1 ... 𝑁 ) ) → ( 𝐴 ‘ 𝐼 ) ∈ ℂ )

Proof

Step	Hyp	Ref	Expression
1		fveere	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐼 ∈ ( 1 ... 𝑁 ) ) → ( 𝐴 ‘ 𝐼 ) ∈ ℝ )
2	1	recnd	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐼 ∈ ( 1 ... 𝑁 ) ) → ( 𝐴 ‘ 𝐼 ) ∈ ℂ )