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

Detailed syntax breakdown of Axiom ax-resscn
StepHypRef Expression
1 cr 10534 . 2 class
2 cc 10533 . 2 class
31, 2wss 3919 1 wff ℝ ⊆ ℂ
Colors of variables: wff setvar class
This axiom is referenced by:  recn  10625  reex  10626  recni  10653  qsscn  12356  ioosscn  12796  unitsscn  12887  reexpcl  13451  rpexpcl  13453  reexpclz  13454  expge0  13470  expge1  13471  rlimrecl  14937  abscn2  14955  recn2  14957  imcn2  14958  climabs  14960  climre  14962  climim  14963  rlimabs  14965  rlimre  14967  rlimim  14968  caurcvgr  15030  caucvgrlem2  15031  caurcvg  15033  fsumrecl  15091  fsumrpcl  15094  fsumge0  15150  fsumre  15163  fsumim  15164  fprodrecl  15307  fprodrpcl  15310  fprodreclf  15313  fprodge0  15347  fprodge1  15349  rerisefaccl  15371  refallfaccl  15372  rprisefaccl  15377  reeff1  15473  nthruc  15605  regsumfsum  20166  rge0srg  20169  rebase  20302  re0g  20308  regsumsupp  20318  remet  23401  tgioo2  23414  xrsdsre  23421  recld2  23425  reperf  23430  iitopon  23490  dfii3  23494  abscncf  23512  recncf  23513  imcncf  23514  abscncfALT  23535  cnmptre  23538  iimulcn  23549  icchmeo  23552  cnrehmeo  23564  evth  23570  evth2  23571  lebnumlem2  23573  lebnumii  23577  reparphti  23608  cphsqrtcl  23795  resscdrg  23968  ishl2  23980  recms  23990  reust  23991  evthicc  24069  evthicc2  24070  ovolfsf  24081  volcn  24216  volivth  24217  ismbf  24238  cncombf  24268  cnmbf  24269  0plef  24282  itg1ge0  24296  i1faddlem  24303  i1fmul  24306  itg1addlem4  24309  i1fsub  24318  itg1sub  24319  mbfi1fseqlem5  24329  xrge0f  24341  itg20  24347  itg2const  24350  itg2mulc  24357  itg2addlem  24368  i1fibl  24417  itgitg1  24418  iblabslem  24437  iblabs  24438  bddmulibl  24448  recnprss  24513  dvmptresicc  24525  dvcjbr  24558  dvfre  24560  dvnfre  24561  dvferm1  24594  dvferm2  24596  rolle  24599  cmvth  24600  mvth  24601  dvlip  24602  dvlipcn  24603  dvlip2  24604  c1liplem1  24605  c1lip2  24607  dvgt0lem1  24611  dvle  24616  dvivthlem1  24617  dvivth  24619  dvne0  24620  lhop1lem  24622  lhop1  24623  lhop2  24624  lhop  24625  dvcnvrelem1  24626  dvcnvrelem2  24627  dvcnvre  24628  dvcvx  24629  dvfsumle  24630  dvfsumge  24631  dvfsumabs  24632  dvfsumlem2  24636  dvfsumrlim  24640  ftc1a  24646  ftc1lem3  24647  ftc1lem6  24650  ftc1  24651  ftc1cn  24652  ftc2  24653  ftc2ditglem  24654  itgparts  24656  itgsubstlem  24657  itgsubst  24658  itgpowd  24659  aacjcl  24929  aalioulem3  24936  taylthlem2  24975  taylth  24976  abelth2  25043  reeff1olem  25047  efcvx  25050  pilem3  25054  pige3ALT  25118  recosf1o  25133  resinf1o  25134  dvrelog  25234  relogcn  25235  logcnlem5  25243  logcn  25244  dvloglem  25245  dvlog2lem  25249  logccv  25260  dvcxp1  25335  cxpcn3  25343  resqrtcn  25344  loglesqrt  25353  ssscongptld  25414  ressatans  25526  rlimcnp  25557  efrlim  25561  jensenlem1  25578  jensenlem2  25579  jensen  25580  amgm  25582  lgamgulmlem2  25621  ftalem3  25666  basellem9  25680  efnnfsumcl  25694  efchtdvds  25750  lgsdchr  25945  dchrvmasumlem1  26085  dchrisum0lem3  26109  pntlem3  26199  cchhllem  26687  ex-fpar  28253  ipasslem7  28625  fprodex01  30555  rexdiv  30616  fsumrp0cl  30717  xrge0slmod  30953  ccfldsrarelvec  31119  ccfldextdgrr  31120  rmulccn  31231  raddcn  31232  xrge0iifhom  31240  lmlimxrge0  31251  rezh  31272  indsumin  31341  esumpfinvallem  31393  esumpfinval  31394  esumpfinvalf  31395  esumcvg  31405  plymulx0  31877  plymulx  31878  signsplypnf  31880  signsply0  31881  iblidicc  31923  rpsqrtcn  31924  ftc2re  31929  fdvposlt  31930  fdvneggt  31931  fdvposle  31932  fdvnegge  31933  itgexpif  31937  circlemeth  31971  circlemethnat  31972  circlevma  31973  circlemethhgt  31974  logdivsqrle  31981  cvxpconn  32549  cvxsconn  32550  resconn  32553  ivthALT  33743  dnicn  33891  knoppcnlem10  33901  knoppcnlem11  33902  unbdqndv2  33910  knoppndv  33933  knoppcn2  33935  broucube  35039  mblfinlem2  35043  mbfresfi  35051  ftc1cnnclem  35076  ftc1cnnc  35077  ftc1anclem3  35080  ftc1anclem5  35082  ftc1anclem7  35084  ftc1anclem8  35085  ftc1anc  35086  ftc2nc  35087  asindmre  35088  dvreasin  35091  dvreacos  35092  areacirclem1  35093  areacirclem2  35094  areacirclem3  35095  areacirclem4  35096  areacirc  35098  repwsmet  35220  rrnequiv  35221  rrntotbnd  35222  reheibor  35225  iccbnd  35226  resubeqsub  39499  subresre  39500  arearect  40085  areaquad  40086  k0004val0  40780  extoimad  40791  imo72b2lem0  40792  imo72b2lem2  40794  imo72b2lem1  40797  imo72b2  40801  ssrecnpr  40936  sblpnf  40938  radcnvrat  40942  lhe4.4ex1a  40957  refsumcn  41583  rr2sscn2  41928  uzsscn  42045  evthiccabs  42063  climreeq  42185  limciccioolb  42193  limcrecl  42201  limcicciooub  42209  limcleqr  42216  lptioo2cn  42217  lptioo1cn  42218  limclner  42223  liminflimsupclim  42379  resincncf  42447  cncficcgt0  42460  cncfiooicclem1  42465  cncfiooiccre  42467  jumpncnp  42470  dvcosre  42484  dvmptconst  42487  dvmptidg  42489  fperdvper  42491  dvresioo  42493  dvmulcncf  42497  dvdivcncf  42499  dvbdfbdioolem1  42500  ioodvbdlimc1lem1  42503  ioodvbdlimc1lem2  42504  ioodvbdlimc1  42505  ioodvbdlimc2lem  42506  ioodvbdlimc2  42507  itgsin0pilem1  42522  ibliccsinexp  42523  iblioosinexp  42525  itgsinexplem1  42526  itgsinexp  42527  itgcoscmulx  42541  itgsincmulx  42546  itgsubsticclem  42547  itgiccshift  42552  itgperiod  42553  itgsbtaddcnst  42554  dirkeritg  42674  dirkercncflem2  42676  dirkercncflem3  42677  dirkercncflem4  42678  dirkercncf  42679  fourierdlem16  42695  fourierdlem18  42697  fourierdlem21  42700  fourierdlem22  42701  fourierdlem39  42718  fourierdlem42  42721  fourierdlem48  42726  fourierdlem49  42727  fourierdlem53  42731  fourierdlem57  42735  fourierdlem58  42736  fourierdlem59  42737  fourierdlem60  42738  fourierdlem61  42739  fourierdlem62  42740  fourierdlem68  42746  fourierdlem70  42748  fourierdlem72  42750  fourierdlem73  42751  fourierdlem74  42752  fourierdlem75  42753  fourierdlem76  42754  fourierdlem78  42756  fourierdlem80  42758  fourierdlem83  42761  fourierdlem84  42762  fourierdlem85  42763  fourierdlem88  42766  fourierdlem89  42767  fourierdlem90  42768  fourierdlem91  42769  fourierdlem93  42771  fourierdlem94  42772  fourierdlem95  42773  fourierdlem96  42774  fourierdlem97  42775  fourierdlem98  42776  fourierdlem99  42777  fourierdlem101  42779  fourierdlem103  42781  fourierdlem104  42782  fourierdlem111  42789  fourierdlem112  42790  fourierdlem113  42791  fouriercnp  42798  sqwvfoura  42800  sqwvfourb  42801  fouriersw  42803  fouriercn  42804  etransclem2  42808  etransclem18  42824  etransclem23  42829  etransclem46  42852  rrxtopnfi  42859  rrndistlt  42862  sge0sn  42948  sge0tsms  42949  sge0f1o  42951  sge0pr  42963  sge0resplit  42975  sge0iunmptlemre  42984  sge0isummpt2  43001  hoicvr  43117  hoidmvlelem2  43165  refdivmptf  44886  refdivmptfv  44890  amgmlemALT  45261
  Copyright terms: Public domain W3C validator