MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax-resscn Unicode version

Axiom ax-resscn 9424
Description: The real numbers are a subset of the complex numbers. Axiom 1 of 22 for real and complex numbers, justified by theorem axresscn 9400. (Contributed by NM, 1-Mar-1995.)
Assertion
Ref Expression
ax-resscn

Detailed syntax breakdown of Axiom ax-resscn
StepHypRef Expression
1 cr 9366 . 2
2 cc 9365 . 2
31, 2wss 3410 1
Colors of variables: wff setvar class
This axiom is referenced by:  recn  9457  reex  9458  recni  9483  nnsscn  10412  nn0sscn  10669  qsscn  11049  reexpcl  11967  rpexpcl  11969  reexpclz  11970  expge0  11985  expge1  11986  rlimrecl  13144  abscn2  13162  recn2  13164  imcn2  13165  climabs  13167  climre  13169  climim  13170  rlimabs  13172  rlimre  13174  rlimim  13175  caurcvgr  13237  caucvgrlem2  13238  caurcvg  13240  fsumrecl  13297  fsumrpcl  13300  fsumge0  13344  fsumre  13357  fsumim  13358  reeff1  13490  nthruc  13619  rge0srg  17975  rebase  18129  re0g  18135  regsumsupp  18145  remet  20467  tgioo2  20480  xrsdsre  20487  recld2  20491  reperf  20496  iitopon  20555  dfii3  20559  abscncf  20577  recncf  20578  imcncf  20579  abscncfALT  20596  cnmptre  20599  iimulcn  20610  icchmeo  20613  cnrehmeo  20625  evth  20631  evth2  20632  lebnumlem2  20634  lebnumii  20638  reparphti  20669  cphsqrcl  20803  resscdrg  20970  ishl2  20982  recms  20984  reust  20985  evthicc  21043  evthicc2  21044  ovolfsf  21055  volcn  21186  volivth  21187  ismbf  21208  cncombf  21236  cnmbf  21237  0plef  21250  itg1ge0  21264  i1faddlem  21271  i1fmul  21274  itg1addlem4  21277  i1fsub  21286  itg1sub  21287  mbfi1fseqlem5  21297  xrge0f  21309  itg20  21315  itg2const  21318  itg2mulc  21325  itg2addlem  21336  i1fibl  21385  itgitg1  21386  iblabslem  21405  iblabs  21406  bddmulibl  21416  recnprss  21479  dvcjbr  21523  dvfre  21525  dvnfre  21526  dvferm1  21557  dvferm2  21559  rolle  21562  cmvth  21563  mvth  21564  dvlip  21565  dvlipcn  21566  dvlip2  21567  c1liplem1  21568  c1lip2  21570  dvgt0lem1  21574  dvle  21579  dvivthlem1  21580  dvivth  21582  dvne0  21583  lhop1lem  21585  lhop1  21586  lhop2  21587  lhop  21588  dvcnvrelem1  21589  dvcnvrelem2  21590  dvcnvre  21591  dvcvx  21592  dvfsumle  21593  dvfsumge  21594  dvfsumabs  21595  dvfsumlem2  21599  dvfsumrlim  21603  ftc1a  21609  ftc1lem3  21610  ftc1lem6  21613  ftc1  21614  ftc1cn  21615  ftc2  21616  ftc2ditglem  21617  itgparts  21619  itgsubstlem  21620  itgsubst  21621  aacjcl  21893  aalioulem3  21900  taylthlem2  21939  taylth  21940  abelth2  22007  reeff1olem  22011  efcvx  22014  pilem3  22018  pige3  22079  recosf1o  22091  resinf1o  22092  dvrelog  22182  relogcn  22183  logcnlem5  22191  logcn  22192  dvloglem  22193  dvlog2lem  22197  logccv  22208  dvcxp1  22280  cxpcn3  22286  resqrcn  22287  loglesqr  22296  ssscongptld  22320  ressatans  22429  rlimcnp  22459  efrlim  22463  jensenlem1  22480  jensenlem2  22481  jensen  22482  amgm  22484  ftalem3  22512  basellem9  22526  efnnfsumcl  22540  efchtdvds  22597  lgsdchr  22787  dchrvmasumlem1  22844  dchrisum0lem3  22868  pntlem3  22958  cchhllem  23252  readdsubgo  23959  circgrp  23980  ipasslem7  24355  rexdiv  26219  fsumrp0cl  26276  regsumfsum  26368  xrge0slmod  26430  unitsscn  26444  rmulccn  26476  raddcn  26477  xrge0iifhom  26485  lmlimxrge0  26496  rezh  26518  esumpfinvallem  26641  esumpfinval  26642  esumpfinvalf  26643  esumcvg  26653  plymulx0  27066  plymulx  27067  signsplypnf  27069  signsply0  27070  lgamgulmlem2  27134  cvxpcon  27249  cvxscon  27250  rescon  27253  fprodrecl  27584  fprodrpcl  27587  rerisefaccl  27638  refallfaccl  27639  rprisefaccl  27644  mblfinlem2  28551  mbfresfi  28560  ftc1cnnclem  28587  ftc1cnnc  28588  ftc1anclem3  28591  ftc1anclem5  28593  ftc1anclem7  28595  ftc1anclem8  28596  ftc1anc  28597  ftc2nc  28598  asindmre  28601  dvreasin  28604  dvreacos  28605  areacirclem1  28606  areacirclem2  28607  areacirclem3  28608  areacirclem4  28609  areacirc  28611  ivthALT  28652  repwsmet  28855  rrnequiv  28856  rrntotbnd  28857  reheibor  28860  iccbnd  28861  itgpowd  29712  arearect  29713  areaquad  29714  ssrecnpr  29716  sblpnf  29718  lhe4.4ex1a  29725  refsumcn  29874  climreeq  29908  dvcosre  29910  itgsin0pilem1  29912  ibliccsinexp  29913  iblioosinexp  29915  itgsinexplem1  29916  itgsinexp  29917  wallispilem2  29983
  Copyright terms: Public domain W3C validator