Theorem nn0re 11178

Description: A nonnegative integer is a real number. (Contributed by NM, 9-May-2004.)

Assertion

Ref	Expression
nn0re	⊢ (𝐴 ∈ ℕ0 → 𝐴 ∈ ℝ)

Proof of Theorem nn0re

Step	Hyp	Ref	Expression
1		nn0ssre 11173	. 2 ⊢ ℕ0 ⊆ ℝ
2	1	sseli 3564	1 ⊢ (𝐴 ∈ ℕ0 → 𝐴 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 1977  ℝcr 9814  ℕ₀cn0 11169

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-i2m1 9883  ax-1ne0 9884  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552  df-om 6958  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-nn 10898  df-n0 11170

This theorem is referenced by:  nn0ge0  11195  nn0nlt0  11196  nn0le0eq0  11198  nn0p1gt0  11199  elnnnn0c  11215  nn0addge1  11216  nn0addge2  11217  nn0sub  11220  ltsubnn0  11221  nn0negleid  11222  difgtsumgt  11223  nn0n0n1ge2b  11236  nn0ge2m1nn  11237  nn0nndivcl  11239  xnn0xr  11245  nn0nepnf  11248  xnn0nemnf  11251  elznn0nn  11268  nn0lt2  11317  nn0ge0div  11322  nn01to3  11657  xnn0xaddcl  11940  xnn0xadd0  11949  nn0rp0  12150  xnn0xrge0  12196  nn0fz0  12306  elfz0fzfz0  12313  fz0fzelfz0  12314  fz0fzdiffz0  12317  fzctr  12320  difelfzle  12321  difelfznle  12322  fvffz0  12326  nn0p1elfzo  12378  elfzo0le  12379  fzonmapblen  12381  fzofzim  12382  elincfzoext  12393  elfzodifsumelfzo  12401  fzonn0p1  12411  fzonn0p1p1  12413  elfzom1p1elfzo  12414  ssfzoulel  12428  ubmelm1fzo  12430  elfznelfzo  12439  fvinim0ffz  12449  subfzo0  12452  adddivflid  12481  divfl0  12487  fldivnn0le  12495  flltdivnn0lt  12496  quoremnn0ALT  12518  modmuladdnn0  12576  addmodid  12580  modifeq2int  12594  modfzo0difsn  12604  modsumfzodifsn  12605  addmodlteq  12607  ssnn0fi  12646  fsuppmapnn0fiub0  12655  suppssfz  12656  bernneq  12852  bernneq3  12854  facwordi  12938  faclbnd  12939  faclbnd3  12941  faclbnd5  12947  faclbnd6  12948  facubnd  12949  facavg  12950  bcval4  12956  bcval5  12967  bcpasc  12970  hashbnd  12985  hashnnn0genn0  12993  hashnemnf  12994  hashclb  13011  hashneq0  13016  hashsdom  13031  fi1uzind  13134  brfi1indALT  13137  fi1uzindOLD  13140  brfi1indALTOLD  13143  swrdsbslen  13300  swrdspsleq  13301  2swrdeqwrdeq  13305  swrdswrdlem  13311  swrdswrd  13312  swrdccatin1  13334  swrdccatin12lem2  13340  swrdccatin12lem3  13341  swrdccat3  13343  swrdccat  13344  swrdccat3blem  13346  swrdccatid  13348  repswswrd  13382  2cshw  13410  cshweqrep  13418  cshwcsh2id  13425  2swrd2eqwrdeq  13544  isercoll  14246  o1fsum  14386  geomulcvg  14446  rerisefaccl  14587  refallfaccl  14588  rprisefaccl  14593  dvdseq  14874  oddge22np1  14911  nn0ehalf  14933  nn0o1gt2  14935  nn0o  14937  nn0oddm1d2  14939  divalglem5  14958  bitsfi  14997  bitsinv1  15002  gcdn0gt0  15077  nn0gcdid0  15080  absmulgcd  15104  nn0seqcvgd  15121  algcvgblem  15128  algcvga  15130  lcmgcdnn  15162  lcmfun  15196  lcmfass  15197  prmfac1  15269  prmndvdsfaclt  15273  nonsq  15305  hashgcdlem  15331  odzdvds  15338  iserodd  15378  pcprendvds  15383  pcdvdsb  15411  pcidlem  15414  dvdsprmpweqle  15428  difsqpwdvds  15429  pcfaclem  15440  prmunb  15456  ramtcl2  15553  ramubcl  15560  ram0  15564  ramub1lem1  15568  cshwshashlem2  15641  sylow1lem1  17836  pgpssslw  17852  efgsfo  17975  efgred  17984  telgsums  18213  psrbagcon  19192  gsumbagdiaglem  19196  psrridm  19225  coe1tmmul2  19467  gsummoncoe1  19495  prmirredlem  19660  prmirred  19662  mp2pm2mplem4  20433  fvmptnn04ifb  20475  chfacfisf  20478  chfacfisfcpmat  20479  chfacffsupp  20480  chfacfscmul0  20482  chfacfpmmul0  20486  dyaddisj  23170  mdegle0  23641  deg1nn0clb  23654  deg1ge  23662  deg1tmle  23681  ply1divex  23700  plyco0  23752  coeeulem  23784  coeaddlem  23809  coe1termlem  23818  dgreq0  23825  dgrlt  23826  plydivex  23856  aannenlem1  23887  taylfvallem1  23915  tayl0  23920  radcnvlem1  23971  radcnvlem2  23972  dvradcnv  23979  leibpi  24469  log2tlbnd  24472  birthdaylem3  24480  zetacvg  24541  basellem2  24608  basellem3  24609  chpp1  24681  bcmono  24802  bcmax  24803  lgsdinn0  24870  2lgslem1c  24918  dchrisumlem1  24978  ostth2lem2  25123  upgredg  25811  wlkonwlk  26065  cyclnspth  26159  nvnencycllem  26171  wwlknred  26251  wwlknredwwlkn  26254  wwlknredwwlkn0  26255  wwlkextwrd  26256  wwlkextfun  26257  wwlkextinj  26258  wwlkm1edg  26263  wwlkextproplem1  26269  wwlkextproplem2  26270  wwlkextproplem3  26271  clwwlkgt0  26299  clwwlkn0  26302  clwlkisclwwlklem2a1  26307  clwlkisclwwlklem2a2  26308  clwlkisclwwlklem2fv1  26310  clwlkisclwwlklem2fv2  26311  clwlkisclwwlklem2a4  26312  clwlkisclwwlklem2a  26313  clwlkisclwwlklem1  26315  clwlkisclwwlk2  26318  clwwlkel  26321  wwlkext2clwwlk  26331  clwwisshclwwlem  26334  clwlkfclwwlk1hash  26369  clwlkf1clwwlklem1  26373  vdgrf  26425  vdgrfif  26426  eupath2  26507  extwwlkfablem2  26605  numclwwlkovf2ex  26613  numclwwlk7  26641  frgrareggt1  26643  frgrareg  26644  frgraogt3nreg  26647  friendship  26649  nn0sqeq1  28901  hasheuni  29474  eulerpartlems  29749  derangen  30408  faclimlem1  30882  poimirlem28  32607  rrntotbnd  32805  nacsfix  36293  eldioph2lem1  36341  irrapxlem4  36407  pell14qrgt0  36441  pell1qrgaplem  36455  pellqrexplicit  36459  rmxycomplete  36500  jm2.17a  36545  jm2.17b  36546  rmygeid  36549  jm2.22  36580  rmxdiophlem  36600  hbtlem5  36717  hbt  36719  fperiodmullem  38458  dvnxpaek  38832  stoweidlem17  38910  wallispilem3  38960  stirlinglem5  38971  stirlinglem7  38973  fourierdlem16  39016  fourierdlem21  39021  fourierdlem22  39022  fourierdlem83  39082  fourierdlem112  39111  elaa2lem  39126  etransclem23  39150  iccpartigtl  39961  sqrtpwpw2p  39988  fmtnodvds  39994  goldbachth  39997  odz2prm2pw  40013  flsqrt  40046  nn0e  40146  lswn0  40242  pfx2  40275  pfxccatin12lem2  40287  pfxccat3  40289  pfxccat3a  40292  zm1nn  40348  nn0resubcl  40349  fz0addge0  40356  elfzlble  40357  subsubelfzo0  40359  2ffzoeq  40361  nbusgrvtxm1  40607  upgrewlkle2  40808  pthdlem1  40972  crctcsh1wlkn0lem4  41016  crctcsh1wlkn0  41024  crctcsh  41027  wwlksm1edg  41078  wwlksnred  41098  wwlksnredwwlkn  41101  wwlksnredwwlkn0  41102  wwlksnextwrd  41103  wwlksnextfun  41104  wwlksnextinj  41105  wwlksnextproplem2  41116  wwlksnextproplem3  41117  clwlkclwwlklem2a1  41201  clwlkclwwlklem2a2  41202  clwlkclwwlklem2fv1  41204  clwlkclwwlklem2fv2  41205  clwlkclwwlklem2a4  41206  clwlkclwwlklem2a  41207  clwlkclwwlklem2  41209  clwlkclwwlk  41211  clwlkclwwlk2  41212  clwwlksel  41221  wwlksext2clwwlk  41231  clwwisshclwwslem  41234  clwlksf1clwwlklem1  41272  eupth2lems  41406  eupth2  41407  eucrctshift  41411  av-numclwwlkovf2ex  41517  av-numclwwlk7  41545  av-frgrareggt1  41547  av-frgrareg  41548  av-frgraogt3nreg  41551  av-friendship  41553  nn0sumltlt  41921  nn0le2is012  41938  ply1mulgsumlem2  41969  nn0eo  42116  flnn0div2ge  42121  fllog2  42160  dignn0fr  42193  digexp  42199  dig2nn0  42203  0dig2nn0e  42204  dig2bits  42206  dpcl  42311