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

Theorem nn0red 10629
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 10575 . 2  |-  NN0  C_  RR
2 nn0red.1 . 2  |-  ( ph  ->  A  e.  NN0 )
31, 2sseldi 3349 1  |-  ( ph  ->  A  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756   RRcr 9273   NN0cn0 10571
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pow 4465  ax-pr 4526  ax-un 6367  ax-1cn 9332  ax-icn 9333  ax-addcl 9334  ax-addrcl 9335  ax-mulcl 9336  ax-mulrcl 9337  ax-i2m1 9342  ax-1ne0 9343  ax-rnegex 9345  ax-rrecex 9346  ax-cnre 9347
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-reu 2717  df-rab 2719  df-v 2969  df-sbc 3182  df-csb 3284  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-pss 3339  df-nul 3633  df-if 3787  df-pw 3857  df-sn 3873  df-pr 3875  df-tp 3877  df-op 3879  df-uni 4087  df-iun 4168  df-br 4288  df-opab 4346  df-mpt 4347  df-tr 4381  df-eprel 4627  df-id 4631  df-po 4636  df-so 4637  df-fr 4674  df-we 4676  df-ord 4717  df-on 4718  df-lim 4719  df-suc 4720  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5376  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-ov 6089  df-om 6472  df-recs 6824  df-rdg 6858  df-nn 10315  df-n0 10572
This theorem is referenced by:  nn0cnd  10630  nn0readdcl  10634  flmulnn0  11664  quoremz  11686  quoremnn0ALT  11688  modaddmodup  11754  modaddmodlo  11755  expneg  11865  expnbnd  11985  facdiv  12055  faclbnd6  12067  facavg  12069  hashdom  12134  hashun2  12138  hashunx  12141  hashge2el2dif  12176  hashtpg  12178  hashfun  12191  hashf1  12202  seqcoll2  12209  wrdlenge2n0  12253  ccatval1  12268  ccatsymb  12273  cshwidxmod  12432  repswcshw  12438  swrds2  12537  climcnds  13306  geomulcvg  13328  mertenslem1  13336  efcllem  13355  eftlub  13385  ruclem10  13513  bitsfzolem  13622  bitsfzo  13623  bitsmod  13624  sadcaddlem  13645  sadaddlem  13654  sadasslem  13658  sadeq  13660  smuval2  13670  smupvallem  13671  smueqlem  13678  bezoutlem3  13716  bezoutlem4  13717  gcdeq  13728  dvdssqlem  13735  nn0seqcvgd  13737  eucalglt  13752  mulgcddvds  13782  qredeu  13785  prmdiveq  13853  odzdvds  13859  pythagtriplem3  13877  pythagtriplem6  13880  pythagtriplem7  13881  iserodd  13894  pclem  13897  pcpremul  13902  pcidlem  13930  pcgcd1  13935  pc2dvds  13937  pcz  13939  pcprmpw2  13940  fldivp1  13951  pcfaclem  13952  pcfac  13953  pcbc  13954  prmreclem2  13970  prmreclem3  13971  prmreclem4  13972  prmreclem5  13973  4sqlem11  14008  4sqlem12  14009  4sqlem14  14011  vdwlem11  14044  vdwlem12  14045  ramlb  14072  0ram  14073  ram0  14075  ramub1lem2  14080  ramcl  14082  psgnunilem2  15992  odmodnn0  16034  mndodconglem  16035  mndodcong  16036  oddvds  16041  odhash3  16066  gexdvds  16074  sylow1lem1  16088  sylow1lem5  16092  pgpfi  16095  pgpssslw  16104  efgsfo  16227  efgredlemd  16232  efgredlem  16235  efgred  16236  lt6abl  16362  pgpfaclem2  16573  srgbinomlem3  16630  psrbaglesupp  17415  psrbaglesuppOLD  17416  mplmonmul  17523  coe1tmmul2  17709  coe1tmmul2fv  17711  coe1pwmulfv  17713  zringlpirlem3  17885  zlpirlem3  17890  lebnumii  20518  dyadmaxlem  21057  mbfi1fseqlem3  21175  mbfi1fseqlem4  21176  mbfi1fseqlem5  21177  mdegmullem  21529  coe1mul3  21551  coe1mul4  21552  deg1sublt  21562  deg1mul2  21566  deg1tmle  21569  deg1tm  21570  ply1divmo  21587  ply1divex  21588  deg1submon1p  21604  dvdsq1p  21612  fta1glem2  21618  fta1blem  21620  plyco0  21640  plyeq0lem  21658  plypf1  21660  plyaddlem1  21661  coeeulem  21672  dgrub  21682  dgrlb  21684  dgreq  21692  coeaddlem  21696  coemullem  21697  coemulhi  21701  dgrlt  21713  dgradd2  21715  dgrmul  21717  dgrcolem2  21721  dgrco  21722  plydivlem3  21741  plydivlem4  21742  plydivex  21743  plydiveu  21744  fta1lem  21753  quotcan  21755  vieta1lem2  21757  radcnvlem1  21858  dvradcnv  21866  leibpilem1  22315  leibpi  22317  log2tlbnd  22320  birthdaylem2  22326  birthdaylem3  22327  fsumharmonic  22385  basellem3  22400  basellem5  22402  issqf  22454  ppip1le  22479  ppiltx  22495  mumullem2  22498  sgmppw  22516  ppiub  22523  chtublem  22530  chpub  22539  dchrabs  22579  bcmono  22596  bcmax  22597  bcp1ctr  22598  bclbnd  22599  bposlem5  22607  lgseisenlem1  22668  2sqlem7  22689  2sqlem8  22691  chebbnd1lem1  22698  chtppilimlem1  22702  dchrisum0re  22742  mulogsumlem  22760  selberg2lem  22779  pntrlog2bndlem4  22809  pntlemr  22831  pntlemj  22832  pnt  22843  ostth2lem3  22864  spthispth  23440  vdgrfival  23535  eupap1  23565  eupath2lem3  23568  nndiffz1  26043  nexple  26417  oddpwdc  26706  eulerpartlems  26712  eulerpartlemgc  26714  eulerpartlemb  26720  coinfliplem  26830  eluzmn  26904  signsplypnf  26920  signslema  26932  signstfvc  26944  signstfveq0  26947  dmlogdmgm  26979  erdszelem8  27055  erdsze2lem2  27061  cvmliftlem7  27149  snmlff  27187  binomfallfaclem2  27512  binomrisefac  27514  fallfacval4  27515  faclim  27521  rrnequiv  28705  eldioph2lem1  29069  pell1qrge1  29182  rmxypos  29261  ltrmynn0  29262  ltrmxnn0  29263  lermxnn0  29264  jm2.24nn  29273  jm2.24  29277  jm2.19  29313  jm2.26lem3  29321  jm2.27c  29327  hbt  29457  dgraa0p  29477  stoweidlem17  29783  stoweidlem24  29790  wallispilem5  29835  stirlinglem15  29854  modfsummods  30215  wwlknred  30326  nbhashuvtx1  30504  rusgranumwlks  30545  frghash2spot  30627  usgreghash2spotv  30630  numclwwlk5  30676  numclwwlk6  30677  friendshipgt3  30685  ssnn0ssfz  30711  pgrple2abel  30737  gsummoncoe1  30808
  Copyright terms: Public domain W3C validator