Theorem nn0re 12490

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

Syntax hints:   → wi 4   ∈ wcel 2142  ℝcr 11072  ℕ₀cn0 12481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5246  ax-nul 5256  ax-pr 5390  ax-un 7718  ax-1cn 11131  ax-icn 11132  ax-addcl 11133  ax-addrcl 11134  ax-mulcl 11135  ax-mulrcl 11136  ax-i2m1 11141  ax-1ne0 11142  ax-rnegex 11144  ax-rrecex 11145  ax-cnre 11146

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1099  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3077  df-rex 3087  df-reu 3368  df-rab 3415  df-v 3456  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4951  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5542  df-eprel 5547  df-po 5555  df-so 5556  df-fr 5600  df-we 5602  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-pred 6288  df-ord 6349  df-on 6350  df-lim 6351  df-suc 6352  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-fv 6529  df-ov 7399  df-om 7847  df-2nd 7971  df-frecs 8262  df-wrecs 8293  df-recs 8342  df-rdg 8381  df-nn 12211  df-n0 12482

This theorem is referenced by:  nn0ge0  12506  nn0nlt0  12507  nn0le0eq0  12509  nn0p1gt0  12510  elnnnn0c  12526  nn0addge1  12527  nn0addge2  12528  nn0sub  12531  ltsubnn0  12532  nn0negleid  12533  difgtsumgt  12534  nn0le2x  12535  nn0n0n1ge2b  12550  nn0ge2m1nn  12551  nn0nndivcl  12553  xnn0xr  12559  nn0nepnf  12562  xnn0nemnf  12565  elznn0nn  12582  nn0lt2  12636  nn0le2is012  12637  nn0ge0div  12642  nn01to3  12942  xnn0xaddcl  13238  xnn0lem1lt  13247  xnn0lenn0nn0  13248  xnn0xadd0  13250  nn0rp0  13459  xnn0xrge0  13510  nn0fz0  13630  elfz0fzfz0  13638  fz0fzelfz0  13639  fz0fzdiffz0  13642  fzctr  13645  difelfzle  13646  difelfznle  13647  fvffz0  13651  fzoun  13702  nn0p1elfzo  13708  elfzo0le  13709  fzonmapblen  13714  fzofzim  13715  elincfzoext  13729  elfzodifsumelfzo  13737  fzonn0p1  13748  fzonn0p1p1  13750  ssfzoulel  13766  ubmelm1fzo  13769  elfznelfzo  13779  fvinim0ffz  13795  subfzo0  13798  adddivflid  13828  divfl0  13834  fldivnn0le  13842  flltdivnn0lt  13843  quoremnn0ALT  13867  modmuladdnn0  13928  addmodid  13932  modifeq2int  13946  modfzo0difsn  13956  modsumfzodifsn  13957  addmodlteq  13959  ssnn0fi  13998  fsuppmapnn0fiub0  14006  suppssfz  14007  nn0sq11  14145  bernneq  14242  bernneq3  14244  facwordi  14302  faclbnd  14303  faclbnd3  14305  faclbnd5  14311  faclbnd6  14312  facubnd  14313  facavg  14314  bcval4  14320  bcval5  14331  bcpasc  14334  hashbnd  14349  hashnnn0genn0  14356  hashnemnf  14357  hashclb  14371  hashneq0  14377  hashsdom  14394  hashunsnggt  14407  fi1uzind  14520  ccat0  14589  ccat2s1fvw  14652  swrdnd0  14671  swrdsbslen  14678  swrdspsleq  14679  pfxnd0  14702  swrdswrdlem  14717  swrdswrd  14718  swrdccatin1  14738  pfxccatin12lem2  14744  pfxccatin12lem3  14745  pfxccat3  14747  swrdccat  14748  pfxccat3a  14751  swrdccat3blem  14752  repswswrd  14797  2cshw  14826  cshweqrep  14834  cshwcsh2id  14841  2swrd2eqwrdeq  14966  nn0sqeq1  15303  nn0absid  15457  isercoll  15695  o1fsum  15841  geomulcvg  15906  rerisefaccl  16047  refallfaccl  16048  rprisefaccl  16053  dvdseq  16348  oddge22np1  16383  nn0ehalf  16412  nn0o1gt2  16415  nn0o  16417  nn0oddm1d2  16419  bitsfi  16471  bitsinv1  16476  gcdn0gt0  16552  nn0gcdid0  16555  absmulgcd  16583  nn0seqcvgd  16604  algcvgblem  16611  algcvga  16613  lcmgcdnn  16645  lcmfun  16679  lcmfass  16680  prmfac1  16755  prmndvdsfaclt  16760  nonsq  16794  hashgcdlem  16823  odzdvds  16831  iserodd  16871  pcprendvds  16876  pcdvdsb  16905  pcidlem  16908  dvdsprmpweqle  16922  difsqpwdvds  16923  pcfaclem  16934  prmunb  16950  ramtcl2  17047  ramubcl  17054  ram0  17058  ramub1lem1  17062  cshwshashlem2  17132  smndex1iidm  18935  sylow1lem1  19638  pgpssslw  19654  efgsfo  19779  efgred  19788  telgsums  20033  prmirredlem  21524  prmirred  21526  gsumbagdiaglem  21983  psrridm  22014  psdmul  22231  coe1tmmul2  22339  gsummoncoe1  22371  mp2pm2mplem4  22869  fvmptnn04ifb  22911  chfacfisf  22914  chfacfisfcpmat  22915  chfacffsupp  22916  chfacfscmul0  22918  chfacfpmmul0  22922  dyaddisj  25658  mdegle0  26137  deg1nn0clb  26150  deg1ge  26158  deg1tmle  26178  ply1divex  26197  plyco0  26252  coeeulem  26284  coeaddlem  26309  coe1termlem  26318  dgreq0  26325  dgrlt  26326  plydivex  26361  aannenlem1  26392  taylfvallem1  26420  tayl0  26425  radcnvlem1  26476  radcnvlem2  26477  dvradcnv  26484  leibpi  27007  log2tlbnd  27010  birthdaylem3  27018  zetacvg  27079  basellem2  27146  basellem3  27147  chpp1  27219  bcmono  27341  bcmax  27342  lgsdinn0  27409  2lgslem1c  27457  2sq2  27497  2sqreulem1  27510  2sqreultlem  27511  dchrisumlem1  27553  ostth2lem2  27698  nbusgrvtxm1  29580  upgrewlkle2  29807  pthdlem1  29966  crctcshwlkn0lem4  30013  crctcshwlkn0  30021  crctcsh  30024  wwlksm1edg  30081  wwlksnred  30092  wwlksnredwwlkn  30095  wwlksnredwwlkn0  30096  wwlksnextwrd  30097  wwlksnextfun  30098  wwlksnextinj  30099  wwlksnextproplem1  30109  wwlksnextproplem2  30110  wwlksnextproplem3  30111  clwlkclwwlklem2a1  30194  clwlkclwwlklem2a2  30195  clwlkclwwlklem2fv1  30197  clwlkclwwlklem2fv2  30198  clwlkclwwlklem2a4  30199  clwlkclwwlklem2a  30200  clwlkclwwlklem2  30202  clwlkclwwlk  30204  clwlkclwwlk2  30205  clwlkclwwlkf  30210  clwwisshclwwslem  30216  clwwlkel  30248  wwlksext2clwwlk  30259  clwlknf1oclwwlknlem1  30283  clwwlknonex2lem2  30310  eupth2lems  30440  eupth2  30441  eucrctshift  30445  numclwwlk7  30593  frgrreggt1  30595  frgrreg  30596  frgrogt3nreg  30599  friendship  30601  nn0mnfxrd  32953  nn0xmulclb  32973  dpcl  33068  wrdt2ind  33131  hasheuni  34382  eulerpartlems  34657  hgt750lem  34945  0nn0m1nnn0  35463  derangen  35522  faclimlem1  36093  poimirlem28  38147  rrntotbnd  38335  sticksstones22  42785  gcdnn0id  42938  nn0addcom  43084  zaddcomlem  43085  nn0mulcom  43088  nacsfix  43293  eldioph2lem1  43341  irrapxlem4  43402  pell14qrgt0  43436  pell1qrgaplem  43450  pellqrexplicit  43454  rmxycomplete  43494  jm2.17a  43537  jm2.17b  43538  rmygeid  43541  jm2.22  43572  rmxdiophlem  43592  hbtlem5  43705  hbt  43707  fperiodmullem  45882  dvnxpaek  46516  stoweidlem17  46591  wallispilem3  46641  stirlinglem5  46652  stirlinglem7  46654  fourierdlem16  46697  fourierdlem21  46702  fourierdlem22  46703  fourierdlem83  46763  fourierdlem112  46792  elaa2lem  46807  etransclem23  46831  zm1nn  47896  nn0resubcl  47902  fz0addge0  47913  elfzlble  47914  subsubelfzo0  47921  2ffzoeq  47922  addmodne  47944  submodlt  47950  iccpartigtl  48029  lswn0  48050  sqrtpwpw2p  48147  fmtnodvds  48153  goldbachth  48156  odz2prm2pw  48172  flsqrt  48202  nn0e  48319  nn0sumltlt  48972  ply1mulgsumlem2  49009  nn0eo  49150  flnn0div2ge  49155  fllog2  49190  dignn0fr  49223  digexp  49229  dig2nn0  49233  0dig2nn0e  49234  dig2bits  49236  itcovalt2lem2lem1  49295