Axiom ax-resscn 11132

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

Assertion

Ref	Expression
ax-resscn	⊢ ℝ ⊆ ℂ

Detailed syntax breakdown of Axiom ax-resscn

Step	Hyp	Ref	Expression
1		cr 11074	. 2 class ℝ
2		cc 11073	. 2 class ℂ
3	1, 2	wss 3917	1 wff ℝ ⊆ ℂ

This axiom is referenced by:  recn  11165  reex  11166  recni  11195  qsscn  12926  ioosscn  13376  unitsscn  13468  reexpcl  14050  rpexpcl  14052  reexpclz  14054  expge0  14070  expge1  14071  rlimrecl  15553  abscn2  15572  recn2  15574  imcn2  15575  climabs  15577  climre  15579  climim  15580  rlimabs  15582  rlimre  15584  rlimim  15585  caurcvgr  15647  caucvgrlem2  15648  caurcvg  15650  fsumrecl  15707  fsumrpcl  15710  fsumge0  15768  fsumre  15781  fsumim  15782  fprodrecl  15926  fprodrpcl  15929  fprodreclf  15932  fprodge0  15966  fprodge1  15968  rerisefaccl  15990  refallfaccl  15991  rprisefaccl  15996  reeff1  16095  nthruc  16227  regsumfsum  21359  rge0srg  21362  rebase  21522  re0g  21528  regsumsupp  21538  remet  24685  tgioo2  24698  xrsdsre  24706  recld2  24710  reperf  24715  iitopon  24779  dfii3  24783  abscncf  24801  recncf  24802  imcncf  24803  abscncfALT  24825  cnmptre  24828  iimulcnOLD  24842  icchmeo  24845  icchmeoOLD  24846  cnrehmeo  24858  cnrehmeoOLD  24859  evth  24865  evth2  24866  lebnumlem2  24868  lebnumii  24872  reparphtiOLD  24904  cphsqrtcl  25091  resscdrg  25265  ishl2  25277  recms  25287  reust  25288  evthicc  25367  evthicc2  25368  ovolfsf  25379  volcn  25514  volivth  25515  ismbf  25536  cncombf  25566  cnmbf  25567  0plef  25580  itg1ge0  25594  i1faddlem  25601  i1fmul  25604  itg1addlem4  25607  i1fsub  25616  itg1sub  25617  mbfi1fseqlem5  25627  xrge0f  25639  itg20  25645  itg2const  25648  itg2mulc  25655  itg2addlem  25666  i1fibl  25716  itgitg1  25717  iblabslem  25736  iblabs  25737  bddmulibl  25747  recnprss  25812  dvmptresicc  25824  dvcjbr  25860  dvfre  25862  dvnfre  25863  dvferm1  25896  dvferm2  25898  rolle  25901  cmvth  25902  cmvthOLD  25903  mvth  25904  dvlip  25905  dvlipcn  25906  dvlip2  25907  c1liplem1  25908  c1lip2  25910  dvgt0lem1  25914  dvle  25919  dvivthlem1  25920  dvivth  25922  dvne0  25923  lhop1lem  25925  lhop1  25926  lhop2  25927  lhop  25928  dvcnvrelem1  25929  dvcnvrelem2  25930  dvcnvre  25931  dvcvx  25932  dvfsumle  25933  dvfsumleOLD  25934  dvfsumge  25935  dvfsumabs  25936  dvfsumlem2  25940  dvfsumlem2OLD  25941  dvfsumrlim  25945  ftc1a  25951  ftc1lem3  25952  ftc1lem6  25955  ftc1  25956  ftc1cn  25957  ftc2  25958  ftc2ditglem  25959  itgparts  25961  itgsubstlem  25962  itgsubst  25963  itgpowd  25964  aacjcl  26242  aalioulem3  26249  taylthlem2  26289  taylthlem2OLD  26290  taylth  26291  abelth2  26359  reeff1olem  26363  efcvx  26366  pilem3  26370  pige3ALT  26436  recosf1o  26451  resinf1o  26452  dvrelog  26553  relogcn  26554  logcnlem5  26562  logcn  26563  dvloglem  26564  dvlog2lem  26568  logccv  26579  dvcxp1  26656  cxpcn3  26665  resqrtcn  26666  loglesqrt  26678  ssscongptld  26739  ressatans  26851  rlimcnp  26882  efrlim  26886  efrlimOLD  26887  jensenlem1  26904  jensenlem2  26905  jensen  26906  amgm  26908  lgamgulmlem2  26947  ftalem3  26992  basellem9  27006  efnnfsumcl  27020  efchtdvds  27076  lgsdchr  27273  dchrvmasumlem1  27413  dchrisum0lem3  27437  pntlem3  27527  cchhllem  28821  ex-fpar  30398  ipasslem7  30772  fprodex01  32757  indsumin  32792  rexdiv  32853  fsumrp0cl  32969  xrge0slmod  33326  ccfldsrarelvec  33673  ccfldextdgrr  33674  rmulccn  33925  raddcn  33926  xrge0iifhom  33934  lmlimxrge0  33945  rezh  33966  esumpfinvallem  34071  esumpfinval  34072  esumpfinvalf  34073  esumcvg  34083  plymulx0  34545  plymulx  34546  signsplypnf  34548  signsply0  34549  iblidicc  34590  rpsqrtcn  34591  ftc2re  34596  fdvposlt  34597  fdvneggt  34598  fdvposle  34599  fdvnegge  34600  itgexpif  34604  circlemeth  34638  circlemethnat  34639  circlevma  34640  circlemethhgt  34641  logdivsqrle  34648  resconn  35240  ivthALT  36330  dnicn  36487  knoppcnlem10  36497  knoppcnlem11  36498  unbdqndv2  36506  knoppndv  36529  knoppcn2  36531  broucube  37655  mblfinlem2  37659  mbfresfi  37667  ftc1cnnclem  37692  ftc1cnnc  37693  ftc1anclem3  37696  ftc1anclem5  37698  ftc1anclem7  37700  ftc1anclem8  37701  ftc1anc  37702  ftc2nc  37703  asindmre  37704  dvreasin  37707  dvreacos  37708  areacirclem1  37709  areacirclem2  37710  areacirclem3  37711  areacirclem4  37712  areacirc  37714  repwsmet  37835  rrnequiv  37836  rrntotbnd  37837  reheibor  37840  iccbnd  37841  intlewftc  42056  dvrelog2  42059  dvrelog3  42060  aks4d1p1p5  42070  rpsscn  42294  redvmptabs  42355  readvrec2  42356  resuppsinopn  42358  readvcot  42359  resubeqsub  42425  subresre  42426  arearect  43211  areaquad  43212  k0004val0  44150  extoimad  44160  imo72b2lem0  44161  imo72b2lem2  44163  imo72b2lem1  44165  imo72b2  44168  ssrecnpr  44304  sblpnf  44306  radcnvrat  44310  lhe4.4ex1a  44325  refsumcn  45031  rr2sscn2  45369  uzsscn  45478  evthiccabs  45501  climreeq  45618  limciccioolb  45626  limcrecl  45634  limcicciooub  45642  limcleqr  45649  lptioo2cn  45650  lptioo1cn  45651  limclner  45656  liminflimsupclim  45812  resincncf  45880  cncficcgt0  45893  cncfiooicclem1  45898  cncfiooiccre  45900  jumpncnp  45903  dvcosre  45917  dvmptconst  45920  dvmptidg  45922  fperdvper  45924  dvresioo  45926  dvmulcncf  45930  dvdivcncf  45932  dvbdfbdioolem1  45933  ioodvbdlimc1lem1  45936  ioodvbdlimc1lem2  45937  ioodvbdlimc1  45938  ioodvbdlimc2lem  45939  ioodvbdlimc2  45940  itgsin0pilem1  45955  ibliccsinexp  45956  iblioosinexp  45958  itgsinexplem1  45959  itgsinexp  45960  itgcoscmulx  45974  itgsincmulx  45979  itgsubsticclem  45980  itgiccshift  45985  itgperiod  45986  itgsbtaddcnst  45987  dirkeritg  46107  dirkercncflem2  46109  dirkercncflem3  46110  dirkercncflem4  46111  dirkercncf  46112  fourierdlem16  46128  fourierdlem18  46130  fourierdlem21  46133  fourierdlem22  46134  fourierdlem39  46151  fourierdlem42  46154  fourierdlem48  46159  fourierdlem49  46160  fourierdlem53  46164  fourierdlem57  46168  fourierdlem58  46169  fourierdlem59  46170  fourierdlem60  46171  fourierdlem61  46172  fourierdlem62  46173  fourierdlem68  46179  fourierdlem70  46181  fourierdlem72  46183  fourierdlem73  46184  fourierdlem74  46185  fourierdlem75  46186  fourierdlem76  46187  fourierdlem78  46189  fourierdlem80  46191  fourierdlem83  46194  fourierdlem84  46195  fourierdlem85  46196  fourierdlem88  46199  fourierdlem89  46200  fourierdlem90  46201  fourierdlem91  46202  fourierdlem93  46204  fourierdlem94  46205  fourierdlem95  46206  fourierdlem96  46207  fourierdlem97  46208  fourierdlem98  46209  fourierdlem99  46210  fourierdlem101  46212  fourierdlem103  46214  fourierdlem104  46215  fourierdlem111  46222  fourierdlem112  46223  fourierdlem113  46224  fouriercnp  46231  sqwvfoura  46233  sqwvfourb  46234  fouriersw  46236  fouriercn  46237  etransclem2  46241  etransclem18  46257  etransclem23  46262  etransclem46  46285  rrxtopnfi  46292  rrndistlt  46295  sge0sn  46384  sge0tsms  46385  sge0f1o  46387  sge0pr  46399  sge0resplit  46411  sge0iunmptlemre  46420  sge0isummpt2  46437  hoicvr  46553  hoidmvlelem2  46601  lamberte  46896  refdivmptf  48535  refdivmptfv  48539  amgmlemALT  49796