Theorem recni 8181

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

Syntax hints:   e. wcel 2200   CCcc 8020   RRcr 8021

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 8114

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 3204  df-ss 3211

This theorem is referenced by:  resubcli  8432  ltapii  8805  nncni  9143  2cn  9204  3cn  9208  4cn  9211  5cn  9213  6cn  9215  7cn  9217  8cn  9219  9cn  9221  halfcn  9348  8th4div3  9353  nn0cni  9404  numltc  9626  sqge0i  10878  lt2sqi  10879  le2sqi  10880  sq11i  10881  sqrtmsq2i  11686  0.999...  12072  ef01bndlem  12307  sin4lt0  12318  eirraplem  12328  eirr  12330  egt2lt3  12331  sqrt2irraplemnn  12741  modsubi  12982  picn  15501  sinhalfpilem  15505  cosneghalfpi  15512  sinhalfpip  15534  sinhalfpim  15535  coshalfpip  15536  coshalfpim  15537  sincosq1sgn  15540  sincosq2sgn  15541  sincosq3sgn  15542  sincosq4sgn  15543  cosq23lt0  15547  coseq00topi  15549  sincosq1eq  15553  sincos4thpi  15554  tan4thpi  15555  sincos6thpi  15556  2logb9irrALT  15688  taupi  16613