Theorem recni 8031

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

Syntax hints:   e. wcel 2164   CCcc 7870   RRcr 7871

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175  ax-resscn 7964

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-in 3159  df-ss 3166

This theorem is referenced by:  resubcli  8282  ltapii  8654  nncni  8992  2cn  9053  3cn  9057  4cn  9060  5cn  9062  6cn  9064  7cn  9066  8cn  9068  9cn  9070  halfcn  9196  8th4div3  9201  nn0cni  9252  numltc  9473  sqge0i  10697  lt2sqi  10698  le2sqi  10699  sq11i  10700  sqrtmsq2i  11279  0.999...  11664  ef01bndlem  11899  sin4lt0  11910  eirraplem  11920  eirr  11922  egt2lt3  11923  sqrt2irraplemnn  12317  picn  14922  sinhalfpilem  14926  cosneghalfpi  14933  sinhalfpip  14955  sinhalfpim  14956  coshalfpip  14957  coshalfpim  14958  sincosq1sgn  14961  sincosq2sgn  14962  sincosq3sgn  14963  sincosq4sgn  14964  cosq23lt0  14968  coseq00topi  14970  sincosq1eq  14974  sincos4thpi  14975  tan4thpi  14976  sincos6thpi  14977  2logb9irrALT  15106  taupi  15563