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

Detailed syntax breakdown of Axiom ax-resscn
StepHypRef Expression
1 cr 9814 . 2 class
2 cc 9813 . 2 class
31, 2wss 3540 1 wff ℝ ⊆ ℂ
Colors of variables: wff setvar class
This axiom is referenced by:  recn  9905  reex  9906  recni  9931  nnsscn  10902  nn0sscn  11174  qsscn  11675  reexpcl  12739  rpexpcl  12741  reexpclz  12742  expge0  12758  expge1  12759  rlimrecl  14159  abscn2  14177  recn2  14179  imcn2  14180  climabs  14182  climre  14184  climim  14185  rlimabs  14187  rlimre  14189  rlimim  14190  caurcvgr  14252  caucvgrlem2  14253  caurcvg  14255  fsumrecl  14312  fsumrpcl  14315  fsumge0  14368  fsumre  14381  fsumim  14382  fprodrecl  14522  fprodrpcl  14525  fprodreclf  14528  fprodge0  14563  fprodge1  14565  rerisefaccl  14587  refallfaccl  14588  rprisefaccl  14593  reeff1  14689  nthruc  14819  regsumfsum  19633  rge0srg  19636  rebase  19771  re0g  19777  regsumsupp  19787  remet  22401  tgioo2  22414  xrsdsre  22421  recld2  22425  reperf  22430  iitopon  22490  dfii3  22494  abscncf  22512  recncf  22513  imcncf  22514  abscncfALT  22531  cnmptre  22534  iimulcn  22545  icchmeo  22548  cnrehmeo  22560  evth  22566  evth2  22567  lebnumlem2  22569  lebnumii  22573  reparphti  22605  cphsqrtcl  22792  resscdrg  22962  ishl2  22974  recms  22976  reust  22977  evthicc  23035  evthicc2  23036  ovolfsf  23047  volcn  23180  volivth  23181  ismbf  23203  cncombf  23231  cnmbf  23232  0plef  23245  itg1ge0  23259  i1faddlem  23266  i1fmul  23269  itg1addlem4  23272  i1fsub  23281  itg1sub  23282  mbfi1fseqlem5  23292  xrge0f  23304  itg20  23310  itg2const  23313  itg2mulc  23320  itg2addlem  23331  i1fibl  23380  itgitg1  23381  iblabslem  23400  iblabs  23401  bddmulibl  23411  recnprss  23474  dvcjbr  23518  dvfre  23520  dvnfre  23521  dvferm1  23552  dvferm2  23554  rolle  23557  cmvth  23558  mvth  23559  dvlip  23560  dvlipcn  23561  dvlip2  23562  c1liplem1  23563  c1lip2  23565  dvgt0lem1  23569  dvle  23574  dvivthlem1  23575  dvivth  23577  dvne0  23578  lhop1lem  23580  lhop1  23581  lhop2  23582  lhop  23583  dvcnvrelem1  23584  dvcnvrelem2  23585  dvcnvre  23586  dvcvx  23587  dvfsumle  23588  dvfsumge  23589  dvfsumabs  23590  dvfsumlem2  23594  dvfsumrlim  23598  ftc1a  23604  ftc1lem3  23605  ftc1lem6  23608  ftc1  23609  ftc1cn  23610  ftc2  23611  ftc2ditglem  23612  itgparts  23614  itgsubstlem  23615  itgsubst  23616  aacjcl  23886  aalioulem3  23893  taylthlem2  23932  taylth  23933  abelth2  24000  reeff1olem  24004  efcvx  24007  pilem3  24011  pige3  24073  recosf1o  24085  resinf1o  24086  dvrelog  24183  relogcn  24184  logcnlem5  24192  logcn  24193  dvloglem  24194  dvlog2lem  24198  logccv  24209  dvcxp1  24281  cxpcn3  24289  resqrtcn  24290  loglesqrt  24299  ssscongptld  24352  ressatans  24461  rlimcnp  24492  efrlim  24496  jensenlem1  24513  jensenlem2  24514  jensen  24515  amgm  24517  lgamgulmlem2  24556  ftalem3  24601  basellem9  24615  efnnfsumcl  24629  efchtdvds  24685  lgsdchr  24880  dchrvmasumlem1  24984  dchrisum0lem3  25008  pntlem3  25098  cchhllem  25567  ipasslem7  27075  rexdiv  28965  fsumrp0cl  29026  xrge0slmod  29175  unitsscn  29270  rmulccn  29302  raddcn  29303  xrge0iifhom  29311  lmlimxrge0  29322  rezh  29343  esumpfinvallem  29463  esumpfinval  29464  esumpfinvalf  29465  esumcvg  29475  plymulx0  29950  plymulx  29951  signsplypnf  29953  signsply0  29954  cvxpcon  30478  cvxscon  30479  rescon  30482  ivthALT  31500  dnicn  31652  knoppcnlem10  31662  knoppcnlem11  31663  unbdqndv2  31672  knoppndv  31695  knoppcn2  31697  broucube  32613  mblfinlem2  32617  mbfresfi  32626  ftc1cnnclem  32653  ftc1cnnc  32654  ftc1anclem3  32657  ftc1anclem5  32659  ftc1anclem7  32661  ftc1anclem8  32662  ftc1anc  32663  ftc2nc  32664  asindmre  32665  dvreasin  32668  dvreacos  32669  areacirclem1  32670  areacirclem2  32671  areacirclem3  32672  areacirclem4  32673  areacirc  32675  repwsmet  32803  rrnequiv  32804  rrntotbnd  32805  reheibor  32808  iccbnd  32809  itgpowd  36819  arearect  36820  areaquad  36821  k0004val0  37472  extoimad  37486  imo72b2lem0  37487  imo72b2lem2  37489  imo72b2lem1  37493  imo72b2  37497  ssrecnpr  37529  sblpnf  37531  radcnvrat  37535  lhe4.4ex1a  37550  refsumcn  38212  rr2sscn2  38523  ioosscn  38563  evthiccabs  38565  climreeq  38680  limciccioolb  38688  limcrecl  38696  limcicciooub  38704  limcleqr  38711  lptioo2cn  38712  lptioo1cn  38713  limclner  38718  resincncf  38760  cncficcgt0  38774  cncfiooicclem1  38779  cncfiooiccre  38781  jumpncnp  38784  dvcosre  38799  dvmptconst  38803  dvmptidg  38805  fperdvper  38808  dvmptresicc  38809  dvresioo  38811  dvmulcncf  38815  dvdivcncf  38817  dvbdfbdioolem1  38818  ioodvbdlimc1lem1  38821  ioodvbdlimc1lem2  38822  ioodvbdlimc1  38823  ioodvbdlimc2lem  38824  ioodvbdlimc2  38825  itgsin0pilem1  38841  ibliccsinexp  38842  iblioosinexp  38844  itgsinexplem1  38845  itgsinexp  38846  itgcoscmulx  38861  itgsincmulx  38866  itgsubsticclem  38867  itgiccshift  38872  itgperiod  38873  itgsbtaddcnst  38874  dirkeritg  38995  dirkercncflem2  38997  dirkercncflem3  38998  dirkercncflem4  38999  dirkercncf  39000  fourierdlem16  39016  fourierdlem18  39018  fourierdlem21  39021  fourierdlem22  39022  fourierdlem39  39039  fourierdlem42  39042  fourierdlem48  39047  fourierdlem49  39048  fourierdlem53  39052  fourierdlem57  39056  fourierdlem58  39057  fourierdlem59  39058  fourierdlem60  39059  fourierdlem61  39060  fourierdlem62  39061  fourierdlem68  39067  fourierdlem70  39069  fourierdlem72  39071  fourierdlem73  39072  fourierdlem74  39073  fourierdlem75  39074  fourierdlem76  39075  fourierdlem78  39077  fourierdlem80  39079  fourierdlem83  39082  fourierdlem84  39083  fourierdlem85  39084  fourierdlem88  39087  fourierdlem89  39088  fourierdlem90  39089  fourierdlem91  39090  fourierdlem93  39092  fourierdlem94  39093  fourierdlem95  39094  fourierdlem96  39095  fourierdlem97  39096  fourierdlem98  39097  fourierdlem99  39098  fourierdlem101  39100  fourierdlem103  39102  fourierdlem104  39103  fourierdlem111  39110  fourierdlem112  39111  fourierdlem113  39112  fouriercnp  39119  sqwvfoura  39121  sqwvfourb  39122  fouriersw  39124  fouriercn  39125  etransclem2  39129  etransclem18  39145  etransclem23  39150  etransclem46  39173  rrxtopnfi  39182  rrndistlt  39186  sge0sn  39272  sge0tsms  39273  sge0f1o  39275  sge0pr  39287  sge0resplit  39299  sge0iunmptlemre  39308  sge0isummpt2  39325  hoicvr  39438  hoidmvlelem2  39486  refdivmptf  42134  refdivmptfv  42138  amgmlemALT  42358
  Copyright terms: Public domain W3C validator