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  10888  lt2sqi  10889  le2sqi  10890  sq11i  10891  sqrtmsq2i  11696  0.999...  12083  ef01bndlem  12318  sin4lt0  12329  eirraplem  12339  eirr  12341  egt2lt3  12342  sqrt2irraplemnn  12752  modsubi  12993  picn  15513  sinhalfpilem  15517  cosneghalfpi  15524  sinhalfpip  15546  sinhalfpim  15547  coshalfpip  15548  coshalfpim  15549  sincosq1sgn  15552  sincosq2sgn  15553  sincosq3sgn  15554  sincosq4sgn  15555  cosq23lt0  15559  coseq00topi  15561  sincosq1eq  15565  sincos4thpi  15566  tan4thpi  15567  sincos6thpi  15568  2logb9irrALT  15700  taupi  16680