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

Theorem nn0red 10624
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 10570 . 2  |-  NN0  C_  RR
2 nn0red.1 . 2  |-  ( ph  ->  A  e.  NN0 )
31, 2sseldi 3342 1  |-  ( ph  ->  A  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1755   RRcr 9268   NN0cn0 10566
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519  ax-un 6361  ax-1cn 9327  ax-icn 9328  ax-addcl 9329  ax-addrcl 9330  ax-mulcl 9331  ax-mulrcl 9332  ax-i2m1 9337  ax-1ne0 9338  ax-rnegex 9340  ax-rrecex 9341  ax-cnre 9342
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 959  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-reu 2712  df-rab 2714  df-v 2964  df-sbc 3176  df-csb 3277  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-pss 3332  df-nul 3626  df-if 3780  df-pw 3850  df-sn 3866  df-pr 3868  df-tp 3870  df-op 3872  df-uni 4080  df-iun 4161  df-br 4281  df-opab 4339  df-mpt 4340  df-tr 4374  df-eprel 4619  df-id 4623  df-po 4628  df-so 4629  df-fr 4666  df-we 4668  df-ord 4709  df-on 4710  df-lim 4711  df-suc 4712  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-iota 5369  df-fun 5408  df-fn 5409  df-f 5410  df-f1 5411  df-fo 5412  df-f1o 5413  df-fv 5414  df-ov 6083  df-om 6466  df-recs 6818  df-rdg 6852  df-nn 10310  df-n0 10567
This theorem is referenced by:  nn0cnd  10625  nn0readdcl  10629  flmulnn0  11655  quoremz  11677  modaddmodup  11745  modaddmodlo  11746  expneg  11856  expnbnd  11976  facdiv  12046  faclbnd6  12058  facavg  12060  hashdom  12125  hashun2  12129  hashunx  12132  hashge2el2dif  12167  hashtpg  12169  hashfun  12182  hashf1  12193  seqcoll2  12200  wrdlenge2n0  12244  ccatval1  12259  ccatsymb  12264  cshwidxmod  12423  repswcshw  12429  swrds2  12528  climcnds  13296  geomulcvg  13318  mertenslem1  13326  efcllem  13345  eftlub  13375  ruclem10  13503  bitsfzolem  13612  bitsfzo  13613  bitsmod  13614  sadcaddlem  13635  sadaddlem  13644  sadasslem  13648  sadeq  13650  smuval2  13660  smupvallem  13661  smueqlem  13668  bezoutlem3  13706  bezoutlem4  13707  gcdeq  13718  dvdssqlem  13725  nn0seqcvgd  13727  eucalglt  13742  mulgcddvds  13772  qredeu  13775  prmdiveq  13843  odzdvds  13849  pythagtriplem3  13867  pythagtriplem6  13870  pythagtriplem7  13871  iserodd  13884  pclem  13887  pcpremul  13892  pcidlem  13920  pcgcd1  13925  pc2dvds  13927  pcz  13929  pcprmpw2  13930  fldivp1  13941  pcfaclem  13942  pcfac  13943  pcbc  13944  prmreclem2  13960  prmreclem3  13961  prmreclem4  13962  prmreclem5  13963  4sqlem11  13998  4sqlem12  13999  4sqlem14  14001  vdwlem11  14034  vdwlem12  14035  ramlb  14062  0ram  14063  ram0  14065  ramub1lem2  14070  ramcl  14072  psgnunilem2  15980  odmodnn0  16022  mndodconglem  16023  mndodcong  16024  oddvds  16029  odhash3  16054  gexdvds  16062  sylow1lem1  16076  sylow1lem5  16080  pgpfi  16083  pgpssslw  16092  efgsfo  16215  efgredlemd  16220  efgredlem  16223  efgred  16224  lt6abl  16350  pgpfaclem2  16556  psrbaglesupp  17368  psrbaglesuppOLD  17369  mplmonmul  17476  coe1tmmul2  17626  coe1tmmul2fv  17628  coe1pwmulfv  17630  zringlpirlem3  17746  zlpirlem3  17751  lebnumii  20379  dyadmaxlem  20918  mbfi1fseqlem3  21036  mbfi1fseqlem4  21037  mbfi1fseqlem5  21038  mdegmullem  21433  coe1mul3  21455  coe1mul4  21456  deg1sublt  21466  deg1mul2  21470  deg1tmle  21473  deg1tm  21474  ply1divmo  21491  ply1divex  21492  deg1submon1p  21508  dvdsq1p  21516  fta1glem2  21522  fta1blem  21524  plyco0  21544  plyeq0lem  21562  plypf1  21564  plyaddlem1  21565  coeeulem  21576  dgrub  21586  dgrlb  21588  dgreq  21596  coeaddlem  21600  coemullem  21601  coemulhi  21605  dgrlt  21617  dgradd2  21619  dgrmul  21621  dgrcolem2  21625  dgrco  21626  plydivlem3  21645  plydivlem4  21646  plydivex  21647  plydiveu  21648  fta1lem  21657  quotcan  21659  vieta1lem2  21661  radcnvlem1  21762  dvradcnv  21770  leibpilem1  22219  leibpi  22221  log2tlbnd  22224  birthdaylem2  22230  birthdaylem3  22231  fsumharmonic  22289  basellem3  22304  basellem5  22306  issqf  22358  ppip1le  22383  ppiltx  22399  mumullem2  22402  sgmppw  22420  ppiub  22427  chtublem  22434  chpub  22443  dchrabs  22483  bcmono  22500  bcmax  22501  bcp1ctr  22502  bclbnd  22503  bposlem5  22511  lgseisenlem1  22572  2sqlem7  22593  2sqlem8  22595  chebbnd1lem1  22602  chtppilimlem1  22606  dchrisum0re  22646  mulogsumlem  22664  selberg2lem  22683  pntrlog2bndlem4  22713  pntlemr  22735  pntlemj  22736  pnt  22747  ostth2lem3  22768  spthispth  23294  vdgrfival  23389  eupap1  23419  eupath2lem3  23422  nndiffz1  25897  nexple  26301  oddpwdc  26584  eulerpartlems  26590  eulerpartlemgc  26592  eulerpartlemb  26598  coinfliplem  26708  eluzmn  26782  signsplypnf  26798  signslema  26810  signstfvc  26822  signstfveq0  26825  dmlogdmgm  26857  erdszelem8  26933  erdsze2lem2  26939  cvmliftlem7  27027  snmlff  27065  binomfallfaclem2  27389  binomrisefac  27391  fallfacval4  27392  faclim  27398  rrnequiv  28575  eldioph2lem1  28940  pell1qrge1  29053  rmxypos  29132  ltrmynn0  29133  ltrmxnn0  29134  lermxnn0  29135  jm2.24nn  29144  jm2.24  29148  jm2.19  29184  jm2.26lem3  29192  jm2.27c  29198  hbt  29328  dgraa0p  29348  stoweidlem17  29655  stoweidlem24  29662  wallispilem5  29707  stirlinglem15  29726  modfsummods  30087  wwlknred  30198  nbhashuvtx1  30376  rusgranumwlks  30417  frghash2spot  30499  usgreghash2spotv  30502  numclwwlk5  30548  numclwwlk6  30549  friendshipgt3  30557  pgrple2abel  30596
  Copyright terms: Public domain W3C validator