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

Theorem nn0re 11148
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 11143 . 2 0 ⊆ ℝ
21sseli 3563 1 (𝐴 ∈ ℕ0𝐴 ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1976  cr 9791  0cn0 11139
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-i2m1 9860  ax-1ne0 9861  ax-rnegex 9863  ax-rrecex 9864  ax-cnre 9865
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-ral 2900  df-rex 2901  df-reu 2902  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-ov 6530  df-om 6935  df-wrecs 7271  df-recs 7332  df-rdg 7370  df-nn 10868  df-n0 11140
This theorem is referenced by:  nn0ge0  11165  nn0nlt0  11166  nn0le0eq0  11168  nn0p1gt0  11169  elnnnn0c  11185  nn0addge1  11186  nn0addge2  11187  nn0sub  11190  ltsubnn0  11191  nn0negleid  11192  difgtsumgt  11193  nn0n0n1ge2b  11206  nn0ge2m1nn  11207  nn0nndivcl  11209  elznn0nn  11224  nn0lt2  11273  nn0ge0div  11278  nn01to3  11613  nn0rp0  12106  nn0fz0  12261  elfz0fzfz0  12268  fz0fzelfz0  12269  fz0fzdiffz0  12272  fzctr  12275  difelfzle  12276  difelfznle  12277  fvffz0  12281  nn0p1elfzo  12333  elfzo0le  12334  fzonmapblen  12336  fzofzim  12337  elincfzoext  12348  elfzodifsumelfzo  12356  fzonn0p1  12366  fzonn0p1p1  12368  elfzom1p1elfzo  12369  ssfzoulel  12383  ubmelm1fzo  12385  elfznelfzo  12394  fvinim0ffz  12404  subfzo0  12407  adddivflid  12436  divfl0  12442  fldivnn0le  12450  flltdivnn0lt  12451  quoremnn0ALT  12473  modmuladdnn0  12531  addmodid  12535  modifeq2int  12549  modfzo0difsn  12559  modsumfzodifsn  12560  addmodlteq  12562  ssnn0fi  12601  fsuppmapnn0fiub0  12610  suppssfz  12611  bernneq  12807  bernneq3  12809  facwordi  12893  faclbnd  12894  faclbnd3  12896  faclbnd5  12902  faclbnd6  12903  facubnd  12904  facavg  12905  bcval4  12911  bcval5  12922  bcpasc  12925  hashbnd  12940  hashnnn0genn0  12945  hashnemnf  12946  hashclb  12963  hashneq0  12968  hashsdom  12983  fi1uzind  13080  brfi1indALT  13083  fi1uzindOLD  13086  brfi1indALTOLD  13089  swrdsbslen  13246  swrdspsleq  13247  2swrdeqwrdeq  13251  swrdswrdlem  13257  swrdswrd  13258  swrdccatin1  13280  swrdccatin12lem2  13286  swrdccatin12lem3  13287  swrdccat3  13289  swrdccat  13290  swrdccat3blem  13292  swrdccatid  13294  repswswrd  13328  2cshw  13356  cshweqrep  13364  cshwcsh2id  13371  2swrd2eqwrdeq  13490  isercoll  14192  o1fsum  14332  geomulcvg  14392  rerisefaccl  14533  refallfaccl  14534  rprisefaccl  14539  dvdseq  14820  oddge22np1  14857  nn0ehalf  14879  nn0o1gt2  14881  nn0o  14883  nn0oddm1d2  14885  divalglem5  14904  bitsfi  14943  bitsinv1  14948  gcdn0gt0  15023  nn0gcdid0  15026  absmulgcd  15050  nn0seqcvgd  15067  algcvgblem  15074  algcvga  15076  lcmgcdnn  15108  lcmfun  15142  lcmfass  15143  prmfac1  15215  prmndvdsfaclt  15219  nonsq  15251  hashgcdlem  15277  odzdvds  15284  iserodd  15324  pcprendvds  15329  pcdvdsb  15357  pcidlem  15360  dvdsprmpweqle  15374  difsqpwdvds  15375  pcfaclem  15386  prmunb  15402  ramtcl2  15499  ramubcl  15506  ram0  15510  ramub1lem1  15514  cshwshashlem2  15587  sylow1lem1  17782  pgpssslw  17798  efgsfo  17921  efgred  17930  telgsums  18159  psrbagcon  19138  gsumbagdiaglem  19142  psrridm  19171  coe1tmmul2  19413  gsummoncoe1  19441  prmirredlem  19605  prmirred  19607  mp2pm2mplem4  20375  fvmptnn04ifb  20417  chfacfisf  20420  chfacfisfcpmat  20421  chfacffsupp  20422  chfacfscmul0  20424  chfacfpmmul0  20428  dyaddisj  23087  mdegle0  23558  deg1nn0clb  23571  deg1ge  23579  deg1tmle  23598  ply1divex  23617  plyco0  23669  coeeulem  23701  coeaddlem  23726  coe1termlem  23735  dgreq0  23742  dgrlt  23743  plydivex  23773  aannenlem1  23804  taylfvallem1  23832  tayl0  23837  radcnvlem1  23888  radcnvlem2  23889  dvradcnv  23896  leibpi  24386  log2tlbnd  24389  birthdaylem3  24397  zetacvg  24458  basellem2  24525  basellem3  24526  chpp1  24598  bcmono  24719  bcmax  24720  lgsdinn0  24787  2lgslem1c  24835  dchrisumlem1  24895  ostth2lem2  25040  wlkonwlk  25831  cyclnspth  25925  nvnencycllem  25937  wwlknred  26017  wwlknredwwlkn  26020  wwlknredwwlkn0  26021  wwlkextwrd  26022  wwlkextfun  26023  wwlkextinj  26024  wwlkm1edg  26029  wwlkextproplem1  26035  wwlkextproplem2  26036  wwlkextproplem3  26037  clwwlkgt0  26065  clwwlkn0  26068  clwlkisclwwlklem2a1  26073  clwlkisclwwlklem2a2  26074  clwlkisclwwlklem2fv1  26076  clwlkisclwwlklem2fv2  26077  clwlkisclwwlklem2a4  26078  clwlkisclwwlklem2a  26079  clwlkisclwwlklem1  26081  clwlkisclwwlk2  26084  clwwlkel  26087  wwlkext2clwwlk  26097  clwwisshclwwlem  26100  clwlkfclwwlk1hash  26135  clwlkf1clwwlklem1  26139  vdgrf  26191  vdgrfif  26192  eupath2  26273  extwwlkfablem2  26371  numclwwlkovf2ex  26379  numclwwlk7  26407  frgrareggt1  26409  frgrareg  26410  frgraogt3nreg  26413  friendship  26415  nn0sqeq1  28707  hasheuni  29280  eulerpartlems  29555  derangen  30214  faclimlem1  30688  poimirlem28  32403  rrntotbnd  32601  nacsfix  36089  eldioph2lem1  36137  irrapxlem4  36203  pell14qrgt0  36237  pell1qrgaplem  36251  pellqrexplicit  36255  rmxycomplete  36296  jm2.17a  36341  jm2.17b  36342  rmygeid  36345  jm2.22  36376  rmxdiophlem  36396  hbtlem5  36513  hbt  36515  fperiodmullem  38254  dvnxpaek  38629  stoweidlem17  38707  wallispilem3  38757  stirlinglem5  38768  stirlinglem7  38770  fourierdlem16  38813  fourierdlem21  38818  fourierdlem22  38819  fourierdlem83  38879  fourierdlem112  38908  elaa2lem  38923  etransclem23  38947  iccpartigtl  39759  sqrtpwpw2p  39786  fmtnodvds  39792  goldbachth  39795  odz2prm2pw  39811  flsqrt  39844  nn0e  39944  lswn0  40040  pfx2  40073  pfxccatin12lem2  40085  pfxccat3  40087  pfxccat3a  40090  zm1nn  40168  nn0resubcl  40169  fz0addge0  40176  elfzlble  40177  subsubelfzo0  40179  2ffzoeq  40181  xnn0xr  40197  xnn0xrge0  40198  nn0nepnf  40201  xnn0nemnf  40204  xnn0xaddcl  40208  xnn0xadd0  40210  upgredg  40365  nbusgrvtxm1  40602  upgrewlkle2  40803  pthdlem1  40967  crctcsh1wlkn0lem4  41011  crctcsh1wlkn0  41019  crctcsh  41022  wwlksm1edg  41073  wwlksnred  41093  wwlksnredwwlkn  41096  wwlksnredwwlkn0  41097  wwlksnextwrd  41098  wwlksnextfun  41099  wwlksnextinj  41100  wwlksnextproplem2  41111  wwlksnextproplem3  41112  clwlkclwwlklem2a1  41196  clwlkclwwlklem2a2  41197  clwlkclwwlklem2fv1  41199  clwlkclwwlklem2fv2  41200  clwlkclwwlklem2a4  41201  clwlkclwwlklem2a  41202  clwlkclwwlklem2  41204  clwlkclwwlk  41206  clwlkclwwlk2  41207  clwwlksel  41216  wwlksext2clwwlk  41226  clwwisshclwwslem  41229  clwlksf1clwwlklem1  41267  eupth2lems  41401  eupth2  41402  eucrctshift  41406  av-numclwwlkovf2ex  41512  av-numclwwlk7  41540  av-frgrareggt1  41542  av-frgrareg  41543  av-frgraogt3nreg  41546  av-friendship  41548  nn0sumltlt  41916  nn0le2is012  41933  ply1mulgsumlem2  41964  nn0eo  42111  flnn0div2ge  42116  fllog2  42155  dignn0fr  42188  digexp  42194  dig2nn0  42198  0dig2nn0e  42199  dig2bits  42201  dpcl  42267
  Copyright terms: Public domain W3C validator