Theorem nn0re 12288

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

Syntax hints:   → wi 4   ∈ wcel 2104  ℝcr 10916  ℕ₀cn0 12279

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707  ax-sep 5232  ax-nul 5239  ax-pr 5361  ax-un 7620  ax-1cn 10975  ax-icn 10976  ax-addcl 10977  ax-addrcl 10978  ax-mulcl 10979  ax-mulrcl 10980  ax-i2m1 10985  ax-1ne0 10986  ax-rnegex 10988  ax-rrecex 10989  ax-cnre 10990

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3286  df-rab 3287  df-v 3439  df-sbc 3722  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-pss 3911  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4845  df-iun 4933  df-br 5082  df-opab 5144  df-mpt 5165  df-tr 5199  df-id 5500  df-eprel 5506  df-po 5514  df-so 5515  df-fr 5555  df-we 5557  df-xp 5606  df-rel 5607  df-cnv 5608  df-co 5609  df-dm 5610  df-rn 5611  df-res 5612  df-ima 5613  df-pred 6217  df-ord 6284  df-on 6285  df-lim 6286  df-suc 6287  df-iota 6410  df-fun 6460  df-fn 6461  df-f 6462  df-f1 6463  df-fo 6464  df-f1o 6465  df-fv 6466  df-ov 7310  df-om 7745  df-2nd 7864  df-frecs 8128  df-wrecs 8159  df-recs 8233  df-rdg 8272  df-nn 12020  df-n0 12280

