MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nn0red Structured version   Visualization version   Unicode version

Theorem nn0red 10923
Description: A nonnegative integer is a real number. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
nn0red.1  |-  ( ph  ->  A  e.  NN0 )
Assertion
Ref Expression
nn0red  |-  ( ph  ->  A  e.  RR )

Proof of Theorem nn0red
StepHypRef Expression
1 nn0ssre 10870 . 2  |-  NN0  C_  RR
2 nn0red.1 . 2  |-  ( ph  ->  A  e.  NN0 )
31, 2sseldi 3429 1  |-  ( ph  ->  A  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1886   RRcr 9535   NN0cn0 10866
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-8 1888  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-sep 4524  ax-nul 4533  ax-pow 4580  ax-pr 4638  ax-un 6580  ax-1cn 9594  ax-icn 9595  ax-addcl 9596  ax-addrcl 9597  ax-mulcl 9598  ax-mulrcl 9599  ax-i2m1 9604  ax-1ne0 9605  ax-rnegex 9607  ax-rrecex 9608  ax-cnre 9609
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 985  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-ral 2741  df-rex 2742  df-reu 2743  df-rab 2745  df-v 3046  df-sbc 3267  df-csb 3363  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-pss 3419  df-nul 3731  df-if 3881  df-pw 3952  df-sn 3968  df-pr 3970  df-tp 3972  df-op 3974  df-uni 4198  df-iun 4279  df-br 4402  df-opab 4461  df-mpt 4462  df-tr 4497  df-eprel 4744  df-id 4748  df-po 4754  df-so 4755  df-fr 4792  df-we 4794  df-xp 4839  df-rel 4840  df-cnv 4841  df-co 4842  df-dm 4843  df-rn 4844  df-res 4845  df-ima 4846  df-pred 5379  df-ord 5425  df-on 5426  df-lim 5427  df-suc 5428  df-iota 5545  df-fun 5583  df-fn 5584  df-f 5585  df-f1 5586  df-fo 5587  df-f1o 5588  df-fv 5589  df-ov 6291  df-om 6690  df-wrecs 7025  df-recs 7087  df-rdg 7125  df-nn 10607  df-n0 10867
This theorem is referenced by:  nn0cnd  10924  nn0readdcl  10928  flmulnn0  12057  quoremz  12079  quoremnn0ALT  12081  modaddmodup  12150  modaddmodlo  12151  expneg  12277  expnbnd  12398  facdiv  12469  faclbnd6  12481  hashdom  12555  hashun2  12559  hashunx  12562  hashfun  12606  hashf1  12617  seqcoll2  12625  hashge2el2dif  12634  hashtpg  12638  wrdlenge2n0  12700  ccatsymb  12724  ccatrn  12730  ccat2s1fvw  12766  swrdnd  12783  swrdccat3blem  12846  cshwidxmod  12900  repswcshw  12906  swrds2  13013  modfsummods  13846  climcnds  13902  geomulcvg  13925  mertenslem1  13933  binomfallfaclem2  14086  binomrisefac  14088  fallfacval4  14089  efcllem  14125  eftlub  14156  ruclem10  14284  bitsfzolem  14400  bitsfzolemOLD  14401  bitsfzo  14402  bitsmod  14403  sadcaddlem  14424  sadaddlem  14433  sadasslem  14437  sadeq  14439  smuval2  14449  smupvallem  14450  smueqlem  14457  bezoutlem3OLD  14498  bezoutlem4OLD  14499  bezoutlem3  14501  bezoutlem4  14502  gcdeq  14513  dvdssqlem  14520  nn0seqcvgd  14522  eucalglt  14537  lcmneg  14561  mulgcddvds  14654  qredeu  14657  prmdiveq  14727  odzdvds  14733  odzdvdsOLD  14739  pythagtriplem3  14761  pythagtriplem6  14764  pythagtriplem7  14765  iserodd  14778  pclem  14781  pcpremul  14786  pcidlem  14814  pcgcd1  14819  pc2dvds  14821  pcz  14823  pcprmpw2  14824  fldivp1  14835  pcfaclem  14836  pcfac  14837  pcbc  14838  prmreclem2  14854  prmreclem3  14855  prmreclem4  14856  prmreclem5  14857  4sqlem11  14892  4sqlem12  14893  4sqlem14OLD  14895  4sqlem14  14901  vdwlem11  14934  vdwlem12  14935  ramlb  14970  0ram  14971  ram0  14973  ramub1lem2  14978  ramcl  14980  psgnunilem2  17129  odmodnn0  17182  mndodconglem  17183  mndodcong  17184  oddvds  17189  odhash3  17218  gexdvds  17228  sylow1lem1  17243  sylow1lem5  17247  pgpfi  17250  pgpssslw  17259  efgsfo  17382  efgredlemd  17387  efgredlem  17390  efgred  17391  lt6abl  17522  telgsums  17616  pgpfaclem2  17708  srgbinomlem3  17768  psrbaglesupp  18585  mplmonmul  18681  coe1tmmul2  18862  coe1tmmul2fv  18864  coe1pwmulfv  18866  gsummoncoe1  18891  zringlpirlem3OLD  19048  zringlpirlem3  19050  fvmptnn04if  19866  fvmptnn04ifc  19869  fvmptnn04ifd  19870  chfacfscmulgsum  19877  chfacfpmmulgsum  19881  lebnumii  21990  dyadmaxlem  22548  mbfi1fseqlem3  22668  mbfi1fseqlem4  22669  mbfi1fseqlem5  22670  mdegmullem  23020  coe1mul3  23041  coe1mul4  23042  deg1sublt  23052  deg1mul2  23056  deg1tmle  23059  deg1tm  23060  ply1divmo  23079  ply1divex  23080  deg1submon1p  23096  dvdsq1p  23104  fta1glem2  23110  fta1blem  23112  plyco0  23139  plyeq0lem  23157  plypf1  23159  plyaddlem1  23160  coeeulem  23171  dgrub  23181  dgrlb  23183  dgreq  23191  coeaddlem  23196  coemullem  23197  coemulhi  23201  dgrlt  23213  dgradd2  23215  dgrmul  23217  dgrcolem2  23221  dgrco  23222  plydivlem3  23241  plydivlem4  23242  plydivex  23243  plydiveu  23244  fta1lem  23253  quotcan  23255  vieta1lem2  23257  radcnvlem1  23361  dvradcnv  23369  leibpilem1  23859  leibpi  23861  log2tlbnd  23864  birthdaylem2  23871  birthdaylem3  23872  fsumharmonic  23930  dmlogdmgm  23942  basellem3  24002  basellem5  24004  issqf  24056  ppip1le  24081  ppiltx  24097  mumullem2  24100  sgmppw  24118  ppiub  24125  chtublem  24132  chpub  24141  dchrabs  24181  bcmono  24198  bcmax  24199  bcp1ctr  24200  bclbnd  24201  bposlem5  24209  lgseisenlem1  24270  2sqlem7  24291  2sqlem8  24293  chebbnd1lem1  24300  chtppilimlem1  24304  dchrisum0re  24344  mulogsumlem  24362  selberg2lem  24381  pntrlog2bndlem4  24411  pntlemr  24433  pntlemj  24434  pnt  24445  ostth2lem3  24466  spthispth  25296  wwlknred  25444  wwlkextproplem2  25463  vdgrfival  25618  nbhashuvtx1  25636  rusgranumwlks  25677  eupap1  25697  eupath2lem3  25700  frghash2spot  25784  usgreghash2spotv  25787  numclwwlk5  25833  numclwwlk6  25834  friendshipgt3  25842  nndiffz1  28359  2sqmod  28402  nexple  28824  oddpwdc  29180  eulerpartlems  29186  eulerpartlemgc  29188  eulerpartlemb  29194  coinfliplem  29304  eluzmn  29416  signsplypnf  29432  signslema  29444  signstfvc  29456  signstfveq0  29459  erdszelem8  29914  erdsze2lem2  29920  cvmliftlem7  30007  snmlff  30045  bcprod  30367  poimirlem3  31936  poimirlem4  31937  poimirlem6  31939  poimirlem7  31940  poimirlem10  31943  poimirlem11  31944  poimirlem12  31945  poimirlem13  31946  poimirlem15  31948  poimirlem16  31949  poimirlem17  31950  poimirlem19  31952  poimirlem20  31953  poimirlem21  31954  poimirlem22  31955  poimirlem23  31956  poimirlem24  31957  poimirlem25  31958  poimirlem26  31959  poimirlem29  31962  poimirlem30  31963  poimirlem31  31964  rrnequiv  32160  eldioph2lem1  35596  pell1qrge1  35710  rmxypos  35791  ltrmynn0  35792  ltrmxnn0  35793  lermxnn0  35794  jm2.24nn  35803  jm2.24  35807  jm2.19  35842  jm2.26lem3  35850  jm2.27c  35856  hbt  35983  dgraa0p  36009  binomcxplemnn0  36692  fsumnncl  37644  mccllem  37671  ioodvbdlimc1lem2  37798  ioodvbdlimc1lem2OLD  37800  ioodvbdlimc2lem  37802  ioodvbdlimc2lemOLD  37803  dvnxpaek  37811  dvnmul  37812  dvnprodlem2  37816  stoweidlem17  37871  stoweidlem24  37878  wallispilem5  37925  stirlinglem15  37944  fourierdlem48  38012  fourierdlem83  38047  fourierdlem103  38067  fourierdlem104  38068  sqwvfoura  38086  elaa2lem  38091  elaa2lemOLD  38092  etransclem10  38103  etransclem19  38112  etransclem20  38113  etransclem21  38114  etransclem22  38115  etransclem23  38116  etransclem24  38117  etransclem27  38120  etransclem32  38125  etransclem35  38128  etransclem44  38137  etransclem45  38138  etransclem46  38139  etransclem47  38140  etransclem48OLD  38141  etransclem48  38142  etransc  38143  rrndistlt  38153  gcdzeq  38787  pfxsuffeqwrdeq  38941  vtxdgfival  39513  vtxduhgrfiun  39522  ssnn0ssfz  40117  pgrple2abl  40137  nn0eo  40322  fllog2  40366  aacllem  40527
  Copyright terms: Public domain W3C validator