MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax-resscn Structured version   Visualization version   GIF version

Axiom ax-resscn 9849
Description: The real numbers are a subset of the complex numbers. Axiom 1 of 22 for real and complex numbers, justified by theorem axresscn 9825. (Contributed by NM, 1-Mar-1995.)
Assertion
Ref Expression
ax-resscn ℝ ⊆ ℂ

Detailed syntax breakdown of Axiom ax-resscn
StepHypRef Expression
1 cr 9791 . 2 class
2 cc 9790 . 2 class
31, 2wss 3539 1 wff ℝ ⊆ ℂ
Colors of variables: wff setvar class
This axiom is referenced by:  recn  9882  reex  9883  recni  9908  nnsscn  10874  nn0sscn  11146  qsscn  11633  reexpcl  12696  rpexpcl  12698  reexpclz  12699  expge0  12715  expge1  12716  rlimrecl  14107  abscn2  14125  recn2  14127  imcn2  14128  climabs  14130  climre  14132  climim  14133  rlimabs  14135  rlimre  14137  rlimim  14138  caurcvgr  14200  caucvgrlem2  14201  caurcvg  14203  fsumrecl  14260  fsumrpcl  14263  fsumge0  14316  fsumre  14329  fsumim  14330  fprodrecl  14470  fprodrpcl  14473  fprodreclf  14476  fprodge0  14511  fprodge1  14513  rerisefaccl  14535  refallfaccl  14536  rprisefaccl  14541  reeff1  14637  nthruc  14767  regsumfsum  19581  rge0srg  19584  rebase  19718  re0g  19724  regsumsupp  19734  remet  22348  tgioo2  22361  xrsdsre  22368  recld2  22372  reperf  22377  iitopon  22437  dfii3  22441  abscncf  22459  recncf  22460  imcncf  22461  abscncfALT  22478  cnmptre  22481  iimulcn  22492  icchmeo  22495  cnrehmeo  22507  evth  22513  evth2  22514  lebnumlem2  22516  lebnumii  22520  reparphti  22552  cphsqrtcl  22736  resscdrg  22906  ishl2  22918  recms  22920  reust  22921  evthicc  22979  evthicc2  22980  ovolfsf  22991  volcn  23124  volivth  23125  ismbf  23147  cncombf  23175  cnmbf  23176  0plef  23189  itg1ge0  23203  i1faddlem  23210  i1fmul  23213  itg1addlem4  23216  i1fsub  23225  itg1sub  23226  mbfi1fseqlem5  23236  xrge0f  23248  itg20  23254  itg2const  23257  itg2mulc  23264  itg2addlem  23275  i1fibl  23324  itgitg1  23325  iblabslem  23344  iblabs  23345  bddmulibl  23355  recnprss  23418  dvcjbr  23462  dvfre  23464  dvnfre  23465  dvferm1  23496  dvferm2  23498  rolle  23501  cmvth  23502  mvth  23503  dvlip  23504  dvlipcn  23505  dvlip2  23506  c1liplem1  23507  c1lip2  23509  dvgt0lem1  23513  dvle  23518  dvivthlem1  23519  dvivth  23521  dvne0  23522  lhop1lem  23524  lhop1  23525  lhop2  23526  lhop  23527  dvcnvrelem1  23528  dvcnvrelem2  23529  dvcnvre  23530  dvcvx  23531  dvfsumle  23532  dvfsumge  23533  dvfsumabs  23534  dvfsumlem2  23538  dvfsumrlim  23542  ftc1a  23548  ftc1lem3  23549  ftc1lem6  23552  ftc1  23553  ftc1cn  23554  ftc2  23555  ftc2ditglem  23556  itgparts  23558  itgsubstlem  23559  itgsubst  23560  aacjcl  23830  aalioulem3  23837  taylthlem2  23876  taylth  23877  abelth2  23944  reeff1olem  23948  efcvx  23951  pilem3  23955  pige3  24017  recosf1o  24029  resinf1o  24030  dvrelog  24127  relogcn  24128  logcnlem5  24136  logcn  24137  dvloglem  24138  dvlog2lem  24142  logccv  24153  dvcxp1  24225  cxpcn3  24233  resqrtcn  24234  loglesqrt  24243  ssscongptld  24296  ressatans  24405  rlimcnp  24436  efrlim  24440  jensenlem1  24457  jensenlem2  24458  jensen  24459  amgm  24461  lgamgulmlem2  24500  ftalem3  24545  basellem9  24559  efnnfsumcl  24573  efchtdvds  24629  lgsdchr  24824  dchrvmasumlem1  24928  dchrisum0lem3  24952  pntlem3  25042  cchhllem  25512  ipasslem7  26868  rexdiv  28758  fsumrp0cl  28819  xrge0slmod  28968  unitsscn  29063  rmulccn  29095  raddcn  29096  xrge0iifhom  29104  lmlimxrge0  29115  rezh  29136  esumpfinvallem  29256  esumpfinval  29257  esumpfinvalf  29258  esumcvg  29268  plymulx0  29743  plymulx  29744  signsplypnf  29746  signsply0  29747  cvxpcon  30271  cvxscon  30272  rescon  30275  ivthALT  31293  dnicn  31445  knoppcnlem10  31455  knoppcnlem11  31456  unbdqndv2  31465  knoppndv  31488  knoppcn2  31490  broucube  32396  mblfinlem2  32400  mbfresfi  32409  ftc1cnnclem  32436  ftc1cnnc  32437  ftc1anclem3  32440  ftc1anclem5  32442  ftc1anclem7  32444  ftc1anclem8  32445  ftc1anc  32446  ftc2nc  32447  asindmre  32448  dvreasin  32451  dvreacos  32452  areacirclem1  32453  areacirclem2  32454  areacirclem3  32455  areacirclem4  32456  areacirc  32458  repwsmet  32586  rrnequiv  32587  rrntotbnd  32588  reheibor  32591  iccbnd  32592  itgpowd  36602  arearect  36603  areaquad  36604  k0004val0  37255  extoimad  37269  imo72b2lem0  37270  imo72b2lem2  37272  imo72b2lem1  37276  imo72b2  37280  ssrecnpr  37312  sblpnf  37314  radcnvrat  37318  lhe4.4ex1a  37333  refsumcn  37995  rr2sscn2  38306  ioosscn  38346  evthiccabs  38348  climreeq  38463  limciccioolb  38471  limcrecl  38479  limcicciooub  38487  limcleqr  38494  lptioo2cn  38495  lptioo1cn  38496  limclner  38501  resincncf  38543  cncficcgt0  38557  cncfiooicclem1  38562  cncfiooiccre  38564  jumpncnp  38567  dvcosre  38582  dvmptconst  38586  dvmptidg  38588  fperdvper  38591  dvmptresicc  38592  dvresioo  38594  dvmulcncf  38598  dvdivcncf  38600  dvbdfbdioolem1  38601  ioodvbdlimc1lem1  38604  ioodvbdlimc1lem2  38605  ioodvbdlimc1  38606  ioodvbdlimc2lem  38607  ioodvbdlimc2  38608  itgsin0pilem1  38624  ibliccsinexp  38625  iblioosinexp  38627  itgsinexplem1  38628  itgsinexp  38629  itgcoscmulx  38644  itgsincmulx  38649  itgsubsticclem  38650  itgiccshift  38655  itgperiod  38656  itgsbtaddcnst  38657  dirkeritg  38778  dirkercncflem2  38780  dirkercncflem3  38781  dirkercncflem4  38782  dirkercncf  38783  fourierdlem16  38799  fourierdlem18  38801  fourierdlem21  38804  fourierdlem22  38805  fourierdlem39  38822  fourierdlem42  38825  fourierdlem48  38830  fourierdlem49  38831  fourierdlem53  38835  fourierdlem57  38839  fourierdlem58  38840  fourierdlem59  38841  fourierdlem60  38842  fourierdlem61  38843  fourierdlem62  38844  fourierdlem68  38850  fourierdlem70  38852  fourierdlem72  38854  fourierdlem73  38855  fourierdlem74  38856  fourierdlem75  38857  fourierdlem76  38858  fourierdlem78  38860  fourierdlem80  38862  fourierdlem83  38865  fourierdlem84  38866  fourierdlem85  38867  fourierdlem88  38870  fourierdlem89  38871  fourierdlem90  38872  fourierdlem91  38873  fourierdlem93  38875  fourierdlem94  38876  fourierdlem95  38877  fourierdlem96  38878  fourierdlem97  38879  fourierdlem98  38880  fourierdlem99  38881  fourierdlem101  38883  fourierdlem103  38885  fourierdlem104  38886  fourierdlem111  38893  fourierdlem112  38894  fourierdlem113  38895  fouriercnp  38902  sqwvfoura  38904  sqwvfourb  38905  fouriersw  38907  fouriercn  38908  etransclem2  38912  etransclem18  38928  etransclem23  38933  etransclem46  38956  rrxtopnfi  38965  rrndistlt  38969  sge0sn  39055  sge0tsms  39056  sge0f1o  39058  sge0pr  39070  sge0resplit  39082  sge0iunmptlemre  39091  sge0isummpt2  39108  hoicvr  39221  hoidmvlelem2  39269  refdivmptf  42115  refdivmptfv  42119  amgmlemALT  42300
  Copyright terms: Public domain W3C validator