Theorem nn0re 12510

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℝcr 11128  ℕ₀cn0 12501

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 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402  ax-un 7729  ax-1cn 11187  ax-icn 11188  ax-addcl 11189  ax-addrcl 11190  ax-mulcl 11191  ax-mulrcl 11192  ax-i2m1 11197  ax-1ne0 11198  ax-rnegex 11200  ax-rrecex 11201  ax-cnre 11202

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 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-iun 4969  df-br 5120  df-opab 5182  df-mpt 5202  df-tr 5230  df-id 5548  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-we 5608  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6290  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6484  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-ov 7408  df-om 7862  df-2nd 7989  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-nn 12241  df-n0 12502

This theorem is referenced by:  nn0ge0  12526  nn0nlt0  12527  nn0le0eq0  12529  nn0p1gt0  12530  elnnnn0c  12546  nn0addge1  12547  nn0addge2  12548  nn0sub  12551  ltsubnn0  12552  nn0negleid  12553  difgtsumgt  12554  nn0le2x  12555  nn0n0n1ge2b  12570  nn0ge2m1nn  12571  nn0nndivcl  12573  xnn0xr  12579  nn0nepnf  12582  xnn0nemnf  12585  elznn0nn  12602  nn0lt2  12656  nn0le2is012  12657  nn0ge0div  12662  nn01to3  12957  xnn0xaddcl  13251  xnn0lem1lt  13260  xnn0lenn0nn0  13261  xnn0xadd0  13263  nn0rp0  13472  xnn0xrge0  13523  nn0fz0  13642  elfz0fzfz0  13650  fz0fzelfz0  13651  fz0fzdiffz0  13654  fzctr  13657  difelfzle  13658  difelfznle  13659  fvffz0  13663  fzoun  13713  nn0p1elfzo  13719  elfzo0le  13720  fzonmapblen  13725  fzofzim  13726  elincfzoext  13739  elfzodifsumelfzo  13747  fzonn0p1  13758  fzonn0p1p1  13760  ssfzoulel  13776  ubmelm1fzo  13779  elfznelfzo  13788  fvinim0ffz  13802  subfzo0  13805  adddivflid  13835  divfl0  13841  fldivnn0le  13849  flltdivnn0lt  13850  quoremnn0ALT  13874  modmuladdnn0  13933  addmodid  13937  modifeq2int  13951  modfzo0difsn  13961  modsumfzodifsn  13962  addmodlteq  13964  ssnn0fi  14003  fsuppmapnn0fiub0  14011  suppssfz  14012  nn0sq11  14150  bernneq  14247  bernneq3  14249  facwordi  14307  faclbnd  14308  faclbnd3  14310  faclbnd5  14316  faclbnd6  14317  facubnd  14318  facavg  14319  bcval4  14325  bcval5  14336  bcpasc  14339  hashbnd  14354  hashnnn0genn0  14361  hashnemnf  14362  hashclb  14376  hashneq0  14382  hashsdom  14399  hashunsnggt  14412  fi1uzind  14525  ccat0  14594  ccat2s1fvw  14656  swrdnd0  14675  swrdsbslen  14682  swrdspsleq  14683  pfxnd0  14706  swrdswrdlem  14722  swrdswrd  14723  swrdccatin1  14743  pfxccatin12lem2  14749  pfxccatin12lem3  14750  pfxccat3  14752  swrdccat  14753  pfxccat3a  14756  swrdccat3blem  14757  repswswrd  14802  2cshw  14831  cshweqrep  14839  cshwcsh2id  14847  2swrd2eqwrdeq  14972  nn0sqeq1  15295  isercoll  15684  o1fsum  15829  geomulcvg  15892  rerisefaccl  16033  refallfaccl  16034  rprisefaccl  16039  dvdseq  16333  oddge22np1  16368  nn0ehalf  16397  nn0o1gt2  16400  nn0o  16402  nn0oddm1d2  16404  bitsfi  16456  bitsinv1  16461  gcdn0gt0  16537  nn0gcdid0  16540  absmulgcd  16568  nn0seqcvgd  16589  algcvgblem  16596  algcvga  16598  lcmgcdnn  16630  lcmfun  16664  lcmfass  16665  prmfac1  16739  prmndvdsfaclt  16744  nonsq  16778  hashgcdlem  16807  odzdvds  16815  iserodd  16855  pcprendvds  16860  pcdvdsb  16889  pcidlem  16892  dvdsprmpweqle  16906  difsqpwdvds  16907  pcfaclem  16918  prmunb  16934  ramtcl2  17031  ramubcl  17038  ram0  17042  ramub1lem1  17046  cshwshashlem2  17116  smndex1iidm  18879  sylow1lem1  19579  pgpssslw  19595  efgsfo  19720  efgred  19729  telgsums  19974  prmirredlem  21433  prmirred  21435  gsumbagdiaglem  21890  psrridm  21923  psdmul  22104  coe1tmmul2  22213  gsummoncoe1  22246  mp2pm2mplem4  22747  fvmptnn04ifb  22789  chfacfisf  22792  chfacfisfcpmat  22793  chfacffsupp  22794  chfacfscmul0  22796  chfacfpmmul0  22800  dyaddisj  25549  mdegle0  26034  deg1nn0clb  26047  deg1ge  26055  deg1tmle  26075  ply1divex  26094  plyco0  26149  coeeulem  26181  coeaddlem  26206  coe1termlem  26215  dgreq0  26223  dgrlt  26224  plydivex  26257  aannenlem1  26288  taylfvallem1  26316  tayl0  26321  radcnvlem1  26374  radcnvlem2  26375  dvradcnv  26382  leibpi  26904  log2tlbnd  26907  birthdaylem3  26915  zetacvg  26977  basellem2  27044  basellem3  27045  chpp1  27117  bcmono  27240  bcmax  27241  lgsdinn0  27308  2lgslem1c  27356  2sq2  27396  2sqreulem1  27409  2sqreultlem  27410  dchrisumlem1  27452  ostth2lem2  27597  nbusgrvtxm1  29358  upgrewlkle2  29586  pthdlem1  29748  crctcshwlkn0lem4  29795  crctcshwlkn0  29803  crctcsh  29806  wwlksm1edg  29863  wwlksnred  29874  wwlksnredwwlkn  29877  wwlksnredwwlkn0  29878  wwlksnextwrd  29879  wwlksnextfun  29880  wwlksnextinj  29881  wwlksnextproplem1  29891  wwlksnextproplem2  29892  wwlksnextproplem3  29893  clwlkclwwlklem2a1  29973  clwlkclwwlklem2a2  29974  clwlkclwwlklem2fv1  29976  clwlkclwwlklem2fv2  29977  clwlkclwwlklem2a4  29978  clwlkclwwlklem2a  29979  clwlkclwwlklem2  29981  clwlkclwwlk  29983  clwlkclwwlk2  29984  clwlkclwwlkf  29989  clwwisshclwwslem  29995  clwwlkel  30027  wwlksext2clwwlk  30038  clwlknf1oclwwlknlem1  30062  clwwlknonex2lem2  30089  eupth2lems  30219  eupth2  30220  eucrctshift  30224  numclwwlk7  30372  frgrreggt1  30374  frgrreg  30375  frgrogt3nreg  30378  friendship  30380  nn0xmulclb  32748  dpcl  32865  wrdt2ind  32929  hasheuni  34116  eulerpartlems  34392  hgt750lem  34683  0nn0m1nnn0  35135  derangen  35194  faclimlem1  35760  poimirlem28  37672  rrntotbnd  37860  sticksstones22  42181  factwoffsmonot  42255  gcdnn0id  42378  nn0addcom  42493  zaddcomlem  42494  nn0mulcom  42497  nacsfix  42735  eldioph2lem1  42783  irrapxlem4  42848  pell14qrgt0  42882  pell1qrgaplem  42896  pellqrexplicit  42900  rmxycomplete  42941  jm2.17a  42984  jm2.17b  42985  rmygeid  42988  jm2.22  43019  rmxdiophlem  43039  hbtlem5  43152  hbt  43154  fperiodmullem  45332  dvnxpaek  45971  stoweidlem17  46046  wallispilem3  46096  stirlinglem5  46107  stirlinglem7  46109  fourierdlem16  46152  fourierdlem21  46157  fourierdlem22  46158  fourierdlem83  46218  fourierdlem112  46247  elaa2lem  46262  etransclem23  46286  zm1nn  47331  nn0resubcl  47337  fz0addge0  47348  elfzlble  47349  subsubelfzo0  47355  2ffzoeq  47356  addmodne  47373  submodlt  47379  iccpartigtl  47437  lswn0  47458  sqrtpwpw2p  47552  fmtnodvds  47558  goldbachth  47561  odz2prm2pw  47577  flsqrt  47607  nn0e  47711  nn0sumltlt  48325  ply1mulgsumlem2  48363  nn0eo  48508  flnn0div2ge  48513  fllog2  48548  dignn0fr  48581  digexp  48587  dig2nn0  48591  0dig2nn0e  48592  dig2bits  48594  itcovalt2lem2lem1  48653