Axiom ax-resscn 10929

Description: The real numbers are a subset of the complex numbers. Axiom 1 of 22 for real and complex numbers, justified by Theorem axresscn 10905. (Contributed by NM, 1-Mar-1995.)

Assertion

Ref	Expression
ax-resscn	⊢ ℝ ⊆ ℂ

Detailed syntax breakdown of Axiom ax-resscn

Step	Hyp	Ref	Expression
1		cr 10871	. 2 class ℝ
2		cc 10870	. 2 class ℂ
3	1, 2	wss 3892	1 wff ℝ ⊆ ℂ

This axiom is referenced by:  recn  10962  reex  10963  recni  10990  qsscn  12699  ioosscn  13140  unitsscn  13231  reexpcl  13797  rpexpcl  13799  reexpclz  13800  expge0  13817  expge1  13818  rlimrecl  15287  abscn2  15306  recn2  15308  imcn2  15309  climabs  15311  climre  15313  climim  15314  rlimabs  15316  rlimre  15318  rlimim  15319  caurcvgr  15383  caucvgrlem2  15384  caurcvg  15386  fsumrecl  15444  fsumrpcl  15447  fsumge0  15505  fsumre  15518  fsumim  15519  fprodrecl  15661  fprodrpcl  15664  fprodreclf  15667  fprodge0  15701  fprodge1  15703  rerisefaccl  15725  refallfaccl  15726  rprisefaccl  15731  reeff1  15827  nthruc  15959  regsumfsum  20664  rge0srg  20667  rebase  20809  re0g  20815  regsumsupp  20825  remet  23951  tgioo2  23964  xrsdsre  23971  recld2  23975  reperf  23980  iitopon  24040  dfii3  24044  abscncf  24062  recncf  24063  imcncf  24064  abscncfALT  24085  cnmptre  24088  iimulcn  24099  icchmeo  24102  cnrehmeo  24114  evth  24120  evth2  24121  lebnumlem2  24123  lebnumii  24127  reparphti  24158  cphsqrtcl  24346  resscdrg  24520  ishl2  24532  recms  24542  reust  24543  evthicc  24621  evthicc2  24622  ovolfsf  24633  volcn  24768  volivth  24769  ismbf  24790  cncombf  24820  cnmbf  24821  0plef  24834  itg1ge0  24848  i1faddlem  24855  i1fmul  24858  itg1addlem4  24861  itg1addlem4OLD  24862  i1fsub  24871  itg1sub  24872  mbfi1fseqlem5  24882  xrge0f  24894  itg20  24900  itg2const  24903  itg2mulc  24910  itg2addlem  24921  i1fibl  24970  itgitg1  24971  iblabslem  24990  iblabs  24991  bddmulibl  25001  recnprss  25066  dvmptresicc  25078  dvcjbr  25111  dvfre  25113  dvnfre  25114  dvferm1  25147  dvferm2  25149  rolle  25152  cmvth  25153  mvth  25154  dvlip  25155  dvlipcn  25156  dvlip2  25157  c1liplem1  25158  c1lip2  25160  dvgt0lem1  25164  dvle  25169  dvivthlem1  25170  dvivth  25172  dvne0  25173  lhop1lem  25175  lhop1  25176  lhop2  25177  lhop  25178  dvcnvrelem1  25179  dvcnvrelem2  25180  dvcnvre  25181  dvcvx  25182  dvfsumle  25183  dvfsumge  25184  dvfsumabs  25185  dvfsumlem2  25189  dvfsumrlim  25193  ftc1a  25199  ftc1lem3  25200  ftc1lem6  25203  ftc1  25204  ftc1cn  25205  ftc2  25206  ftc2ditglem  25207  itgparts  25209  itgsubstlem  25210  itgsubst  25211  itgpowd  25212  aacjcl  25485  aalioulem3  25492  taylthlem2  25531  taylth  25532  abelth2  25599  reeff1olem  25603  efcvx  25606  pilem3  25610  pige3ALT  25674  recosf1o  25689  resinf1o  25690  dvrelog  25790  relogcn  25791  logcnlem5  25799  logcn  25800  dvloglem  25801  dvlog2lem  25805  logccv  25816  dvcxp1  25891  cxpcn3  25899  resqrtcn  25900  loglesqrt  25909  ssscongptld  25970  ressatans  26082  rlimcnp  26113  efrlim  26117  jensenlem1  26134  jensenlem2  26135  jensen  26136  amgm  26138  lgamgulmlem2  26177  ftalem3  26222  basellem9  26236  efnnfsumcl  26250  efchtdvds  26306  lgsdchr  26501  dchrvmasumlem1  26641  dchrisum0lem3  26665  pntlem3  26755  cchhllem  27252  cchhllemOLD  27253  ex-fpar  28822  ipasslem7  29194  fprodex01  31135  rexdiv  31196  fsumrp0cl  31300  xrge0slmod  31544  ccfldsrarelvec  31737  ccfldextdgrr  31738  rmulccn  31874  raddcn  31875  xrge0iifhom  31883  lmlimxrge0  31894  rezh  31917  indsumin  31986  esumpfinvallem  32038  esumpfinval  32039  esumpfinvalf  32040  esumcvg  32050  plymulx0  32522  plymulx  32523  signsplypnf  32525  signsply0  32526  iblidicc  32568  rpsqrtcn  32569  ftc2re  32574  fdvposlt  32575  fdvneggt  32576  fdvposle  32577  fdvnegge  32578  itgexpif  32582  circlemeth  32616  circlemethnat  32617  circlevma  32618  circlemethhgt  32619  logdivsqrle  32626  cvxpconn  33200  cvxsconn  33201  resconn  33204  ivthALT  34520  dnicn  34668  knoppcnlem10  34678  knoppcnlem11  34679  unbdqndv2  34687  knoppndv  34710  knoppcn2  34712  broucube  35807  mblfinlem2  35811  mbfresfi  35819  ftc1cnnclem  35844  ftc1cnnc  35845  ftc1anclem3  35848  ftc1anclem5  35850  ftc1anclem7  35852  ftc1anclem8  35853  ftc1anc  35854  ftc2nc  35855  asindmre  35856  dvreasin  35859  dvreacos  35860  areacirclem1  35861  areacirclem2  35862  areacirclem3  35863  areacirclem4  35864  areacirc  35866  repwsmet  35988  rrnequiv  35989  rrntotbnd  35990  reheibor  35993  iccbnd  35994  intlewftc  40066  dvrelog2  40069  dvrelog3  40070  aks4d1p1p5  40080  resubeqsub  40408  subresre  40409  arearect  41043  areaquad  41044  k0004val0  41734  extoimad  41745  imo72b2lem0  41746  imo72b2lem2  41748  imo72b2lem1  41750  imo72b2  41753  ssrecnpr  41896  sblpnf  41898  radcnvrat  41902  lhe4.4ex1a  41917  refsumcn  42543  rr2sscn2  42876  uzsscn  42987  evthiccabs  43005  climreeq  43125  limciccioolb  43133  limcrecl  43141  limcicciooub  43149  limcleqr  43156  lptioo2cn  43157  lptioo1cn  43158  limclner  43163  liminflimsupclim  43319  resincncf  43387  cncficcgt0  43400  cncfiooicclem1  43405  cncfiooiccre  43407  jumpncnp  43410  dvcosre  43424  dvmptconst  43427  dvmptidg  43429  fperdvper  43431  dvresioo  43433  dvmulcncf  43437  dvdivcncf  43439  dvbdfbdioolem1  43440  ioodvbdlimc1lem1  43443  ioodvbdlimc1lem2  43444  ioodvbdlimc1  43445  ioodvbdlimc2lem  43446  ioodvbdlimc2  43447  itgsin0pilem1  43462  ibliccsinexp  43463  iblioosinexp  43465  itgsinexplem1  43466  itgsinexp  43467  itgcoscmulx  43481  itgsincmulx  43486  itgsubsticclem  43487  itgiccshift  43492  itgperiod  43493  itgsbtaddcnst  43494  dirkeritg  43614  dirkercncflem2  43616  dirkercncflem3  43617  dirkercncflem4  43618  dirkercncf  43619  fourierdlem16  43635  fourierdlem18  43637  fourierdlem21  43640  fourierdlem22  43641  fourierdlem39  43658  fourierdlem42  43661  fourierdlem48  43666  fourierdlem49  43667  fourierdlem53  43671  fourierdlem57  43675  fourierdlem58  43676  fourierdlem59  43677  fourierdlem60  43678  fourierdlem61  43679  fourierdlem62  43680  fourierdlem68  43686  fourierdlem70  43688  fourierdlem72  43690  fourierdlem73  43691  fourierdlem74  43692  fourierdlem75  43693  fourierdlem76  43694  fourierdlem78  43696  fourierdlem80  43698  fourierdlem83  43701  fourierdlem84  43702  fourierdlem85  43703  fourierdlem88  43706  fourierdlem89  43707  fourierdlem90  43708  fourierdlem91  43709  fourierdlem93  43711  fourierdlem94  43712  fourierdlem95  43713  fourierdlem96  43714  fourierdlem97  43715  fourierdlem98  43716  fourierdlem99  43717  fourierdlem101  43719  fourierdlem103  43721  fourierdlem104  43722  fourierdlem111  43729  fourierdlem112  43730  fourierdlem113  43731  fouriercnp  43738  sqwvfoura  43740  sqwvfourb  43741  fouriersw  43743  fouriercn  43744  etransclem2  43748  etransclem18  43764  etransclem23  43769  etransclem46  43792  rrxtopnfi  43799  rrndistlt  43802  sge0sn  43888  sge0tsms  43889  sge0f1o  43891  sge0pr  43903  sge0resplit  43915  sge0iunmptlemre  43924  sge0isummpt2  43941  hoicvr  44057  hoidmvlelem2  44105  refdivmptf  45857  refdivmptfv  45861  amgmlemALT  46476