Theorem nn0re 12440

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℝcr 11031  ℕ₀cn0 12431

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 2709  ax-sep 5232  ax-nul 5242  ax-pr 5371  ax-un 7683  ax-1cn 11090  ax-icn 11091  ax-addcl 11092  ax-addrcl 11093  ax-mulcl 11094  ax-mulrcl 11095  ax-i2m1 11100  ax-1ne0 11101  ax-rnegex 11103  ax-rrecex 11104  ax-cnre 11105

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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6260  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-ov 7364  df-om 7812  df-2nd 7937  df-frecs 8225  df-wrecs 8256  df-recs 8305  df-rdg 8343  df-nn 12169  df-n0 12432

This theorem is referenced by:  nn0ge0  12456  nn0nlt0  12457  nn0le0eq0  12459  nn0p1gt0  12460  elnnnn0c  12476  nn0addge1  12477  nn0addge2  12478  nn0sub  12481  ltsubnn0  12482  nn0negleid  12483  difgtsumgt  12484  nn0le2x  12485  nn0n0n1ge2b  12500  nn0ge2m1nn  12501  nn0nndivcl  12503  xnn0xr  12509  nn0nepnf  12512  xnn0nemnf  12515  elznn0nn  12532  nn0lt2  12586  nn0le2is012  12587  nn0ge0div  12592  nn01to3  12885  xnn0xaddcl  13181  xnn0lem1lt  13190  xnn0lenn0nn0  13191  xnn0xadd0  13193  nn0rp0  13402  xnn0xrge0  13453  nn0fz0  13573  elfz0fzfz0  13581  fz0fzelfz0  13582  fz0fzdiffz0  13585  fzctr  13588  difelfzle  13589  difelfznle  13590  fvffz0  13594  fzoun  13645  nn0p1elfzo  13651  elfzo0le  13652  fzonmapblen  13657  fzofzim  13658  elincfzoext  13672  elfzodifsumelfzo  13680  fzonn0p1  13691  fzonn0p1p1  13693  ssfzoulel  13709  ubmelm1fzo  13712  elfznelfzo  13722  fvinim0ffz  13738  subfzo0  13741  adddivflid  13771  divfl0  13777  fldivnn0le  13785  flltdivnn0lt  13786  quoremnn0ALT  13810  modmuladdnn0  13871  addmodid  13875  modifeq2int  13889  modfzo0difsn  13899  modsumfzodifsn  13900  addmodlteq  13902  ssnn0fi  13941  fsuppmapnn0fiub0  13949  suppssfz  13950  nn0sq11  14088  bernneq  14185  bernneq3  14187  facwordi  14245  faclbnd  14246  faclbnd3  14248  faclbnd5  14254  faclbnd6  14255  facubnd  14256  facavg  14257  bcval4  14263  bcval5  14274  bcpasc  14277  hashbnd  14292  hashnnn0genn0  14299  hashnemnf  14300  hashclb  14314  hashneq0  14320  hashsdom  14337  hashunsnggt  14350  fi1uzind  14463  ccat0  14532  ccat2s1fvw  14595  swrdnd0  14614  swrdsbslen  14621  swrdspsleq  14622  pfxnd0  14645  swrdswrdlem  14660  swrdswrd  14661  swrdccatin1  14681  pfxccatin12lem2  14687  pfxccatin12lem3  14688  pfxccat3  14690  swrdccat  14691  pfxccat3a  14694  swrdccat3blem  14695  repswswrd  14740  2cshw  14769  cshweqrep  14777  cshwcsh2id  14784  2swrd2eqwrdeq  14909  nn0sqeq1  15232  nn0absid  15386  isercoll  15624  o1fsum  15770  geomulcvg  15835  rerisefaccl  15976  refallfaccl  15977  rprisefaccl  15982  dvdseq  16277  oddge22np1  16312  nn0ehalf  16341  nn0o1gt2  16344  nn0o  16346  nn0oddm1d2  16348  bitsfi  16400  bitsinv1  16405  gcdn0gt0  16481  nn0gcdid0  16484  absmulgcd  16512  nn0seqcvgd  16533  algcvgblem  16540  algcvga  16542  lcmgcdnn  16574  lcmfun  16608  lcmfass  16609  prmfac1  16684  prmndvdsfaclt  16689  nonsq  16723  hashgcdlem  16752  odzdvds  16760  iserodd  16800  pcprendvds  16805  pcdvdsb  16834  pcidlem  16837  dvdsprmpweqle  16851  difsqpwdvds  16852  pcfaclem  16863  prmunb  16879  ramtcl2  16976  ramubcl  16983  ram0  16987  ramub1lem1  16991  cshwshashlem2  17061  smndex1iidm  18863  sylow1lem1  19567  pgpssslw  19583  efgsfo  19708  efgred  19717  telgsums  19962  prmirredlem  21465  prmirred  21467  gsumbagdiaglem  21923  psrridm  21954  psdmul  22145  coe1tmmul2  22254  gsummoncoe1  22286  mp2pm2mplem4  22787  fvmptnn04ifb  22829  chfacfisf  22832  chfacfisfcpmat  22833  chfacffsupp  22834  chfacfscmul0  22836  chfacfpmmul0  22840  dyaddisj  25576  mdegle0  26055  deg1nn0clb  26068  deg1ge  26076  deg1tmle  26096  ply1divex  26115  plyco0  26170  coeeulem  26202  coeaddlem  26227  coe1termlem  26236  dgreq0  26243  dgrlt  26244  plydivex  26277  aannenlem1  26308  taylfvallem1  26336  tayl0  26341  radcnvlem1  26394  radcnvlem2  26395  dvradcnv  26402  leibpi  26922  log2tlbnd  26925  birthdaylem3  26933  zetacvg  26995  basellem2  27062  basellem3  27063  chpp1  27135  bcmono  27257  bcmax  27258  lgsdinn0  27325  2lgslem1c  27373  2sq2  27413  2sqreulem1  27426  2sqreultlem  27427  dchrisumlem1  27469  ostth2lem2  27614  nbusgrvtxm1  29465  upgrewlkle2  29693  pthdlem1  29852  crctcshwlkn0lem4  29899  crctcshwlkn0  29907  crctcsh  29910  wwlksm1edg  29967  wwlksnred  29978  wwlksnredwwlkn  29981  wwlksnredwwlkn0  29982  wwlksnextwrd  29983  wwlksnextfun  29984  wwlksnextinj  29985  wwlksnextproplem1  29995  wwlksnextproplem2  29996  wwlksnextproplem3  29997  clwlkclwwlklem2a1  30080  clwlkclwwlklem2a2  30081  clwlkclwwlklem2fv1  30083  clwlkclwwlklem2fv2  30084  clwlkclwwlklem2a4  30085  clwlkclwwlklem2a  30086  clwlkclwwlklem2  30088  clwlkclwwlk  30090  clwlkclwwlk2  30091  clwlkclwwlkf  30096  clwwisshclwwslem  30102  clwwlkel  30134  wwlksext2clwwlk  30145  clwlknf1oclwwlknlem1  30169  clwwlknonex2lem2  30196  eupth2lems  30326  eupth2  30327  eucrctshift  30331  numclwwlk7  30479  frgrreggt1  30481  frgrreg  30482  frgrogt3nreg  30485  friendship  30487  nn0mnfxrd  32842  nn0xmulclb  32862  dpcl  32968  wrdt2ind  33031  hasheuni  34248  eulerpartlems  34523  hgt750lem  34814  0nn0m1nnn0  35314  derangen  35373  faclimlem1  35944  poimirlem28  37986  rrntotbnd  38174  sticksstones22  42624  gcdnn0id  42778  nn0addcom  42924  zaddcomlem  42925  nn0mulcom  42928  nacsfix  43161  eldioph2lem1  43209  irrapxlem4  43274  pell14qrgt0  43308  pell1qrgaplem  43322  pellqrexplicit  43326  rmxycomplete  43366  jm2.17a  43409  jm2.17b  43410  rmygeid  43413  jm2.22  43444  rmxdiophlem  43464  hbtlem5  43577  hbt  43579  fperiodmullem  45757  dvnxpaek  46391  stoweidlem17  46466  wallispilem3  46516  stirlinglem5  46527  stirlinglem7  46529  fourierdlem16  46572  fourierdlem21  46577  fourierdlem22  46578  fourierdlem83  46638  fourierdlem112  46667  elaa2lem  46682  etransclem23  46706  zm1nn  47765  nn0resubcl  47771  fz0addge0  47782  elfzlble  47783  subsubelfzo0  47790  2ffzoeq  47791  addmodne  47813  submodlt  47819  iccpartigtl  47898  lswn0  47919  sqrtpwpw2p  48016  fmtnodvds  48022  goldbachth  48025  odz2prm2pw  48041  flsqrt  48071  nn0e  48188  nn0sumltlt  48841  ply1mulgsumlem2  48878  nn0eo  49019  flnn0div2ge  49024  fllog2  49059  dignn0fr  49092  digexp  49098  dig2nn0  49102  0dig2nn0e  49103  dig2bits  49105  itcovalt2lem2lem1  49164