Theorem nn0re 12437

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

Syntax hints:   → wi 4   ∈ wcel 2119  ℝcr 11028  ℕ₀cn0 12428

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pr 5362  ax-un 7678  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-i2m1 11097  ax-1ne0 11098  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-iun 4923  df-br 5073  df-opab 5135  df-mpt 5154  df-tr 5180  df-id 5513  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-we 5573  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-pred 6252  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-ov 7359  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-nn 12166  df-n0 12429

This theorem is referenced by:  nn0ge0  12453  nn0nlt0  12454  nn0le0eq0  12456  nn0p1gt0  12457  elnnnn0c  12473  nn0addge1  12474  nn0addge2  12475  nn0sub  12478  ltsubnn0  12479  nn0negleid  12480  difgtsumgt  12481  nn0le2x  12482  nn0n0n1ge2b  12497  nn0ge2m1nn  12498  nn0nndivcl  12500  xnn0xr  12506  nn0nepnf  12509  xnn0nemnf  12512  elznn0nn  12529  nn0lt2  12583  nn0le2is012  12584  nn0ge0div  12589  nn01to3  12882  xnn0xaddcl  13178  xnn0lem1lt  13187  xnn0lenn0nn0  13188  xnn0xadd0  13190  nn0rp0  13399  xnn0xrge0  13450  nn0fz0  13570  elfz0fzfz0  13578  fz0fzelfz0  13579  fz0fzdiffz0  13582  fzctr  13585  difelfzle  13586  difelfznle  13587  fvffz0  13591  fzoun  13642  nn0p1elfzo  13648  elfzo0le  13649  fzonmapblen  13654  fzofzim  13655  elincfzoext  13669  elfzodifsumelfzo  13677  fzonn0p1  13688  fzonn0p1p1  13690  ssfzoulel  13706  ubmelm1fzo  13709  elfznelfzo  13719  fvinim0ffz  13735  subfzo0  13738  adddivflid  13768  divfl0  13774  fldivnn0le  13782  flltdivnn0lt  13783  quoremnn0ALT  13807  modmuladdnn0  13868  addmodid  13872  modifeq2int  13886  modfzo0difsn  13896  modsumfzodifsn  13897  addmodlteq  13899  ssnn0fi  13938  fsuppmapnn0fiub0  13946  suppssfz  13947  nn0sq11  14085  bernneq  14182  bernneq3  14184  facwordi  14242  faclbnd  14243  faclbnd3  14245  faclbnd5  14251  faclbnd6  14252  facubnd  14253  facavg  14254  bcval4  14260  bcval5  14271  bcpasc  14274  hashbnd  14289  hashnnn0genn0  14296  hashnemnf  14297  hashclb  14311  hashneq0  14317  hashsdom  14334  hashunsnggt  14347  fi1uzind  14460  ccat0  14529  ccat2s1fvw  14592  swrdnd0  14611  swrdsbslen  14618  swrdspsleq  14619  pfxnd0  14642  swrdswrdlem  14657  swrdswrd  14658  swrdccatin1  14678  pfxccatin12lem2  14684  pfxccatin12lem3  14685  pfxccat3  14687  swrdccat  14688  pfxccat3a  14691  swrdccat3blem  14692  repswswrd  14737  2cshw  14766  cshweqrep  14774  cshwcsh2id  14781  2swrd2eqwrdeq  14906  nn0sqeq1  15229  nn0absid  15383  isercoll  15621  o1fsum  15767  geomulcvg  15832  rerisefaccl  15973  refallfaccl  15974  rprisefaccl  15979  dvdseq  16274  oddge22np1  16309  nn0ehalf  16338  nn0o1gt2  16341  nn0o  16343  nn0oddm1d2  16345  bitsfi  16397  bitsinv1  16402  gcdn0gt0  16478  nn0gcdid0  16481  absmulgcd  16509  nn0seqcvgd  16530  algcvgblem  16537  algcvga  16539  lcmgcdnn  16571  lcmfun  16605  lcmfass  16606  prmfac1  16681  prmndvdsfaclt  16686  nonsq  16720  hashgcdlem  16749  odzdvds  16757  iserodd  16797  pcprendvds  16802  pcdvdsb  16831  pcidlem  16834  dvdsprmpweqle  16848  difsqpwdvds  16849  pcfaclem  16860  prmunb  16876  ramtcl2  16973  ramubcl  16980  ram0  16984  ramub1lem1  16988  cshwshashlem2  17058  smndex1iidm  18860  sylow1lem1  19564  pgpssslw  19580  efgsfo  19705  efgred  19714  telgsums  19959  prmirredlem  21447  prmirred  21449  gsumbagdiaglem  21906  psrridm  21937  psdmul  22154  coe1tmmul2  22262  gsummoncoe1  22294  mp2pm2mplem4  22792  fvmptnn04ifb  22834  chfacfisf  22837  chfacfisfcpmat  22838  chfacffsupp  22839  chfacfscmul0  22841  chfacfpmmul0  22845  dyaddisj  25581  mdegle0  26060  deg1nn0clb  26073  deg1ge  26081  deg1tmle  26101  ply1divex  26120  plyco0  26175  coeeulem  26207  coeaddlem  26232  coe1termlem  26241  dgreq0  26248  dgrlt  26249  plydivex  26281  aannenlem1  26312  taylfvallem1  26340  tayl0  26345  radcnvlem1  26396  radcnvlem2  26397  dvradcnv  26404  leibpi  26924  log2tlbnd  26927  birthdaylem3  26935  zetacvg  26996  basellem2  27063  basellem3  27064  chpp1  27136  bcmono  27258  bcmax  27259  lgsdinn0  27326  2lgslem1c  27374  2sq2  27414  2sqreulem1  27427  2sqreultlem  27428  dchrisumlem1  27470  ostth2lem2  27615  nbusgrvtxm1  29466  upgrewlkle2  29693  pthdlem1  29852  crctcshwlkn0lem4  29899  crctcshwlkn0  29907  crctcsh  29910  wwlksm1edg  29967  wwlksnred  29978  wwlksnredwwlkn  29981  wwlksnredwwlkn0  29982  wwlksnextwrd  29983  wwlksnextfun  29984  wwlksnextinj  29985  wwlksnextproplem1  29995  wwlksnextproplem2  29996  wwlksnextproplem3  29997  clwlkclwwlklem2a1  30080  clwlkclwwlklem2a2  30081  clwlkclwwlklem2fv1  30083  clwlkclwwlklem2fv2  30084  clwlkclwwlklem2a4  30085  clwlkclwwlklem2a  30086  clwlkclwwlklem2  30088  clwlkclwwlk  30090  clwlkclwwlk2  30091  clwlkclwwlkf  30096  clwwisshclwwslem  30102  clwwlkel  30134  wwlksext2clwwlk  30145  clwlknf1oclwwlknlem1  30169  clwwlknonex2lem2  30196  eupth2lems  30326  eupth2  30327  eucrctshift  30331  numclwwlk7  30479  frgrreggt1  30481  frgrreg  30482  frgrogt3nreg  30485  friendship  30487  nn0mnfxrd  32843  nn0xmulclb  32863  dpcl  32969  wrdt2ind  33032  hasheuni  34269  eulerpartlems  34544  hgt750lem  34835  0nn0m1nnn0  35341  derangen  35400  faclimlem1  35971  poimirlem28  38015  rrntotbnd  38203  sticksstones22  42653  gcdnn0id  42806  nn0addcom  42952  zaddcomlem  42953  nn0mulcom  42956  nacsfix  43161  eldioph2lem1  43209  irrapxlem4  43270  pell14qrgt0  43304  pell1qrgaplem  43318  pellqrexplicit  43322  rmxycomplete  43362  jm2.17a  43405  jm2.17b  43406  rmygeid  43409  jm2.22  43440  rmxdiophlem  43460  hbtlem5  43573  hbt  43575  fperiodmullem  45751  dvnxpaek  46385  stoweidlem17  46460  wallispilem3  46510  stirlinglem5  46521  stirlinglem7  46523  fourierdlem16  46566  fourierdlem21  46571  fourierdlem22  46572  fourierdlem83  46632  fourierdlem112  46661  elaa2lem  46676  etransclem23  46700  zm1nn  47765  nn0resubcl  47771  fz0addge0  47782  elfzlble  47783  subsubelfzo0  47790  2ffzoeq  47791  addmodne  47813  submodlt  47819  iccpartigtl  47898  lswn0  47919  sqrtpwpw2p  48016  fmtnodvds  48022  goldbachth  48025  odz2prm2pw  48041  flsqrt  48071  nn0e  48188  nn0sumltlt  48841  ply1mulgsumlem2  48878  nn0eo  49019  flnn0div2ge  49024  fllog2  49059  dignn0fr  49092  digexp  49098  dig2nn0  49102  0dig2nn0e  49103  dig2bits  49105  itcovalt2lem2lem1  49164