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

Theorem nn0red 12180
Description: A nonnegative integer is a real number. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
nn0red.1 (𝜑𝐴 ∈ ℕ0)
Assertion
Ref Expression
nn0red (𝜑𝐴 ∈ ℝ)

Proof of Theorem nn0red
StepHypRef Expression
1 nn0ssre 12123 . 2 0 ⊆ ℝ
2 nn0red.1 . 2 (𝜑𝐴 ∈ ℕ0)
31, 2sselid 3915 1 (𝜑𝐴 ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2112  cr 10757  0cn0 12119
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2710  ax-sep 5208  ax-nul 5215  ax-pr 5338  ax-un 7544  ax-1cn 10816  ax-icn 10817  ax-addcl 10818  ax-addrcl 10819  ax-mulcl 10820  ax-mulrcl 10821  ax-i2m1 10826  ax-1ne0 10827  ax-rnegex 10829  ax-rrecex 10830  ax-cnre 10831
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2818  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-reu 3071  df-rab 3073  df-v 3425  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4456  df-pw 4531  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4836  df-iun 4922  df-br 5070  df-opab 5132  df-mpt 5152  df-tr 5178  df-id 5471  df-eprel 5477  df-po 5485  df-so 5486  df-fr 5526  df-we 5528  df-xp 5574  df-rel 5575  df-cnv 5576  df-co 5577  df-dm 5578  df-rn 5579  df-res 5580  df-ima 5581  df-pred 6178  df-ord 6236  df-on 6237  df-lim 6238  df-suc 6239  df-iota 6358  df-fun 6402  df-fn 6403  df-f 6404  df-f1 6405  df-fo 6406  df-f1o 6407  df-fv 6408  df-ov 7237  df-om 7666  df-wrecs 8070  df-recs 8131  df-rdg 8169  df-nn 11860  df-n0 12120
This theorem is referenced by:  nn0cnd  12181  nn0readdcl  12185  eluzmn  12474  flmulnn0  13431  quoremz  13459  quoremnn0ALT  13461  modaddmodup  13538  modaddmodlo  13539  expneg  13674  expnbnd  13831  facdiv  13885  faclbnd6  13897  hashdom  13978  hashun2  13982  hashunx  13985  hashfun  14036  hashf1  14055  seqcoll2  14063  hashge2el2dif  14078  hashtpg  14083  wrdlenge2n0  14139  ccatsymb  14171  ccatrn  14178  ccatalpha  14182  ccat2s1fvw  14233  ccat2s1fvwOLD  14234  swrdnd  14251  swrdnd0  14254  pfxnd0  14285  pfxsuffeqwrdeq  14295  swrdccat3blem  14336  cshwidxmod  14400  repswcshw  14409  swrds2  14537  modfsummods  15389  climcnds  15447  geomulcvg  15472  mertenslem1  15480  binomfallfaclem2  15634  binomrisefac  15636  fallfacval4  15637  efcllem  15671  eftlub  15702  ruclem10  15832  oddge22np1  15942  nn0oddm1d2  15978  divalglem5  15990  bitsfzolem  16025  bitsfzo  16026  bitsmod  16027  sadcaddlem  16048  sadaddlem  16057  sadasslem  16061  sadeq  16063  smuval2  16073  smupvallem  16074  smueqlem  16081  bezoutlem3  16133  bezoutlem4  16134  gcdzeq  16146  dvdssqlem  16155  nn0seqcvgd  16159  eucalglt  16174  lcmneg  16192  mulgcddvds  16244  qredeu  16247  prmdiveq  16371  odzdvds  16380  pythagtriplem3  16403  pythagtriplem6  16406  pythagtriplem7  16407  iserodd  16420  pclem  16423  pcpremul  16428  pcidlem  16457  pcgcd1  16462  pc2dvds  16464  pcz  16466  pcprmpw2  16467  fldivp1  16482  pcfaclem  16483  pcfac  16484  pcbc  16485  prmreclem2  16502  prmreclem3  16503  prmreclem4  16504  prmreclem5  16505  4sqlem11  16540  4sqlem12  16541  4sqlem14  16543  vdwlem11  16576  vdwlem12  16577  ramlb  16604  0ram  16605  ram0  16607  ramub1lem2  16612  ramcl  16614  psgnunilem2  18919  odmodnn0  18964  mndodconglem  18965  mndodcong  18966  oddvds  18971  odhash3  18997  gexdvds  19005  sylow1lem1  19019  sylow1lem5  19023  pgpfi  19026  pgpssslw  19035  efgsfo  19161  efgredlemd  19166  efgredlem  19169  efgred  19170  lt6abl  19312  telgsums  19410  pgpfaclem2  19501  srgbinomlem3  19589  zringlpirlem3  20483  psrbaglesupp  20914  psrbaglesuppOLD  20915  psrbagcon  20920  mplmonmul  21024  coe1tmmul2  21228  coe1tmmul2fv  21230  coe1pwmulfv  21232  gsummoncoe1  21256  fvmptnn04if  21777  fvmptnn04ifc  21780  fvmptnn04ifd  21781  chfacfscmulgsum  21788  chfacfpmmulgsum  21792  lebnumii  23894  dyadmaxlem  24525  mbfi1fseqlem3  24646  mbfi1fseqlem4  24647  mbfi1fseqlem5  24648  mdegmullem  25007  coe1mul3  25028  coe1mul4  25029  deg1sublt  25039  deg1mul2  25043  deg1tmle  25046  deg1tm  25047  ply1divmo  25064  ply1divex  25065  deg1submon1p  25081  dvdsq1p  25089  fta1glem2  25095  fta1blem  25097  plyco0  25117  plyeq0lem  25135  plypf1  25137  plyaddlem1  25138  coeeulem  25149  dgrub  25159  dgrlb  25161  dgreq  25169  coeaddlem  25174  coemullem  25175  coemulhi  25179  dgrlt  25191  dgradd2  25193  dgrmul  25195  dgrcolem2  25199  dgrco  25200  plydivlem3  25219  plydivlem4  25220  plydivex  25221  plydiveu  25222  fta1lem  25231  quotcan  25233  vieta1lem2  25235  radcnvlem1  25336  dvradcnv  25344  leibpi  25856  log2tlbnd  25859  birthdaylem2  25866  birthdaylem3  25867  fsumharmonic  25925  dmlogdmgm  25937  basellem3  25996  basellem5  25998  issqf  26049  ppip1le  26074  ppiltx  26090  mumullem2  26093  sgmppw  26109  ppiub  26116  chtublem  26123  chpub  26132  dchrabs  26172  bcmono  26189  bcmax  26190  bcp1ctr  26191  bclbnd  26192  bposlem5  26200  gausslemma2dlem0h  26275  gausslemma2dlem4  26281  gausslemma2dlem6  26284  lgseisenlem1  26287  2lgsoddprmlem2  26321  2sqlem7  26336  2sqlem8  26338  2sq2  26345  2sqmod  26348  chebbnd1lem1  26381  chtppilimlem1  26385  dchrisum0re  26425  mulogsumlem  26443  selberg2lem  26462  pntrlog2bndlem4  26492  pntlemr  26514  pntlemj  26515  pnt  26526  ostth2lem3  26547  vtxdgfival  27588  vtxdfiun  27601  vtxdginducedm1fi  27663  crctcsh  27939  wwlksnred  28007  wwlksnextproplem2  28025  rusgrnumwwlks  28089  eupth2lems  28352  eucrct2eupth  28359  numclwlk1lem1  28483  numclwwlk5  28502  numclwwlk6  28504  friendshipgt3  28512  nnmulge  30824  nndiffz1  30858  prmdvdsbc  30881  pfxlsw2ccat  30975  wrdt2ind  30976  cycpmrn  31160  cyc3conja  31174  nexple  31720  oddpwdc  32064  eulerpartlems  32070  eulerpartlemgc  32072  eulerpartlemb  32078  coinfliplem  32188  signsplypnf  32272  signslema  32284  signstfvc  32296  signstfveq0  32299  fsum2dsub  32330  reprlt  32342  reprgt  32344  reprinfz1  32345  breprexplemc  32355  lpadmax  32405  lpadright  32407  usgrgt2cycl  32835  acycgr1v  32854  erdszelem8  32903  erdsze2lem2  32909  cvmliftlem7  32996  snmlff  33034  bcprod  33453  poimirlem3  35553  poimirlem4  35554  poimirlem6  35556  poimirlem7  35557  poimirlem10  35560  poimirlem11  35561  poimirlem12  35562  poimirlem13  35563  poimirlem15  35565  poimirlem16  35566  poimirlem17  35567  poimirlem19  35569  poimirlem20  35570  poimirlem21  35571  poimirlem22  35572  poimirlem23  35573  poimirlem24  35574  poimirlem25  35575  poimirlem26  35576  poimirlem29  35579  poimirlem30  35580  poimirlem31  35581  rrnequiv  35766  lcmineqlem17  39823  lcmineqlem21  39827  3lexlogpow5ineq5  39838  aks4d1p1p4  39848  aks4d1p1p7  39851  aks4d1p3  39855  aks4d1p7d1  39859  2np3bcnp1  39863  2ap1caineq  39864  sticksstones6  39870  sticksstones7  39871  sticksstones22  39887  frlmvscadiccat  39998  fltnltalem  40249  eldioph2lem1  40332  pell1qrge1  40442  rmxypos  40519  ltrmynn0  40520  ltrmxnn0  40521  lermxnn0  40522  jm2.24nn  40531  jm2.24  40535  jm2.19  40565  jm2.26lem3  40573  jm2.27c  40579  hbt  40705  dgraa0p  40724  binomcxplemnn0  41687  fsumnncl  42833  mccllem  42858  ioodvbdlimc1lem2  43193  ioodvbdlimc2lem  43195  dvnxpaek  43203  dvnmul  43204  dvnprodlem2  43208  stoweidlem17  43278  stoweidlem24  43285  wallispilem5  43330  stirlinglem15  43349  fourierdlem48  43415  fourierdlem83  43450  fourierdlem103  43470  fourierdlem104  43471  sqwvfoura  43489  elaa2lem  43494  etransclem10  43505  etransclem19  43514  etransclem20  43515  etransclem21  43516  etransclem22  43517  etransclem23  43518  etransclem24  43519  etransclem27  43522  etransclem32  43527  etransclem35  43530  etransclem44  43539  etransclem45  43540  etransclem46  43541  etransclem47  43542  etransclem48  43543  etransc  43544  rrndistlt  43551  fmtnoge3  44700  sqrtpwpw2p  44708  fmtnosqrt  44709  flsqrt  44763  lighneallem4a  44778  ssnn0ssfz  45403  pgrple2abl  45419  nn0eo  45592  fllog2  45632  itcovalt2lem2lem1  45737  aacllem  46221
  Copyright terms: Public domain W3C validator