Theorem recni 8119

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

Syntax hints:   e. wcel 2178   CCcc 7958   RRcr 7959

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189  ax-resscn 8052

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-in 3180  df-ss 3187

This theorem is referenced by:  resubcli  8370  ltapii  8743  nncni  9081  2cn  9142  3cn  9146  4cn  9149  5cn  9151  6cn  9153  7cn  9155  8cn  9157  9cn  9159  halfcn  9286  8th4div3  9291  nn0cni  9342  numltc  9564  sqge0i  10808  lt2sqi  10809  le2sqi  10810  sq11i  10811  sqrtmsq2i  11561  0.999...  11947  ef01bndlem  12182  sin4lt0  12193  eirraplem  12203  eirr  12205  egt2lt3  12206  sqrt2irraplemnn  12616  modsubi  12857  picn  15374  sinhalfpilem  15378  cosneghalfpi  15385  sinhalfpip  15407  sinhalfpim  15408  coshalfpip  15409  coshalfpim  15410  sincosq1sgn  15413  sincosq2sgn  15414  sincosq3sgn  15415  sincosq4sgn  15416  cosq23lt0  15420  coseq00topi  15422  sincosq1eq  15426  sincos4thpi  15427  tan4thpi  15428  sincos6thpi  15429  2logb9irrALT  15561  taupi  16214