Theorem nn0re 12408

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

Syntax hints:   → wi 4   ∈ wcel 2113  ℝcr 11023  ℕ₀cn0 12399

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375  ax-un 7678  ax-1cn 11082  ax-icn 11083  ax-addcl 11084  ax-addrcl 11085  ax-mulcl 11086  ax-mulrcl 11087  ax-i2m1 11092  ax-1ne0 11093  ax-rnegex 11095  ax-rrecex 11096  ax-cnre 11097

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-ral 3050  df-rex 3059  df-reu 3349  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-iun 4946  df-br 5097  df-opab 5159  df-mpt 5178  df-tr 5204  df-id 5517  df-eprel 5522  df-po 5530  df-so 5531  df-fr 5575  df-we 5577  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-pred 6257  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-ov 7359  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-nn 12144  df-n0 12400

This theorem is referenced by:  nn0ge0  12424  nn0nlt0  12425  nn0le0eq0  12427  nn0p1gt0  12428  elnnnn0c  12444  nn0addge1  12445  nn0addge2  12446  nn0sub  12449  ltsubnn0  12450  nn0negleid  12451  difgtsumgt  12452  nn0le2x  12453  nn0n0n1ge2b  12468  nn0ge2m1nn  12469  nn0nndivcl  12471  xnn0xr  12477  nn0nepnf  12480  xnn0nemnf  12483  elznn0nn  12500  nn0lt2  12553  nn0le2is012  12554  nn0ge0div  12559  nn01to3  12852  xnn0xaddcl  13148  xnn0lem1lt  13157  xnn0lenn0nn0  13158  xnn0xadd0  13160  nn0rp0  13369  xnn0xrge0  13420  nn0fz0  13539  elfz0fzfz0  13547  fz0fzelfz0  13548  fz0fzdiffz0  13551  fzctr  13554  difelfzle  13555  difelfznle  13556  fvffz0  13560  fzoun  13610  nn0p1elfzo  13616  elfzo0le  13617  fzonmapblen  13622  fzofzim  13623  elincfzoext  13637  elfzodifsumelfzo  13645  fzonn0p1  13656  fzonn0p1p1  13658  ssfzoulel  13674  ubmelm1fzo  13677  elfznelfzo  13687  fvinim0ffz  13703  subfzo0  13706  adddivflid  13736  divfl0  13742  fldivnn0le  13750  flltdivnn0lt  13751  quoremnn0ALT  13775  modmuladdnn0  13836  addmodid  13840  modifeq2int  13854  modfzo0difsn  13864  modsumfzodifsn  13865  addmodlteq  13867  ssnn0fi  13906  fsuppmapnn0fiub0  13914  suppssfz  13915  nn0sq11  14053  bernneq  14150  bernneq3  14152  facwordi  14210  faclbnd  14211  faclbnd3  14213  faclbnd5  14219  faclbnd6  14220  facubnd  14221  facavg  14222  bcval4  14228  bcval5  14239  bcpasc  14242  hashbnd  14257  hashnnn0genn0  14264  hashnemnf  14265  hashclb  14279  hashneq0  14285  hashsdom  14302  hashunsnggt  14315  fi1uzind  14428  ccat0  14497  ccat2s1fvw  14560  swrdnd0  14579  swrdsbslen  14586  swrdspsleq  14587  pfxnd0  14610  swrdswrdlem  14625  swrdswrd  14626  swrdccatin1  14646  pfxccatin12lem2  14652  pfxccatin12lem3  14653  pfxccat3  14655  swrdccat  14656  pfxccat3a  14659  swrdccat3blem  14660  repswswrd  14705  2cshw  14734  cshweqrep  14742  cshwcsh2id  14749  2swrd2eqwrdeq  14874  nn0sqeq1  15197  nn0absid  15351  isercoll  15589  o1fsum  15734  geomulcvg  15797  rerisefaccl  15938  refallfaccl  15939  rprisefaccl  15944  dvdseq  16239  oddge22np1  16274  nn0ehalf  16303  nn0o1gt2  16306  nn0o  16308  nn0oddm1d2  16310  bitsfi  16362  bitsinv1  16367  gcdn0gt0  16443  nn0gcdid0  16446  absmulgcd  16474  nn0seqcvgd  16495  algcvgblem  16502  algcvga  16504  lcmgcdnn  16536  lcmfun  16570  lcmfass  16571  prmfac1  16645  prmndvdsfaclt  16650  nonsq  16684  hashgcdlem  16713  odzdvds  16721  iserodd  16761  pcprendvds  16766  pcdvdsb  16795  pcidlem  16798  dvdsprmpweqle  16812  difsqpwdvds  16813  pcfaclem  16824  prmunb  16840  ramtcl2  16937  ramubcl  16944  ram0  16948  ramub1lem1  16952  cshwshashlem2  17022  smndex1iidm  18824  sylow1lem1  19525  pgpssslw  19541  efgsfo  19666  efgred  19675  telgsums  19920  prmirredlem  21425  prmirred  21427  gsumbagdiaglem  21884  psrridm  21916  psdmul  22107  coe1tmmul2  22216  gsummoncoe1  22250  mp2pm2mplem4  22751  fvmptnn04ifb  22793  chfacfisf  22796  chfacfisfcpmat  22797  chfacffsupp  22798  chfacfscmul0  22800  chfacfpmmul0  22804  dyaddisj  25551  mdegle0  26036  deg1nn0clb  26049  deg1ge  26057  deg1tmle  26077  ply1divex  26096  plyco0  26151  coeeulem  26183  coeaddlem  26208  coe1termlem  26217  dgreq0  26225  dgrlt  26226  plydivex  26259  aannenlem1  26290  taylfvallem1  26318  tayl0  26323  radcnvlem1  26376  radcnvlem2  26377  dvradcnv  26384  leibpi  26906  log2tlbnd  26909  birthdaylem3  26917  zetacvg  26979  basellem2  27046  basellem3  27047  chpp1  27119  bcmono  27242  bcmax  27243  lgsdinn0  27310  2lgslem1c  27358  2sq2  27398  2sqreulem1  27411  2sqreultlem  27412  dchrisumlem1  27454  ostth2lem2  27599  nbusgrvtxm1  29401  upgrewlkle2  29629  pthdlem1  29788  crctcshwlkn0lem4  29835  crctcshwlkn0  29843  crctcsh  29846  wwlksm1edg  29903  wwlksnred  29914  wwlksnredwwlkn  29917  wwlksnredwwlkn0  29918  wwlksnextwrd  29919  wwlksnextfun  29920  wwlksnextinj  29921  wwlksnextproplem1  29931  wwlksnextproplem2  29932  wwlksnextproplem3  29933  clwlkclwwlklem2a1  30016  clwlkclwwlklem2a2  30017  clwlkclwwlklem2fv1  30019  clwlkclwwlklem2fv2  30020  clwlkclwwlklem2a4  30021  clwlkclwwlklem2a  30022  clwlkclwwlklem2  30024  clwlkclwwlk  30026  clwlkclwwlk2  30027  clwlkclwwlkf  30032  clwwisshclwwslem  30038  clwwlkel  30070  wwlksext2clwwlk  30081  clwlknf1oclwwlknlem1  30105  clwwlknonex2lem2  30132  eupth2lems  30262  eupth2  30263  eucrctshift  30267  numclwwlk7  30415  frgrreggt1  30417  frgrreg  30418  frgrogt3nreg  30421  friendship  30423  nn0mnfxrd  32780  nn0xmulclb  32800  dpcl  32921  wrdt2ind  32984  hasheuni  34191  eulerpartlems  34466  hgt750lem  34757  0nn0m1nnn0  35256  derangen  35315  faclimlem1  35886  poimirlem28  37788  rrntotbnd  37976  sticksstones22  42361  gcdnn0id  42526  nn0addcom  42659  zaddcomlem  42660  nn0mulcom  42663  nacsfix  42896  eldioph2lem1  42944  irrapxlem4  43009  pell14qrgt0  43043  pell1qrgaplem  43057  pellqrexplicit  43061  rmxycomplete  43101  jm2.17a  43144  jm2.17b  43145  rmygeid  43148  jm2.22  43179  rmxdiophlem  43199  hbtlem5  43312  hbt  43314  fperiodmullem  45493  dvnxpaek  46128  stoweidlem17  46203  wallispilem3  46253  stirlinglem5  46264  stirlinglem7  46266  fourierdlem16  46309  fourierdlem21  46314  fourierdlem22  46315  fourierdlem83  46375  fourierdlem112  46404  elaa2lem  46419  etransclem23  46443  zm1nn  47490  nn0resubcl  47496  fz0addge0  47507  elfzlble  47508  subsubelfzo0  47514  2ffzoeq  47515  addmodne  47532  submodlt  47538  iccpartigtl  47611  lswn0  47632  sqrtpwpw2p  47726  fmtnodvds  47732  goldbachth  47735  odz2prm2pw  47751  flsqrt  47781  nn0e  47885  nn0sumltlt  48538  ply1mulgsumlem2  48575  nn0eo  48716  flnn0div2ge  48721  fllog2  48756  dignn0fr  48789  digexp  48795  dig2nn0  48799  0dig2nn0e  48800  dig2bits  48802  itcovalt2lem2lem1  48861