Theorem nn0re 12622

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  ℝcr 11206  ℕ₀cn0 12613

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5391  ax-un 7755  ax-1cn 11265  ax-icn 11266  ax-addcl 11267  ax-addrcl 11268  ax-mulcl 11269  ax-mulrcl 11270  ax-i2m1 11275  ax-1ne0 11276  ax-rnegex 11278  ax-rrecex 11279  ax-cnre 11280

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3848  df-ss 3897  df-pss 4013  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6307  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6497  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7427  df-om 7882  df-2nd 8006  df-frecs 8307  df-wrecs 8338  df-recs 8387  df-rdg 8426  df-nn 12343  df-n0 12614

This theorem is used by:  nn0ge0  12638  nn0nlt0  12639  nn0le0eq0  12641  nn0p1gt0  12642  elnnnn0c  12658  nn0addge1  12659  nn0addge2  12660  nn0sub  12663  ltsubnn0  12664  nn0negleid  12665  difgtsumgt  12666  nn0le2x  12667  nn0n0n1ge2b  12682  nn0ge2m1nn  12683  nn0nndivcl  12685  xnn0xr  12691  nn0nepnf  12694  xnn0nemnf  12697  elznn0nn  12714  0nn0m1nnn0  12760  nn0lt2  12769  nn0le2is012  12770  nn0ge0div  12775  nn01to3  13075  xnn0xaddcl  13372  xnn0lem1lt  13381  xnn0lenn0nn0  13382  xnn0xadd0  13384  nn0rp0  13593  xnn0xrge0  13644  nn0fz0  13766  elfz0fzfz0  13774  fz0fzelfz0  13775  fz0fzdiffz0  13778  difelfzle  13782  difelfznle  13783  fvffz0  13787  fzoun  13838  nn0p1elfzo  13844  elfzo0le  13845  fzonmapblen  13850  fzofzim  13851  elincfzoext  13865  elfzodifsumelfzo  13873  fzonn0p1  13884  fzonn0p1p1  13886  ssfzoulel  13902  ubmelm1fzo  13905  elfznelfzo  13915  fvinim0ffz  13931  subfzo0  13935  adddivflid  13965  divfl0  13971  fldivnn0le  13979  flltdivnn0lt  13980  quoremnn0ALT  14004  modmuladdnn0  14065  addmodid  14069  modifeq2int  14083  modfzo0difsn  14093  modsumfzodifsn  14094  addmodlteq  14096  ssnn0fi  14135  fsuppmapnn0fiub0  14143  suppssfz  14144  nn0sq11  14282  bernneq  14380  bernneq3  14382  facwordi  14440  faclbnd  14441  faclbnd3  14443  faclbnd5  14449  faclbnd6  14450  facubnd  14451  facavg  14452  bcval4  14458  bcval5  14469  bcpasc  14472  hashbnd  14487  hashnnn0genn0  14494  hashnemnf  14495  hashclb  14509  hashneq0  14515  hashsdom  14532  hashunsnggt  14545  fi1uzind  14659  ccat0  14728  ccat2s1fvw  14794  swrdnd0  14815  swrdsbslen  14822  swrdspsleq  14823  pfxnd0  14846  swrdswrdlem  14861  swrdswrd  14862  swrdccatin1  14882  pfxccatin12lem2  14888  pfxccatin12lem3  14889  pfxccat3  14891  swrdccat  14892  pfxccat3a  14895  swrdccat3blem  14896  repswswrd  14943  2cshw  14972  cshweqrep  14980  cshwcsh2id  14987  2swrd2eqwrdeq  15115  nn0sqeq1  15452  nn0absid  15606  isercoll  15844  o1fsum  15989  geomulcvg  16054  rerisefaccl  16193  refallfaccl  16194  rprisefaccl  16199  dvdseq  16493  oddge22np1  16528  nn0ehalf  16557  nn0o1gt2  16560  nn0o  16562  nn0oddm1d2  16564  bitsfi  16616  bitsinv1  16621  gcdn0gt0  16699  nn0gcdid0  16702  gcdnn0id  16709  absmulgcd  16731  nn0seqcvgd  16754  algcvgblem  16761  algcvga  16763  lcmgcdnn  16795  lcmfun  16829  lcmfass  16830  prmfac1  16905  prmndvdsfaclt  16910  nonsq  16944  hashgcdlem  16974  odzdvds  16982  iserodd  17022  pcprendvds  17027  pcdvdsb  17056  pcidlem  17059  dvdsprmpweqle  17073  difsqpwdvds  17074  pcfaclem  17085  prmunb  17101  ramtcl2  17198  ramubcl  17205  ram0  17209  ramub1lem1  17213  cshwshashlem2  17283  smndex1iidm  19106  sylow1lem1  19821  pgpssslw  19837  efgsfo  19962  efgred  19971  telgsums  20216  prmirredlem  21787  prmirred  21789  gsumbagdiaglem  22248  psrridm  22279  psdmul  22496  coe1tmmul2  22604  gsummoncoe1  22635  mp2pm2mplem4  23136  fvmptnn04ifb  23178  chfacfisf  23181  chfacfisfcpmat  23182  chfacffsupp  23183  chfacfscmul0  23185  chfacfpmmul0  23189  dyaddisj  25926  mdegle0  26404  deg1nn0clb  26417  deg1ge  26425  deg1tmle  26445  ply1divex  26464  plyco0  26519  coeeulem  26552  coeaddlem  26577  coe1termlem  26586  dgreq0  26593  dgrlt  26594  plydivex  26627  aannenlem1  26664  taylfvallem1  26693  tayl0  26698  radcnvlem1  26749  radcnvlem2  26750  dvradcnv  26757  leibpi  27279  log2tlbnd  27282  birthdaylem3  27290  zetacvg  27351  basellem2  27418  basellem3  27419  chpp1  27491  bcmono  27613  bcmax  27614  lgsdinn0  27681  2lgslem1c  27729  2sq2  27769  2sqreulem1  27782  2sqreultlem  27783  dchrisumlem1  27825  ostth2lem2  27970  nbusgrvtxm1  29969  upgrewlkle2  30196  pthdlem1  30361  crctcshwlkn0lem4  30411  crctcshwlkn0  30419  crctcsh  30422  wwlksm1edg  30479  wwlksnred  30490  wwlksnredwwlkn  30493  wwlksnredwwlkn0  30494  wwlksnextwrd  30495  wwlksnextfun  30496  wwlksnextinj  30497  wwlksnextproplem1  30507  wwlksnextproplem2  30508  wwlksnextproplem3  30509  clwlkclwwlklem2a1  30592  clwlkclwwlklem2a2  30593  clwlkclwwlklem2fv1  30595  clwlkclwwlklem2fv2  30596  clwlkclwwlklem2a4  30597  clwlkclwwlklem2a  30598  clwlkclwwlklem2  30600  clwlkclwwlk  30602  clwlkclwwlk2  30603  clwlkclwwlkf  30608  clwwisshclwwslem  30614  clwwlkel  30646  wwlksext2clwwlk  30657  clwlknf1oclwwlknlem1  30681  clwwlknonex2lem2  30708  eupth2lems  30848  eupth2  30849  eucrctshift  30853  numclwwlk7  31001  frgrreggt1  31003  frgrreg  31004  frgrogt3nreg  31007  friendship  31009  nn0mnfxrd  33393  nn0xmulclb  33413  dpcl  33507  wrdt2ind  33566  hasheuni  34767  eulerpartlems  35042  hgt750lem  35330  derangen  36055  faclimlem1  36632  poimirlem28  38703  rrntotbnd  38907  sticksstones22  43355  nn0addcom  43663  zaddcomlem  43664  nn0mulcom  43667  nacsfix  43860  eldioph2lem1  43908  irrapxlem4  43969  pell14qrgt0  44003  pell1qrgaplem  44017  pellqrexplicit  44021  rmxycomplete  44061  jm2.17a  44104  jm2.17b  44105  rmygeid  44108  jm2.22  44139  rmxdiophlem  44159  hbtlem5  44267  hbt  44269  fperiodmullem  46455  dvnxpaek  47088  stoweidlem17  47163  wallispilem3  47213  stirlinglem5  47224  stirlinglem7  47226  fourierdlem16  47269  fourierdlem21  47274  fourierdlem22  47275  fourierdlem83  47335  fourierdlem112  47364  elaa2lem  47379  etransclem23  47403  zm1nn  48508  nn0resubcl  48514  fz0addge0  48525  elfzlble  48526  subsubelfzo0  48533  2ffzoeq  48534  addmodne  48556  submodlt  48562  iccpartigtl  48641  lswn0  48662  sqrtpwpw2p  48759  fmtnodvds  48765  goldbachth  48768  odz2prm2pw  48784  flsqrt  48814  nn0e  48931  nn0sumltlt  49598  ply1mulgsumlem2  49635  nn0eo  49776  flnn0div2ge  49781  fllog2  49816  dignn0fr  49849  digexp  49855  dig2nn0  49859  0dig2nn0e  49860  dig2bits  49862  itcovalt2lem2lem1  49921