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

Detailed syntax breakdown of Axiom ax-resscn
StepHypRef Expression
1 cr 9895 . 2 class
2 cc 9894 . 2 class
31, 2wss 3560 1 wff ℝ ⊆ ℂ
Colors of variables: wff setvar class
This axiom is referenced by:  recn  9986  reex  9987  recni  10012  nnsscn  10985  nn0sscn  11257  qsscn  11759  reexpcl  12833  rpexpcl  12835  reexpclz  12836  expge0  12852  expge1  12853  rlimrecl  14261  abscn2  14279  recn2  14281  imcn2  14282  climabs  14284  climre  14286  climim  14287  rlimabs  14289  rlimre  14291  rlimim  14292  caurcvgr  14354  caucvgrlem2  14355  caurcvg  14357  fsumrecl  14414  fsumrpcl  14417  fsumge0  14473  fsumre  14486  fsumim  14487  fprodrecl  14627  fprodrpcl  14630  fprodreclf  14633  fprodge0  14668  fprodge1  14670  rerisefaccl  14692  refallfaccl  14693  rprisefaccl  14698  reeff1  14794  nthruc  14924  regsumfsum  19754  rge0srg  19757  rebase  19892  re0g  19898  regsumsupp  19908  remet  22533  tgioo2  22546  xrsdsre  22553  recld2  22557  reperf  22562  iitopon  22622  dfii3  22626  abscncf  22644  recncf  22645  imcncf  22646  abscncfALT  22663  cnmptre  22666  iimulcn  22677  icchmeo  22680  cnrehmeo  22692  evth  22698  evth2  22699  lebnumlem2  22701  lebnumii  22705  reparphti  22737  cphsqrtcl  22924  resscdrg  23094  ishl2  23106  recms  23108  reust  23109  evthicc  23168  evthicc2  23169  ovolfsf  23180  volcn  23314  volivth  23315  ismbf  23337  cncombf  23365  cnmbf  23366  0plef  23379  itg1ge0  23393  i1faddlem  23400  i1fmul  23403  itg1addlem4  23406  i1fsub  23415  itg1sub  23416  mbfi1fseqlem5  23426  xrge0f  23438  itg20  23444  itg2const  23447  itg2mulc  23454  itg2addlem  23465  i1fibl  23514  itgitg1  23515  iblabslem  23534  iblabs  23535  bddmulibl  23545  recnprss  23608  dvcjbr  23652  dvfre  23654  dvnfre  23655  dvferm1  23686  dvferm2  23688  rolle  23691  cmvth  23692  mvth  23693  dvlip  23694  dvlipcn  23695  dvlip2  23696  c1liplem1  23697  c1lip2  23699  dvgt0lem1  23703  dvle  23708  dvivthlem1  23709  dvivth  23711  dvne0  23712  lhop1lem  23714  lhop1  23715  lhop2  23716  lhop  23717  dvcnvrelem1  23718  dvcnvrelem2  23719  dvcnvre  23720  dvcvx  23721  dvfsumle  23722  dvfsumge  23723  dvfsumabs  23724  dvfsumlem2  23728  dvfsumrlim  23732  ftc1a  23738  ftc1lem3  23739  ftc1lem6  23742  ftc1  23743  ftc1cn  23744  ftc2  23745  ftc2ditglem  23746  itgparts  23748  itgsubstlem  23749  itgsubst  23750  aacjcl  24020  aalioulem3  24027  taylthlem2  24066  taylth  24067  abelth2  24134  reeff1olem  24138  efcvx  24141  pilem3  24145  pige3  24207  recosf1o  24219  resinf1o  24220  dvrelog  24317  relogcn  24318  logcnlem5  24326  logcn  24327  dvloglem  24328  dvlog2lem  24332  logccv  24343  dvcxp1  24415  cxpcn3  24423  resqrtcn  24424  loglesqrt  24433  ssscongptld  24486  ressatans  24595  rlimcnp  24626  efrlim  24630  jensenlem1  24647  jensenlem2  24648  jensen  24649  amgm  24651  lgamgulmlem2  24690  ftalem3  24735  basellem9  24749  efnnfsumcl  24763  efchtdvds  24819  lgsdchr  25014  dchrvmasumlem1  25118  dchrisum0lem3  25142  pntlem3  25232  cchhllem  25701  ipasslem7  27579  rexdiv  29461  fsumrp0cl  29522  xrge0slmod  29671  unitsscn  29766  rmulccn  29798  raddcn  29799  xrge0iifhom  29807  lmlimxrge0  29818  rezh  29839  esumpfinvallem  29959  esumpfinval  29960  esumpfinvalf  29961  esumcvg  29971  plymulx0  30446  plymulx  30447  signsplypnf  30449  signsply0  30450  ftc2re  30492  itgexpif  30493  cvxpconn  30985  cvxsconn  30986  resconn  30989  ivthALT  32025  dnicn  32177  knoppcnlem10  32187  knoppcnlem11  32188  unbdqndv2  32197  knoppndv  32220  knoppcn2  32222  broucube  33114  mblfinlem2  33118  mbfresfi  33127  ftc1cnnclem  33154  ftc1cnnc  33155  ftc1anclem3  33158  ftc1anclem5  33160  ftc1anclem7  33162  ftc1anclem8  33163  ftc1anc  33164  ftc2nc  33165  asindmre  33166  dvreasin  33169  dvreacos  33170  areacirclem1  33171  areacirclem2  33172  areacirclem3  33173  areacirclem4  33174  areacirc  33176  repwsmet  33304  rrnequiv  33305  rrntotbnd  33306  reheibor  33309  iccbnd  33310  itgpowd  37320  arearect  37321  areaquad  37322  k0004val0  37973  extoimad  37985  imo72b2lem0  37986  imo72b2lem2  37988  imo72b2lem1  37992  imo72b2  37996  ssrecnpr  38028  sblpnf  38030  radcnvrat  38034  lhe4.4ex1a  38049  refsumcn  38711  rr2sscn2  39081  ioosscn  39162  evthiccabs  39164  climreeq  39281  limciccioolb  39289  limcrecl  39297  limcicciooub  39305  limcleqr  39312  lptioo2cn  39313  lptioo1cn  39314  limclner  39319  resincncf  39423  cncficcgt0  39436  cncfiooicclem1  39441  cncfiooiccre  39443  jumpncnp  39446  dvcosre  39461  dvmptconst  39465  dvmptidg  39467  fperdvper  39470  dvmptresicc  39471  dvresioo  39473  dvmulcncf  39477  dvdivcncf  39479  dvbdfbdioolem1  39480  ioodvbdlimc1lem1  39483  ioodvbdlimc1lem2  39484  ioodvbdlimc1  39485  ioodvbdlimc2lem  39486  ioodvbdlimc2  39487  itgsin0pilem1  39502  ibliccsinexp  39503  iblioosinexp  39505  itgsinexplem1  39506  itgsinexp  39507  itgcoscmulx  39522  itgsincmulx  39527  itgsubsticclem  39528  itgiccshift  39533  itgperiod  39534  itgsbtaddcnst  39535  dirkeritg  39656  dirkercncflem2  39658  dirkercncflem3  39659  dirkercncflem4  39660  dirkercncf  39661  fourierdlem16  39677  fourierdlem18  39679  fourierdlem21  39682  fourierdlem22  39683  fourierdlem39  39700  fourierdlem42  39703  fourierdlem48  39708  fourierdlem49  39709  fourierdlem53  39713  fourierdlem57  39717  fourierdlem58  39718  fourierdlem59  39719  fourierdlem60  39720  fourierdlem61  39721  fourierdlem62  39722  fourierdlem68  39728  fourierdlem70  39730  fourierdlem72  39732  fourierdlem73  39733  fourierdlem74  39734  fourierdlem75  39735  fourierdlem76  39736  fourierdlem78  39738  fourierdlem80  39740  fourierdlem83  39743  fourierdlem84  39744  fourierdlem85  39745  fourierdlem88  39748  fourierdlem89  39749  fourierdlem90  39750  fourierdlem91  39751  fourierdlem93  39753  fourierdlem94  39754  fourierdlem95  39755  fourierdlem96  39756  fourierdlem97  39757  fourierdlem98  39758  fourierdlem99  39759  fourierdlem101  39761  fourierdlem103  39763  fourierdlem104  39764  fourierdlem111  39771  fourierdlem112  39772  fourierdlem113  39773  fouriercnp  39780  sqwvfoura  39782  sqwvfourb  39783  fouriersw  39785  fouriercn  39786  etransclem2  39790  etransclem18  39806  etransclem23  39811  etransclem46  39834  rrxtopnfi  39843  rrndistlt  39847  sge0sn  39933  sge0tsms  39934  sge0f1o  39936  sge0pr  39948  sge0resplit  39960  sge0iunmptlemre  39969  sge0isummpt2  39986  hoicvr  40099  hoidmvlelem2  40147  refdivmptf  41658  refdivmptfv  41662  amgmlemALT  41882
  Copyright terms: Public domain W3C validator