Theorem nn0re 12532

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 12527	. 2 ⊢ ℕ0 ⊆ ℝ
2	1	sseli 3990	1 ⊢ (𝐴 ∈ ℕ0 → 𝐴 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2105  ℝcr 11151  ℕ₀cn0 12523

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437  ax-un 7753  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-i2m1 11220  ax-1ne0 11221  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-ov 7433  df-om 7887  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-nn 12264  df-n0 12524

This theorem is referenced by:  nn0ge0  12548  nn0nlt0  12549  nn0le0eq0  12551  nn0p1gt0  12552  elnnnn0c  12568  nn0addge1  12569  nn0addge2  12570  nn0sub  12573  ltsubnn0  12574  nn0negleid  12575  difgtsumgt  12576  nn0le2x  12577  nn0n0n1ge2b  12592  nn0ge2m1nn  12593  nn0nndivcl  12595  xnn0xr  12601  nn0nepnf  12604  xnn0nemnf  12607  elznn0nn  12624  nn0lt2  12678  nn0le2is012  12679  nn0ge0div  12684  nn01to3  12980  xnn0xaddcl  13273  xnn0lem1lt  13282  xnn0lenn0nn0  13283  xnn0xadd0  13285  nn0rp0  13491  xnn0xrge0  13542  nn0fz0  13661  elfz0fzfz0  13669  fz0fzelfz0  13670  fz0fzdiffz0  13673  fzctr  13676  difelfzle  13677  difelfznle  13678  fvffz0  13682  fzoun  13732  nn0p1elfzo  13738  elfzo0le  13739  fzonmapblen  13744  fzofzim  13745  elincfzoext  13758  elfzodifsumelfzo  13766  fzonn0p1  13777  fzonn0p1p1  13779  ssfzoulel  13795  ubmelm1fzo  13798  elfznelfzo  13807  fvinim0ffz  13821  subfzo0  13824  adddivflid  13854  divfl0  13860  fldivnn0le  13868  flltdivnn0lt  13869  quoremnn0ALT  13893  modmuladdnn0  13952  addmodid  13956  modifeq2int  13970  modfzo0difsn  13980  modsumfzodifsn  13981  addmodlteq  13983  ssnn0fi  14022  fsuppmapnn0fiub0  14030  suppssfz  14031  nn0sq11  14168  bernneq  14264  bernneq3  14266  facwordi  14324  faclbnd  14325  faclbnd3  14327  faclbnd5  14333  faclbnd6  14334  facubnd  14335  facavg  14336  bcval4  14342  bcval5  14353  bcpasc  14356  hashbnd  14371  hashnnn0genn0  14378  hashnemnf  14379  hashclb  14393  hashneq0  14399  hashsdom  14416  hashunsnggt  14429  fi1uzind  14542  ccat0  14610  ccat2s1fvw  14672  swrdnd0  14691  swrdsbslen  14698  swrdspsleq  14699  pfxnd0  14722  swrdswrdlem  14738  swrdswrd  14739  swrdccatin1  14759  pfxccatin12lem2  14765  pfxccatin12lem3  14766  pfxccat3  14768  swrdccat  14769  pfxccat3a  14772  swrdccat3blem  14773  repswswrd  14818  2cshw  14847  cshweqrep  14855  cshwcsh2id  14863  2swrd2eqwrdeq  14988  nn0sqeq1  15311  isercoll  15700  o1fsum  15845  geomulcvg  15908  rerisefaccl  16049  refallfaccl  16050  rprisefaccl  16055  dvdseq  16347  oddge22np1  16382  nn0ehalf  16411  nn0o1gt2  16414  nn0o  16416  nn0oddm1d2  16418  bitsfi  16470  bitsinv1  16475  gcdn0gt0  16551  nn0gcdid0  16554  absmulgcd  16582  nn0seqcvgd  16603  algcvgblem  16610  algcvga  16612  lcmgcdnn  16644  lcmfun  16678  lcmfass  16679  prmfac1  16753  prmndvdsfaclt  16758  nonsq  16792  hashgcdlem  16821  odzdvds  16828  iserodd  16868  pcprendvds  16873  pcdvdsb  16902  pcidlem  16905  dvdsprmpweqle  16919  difsqpwdvds  16920  pcfaclem  16931  prmunb  16947  ramtcl2  17044  ramubcl  17051  ram0  17055  ramub1lem1  17059  cshwshashlem2  17130  smndex1iidm  18926  sylow1lem1  19630  pgpssslw  19646  efgsfo  19771  efgred  19780  telgsums  20025  prmirredlem  21500  prmirred  21502  gsumbagdiaglem  21967  psrridm  22000  psdmul  22187  coe1tmmul2  22294  gsummoncoe1  22327  mp2pm2mplem4  22830  fvmptnn04ifb  22872  chfacfisf  22875  chfacfisfcpmat  22876  chfacffsupp  22877  chfacfscmul0  22879  chfacfpmmul0  22883  dyaddisj  25644  mdegle0  26130  deg1nn0clb  26143  deg1ge  26151  deg1tmle  26171  ply1divex  26190  plyco0  26245  coeeulem  26277  coeaddlem  26302  coe1termlem  26311  dgreq0  26319  dgrlt  26320  plydivex  26353  aannenlem1  26384  taylfvallem1  26412  tayl0  26417  radcnvlem1  26470  radcnvlem2  26471  dvradcnv  26478  leibpi  26999  log2tlbnd  27002  birthdaylem3  27010  zetacvg  27072  basellem2  27139  basellem3  27140  chpp1  27212  bcmono  27335  bcmax  27336  lgsdinn0  27403  2lgslem1c  27451  2sq2  27491  2sqreulem1  27504  2sqreultlem  27505  dchrisumlem1  27547  ostth2lem2  27692  nbusgrvtxm1  29410  upgrewlkle2  29638  pthdlem1  29798  crctcshwlkn0lem4  29842  crctcshwlkn0  29850  crctcsh  29853  wwlksm1edg  29910  wwlksnred  29921  wwlksnredwwlkn  29924  wwlksnredwwlkn0  29925  wwlksnextwrd  29926  wwlksnextfun  29927  wwlksnextinj  29928  wwlksnextproplem1  29938  wwlksnextproplem2  29939  wwlksnextproplem3  29940  clwlkclwwlklem2a1  30020  clwlkclwwlklem2a2  30021  clwlkclwwlklem2fv1  30023  clwlkclwwlklem2fv2  30024  clwlkclwwlklem2a4  30025  clwlkclwwlklem2a  30026  clwlkclwwlklem2  30028  clwlkclwwlk  30030  clwlkclwwlk2  30031  clwlkclwwlkf  30036  clwwisshclwwslem  30042  clwwlkel  30074  wwlksext2clwwlk  30085  clwlknf1oclwwlknlem1  30109  clwwlknonex2lem2  30136  eupth2lems  30266  eupth2  30267  eucrctshift  30271  numclwwlk7  30419  frgrreggt1  30421  frgrreg  30422  frgrogt3nreg  30425  friendship  30427  nn0xmulclb  32781  dpcl  32857  wrdt2ind  32922  hasheuni  34065  eulerpartlems  34341  hgt750lem  34644  0nn0m1nnn0  35096  derangen  35156  faclimlem1  35722  poimirlem28  37634  rrntotbnd  37822  sticksstones22  42149  factwoffsmonot  42223  gcdnn0id  42342  nn0addcom  42456  zaddcomlem  42457  nn0mulcom  42460  nacsfix  42699  eldioph2lem1  42747  irrapxlem4  42812  pell14qrgt0  42846  pell1qrgaplem  42860  pellqrexplicit  42864  rmxycomplete  42905  jm2.17a  42948  jm2.17b  42949  rmygeid  42952  jm2.22  42983  rmxdiophlem  43003  hbtlem5  43116  hbt  43118  fperiodmullem  45253  dvnxpaek  45897  stoweidlem17  45972  wallispilem3  46022  stirlinglem5  46033  stirlinglem7  46035  fourierdlem16  46078  fourierdlem21  46083  fourierdlem22  46084  fourierdlem83  46144  fourierdlem112  46173  elaa2lem  46188  etransclem23  46212  zm1nn  47251  nn0resubcl  47257  fz0addge0  47268  elfzlble  47269  subsubelfzo0  47275  2ffzoeq  47276  addmodne  47283  submodlt  47289  iccpartigtl  47347  lswn0  47368  sqrtpwpw2p  47462  fmtnodvds  47468  goldbachth  47471  odz2prm2pw  47487  flsqrt  47517  nn0e  47621  nn0sumltlt  48194  ply1mulgsumlem2  48232  nn0eo  48377  flnn0div2ge  48382  fllog2  48417  dignn0fr  48450  digexp  48456  dig2nn0  48460  0dig2nn0e  48461  dig2bits  48463  itcovalt2lem2lem1  48522