Theorem nn0re 12535

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℝcr 11154  ℕ₀cn0 12526

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-i2m1 11223  ax-1ne0 11224  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-om 7888  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-nn 12267  df-n0 12527

This theorem is referenced by:  nn0ge0  12551  nn0nlt0  12552  nn0le0eq0  12554  nn0p1gt0  12555  elnnnn0c  12571  nn0addge1  12572  nn0addge2  12573  nn0sub  12576  ltsubnn0  12577  nn0negleid  12578  difgtsumgt  12579  nn0le2x  12580  nn0n0n1ge2b  12595  nn0ge2m1nn  12596  nn0nndivcl  12598  xnn0xr  12604  nn0nepnf  12607  xnn0nemnf  12610  elznn0nn  12627  nn0lt2  12681  nn0le2is012  12682  nn0ge0div  12687  nn01to3  12983  xnn0xaddcl  13277  xnn0lem1lt  13286  xnn0lenn0nn0  13287  xnn0xadd0  13289  nn0rp0  13495  xnn0xrge0  13546  nn0fz0  13665  elfz0fzfz0  13673  fz0fzelfz0  13674  fz0fzdiffz0  13677  fzctr  13680  difelfzle  13681  difelfznle  13682  fvffz0  13686  fzoun  13736  nn0p1elfzo  13742  elfzo0le  13743  fzonmapblen  13748  fzofzim  13749  elincfzoext  13762  elfzodifsumelfzo  13770  fzonn0p1  13781  fzonn0p1p1  13783  ssfzoulel  13799  ubmelm1fzo  13802  elfznelfzo  13811  fvinim0ffz  13825  subfzo0  13828  adddivflid  13858  divfl0  13864  fldivnn0le  13872  flltdivnn0lt  13873  quoremnn0ALT  13897  modmuladdnn0  13956  addmodid  13960  modifeq2int  13974  modfzo0difsn  13984  modsumfzodifsn  13985  addmodlteq  13987  ssnn0fi  14026  fsuppmapnn0fiub0  14034  suppssfz  14035  nn0sq11  14172  bernneq  14268  bernneq3  14270  facwordi  14328  faclbnd  14329  faclbnd3  14331  faclbnd5  14337  faclbnd6  14338  facubnd  14339  facavg  14340  bcval4  14346  bcval5  14357  bcpasc  14360  hashbnd  14375  hashnnn0genn0  14382  hashnemnf  14383  hashclb  14397  hashneq0  14403  hashsdom  14420  hashunsnggt  14433  fi1uzind  14546  ccat0  14614  ccat2s1fvw  14676  swrdnd0  14695  swrdsbslen  14702  swrdspsleq  14703  pfxnd0  14726  swrdswrdlem  14742  swrdswrd  14743  swrdccatin1  14763  pfxccatin12lem2  14769  pfxccatin12lem3  14770  pfxccat3  14772  swrdccat  14773  pfxccat3a  14776  swrdccat3blem  14777  repswswrd  14822  2cshw  14851  cshweqrep  14859  cshwcsh2id  14867  2swrd2eqwrdeq  14992  nn0sqeq1  15315  isercoll  15704  o1fsum  15849  geomulcvg  15912  rerisefaccl  16053  refallfaccl  16054  rprisefaccl  16059  dvdseq  16351  oddge22np1  16386  nn0ehalf  16415  nn0o1gt2  16418  nn0o  16420  nn0oddm1d2  16422  bitsfi  16474  bitsinv1  16479  gcdn0gt0  16555  nn0gcdid0  16558  absmulgcd  16586  nn0seqcvgd  16607  algcvgblem  16614  algcvga  16616  lcmgcdnn  16648  lcmfun  16682  lcmfass  16683  prmfac1  16757  prmndvdsfaclt  16762  nonsq  16796  hashgcdlem  16825  odzdvds  16833  iserodd  16873  pcprendvds  16878  pcdvdsb  16907  pcidlem  16910  dvdsprmpweqle  16924  difsqpwdvds  16925  pcfaclem  16936  prmunb  16952  ramtcl2  17049  ramubcl  17056  ram0  17060  ramub1lem1  17064  cshwshashlem2  17134  smndex1iidm  18914  sylow1lem1  19616  pgpssslw  19632  efgsfo  19757  efgred  19766  telgsums  20011  prmirredlem  21483  prmirred  21485  gsumbagdiaglem  21950  psrridm  21983  psdmul  22170  coe1tmmul2  22279  gsummoncoe1  22312  mp2pm2mplem4  22815  fvmptnn04ifb  22857  chfacfisf  22860  chfacfisfcpmat  22861  chfacffsupp  22862  chfacfscmul0  22864  chfacfpmmul0  22868  dyaddisj  25631  mdegle0  26116  deg1nn0clb  26129  deg1ge  26137  deg1tmle  26157  ply1divex  26176  plyco0  26231  coeeulem  26263  coeaddlem  26288  coe1termlem  26297  dgreq0  26305  dgrlt  26306  plydivex  26339  aannenlem1  26370  taylfvallem1  26398  tayl0  26403  radcnvlem1  26456  radcnvlem2  26457  dvradcnv  26464  leibpi  26985  log2tlbnd  26988  birthdaylem3  26996  zetacvg  27058  basellem2  27125  basellem3  27126  chpp1  27198  bcmono  27321  bcmax  27322  lgsdinn0  27389  2lgslem1c  27437  2sq2  27477  2sqreulem1  27490  2sqreultlem  27491  dchrisumlem1  27533  ostth2lem2  27678  nbusgrvtxm1  29396  upgrewlkle2  29624  pthdlem1  29786  crctcshwlkn0lem4  29833  crctcshwlkn0  29841  crctcsh  29844  wwlksm1edg  29901  wwlksnred  29912  wwlksnredwwlkn  29915  wwlksnredwwlkn0  29916  wwlksnextwrd  29917  wwlksnextfun  29918  wwlksnextinj  29919  wwlksnextproplem1  29929  wwlksnextproplem2  29930  wwlksnextproplem3  29931  clwlkclwwlklem2a1  30011  clwlkclwwlklem2a2  30012  clwlkclwwlklem2fv1  30014  clwlkclwwlklem2fv2  30015  clwlkclwwlklem2a4  30016  clwlkclwwlklem2a  30017  clwlkclwwlklem2  30019  clwlkclwwlk  30021  clwlkclwwlk2  30022  clwlkclwwlkf  30027  clwwisshclwwslem  30033  clwwlkel  30065  wwlksext2clwwlk  30076  clwlknf1oclwwlknlem1  30100  clwwlknonex2lem2  30127  eupth2lems  30257  eupth2  30258  eucrctshift  30262  numclwwlk7  30410  frgrreggt1  30412  frgrreg  30413  frgrogt3nreg  30416  friendship  30418  nn0xmulclb  32775  dpcl  32873  wrdt2ind  32938  hasheuni  34086  eulerpartlems  34362  hgt750lem  34666  0nn0m1nnn0  35118  derangen  35177  faclimlem1  35743  poimirlem28  37655  rrntotbnd  37843  sticksstones22  42169  factwoffsmonot  42243  gcdnn0id  42364  nn0addcom  42480  zaddcomlem  42481  nn0mulcom  42484  nacsfix  42723  eldioph2lem1  42771  irrapxlem4  42836  pell14qrgt0  42870  pell1qrgaplem  42884  pellqrexplicit  42888  rmxycomplete  42929  jm2.17a  42972  jm2.17b  42973  rmygeid  42976  jm2.22  43007  rmxdiophlem  43027  hbtlem5  43140  hbt  43142  fperiodmullem  45315  dvnxpaek  45957  stoweidlem17  46032  wallispilem3  46082  stirlinglem5  46093  stirlinglem7  46095  fourierdlem16  46138  fourierdlem21  46143  fourierdlem22  46144  fourierdlem83  46204  fourierdlem112  46233  elaa2lem  46248  etransclem23  46272  zm1nn  47314  nn0resubcl  47320  fz0addge0  47331  elfzlble  47332  subsubelfzo0  47338  2ffzoeq  47339  addmodne  47346  submodlt  47352  iccpartigtl  47410  lswn0  47431  sqrtpwpw2p  47525  fmtnodvds  47531  goldbachth  47534  odz2prm2pw  47550  flsqrt  47580  nn0e  47684  nn0sumltlt  48266  ply1mulgsumlem2  48304  nn0eo  48449  flnn0div2ge  48454  fllog2  48489  dignn0fr  48522  digexp  48528  dig2nn0  48532  0dig2nn0e  48533  dig2bits  48535  itcovalt2lem2lem1  48594