Theorem nn0re 12502

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

Syntax hints:   → wi 4   ∈ wcel 2107  ℝcr 11120  ℕ₀cn0 12493

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5263  ax-nul 5273  ax-pr 5399  ax-un 7723  ax-1cn 11179  ax-icn 11180  ax-addcl 11181  ax-addrcl 11182  ax-mulcl 11183  ax-mulrcl 11184  ax-i2m1 11189  ax-1ne0 11190  ax-rnegex 11192  ax-rrecex 11193  ax-cnre 11194

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-ral 3051  df-rex 3060  df-reu 3358  df-rab 3414  df-v 3459  df-sbc 3764  df-csb 3873  df-dif 3927  df-un 3929  df-in 3931  df-ss 3941  df-pss 3944  df-nul 4307  df-if 4499  df-pw 4575  df-sn 4600  df-pr 4602  df-op 4606  df-uni 4881  df-iun 4966  df-br 5117  df-opab 5179  df-mpt 5199  df-tr 5227  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6287  df-ord 6352  df-on 6353  df-lim 6354  df-suc 6355  df-iota 6480  df-fun 6529  df-fn 6530  df-f 6531  df-f1 6532  df-fo 6533  df-f1o 6534  df-fv 6535  df-ov 7402  df-om 7856  df-2nd 7983  df-frecs 8274  df-wrecs 8305  df-recs 8379  df-rdg 8418  df-nn 12233  df-n0 12494