This theorem is referenced by:  nn0ge0  12304  nn0nlt0  12305  nn0le0eq0  12307  nn0p1gt0  12308  elnnnn0c  12324  nn0addge1  12325  nn0addge2  12326  nn0sub  12329  ltsubnn0  12330  nn0negleid  12331  difgtsumgt  12332  nn0n0n1ge2b  12347  nn0ge2m1nn  12348  nn0nndivcl  12350  xnn0xr  12356  nn0nepnf  12359  xnn0nemnf  12362  elznn0nn  12379  nn0lt2  12429  nn0le2is012  12430  nn0ge0div  12435  nn01to3  12727  xnn0xaddcl  13015  xnn0lem1lt  13024  xnn0lenn0nn0  13025  xnn0xadd0  13027  nn0rp0  13233  xnn0xrge0  13284  nn0fz0  13400  elfz0fzfz0  13407  fz0fzelfz0  13408  fz0fzdiffz0  13411  fzctr  13414  difelfzle  13415  difelfznle  13416  fvffz0  13420  fzoun  13470  nn0p1elfzo  13476  elfzo0le  13477  fzonmapblen  13479  fzofzim  13480  elincfzoext  13491  elfzodifsumelfzo  13499  fzonn0p1  13510  fzonn0p1p1  13512  ssfzoulel  13527  ubmelm1fzo  13529  elfznelfzo  13538  fvinim0ffz  13552  subfzo0  13555  adddivflid  13584  divfl0  13590  fldivnn0le  13598  flltdivnn0lt  13599  quoremnn0ALT  13623  modmuladdnn0  13681  addmodid  13685  modifeq2int  13699  modfzo0difsn  13709  modsumfzodifsn  13710  addmodlteq  13712  ssnn0fi  13751  fsuppmapnn0fiub0  13759  suppssfz  13760  nn0sq11  13897  bernneq  13990  bernneq3  13992  facwordi  14049  faclbnd  14050  faclbnd3  14052  faclbnd5  14058  faclbnd6  14059  facubnd  14060  facavg  14061  bcval4  14067  bcval5  14078  bcpasc  14081  hashbnd  14096  hashnnn0genn0  14103  hashnemnf  14104  hashclb  14118  hashneq0  14124  hashsdom  14141  hashunsnggt  14154  fi1uzind  14256  ccat0  14325  ccat2s1fvw  14394  ccat2s1fvwOLD  14395  swrdnd0  14415  swrdsbslen  14422  swrdspsleq  14423  pfxnd0  14446  swrdswrdlem  14462  swrdswrd  14463  swrdccatin1  14483  pfxccatin12lem2  14489  pfxccatin12lem3  14490  pfxccat3  14492  swrdccat  14493  pfxccat3a  14496  swrdccat3blem  14497  repswswrd  14542  2cshw  14571  cshweqrep  14579  cshwcsh2id  14586  2swrd2eqwrdeq  14711  nn0sqeq1  15033  isercoll  15424  o1fsum  15570  geomulcvg  15633  rerisefaccl  15772  refallfaccl  15773  rprisefaccl  15778  dvdseq  16068  oddge22np1  16103  nn0ehalf  16132  nn0o1gt2  16135  nn0o  16137  nn0oddm1d2  16139  bitsfi  16189  bitsinv1  16194  gcdn0gt0  16270  nn0gcdid0  16273  absmulgcd  16302  nn0seqcvgd  16320  algcvgblem  16327  algcvga  16329  lcmgcdnn  16361  lcmfun  16395  lcmfass  16396  prmfac1  16471  prmndvdsfaclt  16475  nonsq  16508  hashgcdlem  16534  odzdvds  16541  iserodd  16581  pcprendvds  16586  pcdvdsb  16615  pcidlem  16618  dvdsprmpweqle  16632  difsqpwdvds  16633  pcfaclem  16644  prmunb  16660  ramtcl2  16757  ramubcl  16764  ram0  16768  ramub1lem1  16772  cshwshashlem2  16843  smndex1iidm  18585  sylow1lem1  19248  pgpssslw  19264  efgsfo  19390  efgred  19399  telgsums  19639  prmirredlem  20739  prmirred  20741  psrbagconOLD  21179  gsumbagdiaglemOLD  21186  gsumbagdiaglem  21189  psrridm  21218  coe1tmmul2  21492  gsummoncoe1  21520  mp2pm2mplem4  22003  fvmptnn04ifb  22045  chfacfisf  22048  chfacfisfcpmat  22049  chfacffsupp  22050  chfacfscmul0  22052  chfacfpmmul0  22056  dyaddisj  24805  mdegle0  25287  deg1nn0clb  25300  deg1ge  25308  deg1tmle  25327  ply1divex  25346  plyco0  25398  coeeulem  25430  coeaddlem  25455  coe1termlem  25464  dgreq0  25471  dgrlt  25472  plydivex  25502  aannenlem1  25533  taylfvallem1  25561  tayl0  25566  radcnvlem1  25617  radcnvlem2  25618  dvradcnv  25625  leibpi  26137  log2tlbnd  26140  birthdaylem3  26148  zetacvg  26209  basellem2  26276  basellem3  26277  chpp1  26349  bcmono  26470  bcmax  26471  lgsdinn0  26538  2lgslem1c  26586  2sq2  26626  2sqreulem1  26639  2sqreultlem  26640  dchrisumlem1  26682  ostth2lem2  26827  nbusgrvtxm1  27791  upgrewlkle2  28018  pthdlem1  28179  crctcshwlkn0lem4  28223  crctcshwlkn0  28231  crctcsh  28234  wwlksm1edg  28291  wwlksnred  28302  wwlksnredwwlkn  28305  wwlksnredwwlkn0  28306  wwlksnextwrd  28307  wwlksnextfun  28308  wwlksnextinj  28309  wwlksnextproplem1  28319  wwlksnextproplem2  28320  wwlksnextproplem3  28321  clwlkclwwlklem2a1  28401  clwlkclwwlklem2a2  28402  clwlkclwwlklem2fv1  28404  clwlkclwwlklem2fv2  28405  clwlkclwwlklem2a4  28406  clwlkclwwlklem2a  28407  clwlkclwwlklem2  28409  clwlkclwwlk  28411  clwlkclwwlk2  28412  clwlkclwwlkf  28417  clwwisshclwwslem  28423  clwwlkel  28455  wwlksext2clwwlk  28466  clwlknf1oclwwlknlem1  28490  clwwlknonex2lem2  28517  eupth2lems  28647  eupth2  28648  eucrctshift  28652  numclwwlk7  28800  frgrreggt1  28802  frgrreg  28803  frgrogt3nreg  28806  friendship  28808  nn0xmulclb  31139  dpcl  31210  wrdt2ind  31270  hasheuni  32098  eulerpartlems  32372  hgt750lem  32676  0nn0m1nnn0  33116  derangen  33179  faclimlem1  33754  poimirlem28  35849  rrntotbnd  36038  sticksstones22  40166  factwoffsmonot  40205  gcdnn0id  40366  nacsfix  40571  eldioph2lem1  40619  irrapxlem4  40684  pell14qrgt0  40718  pell1qrgaplem  40732  pellqrexplicit  40736  rmxycomplete  40777  jm2.17a  40820  jm2.17b  40821  rmygeid  40824  jm2.22  40855  rmxdiophlem  40875  hbtlem5  40991  hbt  40993  fperiodmullem  42890  dvnxpaek  43532  stoweidlem17  43607  wallispilem3  43657  stirlinglem5  43668  stirlinglem7  43670  fourierdlem16  43713  fourierdlem21  43718  fourierdlem22  43719  fourierdlem83  43779  fourierdlem112  43808  elaa2lem  43823  etransclem23  43847  zm1nn  44852  nn0resubcl  44858  fz0addge0  44869  elfzlble  44870  subsubelfzo0  44876  2ffzoeq  44878  iccpartigtl  44933  lswn0  44954  sqrtpwpw2p  45048  fmtnodvds  45054  goldbachth  45057  odz2prm2pw  45073  flsqrt  45103  nn0e  45207  nn0sumltlt  45744  ply1mulgsumlem2  45786  nn0eo  45932  flnn0div2ge  45937  fllog2  45972  dignn0fr  46005  digexp  46011  dig2nn0  46015  0dig2nn0e  46016  dig2bits  46018  itcovalt2lem2lem1  46077