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

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

Detailed syntax breakdown of Axiom ax-resscn
StepHypRef Expression
1 cr 9512 . 2
2 cc 9511 . 2
31, 2wss 3475 1
Colors of variables: wff setvar class
This axiom is referenced by:  recn  9603  reex  9604  recni  9629  nnsscn  10566  nn0sscn  10825  qsscn  11222  reexpcl  12183  rpexpcl  12185  reexpclz  12186  expge0  12202  expge1  12203  rlimrecl  13403  abscn2  13421  recn2  13423  imcn2  13424  climabs  13426  climre  13428  climim  13429  rlimabs  13431  rlimre  13433  rlimim  13434  caurcvgr  13496  caucvgrlem2  13497  caurcvg  13499  fsumrecl  13556  fsumrpcl  13559  fsumge0  13609  fsumre  13622  fsumim  13623  fprodrecl  13760  fprodrpcl  13763  reeff1  13855  nthruc  13984  rge0srg  18487  rebase  18642  re0g  18648  regsumsupp  18658  remet  21295  tgioo2  21308  xrsdsre  21315  recld2  21319  reperf  21324  iitopon  21383  dfii3  21387  abscncf  21405  recncf  21406  imcncf  21407  abscncfALT  21424  cnmptre  21427  iimulcn  21438  icchmeo  21441  cnrehmeo  21453  evth  21459  evth2  21460  lebnumlem2  21462  lebnumii  21466  reparphti  21497  cphsqrtcl  21631  resscdrg  21798  ishl2  21810  recms  21812  reust  21813  evthicc  21871  evthicc2  21872  ovolfsf  21883  volcn  22015  volivth  22016  ismbf  22037  cncombf  22065  cnmbf  22066  0plef  22079  itg1ge0  22093  i1faddlem  22100  i1fmul  22103  itg1addlem4  22106  i1fsub  22115  itg1sub  22116  mbfi1fseqlem5  22126  xrge0f  22138  itg20  22144  itg2const  22147  itg2mulc  22154  itg2addlem  22165  i1fibl  22214  itgitg1  22215  iblabslem  22234  iblabs  22235  bddmulibl  22245  recnprss  22308  dvcjbr  22352  dvfre  22354  dvnfre  22355  dvferm1  22386  dvferm2  22388  rolle  22391  cmvth  22392  mvth  22393  dvlip  22394  dvlipcn  22395  dvlip2  22396  c1liplem1  22397  c1lip2  22399  dvgt0lem1  22403  dvle  22408  dvivthlem1  22409  dvivth  22411  dvne0  22412  lhop1lem  22414  lhop1  22415  lhop2  22416  lhop  22417  dvcnvrelem1  22418  dvcnvrelem2  22419  dvcnvre  22420  dvcvx  22421  dvfsumle  22422  dvfsumge  22423  dvfsumabs  22424  dvfsumlem2  22428  dvfsumrlim  22432  ftc1a  22438  ftc1lem3  22439  ftc1lem6  22442  ftc1  22443  ftc1cn  22444  ftc2  22445  ftc2ditglem  22446  itgparts  22448  itgsubstlem  22449  itgsubst  22450  aacjcl  22723  aalioulem3  22730  taylthlem2  22769  taylth  22770  abelth2  22837  reeff1olem  22841  efcvx  22844  pilem3  22848  pige3  22910  recosf1o  22922  resinf1o  22923  dvrelog  23018  relogcn  23019  logcnlem5  23027  logcn  23028  dvloglem  23029  dvlog2lem  23033  logccv  23044  dvcxp1  23116  cxpcn3  23122  resqrtcn  23123  loglesqrt  23132  ssscongptld  23156  ressatans  23265  rlimcnp  23295  efrlim  23299  jensenlem1  23316  jensenlem2  23317  jensen  23318  amgm  23320  ftalem3  23348  basellem9  23362  efnnfsumcl  23376  efchtdvds  23433  lgsdchr  23623  dchrvmasumlem1  23680  dchrisum0lem3  23704  pntlem3  23794  cchhllem  24190  readdsubgo  25355  circgrpOLD  25376  ipasslem7  25751  rexdiv  27622  fsumrp0cl  27685  regsumfsum  27772  xrge0slmod  27834  unitsscn  27878  rmulccn  27910  raddcn  27911  xrge0iifhom  27919  lmlimxrge0  27930  rezh  27952  esumpfinvallem  28080  esumpfinval  28081  esumpfinvalf  28082  esumcvg  28092  plymulx0  28504  plymulx  28505  signsplypnf  28507  signsply0  28508  lgamgulmlem2  28572  cvxpcon  28687  cvxscon  28688  rescon  28691  rerisefaccl  29139  refallfaccl  29140  rprisefaccl  29145  mblfinlem2  30052  mbfresfi  30061  ftc1cnnclem  30088  ftc1cnnc  30089  ftc1anclem3  30092  ftc1anclem5  30094  ftc1anclem7  30096  ftc1anclem8  30097  ftc1anc  30098  ftc2nc  30099  asindmre  30102  dvreasin  30105  dvreacos  30106  areacirclem1  30107  areacirclem2  30108  areacirclem3  30109  areacirclem4  30110  areacirc  30112  ivthALT  30153  repwsmet  30330  rrnequiv  30331  rrntotbnd  30332  reheibor  30335  iccbnd  30336  itgpowd  31182  arearect  31183  areaquad  31184  ssrecnpr  31188  sblpnf  31190  radcnvrat  31195  lhe4.4ex1a  31234  refsumcn  31405  ioosscn  31527  evthiccabs  31529  fprodreclf  31596  fprodge0  31597  fprodge1  31598  climreeq  31619  limciccioolb  31627  limcrecl  31635  limcicciooub  31643  limcleqr  31650  lptioo2cn  31651  lptioo1cn  31652  limclner  31657  resincncf  31677  cncficcgt0  31691  cncfiooicclem1  31696  cncfiooiccre  31698  jumpncnp  31701  dvcosre  31706  dvmptconst  31710  dvmptidg  31712  fperdvper  31715  dvmptresicc  31716  dvresioo  31718  dvmulcncf  31722  dvdivcncf  31724  dvbdfbdioolem1  31725  ioodvbdlimc1lem1  31728  ioodvbdlimc1lem2  31729  ioodvbdlimc1  31730  ioodvbdlimc2lem  31731  ioodvbdlimc2  31732  itgsin0pilem1  31748  ibliccsinexp  31749  iblioosinexp  31751  itgsinexplem1  31752  itgsinexp  31753  itgcoscmulx  31768  itgsincmulx  31773  itgsubsticclem  31774  itgiccshift  31779  itgperiod  31780  itgsbtaddcnst  31781  dirkeritg  31884  dirkercncflem2  31886  dirkercncflem3  31887  dirkercncflem4  31888  dirkercncf  31889  fourierdlem16  31905  fourierdlem18  31907  fourierdlem21  31910  fourierdlem22  31911  fourierdlem39  31928  fourierdlem42  31931  fourierdlem48  31937  fourierdlem49  31938  fourierdlem53  31942  fourierdlem57  31946  fourierdlem58  31947  fourierdlem59  31948  fourierdlem60  31949  fourierdlem61  31950  fourierdlem62  31951  fourierdlem68  31957  fourierdlem70  31959  fourierdlem72  31961  fourierdlem73  31962  fourierdlem74  31963  fourierdlem75  31964  fourierdlem76  31965  fourierdlem78  31967  fourierdlem80  31969  fourierdlem83  31972  fourierdlem84  31973  fourierdlem85  31974  fourierdlem88  31977  fourierdlem89  31978  fourierdlem90  31979  fourierdlem91  31980  fourierdlem93  31982  fourierdlem94  31983  fourierdlem95  31984  fourierdlem96  31985  fourierdlem97  31986  fourierdlem98  31987  fourierdlem99  31988  fourierdlem101  31990  fourierdlem103  31992  fourierdlem104  31993  fourierdlem111  32000  fourierdlem112  32001  fourierdlem113  32002  fouriercnp  32009  sqwvfoura  32011  sqwvfourb  32012  fouriersw  32014  fouriercn  32015  etransclem2  32019  etransclem18  32035  etransclem23  32040  etransclem46  32063  extoimad  37981  imo72b2lem0  37982  imo72b2lem2  37984  imo72b2lem1  37988  imo72b2  37993
  Copyright terms: Public domain W3C validator