MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nn0re Structured version   Visualization version   GIF version

Theorem nn0re 11571
Description: A nonnegative integer is a real number. (Contributed by NM, 9-May-2004.)
Assertion
Ref Expression
nn0re (𝐴 ∈ ℕ0𝐴 ∈ ℝ)

Proof of Theorem nn0re
StepHypRef Expression
1 nn0ssre 11566 . 2 0 ⊆ ℝ
21sseli 3801 1 (𝐴 ∈ ℕ0𝐴 ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2157  cr 10223  0cn0 11562
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791  ax-sep 4982  ax-nul 4990  ax-pow 5042  ax-pr 5103  ax-un 7182  ax-1cn 10282  ax-icn 10283  ax-addcl 10284  ax-addrcl 10285  ax-mulcl 10286  ax-mulrcl 10287  ax-i2m1 10292  ax-1ne0 10293  ax-rnegex 10295  ax-rrecex 10296  ax-cnre 10297
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2638  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-ne 2986  df-ral 3108  df-rex 3109  df-reu 3110  df-rab 3112  df-v 3400  df-sbc 3641  df-csb 3736  df-dif 3779  df-un 3781  df-in 3783  df-ss 3790  df-pss 3792  df-nul 4124  df-if 4287  df-pw 4360  df-sn 4378  df-pr 4380  df-tp 4382  df-op 4384  df-uni 4638  df-iun 4721  df-br 4852  df-opab 4914  df-mpt 4931  df-tr 4954  df-id 5226  df-eprel 5231  df-po 5239  df-so 5240  df-fr 5277  df-we 5279  df-xp 5324  df-rel 5325  df-cnv 5326  df-co 5327  df-dm 5328  df-rn 5329  df-res 5330  df-ima 5331  df-pred 5900  df-ord 5946  df-on 5947  df-lim 5948  df-suc 5949  df-iota 6067  df-fun 6106  df-fn 6107  df-f 6108  df-f1 6109  df-fo 6110  df-f1o 6111  df-fv 6112  df-ov 6880  df-om 7299  df-wrecs 7645  df-recs 7707  df-rdg 7745  df-nn 11309  df-n0 11563
This theorem is referenced by:  nn0ge0  11587  nn0nlt0  11588  nn0le0eq0  11590  nn0p1gt0  11591  elnnnn0c  11607  nn0addge1  11608  nn0addge2  11609  nn0sub  11612  ltsubnn0  11613  nn0negleid  11614  difgtsumgt  11615  nn0n0n1ge2b  11628  nn0ge2m1nn  11629  nn0nndivcl  11631  xnn0xr  11637  nn0nepnf  11640  xnn0nemnf  11643  elznn0nn  11660  nn0lt2  11709  nn0le2is012  11710  nn0ge0div  11715  nn01to3  12003  xnn0xaddcl  12287  xnn0lenn0nn0  12296  xnn0xadd0  12298  nn0rp0  12502  xnn0xrge0  12551  nn0fz0  12664  elfz0fzfz0  12671  fz0fzelfz0  12672  fz0fzdiffz0  12675  fzctr  12678  difelfzle  12679  difelfznle  12680  fvffz0  12684  fzoun  12732  nn0p1elfzo  12738  elfzo0le  12739  fzonmapblen  12741  fzofzim  12742  elincfzoext  12753  elfzodifsumelfzo  12761  fzonn0p1  12772  fzonn0p1p1  12774  elfzom1p1elfzo  12775  ssfzoulel  12789  ubmelm1fzo  12791  elfznelfzo  12800  fvinim0ffz  12814  subfzo0  12817  adddivflid  12846  divfl0  12852  fldivnn0le  12860  flltdivnn0lt  12861  quoremnn0ALT  12883  modmuladdnn0  12941  addmodid  12945  modifeq2int  12959  modfzo0difsn  12969  modsumfzodifsn  12970  addmodlteq  12972  ssnn0fi  13011  fsuppmapnn0fiub0  13019  suppssfz  13020  bernneq  13216  bernneq3  13218  facwordi  13299  faclbnd  13300  faclbnd3  13302  faclbnd5  13308  faclbnd6  13309  facubnd  13310  facavg  13311  bcval4  13317  bcval5  13328  bcpasc  13331  hashbnd  13346  hashnnn0genn0  13354  hashnemnf  13355  hashclb  13370  hashneq0  13376  hashsdom  13391  fi1uzind  13499  brfi1indALT  13502  ccat0  13576  swrdsbslen  13675  swrdspsleq  13676  2swrdeqwrdeq  13680  swrdswrdlem  13686  swrdswrd  13687  swrdccatin1  13710  swrdccatin12lem2  13716  swrdccatin12lem3  13717  swrdccat3  13719  swrdccat  13720  swrdccat3blem  13722  swrdccatid  13724  repswswrd  13758  2cshw  13786  cshweqrep  13794  cshwcsh2id  13801  2swrd2eqwrdeq  13924  isercoll  14624  o1fsum  14770  geomulcvg  14832  rerisefaccl  14971  refallfaccl  14972  rprisefaccl  14977  dvdseq  15262  oddge22np1  15296  nn0ehalf  15318  nn0o1gt2  15320  nn0o  15322  nn0oddm1d2  15324  divalglem5  15343  bitsfi  15381  bitsinv1  15386  gcdn0gt0  15461  nn0gcdid0  15464  absmulgcd  15488  nn0seqcvgd  15505  algcvgblem  15512  algcvga  15514  lcmgcdnn  15546  lcmfun  15580  lcmfass  15581  prmfac1  15651  prmndvdsfaclt  15655  nonsq  15687  hashgcdlem  15713  odzdvds  15720  iserodd  15760  pcprendvds  15765  pcdvdsb  15793  pcidlem  15796  dvdsprmpweqle  15810  difsqpwdvds  15811  pcfaclem  15822  prmunb  15838  ramtcl2  15935  ramubcl  15942  ram0  15946  ramub1lem1  15950  cshwshashlem2  16018  sylow1lem1  18217  pgpssslw  18233  efgsfo  18356  efgred  18365  telgsums  18595  psrbagcon  19583  gsumbagdiaglem  19587  psrridm  19616  coe1tmmul2  19857  gsummoncoe1  19885  prmirredlem  20052  prmirred  20054  mp2pm2mplem4  20831  fvmptnn04ifb  20873  chfacfisf  20876  chfacfisfcpmat  20877  chfacffsupp  20878  chfacfscmul0  20880  chfacfpmmul0  20884  dyaddisj  23583  mdegle0  24057  deg1nn0clb  24070  deg1ge  24078  deg1tmle  24097  ply1divex  24116  plyco0  24168  coeeulem  24200  coeaddlem  24225  coe1termlem  24234  dgreq0  24241  dgrlt  24242  plydivex  24272  aannenlem1  24303  taylfvallem1  24331  tayl0  24336  radcnvlem1  24387  radcnvlem2  24388  dvradcnv  24395  leibpi  24889  log2tlbnd  24892  birthdaylem3  24900  zetacvg  24961  basellem2  25028  basellem3  25029  chpp1  25101  bcmono  25222  bcmax  25223  lgsdinn0  25290  2lgslem1c  25338  dchrisumlem1  25398  ostth2lem2  25543  nbusgrvtxm1  26503  upgrewlkle2  26736  pthdlem1  26896  crctcshwlkn0lem4  26940  crctcshwlkn0  26948  crctcsh  26951  wwlksm1edg  27014  wwlksnred  27035  wwlksnredwwlkn  27038  wwlksnredwwlkn0  27039  wwlksnextwrd  27040  wwlksnextfun  27041  wwlksnextinj  27042  wwlksnextproplem1  27053  wwlksnextproplem2  27054  wwlksnextproplem3  27055  clwlkclwwlklem2a1  27141  clwlkclwwlklem2a2  27142  clwlkclwwlklem2fv1  27144  clwlkclwwlklem2fv2  27145  clwlkclwwlklem2a4  27146  clwlkclwwlklem2a  27147  clwlkclwwlklem2  27149  clwlkclwwlk  27151  clwlkclwwlk2  27152  clwlkclwwlkf  27157  clwwisshclwwslem  27163  clwwlkel  27201  wwlksext2clwwlk  27213  wwlksext2clwwlkOLD  27214  clwlksf1clwwlklem1OLD  27245  clwlknf1oclwwlknlem1  27251  clwwlknonex2lem2  27283  eupth2lems  27417  eupth2  27418  eucrctshift  27422  numclwwlk7  27585  frgrreggt1  27587  frgrreg  27588  frgrogt3nreg  27591  friendship  27593  nn0sqeq1  29846  dpcl  29930  hasheuni  30478  eulerpartlems  30753  hgt750lem  31060  derangen  31482  faclimlem1  31956  poimirlem28  33752  rrntotbnd  33948  nacsfix  37778  eldioph2lem1  37826  irrapxlem4  37892  pell14qrgt0  37926  pell1qrgaplem  37940  pellqrexplicit  37944  rmxycomplete  37984  jm2.17a  38029  jm2.17b  38030  rmygeid  38033  jm2.22  38064  rmxdiophlem  38084  hbtlem5  38200  hbt  38202  fperiodmullem  39999  dvnxpaek  40638  stoweidlem17  40714  wallispilem3  40764  stirlinglem5  40775  stirlinglem7  40777  fourierdlem16  40820  fourierdlem21  40825  fourierdlem22  40826  fourierdlem83  40886  fourierdlem112  40915  elaa2lem  40930  etransclem23  40954  zm1nn  41893  nn0resubcl  41894  fz0addge0  41905  elfzlble  41906  subsubelfzo0  41912  2ffzoeq  41914  iccpartigtl  41935  lswn0  41956  pfx2  41988  pfxccatin12lem2  42000  pfxccat3  42002  pfxccat3a  42005  sqrtpwpw2p  42026  fmtnodvds  42032  goldbachth  42035  odz2prm2pw  42051  flsqrt  42084  nn0e  42184  nn0sumltlt  42697  ply1mulgsumlem2  42744  nn0eo  42891  flnn0div2ge  42896  fllog2  42931  dignn0fr  42964  digexp  42970  dig2nn0  42974  0dig2nn0e  42975  dig2bits  42977
  Copyright terms: Public domain W3C validator