Theorem recni 8234

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

Syntax hints:   e. wcel 2202   CCcc 8073   RRcr 8074

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213  ax-resscn 8167

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3207  df-ss 3214

This theorem is referenced by:  resubcli  8484  ltapii  8857  nncni  9195  2cn  9256  3cn  9260  4cn  9263  5cn  9265  6cn  9267  7cn  9269  8cn  9271  9cn  9273  halfcn  9400  8th4div3  9405  nn0cni  9456  numltc  9680  sqge0i  10934  lt2sqi  10935  le2sqi  10936  sq11i  10937  sqrtmsq2i  11758  0.999...  12145  ef01bndlem  12380  sin4lt0  12391  eirraplem  12401  eirr  12403  egt2lt3  12404  sqrt2irraplemnn  12814  modsubi  13055  picn  15581  sinhalfpilem  15585  cosneghalfpi  15592  sinhalfpip  15614  sinhalfpim  15615  coshalfpip  15616  coshalfpim  15617  sincosq1sgn  15620  sincosq2sgn  15621  sincosq3sgn  15622  sincosq4sgn  15623  cosq23lt0  15627  coseq00topi  15629  sincosq1eq  15633  sincos4thpi  15634  tan4thpi  15635  sincos6thpi  15636  2logb9irrALT  15768  taupi  16789