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

Theorem nn0red 10280
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 10230 . 2  |-  NN0  C_  RR
2 nn0red.1 . 2  |-  ( ph  ->  A  e.  NN0 )
31, 2sseldi 3348 1  |-  ( ph  ->  A  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1726   RRcr 8994   NN0cn0 10226
This theorem is referenced by:  nn0cnd  10281  flmulnn0  11234  quoremz  11241  expneg  11394  expnbnd  11513  facdiv  11583  faclbnd6  11595  facavg  11597  hashdom  11658  hashun2  11662  hashunx  11665  hashtpg  11696  hashfun  11705  hashf1  11711  seqcoll2  11718  ccatval1  11750  swrds2  11885  climcnds  12636  geomulcvg  12658  mertenslem1  12666  efcllem  12685  eftlub  12715  ruclem10  12843  bitsfzolem  12951  bitsfzo  12952  bitsmod  12953  sadcaddlem  12974  sadaddlem  12983  sadasslem  12987  sadeq  12989  smuval2  12999  smupvallem  13000  smueqlem  13007  bezoutlem3  13045  bezoutlem4  13046  gcdeq  13057  dvdssqlem  13064  nn0seqcvgd  13066  eucalglt  13081  mulgcddvds  13109  qredeu  13112  prmdiveq  13180  odzdvds  13186  pythagtriplem3  13197  pythagtriplem6  13200  pythagtriplem7  13201  iserodd  13214  pclem  13217  pcpremul  13222  pcidlem  13250  pcgcd1  13255  pc2dvds  13257  pcz  13259  pcprmpw2  13260  fldivp1  13271  pcfaclem  13272  pcfac  13273  pcbc  13274  prmreclem2  13290  prmreclem3  13291  prmreclem4  13292  prmreclem5  13293  4sqlem11  13328  4sqlem12  13329  4sqlem14  13331  vdwlem11  13364  vdwlem12  13365  ramlb  13392  0ram  13393  ram0  13395  ramub1lem2  13400  ramcl  13402  odmodnn0  15183  mndodconglem  15184  mndodcong  15185  oddvds  15190  odhash3  15215  gexdvds  15223  sylow1lem1  15237  sylow1lem5  15241  pgpfi  15244  pgpssslw  15253  efgsfo  15376  efgredlemd  15381  efgredlem  15384  efgred  15385  lt6abl  15509  pgpfaclem2  15645  psrbaglesupp  16438  mplmonmul  16532  coe1tmmul2  16673  coe1tmmul2fv  16675  coe1pwmulfv  16677  zlpirlem3  16775  lebnumii  18996  dyadmaxlem  19494  mbfi1fseqlem3  19612  mbfi1fseqlem4  19613  mbfi1fseqlem5  19614  mdegmullem  20006  coe1mul3  20027  coe1mul4  20028  deg1sublt  20038  deg1mul2  20042  deg1tmle  20045  deg1tm  20046  ply1divmo  20063  ply1divex  20064  deg1submon1p  20080  dvdsq1p  20088  fta1glem2  20094  fta1blem  20096  plyco0  20116  plyeq0lem  20134  plypf1  20136  plyaddlem1  20137  coeeulem  20148  dgrub  20158  dgrlb  20160  dgreq  20168  coeaddlem  20172  coemullem  20173  coemulhi  20177  dgrlt  20189  dgradd2  20191  dgrmul  20193  dgrcolem2  20197  dgrco  20198  plydivlem3  20217  plydivlem4  20218  plydivex  20219  plydiveu  20220  fta1lem  20229  quotcan  20231  vieta1lem2  20233  radcnvlem1  20334  dvradcnv  20342  leibpilem1  20785  leibpi  20787  log2tlbnd  20790  birthdaylem2  20796  birthdaylem3  20797  fsumharmonic  20855  basellem3  20870  basellem5  20872  issqf  20924  ppip1le  20949  ppiltx  20965  mumullem2  20968  sgmppw  20986  ppiub  20993  chtublem  21000  chpub  21009  dchrabs  21049  bcmono  21066  bcmax  21067  bcp1ctr  21068  bclbnd  21069  bposlem5  21077  lgseisenlem1  21138  2sqlem7  21159  2sqlem8  21161  chebbnd1lem1  21168  chtppilimlem1  21172  dchrisum0re  21212  mulogsumlem  21230  selberg2lem  21249  pntrlog2bndlem4  21279  pntlemr  21301  pntlemj  21302  pnt  21313  ostth2lem3  21334  spthispth  21578  vdgrfival  21673  eupap1  21703  eupath2lem3  21706  coinfliplem  24741  dmlogdmgm  24813  erdszelem8  24889  erdsze2lem2  24895  cvmliftlem7  24983  snmlff  25021  binomfallfaclem2  25361  binomrisefac  25363  fallfacval4  25364  faclim  25370  rrnequiv  26558  eldioph2lem1  26832  pell1qrge1  26947  rmxypos  27026  ltrmynn0  27027  ltrmxnn0  27028  lermxnn0  27029  jm2.24nn  27038  jm2.24  27042  jm2.19  27078  jm2.26lem3  27086  jm2.27c  27092  hbt  27325  dgraa0p  27345  psgnunilem2  27409  stoweidlem17  27756  stoweidlem24  27763  wallispilem5  27808  stirlinglem15  27827  nn0readdcl  28121  wrdlenge2n0  28208  ccatsymb  28211  cshwoor  28271  2cshw  28290  lstccats1fst  28297  nbhashuvtx1  28431  frghash2spot  28526  usgreghash2spotv  28529
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4333  ax-nul 4341  ax-pow 4380  ax-pr 4406  ax-un 4704  ax-1cn 9053  ax-icn 9054  ax-addcl 9055  ax-addrcl 9056  ax-mulcl 9057  ax-mulrcl 9058  ax-i2m1 9063  ax-1ne0 9064  ax-rnegex 9066  ax-rrecex 9067  ax-cnre 9068
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-reu 2714  df-rab 2716  df-v 2960  df-sbc 3164  df-csb 3254  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-pss 3338  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-tp 3824  df-op 3825  df-uni 4018  df-iun 4097  df-br 4216  df-opab 4270  df-mpt 4271  df-tr 4306  df-eprel 4497  df-id 4501  df-po 4506  df-so 4507  df-fr 4544  df-we 4546  df-ord 4587  df-on 4588  df-lim 4589  df-suc 4590  df-om 4849  df-xp 4887  df-rel 4888  df-cnv 4889  df-co 4890  df-dm 4891  df-rn 4892  df-res 4893  df-ima 4894  df-iota 5421  df-fun 5459  df-fn 5460  df-f 5461  df-f1 5462  df-fo 5463  df-f1o 5464  df-fv 5465  df-ov 6087  df-recs 6636  df-rdg 6671  df-nn 10006  df-n0 10227
  Copyright terms: Public domain W3C validator