Theorem nn0re 12512

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

Syntax hints:   → wi 4   ∈ wcel 2149  ℝcr 11098  ℕ₀cn0 12503

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pr 5405  ax-un 7733  ax-1cn 11157  ax-icn 11158  ax-addcl 11159  ax-addrcl 11160  ax-mulcl 11161  ax-mulrcl 11162  ax-i2m1 11167  ax-1ne0 11168  ax-rnegex 11170  ax-rrecex 11171  ax-cnre 11172

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-iun 4962  df-br 5114  df-opab 5178  df-mpt 5197  df-tr 5223  df-id 5557  df-eprel 5562  df-po 5570  df-so 5571  df-fr 5615  df-we 5617  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7414  df-om 7862  df-2nd 7986  df-frecs 8277  df-wrecs 8308  df-recs 8357  df-rdg 8396  df-nn 12233  df-n0 12504

This theorem is referenced by:  nn0ge0  12528  nn0nlt0  12529  nn0le0eq0  12531  nn0p1gt0  12532  elnnnn0c  12548  nn0addge1  12549  nn0addge2  12550  nn0sub  12553  ltsubnn0  12554  nn0negleid  12555  difgtsumgt  12556  nn0le2x  12557  nn0n0n1ge2b  12572  nn0ge2m1nn  12573  nn0nndivcl  12575  xnn0xr  12581  nn0nepnf  12584  xnn0nemnf  12587  elznn0nn  12604  nn0lt2  12658  nn0le2is012  12659  nn0ge0div  12664  nn01to3  12964  xnn0xaddcl  13260  xnn0lem1lt  13269  xnn0lenn0nn0  13270  xnn0xadd0  13272  nn0rp0  13481  xnn0xrge0  13532  nn0fz0  13652  elfz0fzfz0  13660  fz0fzelfz0  13661  fz0fzdiffz0  13664  fzctr  13667  difelfzle  13668  difelfznle  13669  fvffz0  13673  fzoun  13724  nn0p1elfzo  13730  elfzo0le  13731  fzonmapblen  13736  fzofzim  13737  elincfzoext  13751  elfzodifsumelfzo  13759  fzonn0p1  13770  fzonn0p1p1  13772  ssfzoulel  13788  ubmelm1fzo  13791  elfznelfzo  13801  fvinim0ffz  13817  subfzo0  13820  adddivflid  13850  divfl0  13856  fldivnn0le  13864  flltdivnn0lt  13865  quoremnn0ALT  13889  modmuladdnn0  13950  addmodid  13954  modifeq2int  13968  modfzo0difsn  13978  modsumfzodifsn  13979  addmodlteq  13981  ssnn0fi  14020  fsuppmapnn0fiub0  14028  suppssfz  14029  nn0sq11  14167  bernneq  14264  bernneq3  14266  facwordi  14324  faclbnd  14325  faclbnd3  14327  faclbnd5  14333  faclbnd6  14334  facubnd  14335  facavg  14336  bcval4  14342  bcval5  14353  bcpasc  14356  hashbnd  14371  hashnnn0genn0  14378  hashnemnf  14379  hashclb  14393  hashneq0  14399  hashsdom  14416  hashunsnggt  14429  fi1uzind  14543  ccat0  14612  ccat2s1fvw  14675  swrdnd0  14694  swrdsbslen  14701  swrdspsleq  14702  pfxnd0  14725  swrdswrdlem  14740  swrdswrd  14741  swrdccatin1  14761  pfxccatin12lem2  14767  pfxccatin12lem3  14768  pfxccat3  14770  swrdccat  14771  pfxccat3a  14774  swrdccat3blem  14775  repswswrd  14820  2cshw  14849  cshweqrep  14857  cshwcsh2id  14864  2swrd2eqwrdeq  14989  nn0sqeq1  15326  nn0absid  15480  isercoll  15718  o1fsum  15864  geomulcvg  15929  rerisefaccl  16070  refallfaccl  16071  rprisefaccl  16076  dvdseq  16371  oddge22np1  16406  nn0ehalf  16435  nn0o1gt2  16438  nn0o  16440  nn0oddm1d2  16442  bitsfi  16494  bitsinv1  16499  gcdn0gt0  16575  nn0gcdid0  16578  absmulgcd  16606  nn0seqcvgd  16627  algcvgblem  16634  algcvga  16636  lcmgcdnn  16668  lcmfun  16702  lcmfass  16703  prmfac1  16778  prmndvdsfaclt  16783  nonsq  16817  hashgcdlem  16846  odzdvds  16854  iserodd  16894  pcprendvds  16899  pcdvdsb  16928  pcidlem  16931  dvdsprmpweqle  16945  difsqpwdvds  16946  pcfaclem  16957  prmunb  16973  ramtcl2  17070  ramubcl  17077  ram0  17081  ramub1lem1  17085  cshwshashlem2  17155  smndex1iidm  18959  sylow1lem1  19667  pgpssslw  19683  efgsfo  19808  efgred  19817  telgsums  20062  prmirredlem  21590  prmirred  21592  gsumbagdiaglem  22049  psrridm  22080  psdmul  22297  coe1tmmul2  22405  gsummoncoe1  22436  mp2pm2mplem4  22934  fvmptnn04ifb  22976  chfacfisf  22979  chfacfisfcpmat  22980  chfacffsupp  22981  chfacfscmul0  22983  chfacfpmmul0  22987  dyaddisj  25723  mdegle0  26202  deg1nn0clb  26215  deg1ge  26223  deg1tmle  26243  ply1divex  26262  plyco0  26317  coeeulem  26349  coeaddlem  26374  coe1termlem  26383  dgreq0  26390  dgrlt  26391  plydivex  26426  aannenlem1  26457  taylfvallem1  26485  tayl0  26490  radcnvlem1  26541  radcnvlem2  26542  dvradcnv  26549  leibpi  27072  log2tlbnd  27075  birthdaylem3  27083  zetacvg  27144  basellem2  27211  basellem3  27212  chpp1  27284  bcmono  27406  bcmax  27407  lgsdinn0  27474  2lgslem1c  27522  2sq2  27562  2sqreulem1  27575  2sqreultlem  27576  dchrisumlem1  27618  ostth2lem2  27763  nbusgrvtxm1  29669  upgrewlkle2  29896  pthdlem1  30055  crctcshwlkn0lem4  30102  crctcshwlkn0  30110  crctcsh  30113  wwlksm1edg  30170  wwlksnred  30181  wwlksnredwwlkn  30184  wwlksnredwwlkn0  30185  wwlksnextwrd  30186  wwlksnextfun  30187  wwlksnextinj  30188  wwlksnextproplem1  30198  wwlksnextproplem2  30199  wwlksnextproplem3  30200  clwlkclwwlklem2a1  30283  clwlkclwwlklem2a2  30284  clwlkclwwlklem2fv1  30286  clwlkclwwlklem2fv2  30287  clwlkclwwlklem2a4  30288  clwlkclwwlklem2a  30289  clwlkclwwlklem2  30291  clwlkclwwlk  30293  clwlkclwwlk2  30294  clwlkclwwlkf  30299  clwwisshclwwslem  30305  clwwlkel  30337  wwlksext2clwwlk  30348  clwlknf1oclwwlknlem1  30372  clwwlknonex2lem2  30399  eupth2lems  30529  eupth2  30530  eucrctshift  30534  numclwwlk7  30682  frgrreggt1  30684  frgrreg  30685  frgrogt3nreg  30688  friendship  30690  nn0mnfxrd  33036  nn0xmulclb  33056  dpcl  33150  wrdt2ind  33213  hasheuni  34419  eulerpartlems  34694  hgt750lem  34982  0nn0m1nnn0  35502  derangen  35562  faclimlem1  36133  poimirlem28  38186  rrntotbnd  38374  sticksstones22  42824  gcdnn0id  42979  nn0addcom  43125  zaddcomlem  43126  nn0mulcom  43129  nacsfix  43334  eldioph2lem1  43382  irrapxlem4  43443  pell14qrgt0  43477  pell1qrgaplem  43491  pellqrexplicit  43495  rmxycomplete  43535  jm2.17a  43578  jm2.17b  43579  rmygeid  43582  jm2.22  43613  rmxdiophlem  43633  hbtlem5  43746  hbt  43748  fperiodmullem  45913  dvnxpaek  46547  stoweidlem17  46622  wallispilem3  46672  stirlinglem5  46683  stirlinglem7  46685  fourierdlem16  46728  fourierdlem21  46733  fourierdlem22  46734  fourierdlem83  46794  fourierdlem112  46823  elaa2lem  46838  etransclem23  46862  zm1nn  47927  nn0resubcl  47933  fz0addge0  47944  elfzlble  47945  subsubelfzo0  47952  2ffzoeq  47953  addmodne  47975  submodlt  47981  iccpartigtl  48060  lswn0  48081  sqrtpwpw2p  48178  fmtnodvds  48184  goldbachth  48187  odz2prm2pw  48203  flsqrt  48233  nn0e  48350  nn0sumltlt  49014  ply1mulgsumlem2  49051  nn0eo  49192  flnn0div2ge  49197  fllog2  49232  dignn0fr  49265  digexp  49271  dig2nn0  49275  0dig2nn0e  49276  dig2bits  49278  itcovalt2lem2lem1  49337