Theorem nn0re 11987

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℝcr 10616  ℕ₀cn0 11978

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2710  ax-sep 5167  ax-nul 5174  ax-pr 5296  ax-un 7481  ax-1cn 10675  ax-icn 10676  ax-addcl 10677  ax-addrcl 10678  ax-mulcl 10679  ax-mulrcl 10680  ax-i2m1 10685  ax-1ne0 10686  ax-rnegex 10688  ax-rrecex 10689  ax-cnre 10690

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-ral 3058  df-rex 3059  df-reu 3060  df-rab 3062  df-v 3400  df-sbc 3681  df-csb 3791  df-dif 3846  df-un 3848  df-in 3850  df-ss 3860  df-pss 3862  df-nul 4212  df-if 4415  df-pw 4490  df-sn 4517  df-pr 4519  df-tp 4521  df-op 4523  df-uni 4797  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5429  df-eprel 5434  df-po 5442  df-so 5443  df-fr 5483  df-we 5485  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-pred 6129  df-ord 6175  df-on 6176  df-lim 6177  df-suc 6178  df-iota 6297  df-fun 6341  df-fn 6342  df-f 6343  df-f1 6344  df-fo 6345  df-f1o 6346  df-fv 6347  df-ov 7175  df-om 7602  df-wrecs 7978  df-recs 8039  df-rdg 8077  df-nn 11719  df-n0 11979

