Theorem recni 7982

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

Syntax hints:   e. wcel 2158   CCcc 7822   RRcr 7823

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 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-11 1516  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2169  ax-resscn 7916

This theorem depends on definitions:  df-bi 117  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-in 3147  df-ss 3154

This theorem is referenced by:  resubcli  8233  ltapii  8605  nncni  8942  2cn  9003  3cn  9007  4cn  9010  5cn  9012  6cn  9014  7cn  9016  8cn  9018  9cn  9020  halfcn  9146  8th4div3  9151  nn0cni  9201  numltc  9422  sqge0i  10620  lt2sqi  10621  le2sqi  10622  sq11i  10623  sqrtmsq2i  11157  0.999...  11542  ef01bndlem  11777  sin4lt0  11787  eirraplem  11797  eirr  11799  egt2lt3  11800  sqrt2irraplemnn  12192  picn  14479  sinhalfpilem  14483  cosneghalfpi  14490  sinhalfpip  14512  sinhalfpim  14513  coshalfpip  14514  coshalfpim  14515  sincosq1sgn  14518  sincosq2sgn  14519  sincosq3sgn  14520  sincosq4sgn  14521  cosq23lt0  14525  coseq00topi  14527  sincosq1eq  14531  sincos4thpi  14532  tan4thpi  14533  sincos6thpi  14534  2logb9irrALT  14663  taupi  15093