Theorem nn0re 12424

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℝcr 11039  ℕ₀cn0 12415

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 5245  ax-nul 5255  ax-pr 5381  ax-un 7692  ax-1cn 11098  ax-icn 11099  ax-addcl 11100  ax-addrcl 11101  ax-mulcl 11102  ax-mulrcl 11103  ax-i2m1 11108  ax-1ne0 11109  ax-rnegex 11111  ax-rrecex 11112  ax-cnre 11113

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 5529  df-eprel 5534  df-po 5542  df-so 5543  df-fr 5587  df-we 5589  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6269  df-ord 6330  df-on 6331  df-lim 6332  df-suc 6333  df-iota 6458  df-fun 6504  df-fn 6505  df-f 6506  df-f1 6507  df-fo 6508  df-f1o 6509  df-fv 6510  df-ov 7373  df-om 7821  df-2nd 7946  df-frecs 8235  df-wrecs 8266  df-recs 8315  df-rdg 8353  df-nn 12160  df-n0 12416

This theorem is referenced by:  nn0ge0  12440  nn0nlt0  12441  nn0le0eq0  12443  nn0p1gt0  12444  elnnnn0c  12460  nn0addge1  12461  nn0addge2  12462  nn0sub  12465  ltsubnn0  12466  nn0negleid  12467  difgtsumgt  12468  nn0le2x  12469  nn0n0n1ge2b  12484  nn0ge2m1nn  12485  nn0nndivcl  12487  xnn0xr  12493  nn0nepnf  12496  xnn0nemnf  12499  elznn0nn  12516  nn0lt2  12569  nn0le2is012  12570  nn0ge0div  12575  nn01to3  12868  xnn0xaddcl  13164  xnn0lem1lt  13173  xnn0lenn0nn0  13174  xnn0xadd0  13176  nn0rp0  13385  xnn0xrge0  13436  nn0fz0  13555  elfz0fzfz0  13563  fz0fzelfz0  13564  fz0fzdiffz0  13567  fzctr  13570  difelfzle  13571  difelfznle  13572  fvffz0  13576  fzoun  13626  nn0p1elfzo  13632  elfzo0le  13633  fzonmapblen  13638  fzofzim  13639  elincfzoext  13653  elfzodifsumelfzo  13661  fzonn0p1  13672  fzonn0p1p1  13674  ssfzoulel  13690  ubmelm1fzo  13693  elfznelfzo  13703  fvinim0ffz  13719  subfzo0  13722  adddivflid  13752  divfl0  13758  fldivnn0le  13766  flltdivnn0lt  13767  quoremnn0ALT  13791  modmuladdnn0  13852  addmodid  13856  modifeq2int  13870  modfzo0difsn  13880  modsumfzodifsn  13881  addmodlteq  13883  ssnn0fi  13922  fsuppmapnn0fiub0  13930  suppssfz  13931  nn0sq11  14069  bernneq  14166  bernneq3  14168  facwordi  14226  faclbnd  14227  faclbnd3  14229  faclbnd5  14235  faclbnd6  14236  facubnd  14237  facavg  14238  bcval4  14244  bcval5  14255  bcpasc  14258  hashbnd  14273  hashnnn0genn0  14280  hashnemnf  14281  hashclb  14295  hashneq0  14301  hashsdom  14318  hashunsnggt  14331  fi1uzind  14444  ccat0  14513  ccat2s1fvw  14576  swrdnd0  14595  swrdsbslen  14602  swrdspsleq  14603  pfxnd0  14626  swrdswrdlem  14641  swrdswrd  14642  swrdccatin1  14662  pfxccatin12lem2  14668  pfxccatin12lem3  14669  pfxccat3  14671  swrdccat  14672  pfxccat3a  14675  swrdccat3blem  14676  repswswrd  14721  2cshw  14750  cshweqrep  14758  cshwcsh2id  14765  2swrd2eqwrdeq  14890  nn0sqeq1  15213  nn0absid  15367  isercoll  15605  o1fsum  15750  geomulcvg  15813  rerisefaccl  15954  refallfaccl  15955  rprisefaccl  15960  dvdseq  16255  oddge22np1  16290  nn0ehalf  16319  nn0o1gt2  16322  nn0o  16324  nn0oddm1d2  16326  bitsfi  16378  bitsinv1  16383  gcdn0gt0  16459  nn0gcdid0  16462  absmulgcd  16490  nn0seqcvgd  16511  algcvgblem  16518  algcvga  16520  lcmgcdnn  16552  lcmfun  16586  lcmfass  16587  prmfac1  16661  prmndvdsfaclt  16666  nonsq  16700  hashgcdlem  16729  odzdvds  16737  iserodd  16777  pcprendvds  16782  pcdvdsb  16811  pcidlem  16814  dvdsprmpweqle  16828  difsqpwdvds  16829  pcfaclem  16840  prmunb  16856  ramtcl2  16953  ramubcl  16960  ram0  16964  ramub1lem1  16968  cshwshashlem2  17038  smndex1iidm  18840  sylow1lem1  19544  pgpssslw  19560  efgsfo  19685  efgred  19694  telgsums  19939  prmirredlem  21444  prmirred  21446  gsumbagdiaglem  21903  psrridm  21935  psdmul  22126  coe1tmmul2  22235  gsummoncoe1  22269  mp2pm2mplem4  22770  fvmptnn04ifb  22812  chfacfisf  22815  chfacfisfcpmat  22816  chfacffsupp  22817  chfacfscmul0  22819  chfacfpmmul0  22823  dyaddisj  25570  mdegle0  26055  deg1nn0clb  26068  deg1ge  26076  deg1tmle  26096  ply1divex  26115  plyco0  26170  coeeulem  26202  coeaddlem  26227  coe1termlem  26236  dgreq0  26244  dgrlt  26245  plydivex  26278  aannenlem1  26309  taylfvallem1  26337  tayl0  26342  radcnvlem1  26395  radcnvlem2  26396  dvradcnv  26403  leibpi  26925  log2tlbnd  26928  birthdaylem3  26936  zetacvg  26998  basellem2  27065  basellem3  27066  chpp1  27138  bcmono  27261  bcmax  27262  lgsdinn0  27329  2lgslem1c  27377  2sq2  27417  2sqreulem1  27430  2sqreultlem  27431  dchrisumlem1  27473  ostth2lem2  27618  nbusgrvtxm1  29470  upgrewlkle2  29698  pthdlem1  29857  crctcshwlkn0lem4  29904  crctcshwlkn0  29912  crctcsh  29915  wwlksm1edg  29972  wwlksnred  29983  wwlksnredwwlkn  29986  wwlksnredwwlkn0  29987  wwlksnextwrd  29988  wwlksnextfun  29989  wwlksnextinj  29990  wwlksnextproplem1  30000  wwlksnextproplem2  30001  wwlksnextproplem3  30002  clwlkclwwlklem2a1  30085  clwlkclwwlklem2a2  30086  clwlkclwwlklem2fv1  30088  clwlkclwwlklem2fv2  30089  clwlkclwwlklem2a4  30090  clwlkclwwlklem2a  30091  clwlkclwwlklem2  30093  clwlkclwwlk  30095  clwlkclwwlk2  30096  clwlkclwwlkf  30101  clwwisshclwwslem  30107  clwwlkel  30139  wwlksext2clwwlk  30150  clwlknf1oclwwlknlem1  30174  clwwlknonex2lem2  30201  eupth2lems  30331  eupth2  30332  eucrctshift  30336  numclwwlk7  30484  frgrreggt1  30486  frgrreg  30487  frgrogt3nreg  30490  friendship  30492  nn0mnfxrd  32848  nn0xmulclb  32868  dpcl  32989  wrdt2ind  33052  hasheuni  34269  eulerpartlems  34544  hgt750lem  34835  0nn0m1nnn0  35335  derangen  35394  faclimlem1  35965  poimirlem28  37928  rrntotbnd  38116  sticksstones22  42567  gcdnn0id  42728  nn0addcom  42861  zaddcomlem  42862  nn0mulcom  42865  nacsfix  43098  eldioph2lem1  43146  irrapxlem4  43211  pell14qrgt0  43245  pell1qrgaplem  43259  pellqrexplicit  43263  rmxycomplete  43303  jm2.17a  43346  jm2.17b  43347  rmygeid  43350  jm2.22  43381  rmxdiophlem  43401  hbtlem5  43514  hbt  43516  fperiodmullem  45694  dvnxpaek  46329  stoweidlem17  46404  wallispilem3  46454  stirlinglem5  46465  stirlinglem7  46467  fourierdlem16  46510  fourierdlem21  46515  fourierdlem22  46516  fourierdlem83  46576  fourierdlem112  46605  elaa2lem  46620  etransclem23  46644  zm1nn  47691  nn0resubcl  47697  fz0addge0  47708  elfzlble  47709  subsubelfzo0  47715  2ffzoeq  47716  addmodne  47733  submodlt  47739  iccpartigtl  47812  lswn0  47833  sqrtpwpw2p  47927  fmtnodvds  47933  goldbachth  47936  odz2prm2pw  47952  flsqrt  47982  nn0e  48086  nn0sumltlt  48739  ply1mulgsumlem2  48776  nn0eo  48917  flnn0div2ge  48922  fllog2  48957  dignn0fr  48990  digexp  48996  dig2nn0  49000  0dig2nn0e  49001  dig2bits  49003  itcovalt2lem2lem1  49062