Theorem nn0re 12393

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℝcr 11008  ℕ₀cn0 12384

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371  ax-un 7671  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-addrcl 11070  ax-mulcl 11071  ax-mulrcl 11072  ax-i2m1 11077  ax-1ne0 11078  ax-rnegex 11080  ax-rrecex 11081  ax-cnre 11082

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 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-iun 4943  df-br 5093  df-opab 5155  df-mpt 5174  df-tr 5200  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-pred 6249  df-ord 6310  df-on 6311  df-lim 6312  df-suc 6313  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-ov 7352  df-om 7800  df-2nd 7925  df-frecs 8214  df-wrecs 8245  df-recs 8294  df-rdg 8332  df-nn 12129  df-n0 12385

This theorem is referenced by:  nn0ge0  12409  nn0nlt0  12410  nn0le0eq0  12412  nn0p1gt0  12413  elnnnn0c  12429  nn0addge1  12430  nn0addge2  12431  nn0sub  12434  ltsubnn0  12435  nn0negleid  12436  difgtsumgt  12437  nn0le2x  12438  nn0n0n1ge2b  12453  nn0ge2m1nn  12454  nn0nndivcl  12456  xnn0xr  12462  nn0nepnf  12465  xnn0nemnf  12468  elznn0nn  12485  nn0lt2  12539  nn0le2is012  12540  nn0ge0div  12545  nn01to3  12842  xnn0xaddcl  13137  xnn0lem1lt  13146  xnn0lenn0nn0  13147  xnn0xadd0  13149  nn0rp0  13358  xnn0xrge0  13409  nn0fz0  13528  elfz0fzfz0  13536  fz0fzelfz0  13537  fz0fzdiffz0  13540  fzctr  13543  difelfzle  13544  difelfznle  13545  fvffz0  13549  fzoun  13599  nn0p1elfzo  13605  elfzo0le  13606  fzonmapblen  13611  fzofzim  13612  elincfzoext  13626  elfzodifsumelfzo  13634  fzonn0p1  13645  fzonn0p1p1  13647  ssfzoulel  13663  ubmelm1fzo  13666  elfznelfzo  13675  fvinim0ffz  13689  subfzo0  13692  adddivflid  13722  divfl0  13728  fldivnn0le  13736  flltdivnn0lt  13737  quoremnn0ALT  13761  modmuladdnn0  13822  addmodid  13826  modifeq2int  13840  modfzo0difsn  13850  modsumfzodifsn  13851  addmodlteq  13853  ssnn0fi  13892  fsuppmapnn0fiub0  13900  suppssfz  13901  nn0sq11  14039  bernneq  14136  bernneq3  14138  facwordi  14196  faclbnd  14197  faclbnd3  14199  faclbnd5  14205  faclbnd6  14206  facubnd  14207  facavg  14208  bcval4  14214  bcval5  14225  bcpasc  14228  hashbnd  14243  hashnnn0genn0  14250  hashnemnf  14251  hashclb  14265  hashneq0  14271  hashsdom  14288  hashunsnggt  14301  fi1uzind  14414  ccat0  14483  ccat2s1fvw  14545  swrdnd0  14564  swrdsbslen  14571  swrdspsleq  14572  pfxnd0  14595  swrdswrdlem  14610  swrdswrd  14611  swrdccatin1  14631  pfxccatin12lem2  14637  pfxccatin12lem3  14638  pfxccat3  14640  swrdccat  14641  pfxccat3a  14644  swrdccat3blem  14645  repswswrd  14690  2cshw  14719  cshweqrep  14727  cshwcsh2id  14735  2swrd2eqwrdeq  14860  nn0sqeq1  15183  nn0absid  15337  isercoll  15575  o1fsum  15720  geomulcvg  15783  rerisefaccl  15924  refallfaccl  15925  rprisefaccl  15930  dvdseq  16225  oddge22np1  16260  nn0ehalf  16289  nn0o1gt2  16292  nn0o  16294  nn0oddm1d2  16296  bitsfi  16348  bitsinv1  16353  gcdn0gt0  16429  nn0gcdid0  16432  absmulgcd  16460  nn0seqcvgd  16481  algcvgblem  16488  algcvga  16490  lcmgcdnn  16522  lcmfun  16556  lcmfass  16557  prmfac1  16631  prmndvdsfaclt  16636  nonsq  16670  hashgcdlem  16699  odzdvds  16707  iserodd  16747  pcprendvds  16752  pcdvdsb  16781  pcidlem  16784  dvdsprmpweqle  16798  difsqpwdvds  16799  pcfaclem  16810  prmunb  16826  ramtcl2  16923  ramubcl  16930  ram0  16934  ramub1lem1  16938  cshwshashlem2  17008  smndex1iidm  18775  sylow1lem1  19477  pgpssslw  19493  efgsfo  19618  efgred  19627  telgsums  19872  prmirredlem  21379  prmirred  21381  gsumbagdiaglem  21837  psrridm  21870  psdmul  22051  coe1tmmul2  22160  gsummoncoe1  22193  mp2pm2mplem4  22694  fvmptnn04ifb  22736  chfacfisf  22739  chfacfisfcpmat  22740  chfacffsupp  22741  chfacfscmul0  22743  chfacfpmmul0  22747  dyaddisj  25495  mdegle0  25980  deg1nn0clb  25993  deg1ge  26001  deg1tmle  26021  ply1divex  26040  plyco0  26095  coeeulem  26127  coeaddlem  26152  coe1termlem  26161  dgreq0  26169  dgrlt  26170  plydivex  26203  aannenlem1  26234  taylfvallem1  26262  tayl0  26267  radcnvlem1  26320  radcnvlem2  26321  dvradcnv  26328  leibpi  26850  log2tlbnd  26853  birthdaylem3  26861  zetacvg  26923  basellem2  26990  basellem3  26991  chpp1  27063  bcmono  27186  bcmax  27187  lgsdinn0  27254  2lgslem1c  27302  2sq2  27342  2sqreulem1  27355  2sqreultlem  27356  dchrisumlem1  27398  ostth2lem2  27543  nbusgrvtxm1  29324  upgrewlkle2  29552  pthdlem1  29711  crctcshwlkn0lem4  29758  crctcshwlkn0  29766  crctcsh  29769  wwlksm1edg  29826  wwlksnred  29837  wwlksnredwwlkn  29840  wwlksnredwwlkn0  29841  wwlksnextwrd  29842  wwlksnextfun  29843  wwlksnextinj  29844  wwlksnextproplem1  29854  wwlksnextproplem2  29855  wwlksnextproplem3  29856  clwlkclwwlklem2a1  29936  clwlkclwwlklem2a2  29937  clwlkclwwlklem2fv1  29939  clwlkclwwlklem2fv2  29940  clwlkclwwlklem2a4  29941  clwlkclwwlklem2a  29942  clwlkclwwlklem2  29944  clwlkclwwlk  29946  clwlkclwwlk2  29947  clwlkclwwlkf  29952  clwwisshclwwslem  29958  clwwlkel  29990  wwlksext2clwwlk  30001  clwlknf1oclwwlknlem1  30025  clwwlknonex2lem2  30052  eupth2lems  30182  eupth2  30183  eucrctshift  30187  numclwwlk7  30335  frgrreggt1  30337  frgrreg  30338  frgrogt3nreg  30341  friendship  30343  nn0xmulclb  32714  dpcl  32831  wrdt2ind  32895  hasheuni  34052  eulerpartlems  34328  hgt750lem  34619  0nn0m1nnn0  35090  derangen  35149  faclimlem1  35720  poimirlem28  37632  rrntotbnd  37820  sticksstones22  42145  gcdnn0id  42306  nn0addcom  42439  zaddcomlem  42440  nn0mulcom  42443  nacsfix  42689  eldioph2lem1  42737  irrapxlem4  42802  pell14qrgt0  42836  pell1qrgaplem  42850  pellqrexplicit  42854  rmxycomplete  42894  jm2.17a  42937  jm2.17b  42938  rmygeid  42941  jm2.22  42972  rmxdiophlem  42992  hbtlem5  43105  hbt  43107  fperiodmullem  45289  dvnxpaek  45927  stoweidlem17  46002  wallispilem3  46052  stirlinglem5  46063  stirlinglem7  46065  fourierdlem16  46108  fourierdlem21  46113  fourierdlem22  46114  fourierdlem83  46174  fourierdlem112  46203  elaa2lem  46218  etransclem23  46242  zm1nn  47290  nn0resubcl  47296  fz0addge0  47307  elfzlble  47308  subsubelfzo0  47314  2ffzoeq  47315  addmodne  47332  submodlt  47338  iccpartigtl  47411  lswn0  47432  sqrtpwpw2p  47526  fmtnodvds  47532  goldbachth  47535  odz2prm2pw  47551  flsqrt  47581  nn0e  47685  nn0sumltlt  48338  ply1mulgsumlem2  48376  nn0eo  48517  flnn0div2ge  48522  fllog2  48557  dignn0fr  48590  digexp  48596  dig2nn0  48600  0dig2nn0e  48601  dig2bits  48603  itcovalt2lem2lem1  48662