This theorem is referenced by:  nn0ge0  12518  nn0nlt0  12519  nn0le0eq0  12521  nn0p1gt0  12522  elnnnn0c  12538  nn0addge1  12539  nn0addge2  12540  nn0sub  12543  ltsubnn0  12544  nn0negleid  12545  difgtsumgt  12546  nn0le2x  12547  nn0n0n1ge2b  12562  nn0ge2m1nn  12563  nn0nndivcl  12565  xnn0xr  12571  nn0nepnf  12574  xnn0nemnf  12577  elznn0nn  12594  nn0lt2  12648  nn0le2is012  12649  nn0ge0div  12654  nn01to3  12949  xnn0xaddcl  13243  xnn0lem1lt  13252  xnn0lenn0nn0  13253  xnn0xadd0  13255  nn0rp0  13461  xnn0xrge0  13512  nn0fz0  13631  elfz0fzfz0  13639  fz0fzelfz0  13640  fz0fzdiffz0  13643  fzctr  13646  difelfzle  13647  difelfznle  13648  fvffz0  13652  fzoun  13702  nn0p1elfzo  13708  elfzo0le  13709  fzonmapblen  13714  fzofzim  13715  elincfzoext  13728  elfzodifsumelfzo  13736  fzonn0p1  13747  fzonn0p1p1  13749  ssfzoulel  13765  ubmelm1fzo  13768  elfznelfzo  13777  fvinim0ffz  13791  subfzo0  13794  adddivflid  13824  divfl0  13830  fldivnn0le  13838  flltdivnn0lt  13839  quoremnn0ALT  13863  modmuladdnn0  13922  addmodid  13926  modifeq2int  13940  modfzo0difsn  13950  modsumfzodifsn  13951  addmodlteq  13953  ssnn0fi  13992  fsuppmapnn0fiub0  14000  suppssfz  14001  nn0sq11  14139  bernneq  14235  bernneq3  14237  facwordi  14295  faclbnd  14296  faclbnd3  14298  faclbnd5  14304  faclbnd6  14305  facubnd  14306  facavg  14307  bcval4  14313  bcval5  14324  bcpasc  14327  hashbnd  14342  hashnnn0genn0  14349  hashnemnf  14350  hashclb  14364  hashneq0  14370  hashsdom  14387  hashunsnggt  14400  fi1uzind  14513  ccat0  14581  ccat2s1fvw  14643  swrdnd0  14662  swrdsbslen  14669  swrdspsleq  14670  pfxnd0  14693  swrdswrdlem  14709  swrdswrd  14710  swrdccatin1  14730  pfxccatin12lem2  14736  pfxccatin12lem3  14737  pfxccat3  14739  swrdccat  14740  pfxccat3a  14743  swrdccat3blem  14744  repswswrd  14789  2cshw  14818  cshweqrep  14826  cshwcsh2id  14834  2swrd2eqwrdeq  14959  nn0sqeq1  15282  isercoll  15671  o1fsum  15816  geomulcvg  15879  rerisefaccl  16020  refallfaccl  16021  rprisefaccl  16026  dvdseq  16318  oddge22np1  16353  nn0ehalf  16382  nn0o1gt2  16385  nn0o  16387  nn0oddm1d2  16389  bitsfi  16441  bitsinv1  16446  gcdn0gt0  16522  nn0gcdid0  16525  absmulgcd  16553  nn0seqcvgd  16574  algcvgblem  16581  algcvga  16583  lcmgcdnn  16615  lcmfun  16649  lcmfass  16650  prmfac1  16724  prmndvdsfaclt  16729  nonsq  16763  hashgcdlem  16792  odzdvds  16800  iserodd  16840  pcprendvds  16845  pcdvdsb  16874  pcidlem  16877  dvdsprmpweqle  16891  difsqpwdvds  16892  pcfaclem  16903  prmunb  16919  ramtcl2  17016  ramubcl  17023  ram0  17027  ramub1lem1  17031  cshwshashlem2  17101  smndex1iidm  18864  sylow1lem1  19564  pgpssslw  19580  efgsfo  19705  efgred  19714  telgsums  19959  prmirredlem  21418  prmirred  21420  gsumbagdiaglem  21875  psrridm  21908  psdmul  22089  coe1tmmul2  22198  gsummoncoe1  22231  mp2pm2mplem4  22732  fvmptnn04ifb  22774  chfacfisf  22777  chfacfisfcpmat  22778  chfacffsupp  22779  chfacfscmul0  22781  chfacfpmmul0  22785  dyaddisj  25534  mdegle0  26019  deg1nn0clb  26032  deg1ge  26040  deg1tmle  26060  ply1divex  26079  plyco0  26134  coeeulem  26166  coeaddlem  26191  coe1termlem  26200  dgreq0  26208  dgrlt  26209  plydivex  26242  aannenlem1  26273  taylfvallem1  26301  tayl0  26306  radcnvlem1  26359  radcnvlem2  26360  dvradcnv  26367  leibpi  26888  log2tlbnd  26891  birthdaylem3  26899  zetacvg  26961  basellem2  27028  basellem3  27029  chpp1  27101  bcmono  27224  bcmax  27225  lgsdinn0  27292  2lgslem1c  27340  2sq2  27380  2sqreulem1  27393  2sqreultlem  27394  dchrisumlem1  27436  ostth2lem2  27581  nbusgrvtxm1  29290  upgrewlkle2  29518  pthdlem1  29680  crctcshwlkn0lem4  29727  crctcshwlkn0  29735  crctcsh  29738  wwlksm1edg  29795  wwlksnred  29806  wwlksnredwwlkn  29809  wwlksnredwwlkn0  29810  wwlksnextwrd  29811  wwlksnextfun  29812  wwlksnextinj  29813  wwlksnextproplem1  29823  wwlksnextproplem2  29824  wwlksnextproplem3  29825  clwlkclwwlklem2a1  29905  clwlkclwwlklem2a2  29906  clwlkclwwlklem2fv1  29908  clwlkclwwlklem2fv2  29909  clwlkclwwlklem2a4  29910  clwlkclwwlklem2a  29911  clwlkclwwlklem2  29913  clwlkclwwlk  29915  clwlkclwwlk2  29916  clwlkclwwlkf  29921  clwwisshclwwslem  29927  clwwlkel  29959  wwlksext2clwwlk  29970  clwlknf1oclwwlknlem1  29994  clwwlknonex2lem2  30021  eupth2lems  30151  eupth2  30152  eucrctshift  30156  numclwwlk7  30304  frgrreggt1  30306  frgrreg  30307  frgrogt3nreg  30310  friendship  30312  nn0xmulclb  32682  dpcl  32783  wrdt2ind  32848  hasheuni  34024  eulerpartlems  34300  hgt750lem  34604  0nn0m1nnn0  35056  derangen  35115  faclimlem1  35681  poimirlem28  37593  rrntotbnd  37781  sticksstones22  42103  factwoffsmonot  42177  gcdnn0id  42302  nn0addcom  42418  zaddcomlem  42419  nn0mulcom  42422  nacsfix  42660  eldioph2lem1  42708  irrapxlem4  42773  pell14qrgt0  42807  pell1qrgaplem  42821  pellqrexplicit  42825  rmxycomplete  42866  jm2.17a  42909  jm2.17b  42910  rmygeid  42913  jm2.22  42944  rmxdiophlem  42964  hbtlem5  43077  hbt  43079  fperiodmullem  45259  dvnxpaek  45901  stoweidlem17  45976  wallispilem3  46026  stirlinglem5  46037  stirlinglem7  46039  fourierdlem16  46082  fourierdlem21  46087  fourierdlem22  46088  fourierdlem83  46148  fourierdlem112  46177  elaa2lem  46192  etransclem23  46216  zm1nn  47259  nn0resubcl  47265  fz0addge0  47276  elfzlble  47277  subsubelfzo0  47283  2ffzoeq  47284  addmodne  47291  submodlt  47297  iccpartigtl  47355  lswn0  47376  sqrtpwpw2p  47470  fmtnodvds  47476  goldbachth  47479  odz2prm2pw  47495  flsqrt  47525  nn0e  47629  nn0sumltlt  48211  ply1mulgsumlem2  48249  nn0eo  48394  flnn0div2ge  48399  fllog2  48434  dignn0fr  48467  digexp  48473  dig2nn0  48477  0dig2nn0e  48478  dig2bits  48480  itcovalt2lem2lem1  48539