Theorem nn0re 12562

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℝcr 11183  ℕ₀cn0 12553

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447  ax-un 7770  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-i2m1 11252  ax-1ne0 11253  ax-rnegex 11255  ax-rrecex 11256  ax-cnre 11257

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-ov 7451  df-om 7904  df-2nd 8031  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-nn 12294  df-n0 12554

This theorem is referenced by:  nn0ge0  12578  nn0nlt0  12579  nn0le0eq0  12581  nn0p1gt0  12582  elnnnn0c  12598  nn0addge1  12599  nn0addge2  12600  nn0sub  12603  ltsubnn0  12604  nn0negleid  12605  difgtsumgt  12606  nn0n0n1ge2b  12621  nn0ge2m1nn  12622  nn0nndivcl  12624  xnn0xr  12630  nn0nepnf  12633  xnn0nemnf  12636  elznn0nn  12653  nn0lt2  12706  nn0le2is012  12707  nn0ge0div  12712  nn01to3  13006  xnn0xaddcl  13297  xnn0lem1lt  13306  xnn0lenn0nn0  13307  xnn0xadd0  13309  nn0rp0  13515  xnn0xrge0  13566  nn0fz0  13682  elfz0fzfz0  13690  fz0fzelfz0  13691  fz0fzdiffz0  13694  fzctr  13697  difelfzle  13698  difelfznle  13699  fvffz0  13703  fzoun  13753  nn0p1elfzo  13759  elfzo0le  13760  fzonmapblen  13762  fzofzim  13763  elincfzoext  13774  elfzodifsumelfzo  13782  fzonn0p1  13793  fzonn0p1p1  13795  ssfzoulel  13810  ubmelm1fzo  13813  elfznelfzo  13822  fvinim0ffz  13836  subfzo0  13839  adddivflid  13869  divfl0  13875  fldivnn0le  13883  flltdivnn0lt  13884  quoremnn0ALT  13908  modmuladdnn0  13966  addmodid  13970  modifeq2int  13984  modfzo0difsn  13994  modsumfzodifsn  13995  addmodlteq  13997  ssnn0fi  14036  fsuppmapnn0fiub0  14044  suppssfz  14045  nn0sq11  14182  bernneq  14278  bernneq3  14280  facwordi  14338  faclbnd  14339  faclbnd3  14341  faclbnd5  14347  faclbnd6  14348  facubnd  14349  facavg  14350  bcval4  14356  bcval5  14367  bcpasc  14370  hashbnd  14385  hashnnn0genn0  14392  hashnemnf  14393  hashclb  14407  hashneq0  14413  hashsdom  14430  hashunsnggt  14443  fi1uzind  14556  ccat0  14624  ccat2s1fvw  14686  swrdnd0  14705  swrdsbslen  14712  swrdspsleq  14713  pfxnd0  14736  swrdswrdlem  14752  swrdswrd  14753  swrdccatin1  14773  pfxccatin12lem2  14779  pfxccatin12lem3  14780  pfxccat3  14782  swrdccat  14783  pfxccat3a  14786  swrdccat3blem  14787  repswswrd  14832  2cshw  14861  cshweqrep  14869  cshwcsh2id  14877  2swrd2eqwrdeq  15002  nn0sqeq1  15325  isercoll  15716  o1fsum  15861  geomulcvg  15924  rerisefaccl  16065  refallfaccl  16066  rprisefaccl  16071  dvdseq  16362  oddge22np1  16397  nn0ehalf  16426  nn0o1gt2  16429  nn0o  16431  nn0oddm1d2  16433  bitsfi  16483  bitsinv1  16488  gcdn0gt0  16564  nn0gcdid0  16567  absmulgcd  16596  nn0seqcvgd  16617  algcvgblem  16624  algcvga  16626  lcmgcdnn  16658  lcmfun  16692  lcmfass  16693  prmfac1  16767  prmndvdsfaclt  16772  nonsq  16806  hashgcdlem  16835  odzdvds  16842  iserodd  16882  pcprendvds  16887  pcdvdsb  16916  pcidlem  16919  dvdsprmpweqle  16933  difsqpwdvds  16934  pcfaclem  16945  prmunb  16961  ramtcl2  17058  ramubcl  17065  ram0  17069  ramub1lem1  17073  cshwshashlem2  17144  smndex1iidm  18936  sylow1lem1  19640  pgpssslw  19656  efgsfo  19781  efgred  19790  telgsums  20035  prmirredlem  21506  prmirred  21508  gsumbagdiaglem  21973  psrridm  22006  psdmul  22193  coe1tmmul2  22300  gsummoncoe1  22333  mp2pm2mplem4  22836  fvmptnn04ifb  22878  chfacfisf  22881  chfacfisfcpmat  22882  chfacffsupp  22883  chfacfscmul0  22885  chfacfpmmul0  22889  dyaddisj  25650  mdegle0  26136  deg1nn0clb  26149  deg1ge  26157  deg1tmle  26177  ply1divex  26196  plyco0  26251  coeeulem  26283  coeaddlem  26308  coe1termlem  26317  dgreq0  26325  dgrlt  26326  plydivex  26357  aannenlem1  26388  taylfvallem1  26416  tayl0  26421  radcnvlem1  26474  radcnvlem2  26475  dvradcnv  26482  leibpi  27003  log2tlbnd  27006  birthdaylem3  27014  zetacvg  27076  basellem2  27143  basellem3  27144  chpp1  27216  bcmono  27339  bcmax  27340  lgsdinn0  27407  2lgslem1c  27455  2sq2  27495  2sqreulem1  27508  2sqreultlem  27509  dchrisumlem1  27551  ostth2lem2  27696  nbusgrvtxm1  29414  upgrewlkle2  29642  pthdlem1  29802  crctcshwlkn0lem4  29846  crctcshwlkn0  29854  crctcsh  29857  wwlksm1edg  29914  wwlksnred  29925  wwlksnredwwlkn  29928  wwlksnredwwlkn0  29929  wwlksnextwrd  29930  wwlksnextfun  29931  wwlksnextinj  29932  wwlksnextproplem1  29942  wwlksnextproplem2  29943  wwlksnextproplem3  29944  clwlkclwwlklem2a1  30024  clwlkclwwlklem2a2  30025  clwlkclwwlklem2fv1  30027  clwlkclwwlklem2fv2  30028  clwlkclwwlklem2a4  30029  clwlkclwwlklem2a  30030  clwlkclwwlklem2  30032  clwlkclwwlk  30034  clwlkclwwlk2  30035  clwlkclwwlkf  30040  clwwisshclwwslem  30046  clwwlkel  30078  wwlksext2clwwlk  30089  clwlknf1oclwwlknlem1  30113  clwwlknonex2lem2  30140  eupth2lems  30270  eupth2  30271  eucrctshift  30275  numclwwlk7  30423  frgrreggt1  30425  frgrreg  30426  frgrogt3nreg  30429  friendship  30431  nn0xmulclb  32778  dpcl  32855  wrdt2ind  32920  hasheuni  34049  eulerpartlems  34325  hgt750lem  34628  0nn0m1nnn0  35080  derangen  35140  faclimlem1  35705  poimirlem28  37608  rrntotbnd  37796  sticksstones22  42125  factwoffsmonot  42199  gcdnn0id  42316  nn0addcom  42426  zaddcomlem  42427  nn0mulcom  42430  nacsfix  42668  eldioph2lem1  42716  irrapxlem4  42781  pell14qrgt0  42815  pell1qrgaplem  42829  pellqrexplicit  42833  rmxycomplete  42874  jm2.17a  42917  jm2.17b  42918  rmygeid  42921  jm2.22  42952  rmxdiophlem  42972  hbtlem5  43085  hbt  43087  fperiodmullem  45218  dvnxpaek  45863  stoweidlem17  45938  wallispilem3  45988  stirlinglem5  45999  stirlinglem7  46001  fourierdlem16  46044  fourierdlem21  46049  fourierdlem22  46050  fourierdlem83  46110  fourierdlem112  46139  elaa2lem  46154  etransclem23  46178  zm1nn  47217  nn0resubcl  47223  fz0addge0  47234  elfzlble  47235  subsubelfzo0  47241  2ffzoeq  47242  iccpartigtl  47297  lswn0  47318  sqrtpwpw2p  47412  fmtnodvds  47418  goldbachth  47421  odz2prm2pw  47437  flsqrt  47467  nn0e  47571  nn0sumltlt  48075  ply1mulgsumlem2  48116  nn0eo  48262  flnn0div2ge  48267  fllog2  48302  dignn0fr  48335  digexp  48341  dig2nn0  48345  0dig2nn0e  48346  dig2bits  48348  itcovalt2lem2lem1  48407