Theorem nn0re 12410

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

Syntax hints:   → wi 4   ∈ wcel 2113  ℝcr 11025  ℕ₀cn0 12401

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377  ax-un 7680  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-addrcl 11087  ax-mulcl 11088  ax-mulrcl 11089  ax-i2m1 11094  ax-1ne0 11095  ax-rnegex 11097  ax-rrecex 11098  ax-cnre 11099

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-tr 5206  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7361  df-om 7809  df-2nd 7934  df-frecs 8223  df-wrecs 8254  df-recs 8303  df-rdg 8341  df-nn 12146  df-n0 12402

This theorem is referenced by:  nn0ge0  12426  nn0nlt0  12427  nn0le0eq0  12429  nn0p1gt0  12430  elnnnn0c  12446  nn0addge1  12447  nn0addge2  12448  nn0sub  12451  ltsubnn0  12452  nn0negleid  12453  difgtsumgt  12454  nn0le2x  12455  nn0n0n1ge2b  12470  nn0ge2m1nn  12471  nn0nndivcl  12473  xnn0xr  12479  nn0nepnf  12482  xnn0nemnf  12485  elznn0nn  12502  nn0lt2  12555  nn0le2is012  12556  nn0ge0div  12561  nn01to3  12854  xnn0xaddcl  13150  xnn0lem1lt  13159  xnn0lenn0nn0  13160  xnn0xadd0  13162  nn0rp0  13371  xnn0xrge0  13422  nn0fz0  13541  elfz0fzfz0  13549  fz0fzelfz0  13550  fz0fzdiffz0  13553  fzctr  13556  difelfzle  13557  difelfznle  13558  fvffz0  13562  fzoun  13612  nn0p1elfzo  13618  elfzo0le  13619  fzonmapblen  13624  fzofzim  13625  elincfzoext  13639  elfzodifsumelfzo  13647  fzonn0p1  13658  fzonn0p1p1  13660  ssfzoulel  13676  ubmelm1fzo  13679  elfznelfzo  13689  fvinim0ffz  13705  subfzo0  13708  adddivflid  13738  divfl0  13744  fldivnn0le  13752  flltdivnn0lt  13753  quoremnn0ALT  13777  modmuladdnn0  13838  addmodid  13842  modifeq2int  13856  modfzo0difsn  13866  modsumfzodifsn  13867  addmodlteq  13869  ssnn0fi  13908  fsuppmapnn0fiub0  13916  suppssfz  13917  nn0sq11  14055  bernneq  14152  bernneq3  14154  facwordi  14212  faclbnd  14213  faclbnd3  14215  faclbnd5  14221  faclbnd6  14222  facubnd  14223  facavg  14224  bcval4  14230  bcval5  14241  bcpasc  14244  hashbnd  14259  hashnnn0genn0  14266  hashnemnf  14267  hashclb  14281  hashneq0  14287  hashsdom  14304  hashunsnggt  14317  fi1uzind  14430  ccat0  14499  ccat2s1fvw  14562  swrdnd0  14581  swrdsbslen  14588  swrdspsleq  14589  pfxnd0  14612  swrdswrdlem  14627  swrdswrd  14628  swrdccatin1  14648  pfxccatin12lem2  14654  pfxccatin12lem3  14655  pfxccat3  14657  swrdccat  14658  pfxccat3a  14661  swrdccat3blem  14662  repswswrd  14707  2cshw  14736  cshweqrep  14744  cshwcsh2id  14751  2swrd2eqwrdeq  14876  nn0sqeq1  15199  nn0absid  15353  isercoll  15591  o1fsum  15736  geomulcvg  15799  rerisefaccl  15940  refallfaccl  15941  rprisefaccl  15946  dvdseq  16241  oddge22np1  16276  nn0ehalf  16305  nn0o1gt2  16308  nn0o  16310  nn0oddm1d2  16312  bitsfi  16364  bitsinv1  16369  gcdn0gt0  16445  nn0gcdid0  16448  absmulgcd  16476  nn0seqcvgd  16497  algcvgblem  16504  algcvga  16506  lcmgcdnn  16538  lcmfun  16572  lcmfass  16573  prmfac1  16647  prmndvdsfaclt  16652  nonsq  16686  hashgcdlem  16715  odzdvds  16723  iserodd  16763  pcprendvds  16768  pcdvdsb  16797  pcidlem  16800  dvdsprmpweqle  16814  difsqpwdvds  16815  pcfaclem  16826  prmunb  16842  ramtcl2  16939  ramubcl  16946  ram0  16950  ramub1lem1  16954  cshwshashlem2  17024  smndex1iidm  18826  sylow1lem1  19527  pgpssslw  19543  efgsfo  19668  efgred  19677  telgsums  19922  prmirredlem  21427  prmirred  21429  gsumbagdiaglem  21886  psrridm  21918  psdmul  22109  coe1tmmul2  22218  gsummoncoe1  22252  mp2pm2mplem4  22753  fvmptnn04ifb  22795  chfacfisf  22798  chfacfisfcpmat  22799  chfacffsupp  22800  chfacfscmul0  22802  chfacfpmmul0  22806  dyaddisj  25553  mdegle0  26038  deg1nn0clb  26051  deg1ge  26059  deg1tmle  26079  ply1divex  26098  plyco0  26153  coeeulem  26185  coeaddlem  26210  coe1termlem  26219  dgreq0  26227  dgrlt  26228  plydivex  26261  aannenlem1  26292  taylfvallem1  26320  tayl0  26325  radcnvlem1  26378  radcnvlem2  26379  dvradcnv  26386  leibpi  26908  log2tlbnd  26911  birthdaylem3  26919  zetacvg  26981  basellem2  27048  basellem3  27049  chpp1  27121  bcmono  27244  bcmax  27245  lgsdinn0  27312  2lgslem1c  27360  2sq2  27400  2sqreulem1  27413  2sqreultlem  27414  dchrisumlem1  27456  ostth2lem2  27601  nbusgrvtxm1  29452  upgrewlkle2  29680  pthdlem1  29839  crctcshwlkn0lem4  29886  crctcshwlkn0  29894  crctcsh  29897  wwlksm1edg  29954  wwlksnred  29965  wwlksnredwwlkn  29968  wwlksnredwwlkn0  29969  wwlksnextwrd  29970  wwlksnextfun  29971  wwlksnextinj  29972  wwlksnextproplem1  29982  wwlksnextproplem2  29983  wwlksnextproplem3  29984  clwlkclwwlklem2a1  30067  clwlkclwwlklem2a2  30068  clwlkclwwlklem2fv1  30070  clwlkclwwlklem2fv2  30071  clwlkclwwlklem2a4  30072  clwlkclwwlklem2a  30073  clwlkclwwlklem2  30075  clwlkclwwlk  30077  clwlkclwwlk2  30078  clwlkclwwlkf  30083  clwwisshclwwslem  30089  clwwlkel  30121  wwlksext2clwwlk  30132  clwlknf1oclwwlknlem1  30156  clwwlknonex2lem2  30183  eupth2lems  30313  eupth2  30314  eucrctshift  30318  numclwwlk7  30466  frgrreggt1  30468  frgrreg  30469  frgrogt3nreg  30472  friendship  30474  nn0mnfxrd  32831  nn0xmulclb  32851  dpcl  32972  wrdt2ind  33035  hasheuni  34242  eulerpartlems  34517  hgt750lem  34808  0nn0m1nnn0  35307  derangen  35366  faclimlem1  35937  poimirlem28  37849  rrntotbnd  38037  sticksstones22  42422  gcdnn0id  42584  nn0addcom  42717  zaddcomlem  42718  nn0mulcom  42721  nacsfix  42954  eldioph2lem1  43002  irrapxlem4  43067  pell14qrgt0  43101  pell1qrgaplem  43115  pellqrexplicit  43119  rmxycomplete  43159  jm2.17a  43202  jm2.17b  43203  rmygeid  43206  jm2.22  43237  rmxdiophlem  43257  hbtlem5  43370  hbt  43372  fperiodmullem  45551  dvnxpaek  46186  stoweidlem17  46261  wallispilem3  46311  stirlinglem5  46322  stirlinglem7  46324  fourierdlem16  46367  fourierdlem21  46372  fourierdlem22  46373  fourierdlem83  46433  fourierdlem112  46462  elaa2lem  46477  etransclem23  46501  zm1nn  47548  nn0resubcl  47554  fz0addge0  47565  elfzlble  47566  subsubelfzo0  47572  2ffzoeq  47573  addmodne  47590  submodlt  47596  iccpartigtl  47669  lswn0  47690  sqrtpwpw2p  47784  fmtnodvds  47790  goldbachth  47793  odz2prm2pw  47809  flsqrt  47839  nn0e  47943  nn0sumltlt  48596  ply1mulgsumlem2  48633  nn0eo  48774  flnn0div2ge  48779  fllog2  48814  dignn0fr  48847  digexp  48853  dig2nn0  48857  0dig2nn0e  48858  dig2bits  48860  itcovalt2lem2lem1  48919