Theorem recni 8190

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 8123	. 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 8029   RRcr 8030

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 8123

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  8441  ltapii  8814  nncni  9152  2cn  9213  3cn  9217  4cn  9220  5cn  9222  6cn  9224  7cn  9226  8cn  9228  9cn  9230  halfcn  9357  8th4div3  9362  nn0cni  9413  numltc  9635  sqge0i  10887  lt2sqi  10888  le2sqi  10889  sq11i  10890  sqrtmsq2i  11695  0.999...  12081  ef01bndlem  12316  sin4lt0  12327  eirraplem  12337  eirr  12339  egt2lt3  12340  sqrt2irraplemnn  12750  modsubi  12991  picn  15510  sinhalfpilem  15514  cosneghalfpi  15521  sinhalfpip  15543  sinhalfpim  15544  coshalfpip  15545  coshalfpim  15546  sincosq1sgn  15549  sincosq2sgn  15550  sincosq3sgn  15551  sincosq4sgn  15552  cosq23lt0  15556  coseq00topi  15558  sincosq1eq  15562  sincos4thpi  15563  tan4thpi  15564  sincos6thpi  15565  2logb9irrALT  15697  taupi  16677