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

Detailed syntax breakdown of Axiom ax-resscn
StepHypRef Expression
1 cr 9973 . 2 class
2 cc 9972 . 2 class
31, 2wss 3607 1 wff ℝ ⊆ ℂ
Colors of variables: wff setvar class
This axiom is referenced by:  recn  10064  reex  10065  recni  10090  nnsscn  11063  nn0sscn  11335  qsscn  11837  reexpcl  12917  rpexpcl  12919  reexpclz  12920  expge0  12936  expge1  12937  rlimrecl  14355  abscn2  14373  recn2  14375  imcn2  14376  climabs  14378  climre  14380  climim  14381  rlimabs  14383  rlimre  14385  rlimim  14386  caurcvgr  14448  caucvgrlem2  14449  caurcvg  14451  fsumrecl  14509  fsumrpcl  14512  fsumge0  14571  fsumre  14584  fsumim  14585  fprodrecl  14727  fprodrpcl  14730  fprodreclf  14733  fprodge0  14768  fprodge1  14770  rerisefaccl  14792  refallfaccl  14793  rprisefaccl  14798  reeff1  14894  nthruc  15025  regsumfsum  19862  rge0srg  19865  rebase  20000  re0g  20006  regsumsupp  20016  remet  22640  tgioo2  22653  xrsdsre  22660  recld2  22664  reperf  22669  iitopon  22729  dfii3  22733  abscncf  22751  recncf  22752  imcncf  22753  abscncfALT  22770  cnmptre  22773  iimulcn  22784  icchmeo  22787  cnrehmeo  22799  evth  22805  evth2  22806  lebnumlem2  22808  lebnumii  22812  reparphti  22843  cphsqrtcl  23030  resscdrg  23200  ishl2  23212  recms  23214  reust  23215  evthicc  23274  evthicc2  23275  ovolfsf  23286  volcn  23420  volivth  23421  ismbf  23442  cncombf  23470  cnmbf  23471  0plef  23484  itg1ge0  23498  i1faddlem  23505  i1fmul  23508  itg1addlem4  23511  i1fsub  23520  itg1sub  23521  mbfi1fseqlem5  23531  xrge0f  23543  itg20  23549  itg2const  23552  itg2mulc  23559  itg2addlem  23570  i1fibl  23619  itgitg1  23620  iblabslem  23639  iblabs  23640  bddmulibl  23650  recnprss  23713  dvcjbr  23757  dvfre  23759  dvnfre  23760  dvferm1  23793  dvferm2  23795  rolle  23798  cmvth  23799  mvth  23800  dvlip  23801  dvlipcn  23802  dvlip2  23803  c1liplem1  23804  c1lip2  23806  dvgt0lem1  23810  dvle  23815  dvivthlem1  23816  dvivth  23818  dvne0  23819  lhop1lem  23821  lhop1  23822  lhop2  23823  lhop  23824  dvcnvrelem1  23825  dvcnvrelem2  23826  dvcnvre  23827  dvcvx  23828  dvfsumle  23829  dvfsumge  23830  dvfsumabs  23831  dvfsumlem2  23835  dvfsumrlim  23839  ftc1a  23845  ftc1lem3  23846  ftc1lem6  23849  ftc1  23850  ftc1cn  23851  ftc2  23852  ftc2ditglem  23853  itgparts  23855  itgsubstlem  23856  itgsubst  23857  aacjcl  24127  aalioulem3  24134  taylthlem2  24173  taylth  24174  abelth2  24241  reeff1olem  24245  efcvx  24248  pilem3  24252  pige3  24314  recosf1o  24326  resinf1o  24327  dvrelog  24428  relogcn  24429  logcnlem5  24437  logcn  24438  dvloglem  24439  dvlog2lem  24443  logccv  24454  dvcxp1  24526  cxpcn3  24534  resqrtcn  24535  loglesqrt  24544  ssscongptld  24597  ressatans  24706  rlimcnp  24737  efrlim  24741  jensenlem1  24758  jensenlem2  24759  jensen  24760  amgm  24762  lgamgulmlem2  24801  ftalem3  24846  basellem9  24860  efnnfsumcl  24874  efchtdvds  24930  lgsdchr  25125  dchrvmasumlem1  25229  dchrisum0lem3  25253  pntlem3  25343  cchhllem  25812  ipasslem7  27819  fprodex01  29699  rexdiv  29762  fsumrp0cl  29823  xrge0slmod  29972  unitsscn  30070  rmulccn  30102  raddcn  30103  xrge0iifhom  30111  lmlimxrge0  30122  rezh  30143  indsumin  30212  esumpfinvallem  30264  esumpfinval  30265  esumpfinvalf  30266  esumcvg  30276  plymulx0  30752  plymulx  30753  signsplypnf  30755  signsply0  30756  iblidicc  30798  rpsqrtcn  30799  ftc2re  30804  fdvposlt  30805  fdvneggt  30806  fdvposle  30807  fdvnegge  30808  itgexpif  30812  circlemeth  30846  circlemethnat  30847  circlevma  30848  circlemethhgt  30849  logdivsqrle  30856  cvxpconn  31350  cvxsconn  31351  resconn  31354  ivthALT  32455  dnicn  32607  knoppcnlem10  32617  knoppcnlem11  32618  unbdqndv2  32627  knoppndv  32650  knoppcn2  32652  broucube  33573  mblfinlem2  33577  mbfresfi  33586  ftc1cnnclem  33613  ftc1cnnc  33614  ftc1anclem3  33617  ftc1anclem5  33619  ftc1anclem7  33621  ftc1anclem8  33622  ftc1anc  33623  ftc2nc  33624  asindmre  33625  dvreasin  33628  dvreacos  33629  areacirclem1  33630  areacirclem2  33631  areacirclem3  33632  areacirclem4  33633  areacirc  33635  repwsmet  33763  rrnequiv  33764  rrntotbnd  33765  reheibor  33768  iccbnd  33769  itgpowd  38117  arearect  38118  areaquad  38119  k0004val0  38769  extoimad  38781  imo72b2lem0  38782  imo72b2lem2  38784  imo72b2lem1  38788  imo72b2  38792  ssrecnpr  38824  sblpnf  38826  radcnvrat  38830  lhe4.4ex1a  38845  refsumcn  39503  rr2sscn2  39895  uzsscn  40019  ioosscn  40034  evthiccabs  40036  climreeq  40163  limciccioolb  40171  limcrecl  40179  limcicciooub  40187  limcleqr  40194  lptioo2cn  40195  lptioo1cn  40196  limclner  40201  liminflimsupclim  40357  resincncf  40406  cncficcgt0  40419  cncfiooicclem1  40424  cncfiooiccre  40426  jumpncnp  40429  dvcosre  40444  dvmptconst  40447  dvmptidg  40449  fperdvper  40451  dvmptresicc  40452  dvresioo  40454  dvmulcncf  40458  dvdivcncf  40460  dvbdfbdioolem1  40461  ioodvbdlimc1lem1  40464  ioodvbdlimc1lem2  40465  ioodvbdlimc1  40466  ioodvbdlimc2lem  40467  ioodvbdlimc2  40468  itgsin0pilem1  40483  ibliccsinexp  40484  iblioosinexp  40486  itgsinexplem1  40487  itgsinexp  40488  itgcoscmulx  40503  itgsincmulx  40508  itgsubsticclem  40509  itgiccshift  40514  itgperiod  40515  itgsbtaddcnst  40516  dirkeritg  40637  dirkercncflem2  40639  dirkercncflem3  40640  dirkercncflem4  40641  dirkercncf  40642  fourierdlem16  40658  fourierdlem18  40660  fourierdlem21  40663  fourierdlem22  40664  fourierdlem39  40681  fourierdlem42  40684  fourierdlem48  40689  fourierdlem49  40690  fourierdlem53  40694  fourierdlem57  40698  fourierdlem58  40699  fourierdlem59  40700  fourierdlem60  40701  fourierdlem61  40702  fourierdlem62  40703  fourierdlem68  40709  fourierdlem70  40711  fourierdlem72  40713  fourierdlem73  40714  fourierdlem74  40715  fourierdlem75  40716  fourierdlem76  40717  fourierdlem78  40719  fourierdlem80  40721  fourierdlem83  40724  fourierdlem84  40725  fourierdlem85  40726  fourierdlem88  40729  fourierdlem89  40730  fourierdlem90  40731  fourierdlem91  40732  fourierdlem93  40734  fourierdlem94  40735  fourierdlem95  40736  fourierdlem96  40737  fourierdlem97  40738  fourierdlem98  40739  fourierdlem99  40740  fourierdlem101  40742  fourierdlem103  40744  fourierdlem104  40745  fourierdlem111  40752  fourierdlem112  40753  fourierdlem113  40754  fouriercnp  40761  sqwvfoura  40763  sqwvfourb  40764  fouriersw  40766  fouriercn  40767  etransclem2  40771  etransclem18  40787  etransclem23  40792  etransclem46  40815  rrxtopnfi  40824  rrndistlt  40828  sge0sn  40914  sge0tsms  40915  sge0f1o  40917  sge0pr  40929  sge0resplit  40941  sge0iunmptlemre  40950  sge0isummpt2  40967  hoicvr  41083  hoidmvlelem2  41131  refdivmptf  42661  refdivmptfv  42665  amgmlemALT  42877
  Copyright terms: Public domain W3C validator