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

Theorem nn0red 10267
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 10217 . 2  |-  NN0  C_  RR
2 nn0red.1 . 2  |-  ( ph  ->  A  e.  NN0 )
31, 2sseldi 3338 1  |-  ( ph  ->  A  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1725   RRcr 8981   NN0cn0 10213
This theorem is referenced by:  nn0cnd  10268  flmulnn0  11221  quoremz  11228  expneg  11381  expnbnd  11500  facdiv  11570  faclbnd6  11582  facavg  11584  hashdom  11645  hashun2  11649  hashunx  11652  hashtpg  11683  hashfun  11692  hashf1  11698  seqcoll2  11705  ccatval1  11737  swrds2  11872  climcnds  12623  geomulcvg  12645  mertenslem1  12653  efcllem  12672  eftlub  12702  ruclem10  12830  bitsfzolem  12938  bitsfzo  12939  bitsmod  12940  sadcaddlem  12961  sadaddlem  12970  sadasslem  12974  sadeq  12976  smuval2  12986  smupvallem  12987  smueqlem  12994  bezoutlem3  13032  bezoutlem4  13033  gcdeq  13044  dvdssqlem  13051  nn0seqcvgd  13053  eucalglt  13068  mulgcddvds  13096  qredeu  13099  prmdiveq  13167  odzdvds  13173  pythagtriplem3  13184  pythagtriplem6  13187  pythagtriplem7  13188  iserodd  13201  pclem  13204  pcpremul  13209  pcidlem  13237  pcgcd1  13242  pc2dvds  13244  pcz  13246  pcprmpw2  13247  fldivp1  13258  pcfaclem  13259  pcfac  13260  pcbc  13261  prmreclem2  13277  prmreclem3  13278  prmreclem4  13279  prmreclem5  13280  4sqlem11  13315  4sqlem12  13316  4sqlem14  13318  vdwlem11  13351  vdwlem12  13352  ramlb  13379  0ram  13380  ram0  13382  ramub1lem2  13387  ramcl  13389  odmodnn0  15170  mndodconglem  15171  mndodcong  15172  oddvds  15177  odhash3  15202  gexdvds  15210  sylow1lem1  15224  sylow1lem5  15228  pgpfi  15231  pgpssslw  15240  efgsfo  15363  efgredlemd  15368  efgredlem  15371  efgred  15372  lt6abl  15496  pgpfaclem2  15632  psrbaglesupp  16425  mplmonmul  16519  coe1tmmul2  16660  coe1tmmul2fv  16662  coe1pwmulfv  16664  zlpirlem3  16762  lebnumii  18983  dyadmaxlem  19481  mbfi1fseqlem3  19601  mbfi1fseqlem4  19602  mbfi1fseqlem5  19603  mdegmullem  19993  coe1mul3  20014  coe1mul4  20015  deg1sublt  20025  deg1mul2  20029  deg1tmle  20032  deg1tm  20033  ply1divmo  20050  ply1divex  20051  deg1submon1p  20067  dvdsq1p  20075  fta1glem2  20081  fta1blem  20083  plyco0  20103  plyeq0lem  20121  plypf1  20123  plyaddlem1  20124  coeeulem  20135  dgrub  20145  dgrlb  20147  dgreq  20155  coeaddlem  20159  coemullem  20160  coemulhi  20164  dgrlt  20176  dgradd2  20178  dgrmul  20180  dgrcolem2  20184  dgrco  20185  plydivlem3  20204  plydivlem4  20205  plydivex  20206  plydiveu  20207  fta1lem  20216  quotcan  20218  vieta1lem2  20220  radcnvlem1  20321  dvradcnv  20329  leibpilem1  20772  leibpi  20774  log2tlbnd  20777  birthdaylem2  20783  birthdaylem3  20784  fsumharmonic  20842  basellem3  20857  basellem5  20859  issqf  20911  ppip1le  20936  ppiltx  20952  mumullem2  20955  sgmppw  20973  ppiub  20980  chtublem  20987  chpub  20996  dchrabs  21036  bcmono  21053  bcmax  21054  bcp1ctr  21055  bclbnd  21056  bposlem5  21064  lgseisenlem1  21125  2sqlem7  21146  2sqlem8  21148  chebbnd1lem1  21155  chtppilimlem1  21159  dchrisum0re  21199  mulogsumlem  21217  selberg2lem  21236  pntrlog2bndlem4  21266  pntlemr  21288  pntlemj  21289  pnt  21300  ostth2lem3  21321  spthispth  21565  vdgrfival  21660  eupap1  21690  eupath2lem3  21693  coinfliplem  24728  dmlogdmgm  24800  erdszelem8  24876  erdsze2lem2  24882  cvmliftlem7  24970  snmlff  25008  binomfallfaclem2  25348  binomrisefac  25350  fallfacval4  25351  faclim  25357  rrnequiv  26535  eldioph2lem1  26809  pell1qrge1  26924  rmxypos  27003  ltrmynn0  27004  ltrmxnn0  27005  lermxnn0  27006  jm2.24nn  27015  jm2.24  27019  jm2.19  27055  jm2.26lem3  27063  jm2.27c  27069  hbt  27302  dgraa0p  27322  psgnunilem2  27386  stoweidlem17  27733  stoweidlem24  27740  wallispilem5  27785  stirlinglem15  27804  nn0readdcl  28083  ccatsymb  28152  cshwoor  28203  2cshw  28222  frghash2spot  28389  usgreghash2spotv  28392
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395  ax-un 4693  ax-1cn 9040  ax-icn 9041  ax-addcl 9042  ax-addrcl 9043  ax-mulcl 9044  ax-mulrcl 9045  ax-i2m1 9050  ax-1ne0 9051  ax-rnegex 9053  ax-rrecex 9054  ax-cnre 9055
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-reu 2704  df-rab 2706  df-v 2950  df-sbc 3154  df-csb 3244  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-pss 3328  df-nul 3621  df-if 3732  df-pw 3793  df-sn 3812  df-pr 3813  df-tp 3814  df-op 3815  df-uni 4008  df-iun 4087  df-br 4205  df-opab 4259  df-mpt 4260  df-tr 4295  df-eprel 4486  df-id 4490  df-po 4495  df-so 4496  df-fr 4533  df-we 4535  df-ord 4576  df-on 4577  df-lim 4578  df-suc 4579  df-om 4838  df-xp 4876  df-rel 4877  df-cnv 4878  df-co 4879  df-dm 4880  df-rn 4881  df-res 4882  df-ima 4883  df-iota 5410  df-fun 5448  df-fn 5449  df-f 5450  df-f1 5451  df-fo 5452  df-f1o 5453  df-fv 5454  df-ov 6076  df-recs 6625  df-rdg 6660  df-nn 9993  df-n0 10214
  Copyright terms: Public domain W3C validator