Metamath Proof Explorer


Theorem recnd

Description: Deduction from real number to complex number. (Contributed by NM, 26-Oct-1999)

Ref Expression
Hypothesis recnd.1
|- ( ph -> A e. RR )
Assertion recnd
|- ( ph -> A e. CC )

Proof

Step Hyp Ref Expression
1 recnd.1
 |-  ( ph -> A e. RR )
2 recn
 |-  ( A e. RR -> A e. CC )
3 1 2 syl
 |-  ( ph -> A e. CC )