Theorem recni 8169

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

Syntax hints:   e. wcel 2200   CCcc 8008   RRcr 8009

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-resscn 8102

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210

This theorem is referenced by:  resubcli  8420  ltapii  8793  nncni  9131  2cn  9192  3cn  9196  4cn  9199  5cn  9201  6cn  9203  7cn  9205  8cn  9207  9cn  9209  halfcn  9336  8th4div3  9341  nn0cni  9392  numltc  9614  sqge0i  10860  lt2sqi  10861  le2sqi  10862  sq11i  10863  sqrtmsq2i  11661  0.999...  12047  ef01bndlem  12282  sin4lt0  12293  eirraplem  12303  eirr  12305  egt2lt3  12306  sqrt2irraplemnn  12716  modsubi  12957  picn  15476  sinhalfpilem  15480  cosneghalfpi  15487  sinhalfpip  15509  sinhalfpim  15510  coshalfpip  15511  coshalfpim  15512  sincosq1sgn  15515  sincosq2sgn  15516  sincosq3sgn  15517  sincosq4sgn  15518  cosq23lt0  15522  coseq00topi  15524  sincosq1eq  15528  sincos4thpi  15529  tan4thpi  15530  sincos6thpi  15531  2logb9irrALT  15663  taupi  16501