Theorem nn0re 12458

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℝcr 11074  ℕ₀cn0 12449

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-un 7714  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-i2m1 11143  ax-1ne0 11144  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-pred 6277  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-ov 7393  df-om 7846  df-2nd 7972  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8381  df-nn 12194  df-n0 12450

This theorem is referenced by:  nn0ge0  12474  nn0nlt0  12475  nn0le0eq0  12477  nn0p1gt0  12478  elnnnn0c  12494  nn0addge1  12495  nn0addge2  12496  nn0sub  12499  ltsubnn0  12500  nn0negleid  12501  difgtsumgt  12502  nn0le2x  12503  nn0n0n1ge2b  12518  nn0ge2m1nn  12519  nn0nndivcl  12521  xnn0xr  12527  nn0nepnf  12530  xnn0nemnf  12533  elznn0nn  12550  nn0lt2  12604  nn0le2is012  12605  nn0ge0div  12610  nn01to3  12907  xnn0xaddcl  13202  xnn0lem1lt  13211  xnn0lenn0nn0  13212  xnn0xadd0  13214  nn0rp0  13423  xnn0xrge0  13474  nn0fz0  13593  elfz0fzfz0  13601  fz0fzelfz0  13602  fz0fzdiffz0  13605  fzctr  13608  difelfzle  13609  difelfznle  13610  fvffz0  13614  fzoun  13664  nn0p1elfzo  13670  elfzo0le  13671  fzonmapblen  13676  fzofzim  13677  elincfzoext  13691  elfzodifsumelfzo  13699  fzonn0p1  13710  fzonn0p1p1  13712  ssfzoulel  13728  ubmelm1fzo  13731  elfznelfzo  13740  fvinim0ffz  13754  subfzo0  13757  adddivflid  13787  divfl0  13793  fldivnn0le  13801  flltdivnn0lt  13802  quoremnn0ALT  13826  modmuladdnn0  13887  addmodid  13891  modifeq2int  13905  modfzo0difsn  13915  modsumfzodifsn  13916  addmodlteq  13918  ssnn0fi  13957  fsuppmapnn0fiub0  13965  suppssfz  13966  nn0sq11  14104  bernneq  14201  bernneq3  14203  facwordi  14261  faclbnd  14262  faclbnd3  14264  faclbnd5  14270  faclbnd6  14271  facubnd  14272  facavg  14273  bcval4  14279  bcval5  14290  bcpasc  14293  hashbnd  14308  hashnnn0genn0  14315  hashnemnf  14316  hashclb  14330  hashneq0  14336  hashsdom  14353  hashunsnggt  14366  fi1uzind  14479  ccat0  14548  ccat2s1fvw  14610  swrdnd0  14629  swrdsbslen  14636  swrdspsleq  14637  pfxnd0  14660  swrdswrdlem  14676  swrdswrd  14677  swrdccatin1  14697  pfxccatin12lem2  14703  pfxccatin12lem3  14704  pfxccat3  14706  swrdccat  14707  pfxccat3a  14710  swrdccat3blem  14711  repswswrd  14756  2cshw  14785  cshweqrep  14793  cshwcsh2id  14801  2swrd2eqwrdeq  14926  nn0sqeq1  15249  nn0absid  15403  isercoll  15641  o1fsum  15786  geomulcvg  15849  rerisefaccl  15990  refallfaccl  15991  rprisefaccl  15996  dvdseq  16291  oddge22np1  16326  nn0ehalf  16355  nn0o1gt2  16358  nn0o  16360  nn0oddm1d2  16362  bitsfi  16414  bitsinv1  16419  gcdn0gt0  16495  nn0gcdid0  16498  absmulgcd  16526  nn0seqcvgd  16547  algcvgblem  16554  algcvga  16556  lcmgcdnn  16588  lcmfun  16622  lcmfass  16623  prmfac1  16697  prmndvdsfaclt  16702  nonsq  16736  hashgcdlem  16765  odzdvds  16773  iserodd  16813  pcprendvds  16818  pcdvdsb  16847  pcidlem  16850  dvdsprmpweqle  16864  difsqpwdvds  16865  pcfaclem  16876  prmunb  16892  ramtcl2  16989  ramubcl  16996  ram0  17000  ramub1lem1  17004  cshwshashlem2  17074  smndex1iidm  18835  sylow1lem1  19535  pgpssslw  19551  efgsfo  19676  efgred  19685  telgsums  19930  prmirredlem  21389  prmirred  21391  gsumbagdiaglem  21846  psrridm  21879  psdmul  22060  coe1tmmul2  22169  gsummoncoe1  22202  mp2pm2mplem4  22703  fvmptnn04ifb  22745  chfacfisf  22748  chfacfisfcpmat  22749  chfacffsupp  22750  chfacfscmul0  22752  chfacfpmmul0  22756  dyaddisj  25504  mdegle0  25989  deg1nn0clb  26002  deg1ge  26010  deg1tmle  26030  ply1divex  26049  plyco0  26104  coeeulem  26136  coeaddlem  26161  coe1termlem  26170  dgreq0  26178  dgrlt  26179  plydivex  26212  aannenlem1  26243  taylfvallem1  26271  tayl0  26276  radcnvlem1  26329  radcnvlem2  26330  dvradcnv  26337  leibpi  26859  log2tlbnd  26862  birthdaylem3  26870  zetacvg  26932  basellem2  26999  basellem3  27000  chpp1  27072  bcmono  27195  bcmax  27196  lgsdinn0  27263  2lgslem1c  27311  2sq2  27351  2sqreulem1  27364  2sqreultlem  27365  dchrisumlem1  27407  ostth2lem2  27552  nbusgrvtxm1  29313  upgrewlkle2  29541  pthdlem1  29703  crctcshwlkn0lem4  29750  crctcshwlkn0  29758  crctcsh  29761  wwlksm1edg  29818  wwlksnred  29829  wwlksnredwwlkn  29832  wwlksnredwwlkn0  29833  wwlksnextwrd  29834  wwlksnextfun  29835  wwlksnextinj  29836  wwlksnextproplem1  29846  wwlksnextproplem2  29847  wwlksnextproplem3  29848  clwlkclwwlklem2a1  29928  clwlkclwwlklem2a2  29929  clwlkclwwlklem2fv1  29931  clwlkclwwlklem2fv2  29932  clwlkclwwlklem2a4  29933  clwlkclwwlklem2a  29934  clwlkclwwlklem2  29936  clwlkclwwlk  29938  clwlkclwwlk2  29939  clwlkclwwlkf  29944  clwwisshclwwslem  29950  clwwlkel  29982  wwlksext2clwwlk  29993  clwlknf1oclwwlknlem1  30017  clwwlknonex2lem2  30044  eupth2lems  30174  eupth2  30175  eucrctshift  30179  numclwwlk7  30327  frgrreggt1  30329  frgrreg  30330  frgrogt3nreg  30333  friendship  30335  nn0xmulclb  32701  dpcl  32818  wrdt2ind  32882  hasheuni  34082  eulerpartlems  34358  hgt750lem  34649  0nn0m1nnn0  35107  derangen  35166  faclimlem1  35737  poimirlem28  37649  rrntotbnd  37837  sticksstones22  42163  gcdnn0id  42324  nn0addcom  42457  zaddcomlem  42458  nn0mulcom  42461  nacsfix  42707  eldioph2lem1  42755  irrapxlem4  42820  pell14qrgt0  42854  pell1qrgaplem  42868  pellqrexplicit  42872  rmxycomplete  42913  jm2.17a  42956  jm2.17b  42957  rmygeid  42960  jm2.22  42991  rmxdiophlem  43011  hbtlem5  43124  hbt  43126  fperiodmullem  45308  dvnxpaek  45947  stoweidlem17  46022  wallispilem3  46072  stirlinglem5  46083  stirlinglem7  46085  fourierdlem16  46128  fourierdlem21  46133  fourierdlem22  46134  fourierdlem83  46194  fourierdlem112  46223  elaa2lem  46238  etransclem23  46262  zm1nn  47307  nn0resubcl  47313  fz0addge0  47324  elfzlble  47325  subsubelfzo0  47331  2ffzoeq  47332  addmodne  47349  submodlt  47355  iccpartigtl  47428  lswn0  47449  sqrtpwpw2p  47543  fmtnodvds  47549  goldbachth  47552  odz2prm2pw  47568  flsqrt  47598  nn0e  47702  nn0sumltlt  48342  ply1mulgsumlem2  48380  nn0eo  48521  flnn0div2ge  48526  fllog2  48561  dignn0fr  48594  digexp  48600  dig2nn0  48604  0dig2nn0e  48605  dig2bits  48607  itcovalt2lem2lem1  48666