Theorem nn0re 12451

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℝcr 11067  ℕ₀cn0 12442

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 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-un 7711  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-i2m1 11136  ax-1ne0 11137  ax-rnegex 11139  ax-rrecex 11140  ax-cnre 11141

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-ov 7390  df-om 7843  df-2nd 7969  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-nn 12187  df-n0 12443

This theorem is referenced by:  nn0ge0  12467  nn0nlt0  12468  nn0le0eq0  12470  nn0p1gt0  12471  elnnnn0c  12487  nn0addge1  12488  nn0addge2  12489  nn0sub  12492  ltsubnn0  12493  nn0negleid  12494  difgtsumgt  12495  nn0le2x  12496  nn0n0n1ge2b  12511  nn0ge2m1nn  12512  nn0nndivcl  12514  xnn0xr  12520  nn0nepnf  12523  xnn0nemnf  12526  elznn0nn  12543  nn0lt2  12597  nn0le2is012  12598  nn0ge0div  12603  nn01to3  12900  xnn0xaddcl  13195  xnn0lem1lt  13204  xnn0lenn0nn0  13205  xnn0xadd0  13207  nn0rp0  13416  xnn0xrge0  13467  nn0fz0  13586  elfz0fzfz0  13594  fz0fzelfz0  13595  fz0fzdiffz0  13598  fzctr  13601  difelfzle  13602  difelfznle  13603  fvffz0  13607  fzoun  13657  nn0p1elfzo  13663  elfzo0le  13664  fzonmapblen  13669  fzofzim  13670  elincfzoext  13684  elfzodifsumelfzo  13692  fzonn0p1  13703  fzonn0p1p1  13705  ssfzoulel  13721  ubmelm1fzo  13724  elfznelfzo  13733  fvinim0ffz  13747  subfzo0  13750  adddivflid  13780  divfl0  13786  fldivnn0le  13794  flltdivnn0lt  13795  quoremnn0ALT  13819  modmuladdnn0  13880  addmodid  13884  modifeq2int  13898  modfzo0difsn  13908  modsumfzodifsn  13909  addmodlteq  13911  ssnn0fi  13950  fsuppmapnn0fiub0  13958  suppssfz  13959  nn0sq11  14097  bernneq  14194  bernneq3  14196  facwordi  14254  faclbnd  14255  faclbnd3  14257  faclbnd5  14263  faclbnd6  14264  facubnd  14265  facavg  14266  bcval4  14272  bcval5  14283  bcpasc  14286  hashbnd  14301  hashnnn0genn0  14308  hashnemnf  14309  hashclb  14323  hashneq0  14329  hashsdom  14346  hashunsnggt  14359  fi1uzind  14472  ccat0  14541  ccat2s1fvw  14603  swrdnd0  14622  swrdsbslen  14629  swrdspsleq  14630  pfxnd0  14653  swrdswrdlem  14669  swrdswrd  14670  swrdccatin1  14690  pfxccatin12lem2  14696  pfxccatin12lem3  14697  pfxccat3  14699  swrdccat  14700  pfxccat3a  14703  swrdccat3blem  14704  repswswrd  14749  2cshw  14778  cshweqrep  14786  cshwcsh2id  14794  2swrd2eqwrdeq  14919  nn0sqeq1  15242  nn0absid  15396  isercoll  15634  o1fsum  15779  geomulcvg  15842  rerisefaccl  15983  refallfaccl  15984  rprisefaccl  15989  dvdseq  16284  oddge22np1  16319  nn0ehalf  16348  nn0o1gt2  16351  nn0o  16353  nn0oddm1d2  16355  bitsfi  16407  bitsinv1  16412  gcdn0gt0  16488  nn0gcdid0  16491  absmulgcd  16519  nn0seqcvgd  16540  algcvgblem  16547  algcvga  16549  lcmgcdnn  16581  lcmfun  16615  lcmfass  16616  prmfac1  16690  prmndvdsfaclt  16695  nonsq  16729  hashgcdlem  16758  odzdvds  16766  iserodd  16806  pcprendvds  16811  pcdvdsb  16840  pcidlem  16843  dvdsprmpweqle  16857  difsqpwdvds  16858  pcfaclem  16869  prmunb  16885  ramtcl2  16982  ramubcl  16989  ram0  16993  ramub1lem1  16997  cshwshashlem2  17067  smndex1iidm  18828  sylow1lem1  19528  pgpssslw  19544  efgsfo  19669  efgred  19678  telgsums  19923  prmirredlem  21382  prmirred  21384  gsumbagdiaglem  21839  psrridm  21872  psdmul  22053  coe1tmmul2  22162  gsummoncoe1  22195  mp2pm2mplem4  22696  fvmptnn04ifb  22738  chfacfisf  22741  chfacfisfcpmat  22742  chfacffsupp  22743  chfacfscmul0  22745  chfacfpmmul0  22749  dyaddisj  25497  mdegle0  25982  deg1nn0clb  25995  deg1ge  26003  deg1tmle  26023  ply1divex  26042  plyco0  26097  coeeulem  26129  coeaddlem  26154  coe1termlem  26163  dgreq0  26171  dgrlt  26172  plydivex  26205  aannenlem1  26236  taylfvallem1  26264  tayl0  26269  radcnvlem1  26322  radcnvlem2  26323  dvradcnv  26330  leibpi  26852  log2tlbnd  26855  birthdaylem3  26863  zetacvg  26925  basellem2  26992  basellem3  26993  chpp1  27065  bcmono  27188  bcmax  27189  lgsdinn0  27256  2lgslem1c  27304  2sq2  27344  2sqreulem1  27357  2sqreultlem  27358  dchrisumlem1  27400  ostth2lem2  27545  nbusgrvtxm1  29306  upgrewlkle2  29534  pthdlem1  29696  crctcshwlkn0lem4  29743  crctcshwlkn0  29751  crctcsh  29754  wwlksm1edg  29811  wwlksnred  29822  wwlksnredwwlkn  29825  wwlksnredwwlkn0  29826  wwlksnextwrd  29827  wwlksnextfun  29828  wwlksnextinj  29829  wwlksnextproplem1  29839  wwlksnextproplem2  29840  wwlksnextproplem3  29841  clwlkclwwlklem2a1  29921  clwlkclwwlklem2a2  29922  clwlkclwwlklem2fv1  29924  clwlkclwwlklem2fv2  29925  clwlkclwwlklem2a4  29926  clwlkclwwlklem2a  29927  clwlkclwwlklem2  29929  clwlkclwwlk  29931  clwlkclwwlk2  29932  clwlkclwwlkf  29937  clwwisshclwwslem  29943  clwwlkel  29975  wwlksext2clwwlk  29986  clwlknf1oclwwlknlem1  30010  clwwlknonex2lem2  30037  eupth2lems  30167  eupth2  30168  eucrctshift  30172  numclwwlk7  30320  frgrreggt1  30322  frgrreg  30323  frgrogt3nreg  30326  friendship  30328  nn0xmulclb  32694  dpcl  32811  wrdt2ind  32875  hasheuni  34075  eulerpartlems  34351  hgt750lem  34642  0nn0m1nnn0  35100  derangen  35159  faclimlem1  35730  poimirlem28  37642  rrntotbnd  37830  sticksstones22  42156  gcdnn0id  42317  nn0addcom  42450  zaddcomlem  42451  nn0mulcom  42454  nacsfix  42700  eldioph2lem1  42748  irrapxlem4  42813  pell14qrgt0  42847  pell1qrgaplem  42861  pellqrexplicit  42865  rmxycomplete  42906  jm2.17a  42949  jm2.17b  42950  rmygeid  42953  jm2.22  42984  rmxdiophlem  43004  hbtlem5  43117  hbt  43119  fperiodmullem  45301  dvnxpaek  45940  stoweidlem17  46015  wallispilem3  46065  stirlinglem5  46076  stirlinglem7  46078  fourierdlem16  46121  fourierdlem21  46126  fourierdlem22  46127  fourierdlem83  46187  fourierdlem112  46216  elaa2lem  46231  etransclem23  46255  zm1nn  47303  nn0resubcl  47309  fz0addge0  47320  elfzlble  47321  subsubelfzo0  47327  2ffzoeq  47328  addmodne  47345  submodlt  47351  iccpartigtl  47424  lswn0  47445  sqrtpwpw2p  47539  fmtnodvds  47545  goldbachth  47548  odz2prm2pw  47564  flsqrt  47594  nn0e  47698  nn0sumltlt  48338  ply1mulgsumlem2  48376  nn0eo  48517  flnn0div2ge  48522  fllog2  48557  dignn0fr  48590  digexp  48596  dig2nn0  48600  0dig2nn0e  48601  dig2bits  48603  itcovalt2lem2lem1  48662