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 10583
Description: The real numbers are a subset of the complex numbers. Axiom 1 of 22 for real and complex numbers, justified by theorem axresscn 10559. (Contributed by NM, 1-Mar-1995.)
Assertion
Ref Expression
ax-resscn ℝ ⊆ ℂ

Detailed syntax breakdown of Axiom ax-resscn
StepHypRef Expression
1 cr 10525 . 2 class
2 cc 10524 . 2 class
31, 2wss 3935 1 wff ℝ ⊆ ℂ
Colors of variables: wff setvar class
This axiom is referenced by:  recn  10616  reex  10617  recni  10644  qsscn  12349  reexpcl  13436  rpexpcl  13438  reexpclz  13439  expge0  13455  expge1  13456  rlimrecl  14927  abscn2  14945  recn2  14947  imcn2  14948  climabs  14950  climre  14952  climim  14953  rlimabs  14955  rlimre  14957  rlimim  14958  caurcvgr  15020  caucvgrlem2  15021  caurcvg  15023  fsumrecl  15081  fsumrpcl  15084  fsumge0  15140  fsumre  15153  fsumim  15154  fprodrecl  15297  fprodrpcl  15300  fprodreclf  15303  fprodge0  15337  fprodge1  15339  rerisefaccl  15361  refallfaccl  15362  rprisefaccl  15367  reeff1  15463  nthruc  15595  regsumfsum  20543  rge0srg  20546  rebase  20680  re0g  20686  regsumsupp  20696  remet  23327  tgioo2  23340  xrsdsre  23347  recld2  23351  reperf  23356  iitopon  23416  dfii3  23420  abscncf  23438  recncf  23439  imcncf  23440  abscncfALT  23457  cnmptre  23460  iimulcn  23471  icchmeo  23474  cnrehmeo  23486  evth  23492  evth2  23493  lebnumlem2  23495  lebnumii  23499  reparphti  23530  cphsqrtcl  23717  resscdrg  23890  ishl2  23902  recms  23912  reust  23913  evthicc  23989  evthicc2  23990  ovolfsf  24001  volcn  24136  volivth  24137  ismbf  24158  cncombf  24188  cnmbf  24189  0plef  24202  itg1ge0  24216  i1faddlem  24223  i1fmul  24226  itg1addlem4  24229  i1fsub  24238  itg1sub  24239  mbfi1fseqlem5  24249  xrge0f  24261  itg20  24267  itg2const  24270  itg2mulc  24277  itg2addlem  24288  i1fibl  24337  itgitg1  24338  iblabslem  24357  iblabs  24358  bddmulibl  24368  recnprss  24431  dvcjbr  24475  dvfre  24477  dvnfre  24478  dvferm1  24511  dvferm2  24513  rolle  24516  cmvth  24517  mvth  24518  dvlip  24519  dvlipcn  24520  dvlip2  24521  c1liplem1  24522  c1lip2  24524  dvgt0lem1  24528  dvle  24533  dvivthlem1  24534  dvivth  24536  dvne0  24537  lhop1lem  24539  lhop1  24540  lhop2  24541  lhop  24542  dvcnvrelem1  24543  dvcnvrelem2  24544  dvcnvre  24545  dvcvx  24546  dvfsumle  24547  dvfsumge  24548  dvfsumabs  24549  dvfsumlem2  24553  dvfsumrlim  24557  ftc1a  24563  ftc1lem3  24564  ftc1lem6  24567  ftc1  24568  ftc1cn  24569  ftc2  24570  ftc2ditglem  24571  itgparts  24573  itgsubstlem  24574  itgsubst  24575  aacjcl  24845  aalioulem3  24852  taylthlem2  24891  taylth  24892  abelth2  24959  reeff1olem  24963  efcvx  24966  pilem3  24970  pige3ALT  25034  recosf1o  25046  resinf1o  25047  dvrelog  25147  relogcn  25148  logcnlem5  25156  logcn  25157  dvloglem  25158  dvlog2lem  25162  logccv  25173  dvcxp1  25248  cxpcn3  25256  resqrtcn  25257  loglesqrt  25266  ssscongptld  25327  ressatans  25439  rlimcnp  25471  efrlim  25475  jensenlem1  25492  jensenlem2  25493  jensen  25494  amgm  25496  lgamgulmlem2  25535  ftalem3  25580  basellem9  25594  efnnfsumcl  25608  efchtdvds  25664  lgsdchr  25859  dchrvmasumlem1  25999  dchrisum0lem3  26023  pntlem3  26113  cchhllem  26601  ex-fpar  28169  ipasslem7  28541  fprodex01  30469  rexdiv  30530  fsumrp0cl  30610  xrge0slmod  30845  ccfldsrarelvec  30956  ccfldextdgrr  30957  unitsscn  31039  rmulccn  31071  raddcn  31072  xrge0iifhom  31080  lmlimxrge0  31091  rezh  31112  indsumin  31181  esumpfinvallem  31233  esumpfinval  31234  esumpfinvalf  31235  esumcvg  31245  plymulx0  31717  plymulx  31718  signsplypnf  31720  signsply0  31721  iblidicc  31763  rpsqrtcn  31764  ftc2re  31769  fdvposlt  31770  fdvneggt  31771  fdvposle  31772  fdvnegge  31773  itgexpif  31777  circlemeth  31811  circlemethnat  31812  circlevma  31813  circlemethhgt  31814  logdivsqrle  31821  cvxpconn  32387  cvxsconn  32388  resconn  32391  ivthALT  33581  dnicn  33729  knoppcnlem10  33739  knoppcnlem11  33740  unbdqndv2  33748  knoppndv  33771  knoppcn2  33773  broucube  34808  mblfinlem2  34812  mbfresfi  34820  ftc1cnnclem  34847  ftc1cnnc  34848  ftc1anclem3  34851  ftc1anclem5  34853  ftc1anclem7  34855  ftc1anclem8  34856  ftc1anc  34857  ftc2nc  34858  asindmre  34859  dvreasin  34862  dvreacos  34863  areacirclem1  34864  areacirclem2  34865  areacirclem3  34866  areacirclem4  34867  areacirc  34869  repwsmet  34995  rrnequiv  34996  rrntotbnd  34997  reheibor  35000  iccbnd  35001  itgpowd  39701  arearect  39702  areaquad  39703  k0004val0  40384  extoimad  40395  imo72b2lem0  40396  imo72b2lem2  40398  imo72b2lem1  40402  imo72b2  40406  ssrecnpr  40520  sblpnf  40522  radcnvrat  40526  lhe4.4ex1a  40541  refsumcn  41167  rr2sscn2  41514  uzsscn  41632  ioosscn  41649  evthiccabs  41651  climreeq  41774  limciccioolb  41782  limcrecl  41790  limcicciooub  41798  limcleqr  41805  lptioo2cn  41806  lptioo1cn  41807  limclner  41812  liminflimsupclim  41968  resincncf  42038  cncficcgt0  42051  cncfiooicclem1  42056  cncfiooiccre  42058  jumpncnp  42061  dvcosre  42076  dvmptconst  42079  dvmptidg  42081  fperdvper  42083  dvmptresicc  42084  dvresioo  42086  dvmulcncf  42090  dvdivcncf  42092  dvbdfbdioolem1  42093  ioodvbdlimc1lem1  42096  ioodvbdlimc1lem2  42097  ioodvbdlimc1  42098  ioodvbdlimc2lem  42099  ioodvbdlimc2  42100  itgsin0pilem1  42115  ibliccsinexp  42116  iblioosinexp  42118  itgsinexplem1  42119  itgsinexp  42120  itgcoscmulx  42134  itgsincmulx  42139  itgsubsticclem  42140  itgiccshift  42145  itgperiod  42146  itgsbtaddcnst  42147  dirkeritg  42268  dirkercncflem2  42270  dirkercncflem3  42271  dirkercncflem4  42272  dirkercncf  42273  fourierdlem16  42289  fourierdlem18  42291  fourierdlem21  42294  fourierdlem22  42295  fourierdlem39  42312  fourierdlem42  42315  fourierdlem48  42320  fourierdlem49  42321  fourierdlem53  42325  fourierdlem57  42329  fourierdlem58  42330  fourierdlem59  42331  fourierdlem60  42332  fourierdlem61  42333  fourierdlem62  42334  fourierdlem68  42340  fourierdlem70  42342  fourierdlem72  42344  fourierdlem73  42345  fourierdlem74  42346  fourierdlem75  42347  fourierdlem76  42348  fourierdlem78  42350  fourierdlem80  42352  fourierdlem83  42355  fourierdlem84  42356  fourierdlem85  42357  fourierdlem88  42360  fourierdlem89  42361  fourierdlem90  42362  fourierdlem91  42363  fourierdlem93  42365  fourierdlem94  42366  fourierdlem95  42367  fourierdlem96  42368  fourierdlem97  42369  fourierdlem98  42370  fourierdlem99  42371  fourierdlem101  42373  fourierdlem103  42375  fourierdlem104  42376  fourierdlem111  42383  fourierdlem112  42384  fourierdlem113  42385  fouriercnp  42392  sqwvfoura  42394  sqwvfourb  42395  fouriersw  42397  fouriercn  42398  etransclem2  42402  etransclem18  42418  etransclem23  42423  etransclem46  42446  rrxtopnfi  42453  rrndistlt  42456  sge0sn  42542  sge0tsms  42543  sge0f1o  42545  sge0pr  42557  sge0resplit  42569  sge0iunmptlemre  42578  sge0isummpt2  42595  hoicvr  42711  hoidmvlelem2  42759  refdivmptf  44500  refdivmptfv  44504  amgmlemALT  44802
  Copyright terms: Public domain W3C validator