This theorem is referenced by:  nn0ge0  12003  nn0nlt0  12004  nn0le0eq0  12006  nn0p1gt0  12007  elnnnn0c  12023  nn0addge1  12024  nn0addge2  12025  nn0sub  12028  ltsubnn0  12029  nn0negleid  12030  difgtsumgt  12031  nn0n0n1ge2b  12046  nn0ge2m1nn  12047  nn0nndivcl  12049  xnn0xr  12055  nn0nepnf  12058  xnn0nemnf  12061  elznn0nn  12078  nn0lt2  12128  nn0le2is012  12129  nn0ge0div  12134  nn01to3  12425  xnn0xaddcl  12713  xnn0lem1lt  12722  xnn0lenn0nn0  12723  xnn0xadd0  12725  nn0rp0  12931  xnn0xrge0  12982  nn0fz0  13098  elfz0fzfz0  13105  fz0fzelfz0  13106  fz0fzdiffz0  13109  fzctr  13112  difelfzle  13113  difelfznle  13114  fvffz0  13118  fzoun  13167  nn0p1elfzo  13173  elfzo0le  13174  fzonmapblen  13176  fzofzim  13177  elincfzoext  13188  elfzodifsumelfzo  13196  fzonn0p1  13207  fzonn0p1p1  13209  ssfzoulel  13224  ubmelm1fzo  13226  elfznelfzo  13235  fvinim0ffz  13249  subfzo0  13252  adddivflid  13281  divfl0  13287  fldivnn0le  13295  flltdivnn0lt  13296  quoremnn0ALT  13318  modmuladdnn0  13376  addmodid  13380  modifeq2int  13394  modfzo0difsn  13404  modsumfzodifsn  13405  addmodlteq  13407  ssnn0fi  13446  fsuppmapnn0fiub0  13454  suppssfz  13455  nn0sq11  13591  bernneq  13684  bernneq3  13686  facwordi  13743  faclbnd  13744  faclbnd3  13746  faclbnd5  13752  faclbnd6  13753  facubnd  13754  facavg  13755  bcval4  13761  bcval5  13772  bcpasc  13775  hashbnd  13790  hashnnn0genn0  13797  hashnemnf  13798  hashclb  13813  hashneq0  13819  hashsdom  13836  hashunsnggt  13849  fi1uzind  13951  ccat0  14020  ccat2s1fvw  14089  ccat2s1fvwOLD  14090  swrdnd0  14110  swrdsbslen  14117  swrdspsleq  14118  pfxnd0  14141  swrdswrdlem  14157  swrdswrd  14158  swrdccatin1  14178  pfxccatin12lem2  14184  pfxccatin12lem3  14185  pfxccat3  14187  swrdccat  14188  pfxccat3a  14191  swrdccat3blem  14192  repswswrd  14237  2cshw  14266  cshweqrep  14274  cshwcsh2id  14281  2swrd2eqwrdeq  14406  nn0sqeq1  14728  isercoll  15119  o1fsum  15263  geomulcvg  15326  rerisefaccl  15465  refallfaccl  15466  rprisefaccl  15471  dvdseq  15761  oddge22np1  15796  nn0ehalf  15825  nn0o1gt2  15828  nn0o  15830  nn0oddm1d2  15832  bitsfi  15882  bitsinv1  15887  gcdn0gt0  15963  nn0gcdid0  15966  absmulgcd  15995  nn0seqcvgd  16013  algcvgblem  16020  algcvga  16022  lcmgcdnn  16054  lcmfun  16088  lcmfass  16089  prmfac1  16164  prmndvdsfaclt  16168  nonsq  16201  hashgcdlem  16227  odzdvds  16234  iserodd  16274  pcprendvds  16279  pcdvdsb  16307  pcidlem  16310  dvdsprmpweqle  16324  difsqpwdvds  16325  pcfaclem  16336  prmunb  16352  ramtcl2  16449  ramubcl  16456  ram0  16460  ramub1lem1  16464  cshwshashlem2  16535  smndex1iidm  18184  sylow1lem1  18843  pgpssslw  18859  efgsfo  18985  efgred  18994  telgsums  19234  prmirredlem  20315  prmirred  20317  psrbagconOLD  20746  gsumbagdiaglemOLD  20753  gsumbagdiaglem  20756  psrridm  20785  coe1tmmul2  21053  gsummoncoe1  21081  mp2pm2mplem4  21562  fvmptnn04ifb  21604  chfacfisf  21607  chfacfisfcpmat  21608  chfacffsupp  21609  chfacfscmul0  21611  chfacfpmmul0  21615  dyaddisj  24350  mdegle0  24832  deg1nn0clb  24845  deg1ge  24853  deg1tmle  24872  ply1divex  24891  plyco0  24943  coeeulem  24975  coeaddlem  25000  coe1termlem  25009  dgreq0  25016  dgrlt  25017  plydivex  25047  aannenlem1  25078  taylfvallem1  25106  tayl0  25111  radcnvlem1  25162  radcnvlem2  25163  dvradcnv  25170  leibpi  25682  log2tlbnd  25685  birthdaylem3  25693  zetacvg  25754  basellem2  25821  basellem3  25822  chpp1  25894  bcmono  26015  bcmax  26016  lgsdinn0  26083  2lgslem1c  26131  2sq2  26171  2sqreulem1  26184  2sqreultlem  26185  dchrisumlem1  26227  ostth2lem2  26372  nbusgrvtxm1  27323  upgrewlkle2  27550  pthdlem1  27709  crctcshwlkn0lem4  27753  crctcshwlkn0  27761  crctcsh  27764  wwlksm1edg  27821  wwlksnred  27832  wwlksnredwwlkn  27835  wwlksnredwwlkn0  27836  wwlksnextwrd  27837  wwlksnextfun  27838  wwlksnextinj  27839  wwlksnextproplem1  27849  wwlksnextproplem2  27850  wwlksnextproplem3  27851  clwlkclwwlklem2a1  27931  clwlkclwwlklem2a2  27932  clwlkclwwlklem2fv1  27934  clwlkclwwlklem2fv2  27935  clwlkclwwlklem2a4  27936  clwlkclwwlklem2a  27937  clwlkclwwlklem2  27939  clwlkclwwlk  27941  clwlkclwwlk2  27942  clwlkclwwlkf  27947  clwwisshclwwslem  27953  clwwlkel  27985  wwlksext2clwwlk  27996  clwlknf1oclwwlknlem1  28020  clwwlknonex2lem2  28047  eupth2lems  28177  eupth2  28178  eucrctshift  28182  numclwwlk7  28330  frgrreggt1  28332  frgrreg  28333  frgrogt3nreg  28336  friendship  28338  nn0xmulclb  30671  dpcl  30742  wrdt2ind  30802  hasheuni  31625  eulerpartlems  31899  hgt750lem  32203  0nn0m1nnn0  32644  derangen  32707  faclimlem1  33284  poimirlem28  35450  rrntotbnd  35639  factwoffsmonot  39776  gcdnn0id  39928  nacsfix  40128  eldioph2lem1  40176  irrapxlem4  40241  pell14qrgt0  40275  pell1qrgaplem  40289  pellqrexplicit  40293  rmxycomplete  40333  jm2.17a  40376  jm2.17b  40377  rmygeid  40380  jm2.22  40411  rmxdiophlem  40431  hbtlem5  40547  hbt  40549  fperiodmullem  42402  dvnxpaek  43047  stoweidlem17  43122  wallispilem3  43172  stirlinglem5  43183  stirlinglem7  43185  fourierdlem16  43228  fourierdlem21  43233  fourierdlem22  43234  fourierdlem83  43294  fourierdlem112  43323  elaa2lem  43338  etransclem23  43362  zm1nn  44357  nn0resubcl  44363  fz0addge0  44374  elfzlble  44375  subsubelfzo0  44381  2ffzoeq  44383  iccpartigtl  44438  lswn0  44459  sqrtpwpw2p  44553  fmtnodvds  44559  goldbachth  44562  odz2prm2pw  44578  flsqrt  44608  nn0e  44712  nn0sumltlt  45249  ply1mulgsumlem2  45291  nn0eo  45437  flnn0div2ge  45442  fllog2  45477  dignn0fr  45510  digexp  45516  dig2nn0  45520  0dig2nn0e  45521  dig2bits  45523  itcovalt2lem2lem1  45582