Theorem recni 8191

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

Syntax hints:   e. wcel 2202   CCcc 8030   RRcr 8031

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-resscn 8124

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3206  df-ss 3213

This theorem is referenced by:  resubcli  8442  ltapii  8815  nncni  9153  2cn  9214  3cn  9218  4cn  9221  5cn  9223  6cn  9225  7cn  9227  8cn  9229  9cn  9231  halfcn  9358  8th4div3  9363  nn0cni  9414  numltc  9636  sqge0i  10889  lt2sqi  10890  le2sqi  10891  sq11i  10892  sqrtmsq2i  11713  0.999...  12100  ef01bndlem  12335  sin4lt0  12346  eirraplem  12356  eirr  12358  egt2lt3  12359  sqrt2irraplemnn  12769  modsubi  13010  picn  15530  sinhalfpilem  15534  cosneghalfpi  15541  sinhalfpip  15563  sinhalfpim  15564  coshalfpip  15565  coshalfpim  15566  sincosq1sgn  15569  sincosq2sgn  15570  sincosq3sgn  15571  sincosq4sgn  15572  cosq23lt0  15576  coseq00topi  15578  sincosq1eq  15582  sincos4thpi  15583  tan4thpi  15584  sincos6thpi  15585  2logb9irrALT  15717  taupi  16729