Theorem nn0re 12446

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℝcr 11037  ℕ₀cn0 12437

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 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375  ax-un 7689  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-i2m1 11106  ax-1ne0 11107  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-tr 5193  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6265  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-ov 7370  df-om 7818  df-2nd 7943  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-rdg 8349  df-nn 12175  df-n0 12438

This theorem is referenced by:  nn0ge0  12462  nn0nlt0  12463  nn0le0eq0  12465  nn0p1gt0  12466  elnnnn0c  12482  nn0addge1  12483  nn0addge2  12484  nn0sub  12487  ltsubnn0  12488  nn0negleid  12489  difgtsumgt  12490  nn0le2x  12491  nn0n0n1ge2b  12506  nn0ge2m1nn  12507  nn0nndivcl  12509  xnn0xr  12515  nn0nepnf  12518  xnn0nemnf  12521  elznn0nn  12538  nn0lt2  12592  nn0le2is012  12593  nn0ge0div  12598  nn01to3  12891  xnn0xaddcl  13187  xnn0lem1lt  13196  xnn0lenn0nn0  13197  xnn0xadd0  13199  nn0rp0  13408  xnn0xrge0  13459  nn0fz0  13579  elfz0fzfz0  13587  fz0fzelfz0  13588  fz0fzdiffz0  13591  fzctr  13594  difelfzle  13595  difelfznle  13596  fvffz0  13600  fzoun  13651  nn0p1elfzo  13657  elfzo0le  13658  fzonmapblen  13663  fzofzim  13664  elincfzoext  13678  elfzodifsumelfzo  13686  fzonn0p1  13697  fzonn0p1p1  13699  ssfzoulel  13715  ubmelm1fzo  13718  elfznelfzo  13728  fvinim0ffz  13744  subfzo0  13747  adddivflid  13777  divfl0  13783  fldivnn0le  13791  flltdivnn0lt  13792  quoremnn0ALT  13816  modmuladdnn0  13877  addmodid  13881  modifeq2int  13895  modfzo0difsn  13905  modsumfzodifsn  13906  addmodlteq  13908  ssnn0fi  13947  fsuppmapnn0fiub0  13955  suppssfz  13956  nn0sq11  14094  bernneq  14191  bernneq3  14193  facwordi  14251  faclbnd  14252  faclbnd3  14254  faclbnd5  14260  faclbnd6  14261  facubnd  14262  facavg  14263  bcval4  14269  bcval5  14280  bcpasc  14283  hashbnd  14298  hashnnn0genn0  14305  hashnemnf  14306  hashclb  14320  hashneq0  14326  hashsdom  14343  hashunsnggt  14356  fi1uzind  14469  ccat0  14538  ccat2s1fvw  14601  swrdnd0  14620  swrdsbslen  14627  swrdspsleq  14628  pfxnd0  14651  swrdswrdlem  14666  swrdswrd  14667  swrdccatin1  14687  pfxccatin12lem2  14693  pfxccatin12lem3  14694  pfxccat3  14696  swrdccat  14697  pfxccat3a  14700  swrdccat3blem  14701  repswswrd  14746  2cshw  14775  cshweqrep  14783  cshwcsh2id  14790  2swrd2eqwrdeq  14915  nn0sqeq1  15238  nn0absid  15392  isercoll  15630  o1fsum  15776  geomulcvg  15841  rerisefaccl  15982  refallfaccl  15983  rprisefaccl  15988  dvdseq  16283  oddge22np1  16318  nn0ehalf  16347  nn0o1gt2  16350  nn0o  16352  nn0oddm1d2  16354  bitsfi  16406  bitsinv1  16411  gcdn0gt0  16487  nn0gcdid0  16490  absmulgcd  16518  nn0seqcvgd  16539  algcvgblem  16546  algcvga  16548  lcmgcdnn  16580  lcmfun  16614  lcmfass  16615  prmfac1  16690  prmndvdsfaclt  16695  nonsq  16729  hashgcdlem  16758  odzdvds  16766  iserodd  16806  pcprendvds  16811  pcdvdsb  16840  pcidlem  16843  dvdsprmpweqle  16857  difsqpwdvds  16858  pcfaclem  16869  prmunb  16885  ramtcl2  16982  ramubcl  16989  ram0  16993  ramub1lem1  16997  cshwshashlem2  17067  smndex1iidm  18869  sylow1lem1  19573  pgpssslw  19589  efgsfo  19714  efgred  19723  telgsums  19968  prmirredlem  21452  prmirred  21454  gsumbagdiaglem  21910  psrridm  21941  psdmul  22132  coe1tmmul2  22241  gsummoncoe1  22273  mp2pm2mplem4  22774  fvmptnn04ifb  22816  chfacfisf  22819  chfacfisfcpmat  22820  chfacffsupp  22821  chfacfscmul0  22823  chfacfpmmul0  22827  dyaddisj  25563  mdegle0  26042  deg1nn0clb  26055  deg1ge  26063  deg1tmle  26083  ply1divex  26102  plyco0  26157  coeeulem  26189  coeaddlem  26214  coe1termlem  26223  dgreq0  26230  dgrlt  26231  plydivex  26263  aannenlem1  26294  taylfvallem1  26322  tayl0  26327  radcnvlem1  26378  radcnvlem2  26379  dvradcnv  26386  leibpi  26906  log2tlbnd  26909  birthdaylem3  26917  zetacvg  26978  basellem2  27045  basellem3  27046  chpp1  27118  bcmono  27240  bcmax  27241  lgsdinn0  27308  2lgslem1c  27356  2sq2  27396  2sqreulem1  27409  2sqreultlem  27410  dchrisumlem1  27452  ostth2lem2  27597  nbusgrvtxm1  29448  upgrewlkle2  29675  pthdlem1  29834  crctcshwlkn0lem4  29881  crctcshwlkn0  29889  crctcsh  29892  wwlksm1edg  29949  wwlksnred  29960  wwlksnredwwlkn  29963  wwlksnredwwlkn0  29964  wwlksnextwrd  29965  wwlksnextfun  29966  wwlksnextinj  29967  wwlksnextproplem1  29977  wwlksnextproplem2  29978  wwlksnextproplem3  29979  clwlkclwwlklem2a1  30062  clwlkclwwlklem2a2  30063  clwlkclwwlklem2fv1  30065  clwlkclwwlklem2fv2  30066  clwlkclwwlklem2a4  30067  clwlkclwwlklem2a  30068  clwlkclwwlklem2  30070  clwlkclwwlk  30072  clwlkclwwlk2  30073  clwlkclwwlkf  30078  clwwisshclwwslem  30084  clwwlkel  30116  wwlksext2clwwlk  30127  clwlknf1oclwwlknlem1  30151  clwwlknonex2lem2  30178  eupth2lems  30308  eupth2  30309  eucrctshift  30313  numclwwlk7  30461  frgrreggt1  30463  frgrreg  30464  frgrogt3nreg  30467  friendship  30469  nn0mnfxrd  32824  nn0xmulclb  32844  dpcl  32950  wrdt2ind  33013  hasheuni  34229  eulerpartlems  34504  hgt750lem  34795  0nn0m1nnn0  35295  derangen  35354  faclimlem1  35925  poimirlem28  37969  rrntotbnd  38157  sticksstones22  42607  gcdnn0id  42761  nn0addcom  42907  zaddcomlem  42908  nn0mulcom  42911  nacsfix  43144  eldioph2lem1  43192  irrapxlem4  43253  pell14qrgt0  43287  pell1qrgaplem  43301  pellqrexplicit  43305  rmxycomplete  43345  jm2.17a  43388  jm2.17b  43389  rmygeid  43392  jm2.22  43423  rmxdiophlem  43443  hbtlem5  43556  hbt  43558  fperiodmullem  45736  dvnxpaek  46370  stoweidlem17  46445  wallispilem3  46495  stirlinglem5  46506  stirlinglem7  46508  fourierdlem16  46551  fourierdlem21  46556  fourierdlem22  46557  fourierdlem83  46617  fourierdlem112  46646  elaa2lem  46661  etransclem23  46685  zm1nn  47750  nn0resubcl  47756  fz0addge0  47767  elfzlble  47768  subsubelfzo0  47775  2ffzoeq  47776  addmodne  47798  submodlt  47804  iccpartigtl  47883  lswn0  47904  sqrtpwpw2p  48001  fmtnodvds  48007  goldbachth  48010  odz2prm2pw  48026  flsqrt  48056  nn0e  48173  nn0sumltlt  48826  ply1mulgsumlem2  48863  nn0eo  49004  flnn0div2ge  49009  fllog2  49044  dignn0fr  49077  digexp  49083  dig2nn0  49087  0dig2nn0e  49088  dig2bits  49090  itcovalt2lem2lem1  49149