Theorem recni 7802

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 7736	. 2 |- RR C_ CC
2		recni.1	. 2 |- A e. RR
3	1, 2	sselii 3099	1 |- A e. CC

Syntax hints:   e. wcel 1481   CCcc 7642   RRcr 7643

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-11 1485  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-resscn 7736

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-in 3082  df-ss 3089

This theorem is referenced by:  resubcli  8049  ltapii  8421  nncni  8754  2cn  8815  3cn  8819  4cn  8822  5cn  8824  6cn  8826  7cn  8828  8cn  8830  9cn  8832  halfcn  8958  8th4div3  8963  nn0cni  9013  numltc  9231  sqge0i  10410  lt2sqi  10411  le2sqi  10412  sq11i  10413  sqrtmsq2i  10939  0.999...  11322  ef01bndlem  11499  sin4lt0  11509  eirraplem  11519  eirr  11521  egt2lt3  11522  sqrt2irraplemnn  11893  picn  12916  sinhalfpilem  12920  cosneghalfpi  12927  sinhalfpip  12949  sinhalfpim  12950  coshalfpip  12951  coshalfpim  12952  sincosq1sgn  12955  sincosq2sgn  12956  sincosq3sgn  12957  sincosq4sgn  12958  cosq23lt0  12962  coseq00topi  12964  sincosq1eq  12968  sincos4thpi  12969  tan4thpi  12970  sincos6thpi  12971  2logb9irrALT  13099  taupi  13430