Theorem nn0re 12508

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

Syntax hints:   → wi 4   ∈ wcel 2143  ℝcr 11094  ℕ₀cn0 12499

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pr 5404  ax-un 7732  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-addrcl 11156  ax-mulcl 11157  ax-mulrcl 11158  ax-i2m1 11163  ax-1ne0 11164  ax-rnegex 11166  ax-rrecex 11167  ax-cnre 11168

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-iun 4958  df-br 5110  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-we 5616  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-ov 7413  df-om 7859  df-2nd 7983  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-nn 12229  df-n0 12500

This theorem is referenced by:  nn0ge0  12524  nn0nlt0  12525  nn0le0eq0  12527  nn0p1gt0  12528  elnnnn0c  12544  nn0addge1  12545  nn0addge2  12546  nn0sub  12549  ltsubnn0  12550  nn0negleid  12551  difgtsumgt  12552  nn0le2x  12553  nn0n0n1ge2b  12568  nn0ge2m1nn  12569  nn0nndivcl  12571  xnn0xr  12577  nn0nepnf  12580  xnn0nemnf  12583  elznn0nn  12600  nn0lt2  12654  nn0le2is012  12655  nn0ge0div  12660  nn01to3  12960  xnn0xaddcl  13256  xnn0lem1lt  13265  xnn0lenn0nn0  13266  xnn0xadd0  13268  nn0rp0  13477  xnn0xrge0  13528  nn0fz0  13649  elfz0fzfz0  13657  fz0fzelfz0  13658  fz0fzdiffz0  13661  fzctr  13664  difelfzle  13665  difelfznle  13666  fvffz0  13670  fzoun  13721  nn0p1elfzo  13727  elfzo0le  13728  fzonmapblen  13733  fzofzim  13734  elincfzoext  13748  elfzodifsumelfzo  13756  fzonn0p1  13767  fzonn0p1p1  13769  ssfzoulel  13785  ubmelm1fzo  13788  elfznelfzo  13798  fvinim0ffz  13814  subfzo0  13817  adddivflid  13847  divfl0  13853  fldivnn0le  13861  flltdivnn0lt  13862  quoremnn0ALT  13886  modmuladdnn0  13947  addmodid  13951  modifeq2int  13965  modfzo0difsn  13975  modsumfzodifsn  13976  addmodlteq  13978  ssnn0fi  14017  fsuppmapnn0fiub0  14025  suppssfz  14026  nn0sq11  14164  bernneq  14261  bernneq3  14263  facwordi  14321  faclbnd  14322  faclbnd3  14324  faclbnd5  14330  faclbnd6  14331  facubnd  14332  facavg  14333  bcval4  14339  bcval5  14350  bcpasc  14353  hashbnd  14368  hashnnn0genn0  14375  hashnemnf  14376  hashclb  14390  hashneq0  14396  hashsdom  14413  hashunsnggt  14426  fi1uzind  14540  ccat0  14609  ccat2s1fvw  14672  swrdnd0  14691  swrdsbslen  14698  swrdspsleq  14699  pfxnd0  14722  swrdswrdlem  14737  swrdswrd  14738  swrdccatin1  14758  pfxccatin12lem2  14764  pfxccatin12lem3  14765  pfxccat3  14767  swrdccat  14768  pfxccat3a  14771  swrdccat3blem  14772  repswswrd  14817  2cshw  14846  cshweqrep  14854  cshwcsh2id  14861  2swrd2eqwrdeq  14986  nn0sqeq1  15323  nn0absid  15477  isercoll  15715  o1fsum  15861  geomulcvg  15926  rerisefaccl  16067  refallfaccl  16068  rprisefaccl  16073  dvdseq  16367  oddge22np1  16402  nn0ehalf  16431  nn0o1gt2  16434  nn0o  16436  nn0oddm1d2  16438  bitsfi  16490  bitsinv1  16495  gcdn0gt0  16571  nn0gcdid0  16574  absmulgcd  16602  nn0seqcvgd  16623  algcvgblem  16630  algcvga  16632  lcmgcdnn  16664  lcmfun  16698  lcmfass  16699  prmfac1  16774  prmndvdsfaclt  16779  nonsq  16813  hashgcdlem  16842  odzdvds  16850  iserodd  16890  pcprendvds  16895  pcdvdsb  16924  pcidlem  16927  dvdsprmpweqle  16941  difsqpwdvds  16942  pcfaclem  16953  prmunb  16969  ramtcl2  17066  ramubcl  17073  ram0  17077  ramub1lem1  17081  cshwshashlem2  17151  smndex1iidm  18955  sylow1lem1  19663  pgpssslw  19679  efgsfo  19804  efgred  19813  telgsums  20058  prmirredlem  21622  prmirred  21624  gsumbagdiaglem  22081  psrridm  22112  psdmul  22329  coe1tmmul2  22437  gsummoncoe1  22468  mp2pm2mplem4  22966  fvmptnn04ifb  23008  chfacfisf  23011  chfacfisfcpmat  23012  chfacffsupp  23013  chfacfscmul0  23015  chfacfpmmul0  23019  dyaddisj  25755  mdegle0  26234  deg1nn0clb  26247  deg1ge  26255  deg1tmle  26275  ply1divex  26294  plyco0  26349  coeeulem  26381  coeaddlem  26406  coe1termlem  26415  dgreq0  26422  dgrlt  26423  plydivex  26458  aannenlem1  26491  taylfvallem1  26520  tayl0  26525  radcnvlem1  26576  radcnvlem2  26577  dvradcnv  26584  leibpi  27107  log2tlbnd  27110  birthdaylem3  27118  zetacvg  27179  basellem2  27246  basellem3  27247  chpp1  27319  bcmono  27441  bcmax  27442  lgsdinn0  27509  2lgslem1c  27557  2sq2  27597  2sqreulem1  27610  2sqreultlem  27611  dchrisumlem1  27653  ostth2lem2  27798  nbusgrvtxm1  29729  upgrewlkle2  29956  pthdlem1  30115  crctcshwlkn0lem4  30162  crctcshwlkn0  30170  crctcsh  30173  wwlksm1edg  30230  wwlksnred  30241  wwlksnredwwlkn  30244  wwlksnredwwlkn0  30245  wwlksnextwrd  30246  wwlksnextfun  30247  wwlksnextinj  30248  wwlksnextproplem1  30258  wwlksnextproplem2  30259  wwlksnextproplem3  30260  clwlkclwwlklem2a1  30343  clwlkclwwlklem2a2  30344  clwlkclwwlklem2fv1  30346  clwlkclwwlklem2fv2  30347  clwlkclwwlklem2a4  30348  clwlkclwwlklem2a  30349  clwlkclwwlklem2  30351  clwlkclwwlk  30353  clwlkclwwlk2  30354  clwlkclwwlkf  30359  clwwisshclwwslem  30365  clwwlkel  30397  wwlksext2clwwlk  30408  clwlknf1oclwwlknlem1  30432  clwwlknonex2lem2  30459  eupth2lems  30589  eupth2  30590  eucrctshift  30594  numclwwlk7  30742  frgrreggt1  30744  frgrreg  30745  frgrogt3nreg  30748  friendship  30750  nn0mnfxrd  33096  nn0xmulclb  33116  dpcl  33210  wrdt2ind  33273  hasheuni  34475  eulerpartlems  34750  hgt750lem  35038  0nn0m1nnn0  35604  derangen  35664  faclimlem1  36235  poimirlem28  38299  rrntotbnd  38487  sticksstones22  42935  gcdnn0id  43090  nn0addcom  43236  zaddcomlem  43237  nn0mulcom  43240  nacsfix  43443  eldioph2lem1  43491  irrapxlem4  43552  pell14qrgt0  43586  pell1qrgaplem  43600  pellqrexplicit  43604  rmxycomplete  43644  jm2.17a  43687  jm2.17b  43688  rmygeid  43691  jm2.22  43722  rmxdiophlem  43742  hbtlem5  43855  hbt  43857  fperiodmullem  46022  dvnxpaek  46656  stoweidlem17  46731  wallispilem3  46781  stirlinglem5  46792  stirlinglem7  46794  fourierdlem16  46837  fourierdlem21  46842  fourierdlem22  46843  fourierdlem83  46903  fourierdlem112  46932  elaa2lem  46947  etransclem23  46971  zm1nn  48039  nn0resubcl  48045  fz0addge0  48056  elfzlble  48057  subsubelfzo0  48064  2ffzoeq  48065  addmodne  48087  submodlt  48093  iccpartigtl  48172  lswn0  48193  sqrtpwpw2p  48290  fmtnodvds  48296  goldbachth  48299  odz2prm2pw  48315  flsqrt  48345  nn0e  48462  nn0sumltlt  49130  ply1mulgsumlem2  49167  nn0eo  49308  flnn0div2ge  49313  fllog2  49348  dignn0fr  49381  digexp  49387  dig2nn0  49391  0dig2nn0e  49392  dig2bits  49394  itcovalt2lem2lem1  49453