Theorem nn0re 12422

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℝcr 11037  ℕ₀cn0 12413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379  ax-un 7690  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-i2m1 11106  ax-1ne0 11107  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-ov 7371  df-om 7819  df-2nd 7944  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-nn 12158  df-n0 12414

This theorem is referenced by:  nn0ge0  12438  nn0nlt0  12439  nn0le0eq0  12441  nn0p1gt0  12442  elnnnn0c  12458  nn0addge1  12459  nn0addge2  12460  nn0sub  12463  ltsubnn0  12464  nn0negleid  12465  difgtsumgt  12466  nn0le2x  12467  nn0n0n1ge2b  12482  nn0ge2m1nn  12483  nn0nndivcl  12485  xnn0xr  12491  nn0nepnf  12494  xnn0nemnf  12497  elznn0nn  12514  nn0lt2  12567  nn0le2is012  12568  nn0ge0div  12573  nn01to3  12866  xnn0xaddcl  13162  xnn0lem1lt  13171  xnn0lenn0nn0  13172  xnn0xadd0  13174  nn0rp0  13383  xnn0xrge0  13434  nn0fz0  13553  elfz0fzfz0  13561  fz0fzelfz0  13562  fz0fzdiffz0  13565  fzctr  13568  difelfzle  13569  difelfznle  13570  fvffz0  13574  fzoun  13624  nn0p1elfzo  13630  elfzo0le  13631  fzonmapblen  13636  fzofzim  13637  elincfzoext  13651  elfzodifsumelfzo  13659  fzonn0p1  13670  fzonn0p1p1  13672  ssfzoulel  13688  ubmelm1fzo  13691  elfznelfzo  13701  fvinim0ffz  13717  subfzo0  13720  adddivflid  13750  divfl0  13756  fldivnn0le  13764  flltdivnn0lt  13765  quoremnn0ALT  13789  modmuladdnn0  13850  addmodid  13854  modifeq2int  13868  modfzo0difsn  13878  modsumfzodifsn  13879  addmodlteq  13881  ssnn0fi  13920  fsuppmapnn0fiub0  13928  suppssfz  13929  nn0sq11  14067  bernneq  14164  bernneq3  14166  facwordi  14224  faclbnd  14225  faclbnd3  14227  faclbnd5  14233  faclbnd6  14234  facubnd  14235  facavg  14236  bcval4  14242  bcval5  14253  bcpasc  14256  hashbnd  14271  hashnnn0genn0  14278  hashnemnf  14279  hashclb  14293  hashneq0  14299  hashsdom  14316  hashunsnggt  14329  fi1uzind  14442  ccat0  14511  ccat2s1fvw  14574  swrdnd0  14593  swrdsbslen  14600  swrdspsleq  14601  pfxnd0  14624  swrdswrdlem  14639  swrdswrd  14640  swrdccatin1  14660  pfxccatin12lem2  14666  pfxccatin12lem3  14667  pfxccat3  14669  swrdccat  14670  pfxccat3a  14673  swrdccat3blem  14674  repswswrd  14719  2cshw  14748  cshweqrep  14756  cshwcsh2id  14763  2swrd2eqwrdeq  14888  nn0sqeq1  15211  nn0absid  15365  isercoll  15603  o1fsum  15748  geomulcvg  15811  rerisefaccl  15952  refallfaccl  15953  rprisefaccl  15958  dvdseq  16253  oddge22np1  16288  nn0ehalf  16317  nn0o1gt2  16320  nn0o  16322  nn0oddm1d2  16324  bitsfi  16376  bitsinv1  16381  gcdn0gt0  16457  nn0gcdid0  16460  absmulgcd  16488  nn0seqcvgd  16509  algcvgblem  16516  algcvga  16518  lcmgcdnn  16550  lcmfun  16584  lcmfass  16585  prmfac1  16659  prmndvdsfaclt  16664  nonsq  16698  hashgcdlem  16727  odzdvds  16735  iserodd  16775  pcprendvds  16780  pcdvdsb  16809  pcidlem  16812  dvdsprmpweqle  16826  difsqpwdvds  16827  pcfaclem  16838  prmunb  16854  ramtcl2  16951  ramubcl  16958  ram0  16962  ramub1lem1  16966  cshwshashlem2  17036  smndex1iidm  18838  sylow1lem1  19539  pgpssslw  19555  efgsfo  19680  efgred  19689  telgsums  19934  prmirredlem  21439  prmirred  21441  gsumbagdiaglem  21898  psrridm  21930  psdmul  22121  coe1tmmul2  22230  gsummoncoe1  22264  mp2pm2mplem4  22765  fvmptnn04ifb  22807  chfacfisf  22810  chfacfisfcpmat  22811  chfacffsupp  22812  chfacfscmul0  22814  chfacfpmmul0  22818  dyaddisj  25565  mdegle0  26050  deg1nn0clb  26063  deg1ge  26071  deg1tmle  26091  ply1divex  26110  plyco0  26165  coeeulem  26197  coeaddlem  26222  coe1termlem  26231  dgreq0  26239  dgrlt  26240  plydivex  26273  aannenlem1  26304  taylfvallem1  26332  tayl0  26337  radcnvlem1  26390  radcnvlem2  26391  dvradcnv  26398  leibpi  26920  log2tlbnd  26923  birthdaylem3  26931  zetacvg  26993  basellem2  27060  basellem3  27061  chpp1  27133  bcmono  27256  bcmax  27257  lgsdinn0  27324  2lgslem1c  27372  2sq2  27412  2sqreulem1  27425  2sqreultlem  27426  dchrisumlem1  27468  ostth2lem2  27613  nbusgrvtxm1  29464  upgrewlkle2  29692  pthdlem1  29851  crctcshwlkn0lem4  29898  crctcshwlkn0  29906  crctcsh  29909  wwlksm1edg  29966  wwlksnred  29977  wwlksnredwwlkn  29980  wwlksnredwwlkn0  29981  wwlksnextwrd  29982  wwlksnextfun  29983  wwlksnextinj  29984  wwlksnextproplem1  29994  wwlksnextproplem2  29995  wwlksnextproplem3  29996  clwlkclwwlklem2a1  30079  clwlkclwwlklem2a2  30080  clwlkclwwlklem2fv1  30082  clwlkclwwlklem2fv2  30083  clwlkclwwlklem2a4  30084  clwlkclwwlklem2a  30085  clwlkclwwlklem2  30087  clwlkclwwlk  30089  clwlkclwwlk2  30090  clwlkclwwlkf  30095  clwwisshclwwslem  30101  clwwlkel  30133  wwlksext2clwwlk  30144  clwlknf1oclwwlknlem1  30168  clwwlknonex2lem2  30195  eupth2lems  30325  eupth2  30326  eucrctshift  30330  numclwwlk7  30478  frgrreggt1  30480  frgrreg  30481  frgrogt3nreg  30484  friendship  30486  nn0mnfxrd  32842  nn0xmulclb  32862  dpcl  32983  wrdt2ind  33046  hasheuni  34263  eulerpartlems  34538  hgt750lem  34829  0nn0m1nnn0  35329  derangen  35388  faclimlem1  35959  poimirlem28  37899  rrntotbnd  38087  sticksstones22  42538  gcdnn0id  42699  nn0addcom  42832  zaddcomlem  42833  nn0mulcom  42836  nacsfix  43069  eldioph2lem1  43117  irrapxlem4  43182  pell14qrgt0  43216  pell1qrgaplem  43230  pellqrexplicit  43234  rmxycomplete  43274  jm2.17a  43317  jm2.17b  43318  rmygeid  43321  jm2.22  43352  rmxdiophlem  43372  hbtlem5  43485  hbt  43487  fperiodmullem  45665  dvnxpaek  46300  stoweidlem17  46375  wallispilem3  46425  stirlinglem5  46436  stirlinglem7  46438  fourierdlem16  46481  fourierdlem21  46486  fourierdlem22  46487  fourierdlem83  46547  fourierdlem112  46576  elaa2lem  46591  etransclem23  46615  zm1nn  47662  nn0resubcl  47668  fz0addge0  47679  elfzlble  47680  subsubelfzo0  47686  2ffzoeq  47687  addmodne  47704  submodlt  47710  iccpartigtl  47783  lswn0  47804  sqrtpwpw2p  47898  fmtnodvds  47904  goldbachth  47907  odz2prm2pw  47923  flsqrt  47953  nn0e  48057  nn0sumltlt  48710  ply1mulgsumlem2  48747  nn0eo  48888  flnn0div2ge  48893  fllog2  48928  dignn0fr  48961  digexp  48967  dig2nn0  48971  0dig2nn0e  48972  dig2bits  48974  itcovalt2lem2lem1  49033