Theorem recni 7971

Description: A real number is a complex number. (Contributed by NM, 1-Mar-1995.)

Hypothesis

Ref	Expression
recni.1	|- A e. RR

Assertion

Ref	Expression
recni	|- A e. CC

Proof of Theorem recni

Step	Hyp	Ref	Expression
1		ax-resscn 7905	. 2 |- RR C_ CC
2		recni.1	. 2 |- A e. RR
3	1, 2	sselii 3154	1 |- A e. CC

Syntax hints:   e. wcel 2148   CCcc 7811   RRcr 7812

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-resscn 7905

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3137  df-ss 3144

This theorem is referenced by:  resubcli  8222  ltapii  8594  nncni  8931  2cn  8992  3cn  8996  4cn  8999  5cn  9001  6cn  9003  7cn  9005  8cn  9007  9cn  9009  halfcn  9135  8th4div3  9140  nn0cni  9190  numltc  9411  sqge0i  10609  lt2sqi  10610  le2sqi  10611  sq11i  10612  sqrtmsq2i  11146  0.999...  11531  ef01bndlem  11766  sin4lt0  11776  eirraplem  11786  eirr  11788  egt2lt3  11789  sqrt2irraplemnn  12181  picn  14293  sinhalfpilem  14297  cosneghalfpi  14304  sinhalfpip  14326  sinhalfpim  14327  coshalfpip  14328  coshalfpim  14329  sincosq1sgn  14332  sincosq2sgn  14333  sincosq3sgn  14334  sincosq4sgn  14335  cosq23lt0  14339  coseq00topi  14341  sincosq1eq  14345  sincos4thpi  14346  tan4thpi  14347  sincos6thpi  14348  2logb9irrALT  14477  taupi  14906