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

Theorem nn0re 11895
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 11890 . 2 0 ⊆ ℝ
21sseli 3967 1 (𝐴 ∈ ℕ0𝐴 ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  cr 10525  0cn0 11886
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326  ax-un 7451  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-i2m1 10594  ax-1ne0 10595  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-ral 3148  df-rex 3149  df-reu 3150  df-rab 3152  df-v 3502  df-sbc 3777  df-csb 3888  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-pss 3958  df-nul 4296  df-if 4471  df-pw 4544  df-sn 4565  df-pr 4567  df-tp 4569  df-op 4571  df-uni 4838  df-iun 4919  df-br 5064  df-opab 5126  df-mpt 5144  df-tr 5170  df-id 5459  df-eprel 5464  df-po 5473  df-so 5474  df-fr 5513  df-we 5515  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-pred 6146  df-ord 6192  df-on 6193  df-lim 6194  df-suc 6195  df-iota 6312  df-fun 6354  df-fn 6355  df-f 6356  df-f1 6357  df-fo 6358  df-f1o 6359  df-fv 6360  df-ov 7151  df-om 7569  df-wrecs 7938  df-recs 7999  df-rdg 8037  df-nn 11628  df-n0 11887
This theorem is referenced by:  nn0ge0  11911  nn0nlt0  11912  nn0le0eq0  11914  nn0p1gt0  11915  elnnnn0c  11931  nn0addge1  11932  nn0addge2  11933  nn0sub  11936  ltsubnn0  11937  nn0negleid  11938  difgtsumgt  11939  nn0n0n1ge2b  11952  nn0ge2m1nn  11953  nn0nndivcl  11955  xnn0xr  11961  nn0nepnf  11964  xnn0nemnf  11967  elznn0nn  11984  nn0lt2  12034  nn0le2is012  12035  nn0ge0div  12040  nn01to3  12330  xnn0xaddcl  12618  xnn0lem1lt  12627  xnn0lenn0nn0  12628  xnn0xadd0  12630  nn0rp0  12833  xnn0xrge0  12881  nn0fz0  12995  elfz0fzfz0  13002  fz0fzelfz0  13003  fz0fzdiffz0  13006  fzctr  13009  difelfzle  13010  difelfznle  13011  fvffz0  13015  fzoun  13064  nn0p1elfzo  13070  elfzo0le  13071  fzonmapblen  13073  fzofzim  13074  elincfzoext  13085  elfzodifsumelfzo  13093  fzonn0p1  13104  fzonn0p1p1  13106  ssfzoulel  13121  ubmelm1fzo  13123  elfznelfzo  13132  fvinim0ffz  13146  subfzo0  13149  adddivflid  13178  divfl0  13184  fldivnn0le  13192  flltdivnn0lt  13193  quoremnn0ALT  13215  modmuladdnn0  13273  addmodid  13277  modifeq2int  13291  modfzo0difsn  13301  modsumfzodifsn  13302  addmodlteq  13304  ssnn0fi  13343  fsuppmapnn0fiub0  13351  suppssfz  13352  nn0sq11  13487  bernneq  13580  bernneq3  13582  facwordi  13639  faclbnd  13640  faclbnd3  13642  faclbnd5  13648  faclbnd6  13649  facubnd  13650  facavg  13651  bcval4  13657  bcval5  13668  bcpasc  13671  hashbnd  13686  hashnnn0genn0  13693  hashnemnf  13694  hashclb  13709  hashneq0  13715  hashsdom  13732  hashunsnggt  13745  fi1uzind  13845  brfi1indALT  13848  ccat0  13919  ccat2s1fvw  13988  ccat2s1fvwOLD  13989  swrdnd0  14009  swrdsbslen  14016  swrdspsleq  14017  pfxnd0  14040  swrdswrdlem  14056  swrdswrd  14057  swrdccatin1  14077  pfxccatin12lem2  14083  pfxccatin12lem3  14084  pfxccat3  14086  swrdccat  14087  pfxccat3a  14090  swrdccat3blem  14091  repswswrd  14136  2cshw  14165  cshweqrep  14173  cshwcsh2id  14180  2swrd2eqwrdeq  14305  nn0sqeq1  14626  isercoll  15014  o1fsum  15158  geomulcvg  15222  rerisefaccl  15361  refallfaccl  15362  rprisefaccl  15367  dvdseq  15654  oddge22np1  15688  nn0ehalf  15719  nn0o1gt2  15722  nn0o  15724  nn0oddm1d2  15726  bitsfi  15776  bitsinv1  15781  gcdn0gt0  15856  nn0gcdid0  15859  absmulgcd  15887  nn0seqcvgd  15904  algcvgblem  15911  algcvga  15913  lcmgcdnn  15945  lcmfun  15979  lcmfass  15980  prmfac1  16053  prmndvdsfaclt  16057  nonsq  16089  hashgcdlem  16115  odzdvds  16122  iserodd  16162  pcprendvds  16167  pcdvdsb  16195  pcidlem  16198  dvdsprmpweqle  16212  difsqpwdvds  16213  pcfaclem  16224  prmunb  16240  ramtcl2  16337  ramubcl  16344  ram0  16348  ramub1lem1  16352  cshwshashlem2  16420  sylow1lem1  18643  pgpssslw  18659  efgsfo  18785  efgred  18794  telgsums  19033  psrbagcon  20070  gsumbagdiaglem  20074  psrridm  20103  coe1tmmul2  20361  gsummoncoe1  20389  prmirredlem  20556  prmirred  20558  mp2pm2mplem4  21333  fvmptnn04ifb  21375  chfacfisf  21378  chfacfisfcpmat  21379  chfacffsupp  21380  chfacfscmul0  21382  chfacfpmmul0  21386  dyaddisj  24112  mdegle0  24586  deg1nn0clb  24599  deg1ge  24607  deg1tmle  24626  ply1divex  24645  plyco0  24697  coeeulem  24729  coeaddlem  24754  coe1termlem  24763  dgreq0  24770  dgrlt  24771  plydivex  24801  aannenlem1  24832  taylfvallem1  24860  tayl0  24865  radcnvlem1  24916  radcnvlem2  24917  dvradcnv  24924  leibpi  25434  log2tlbnd  25437  birthdaylem3  25445  zetacvg  25506  basellem2  25573  basellem3  25574  chpp1  25646  bcmono  25767  bcmax  25768  lgsdinn0  25835  2lgslem1c  25883  2sq2  25923  2sqreulem1  25936  2sqreultlem  25937  dchrisumlem1  25979  ostth2lem2  26124  nbusgrvtxm1  27075  upgrewlkle2  27302  pthdlem1  27461  crctcshwlkn0lem4  27505  crctcshwlkn0  27513  crctcsh  27516  wwlksm1edg  27573  wwlksnred  27584  wwlksnredwwlkn  27587  wwlksnredwwlkn0  27588  wwlksnextwrd  27589  wwlksnextfun  27590  wwlksnextinj  27591  wwlksnextproplem1  27602  wwlksnextproplem2  27603  wwlksnextproplem3  27604  clwlkclwwlklem2a1  27684  clwlkclwwlklem2a2  27685  clwlkclwwlklem2fv1  27687  clwlkclwwlklem2fv2  27688  clwlkclwwlklem2a4  27689  clwlkclwwlklem2a  27690  clwlkclwwlklem2  27692  clwlkclwwlk  27694  clwlkclwwlk2  27695  clwlkclwwlkf  27700  clwwisshclwwslem  27706  clwwlkel  27739  wwlksext2clwwlk  27750  clwlknf1oclwwlknlem1  27774  clwwlknonex2lem2  27801  eupth2lems  27931  eupth2  27932  eucrctshift  27936  numclwwlk7  28084  frgrreggt1  28086  frgrreg  28087  frgrogt3nreg  28090  friendship  28092  nn0xmulclb  30409  dpcl  30481  wrdt2ind  30541  hasheuni  31230  eulerpartlems  31504  hgt750lem  31808  0nn0m1nnn0  32235  derangen  32303  faclimlem1  32859  poimirlem28  34787  rrntotbnd  34982  nacsfix  39174  eldioph2lem1  39222  irrapxlem4  39287  pell14qrgt0  39321  pell1qrgaplem  39335  pellqrexplicit  39339  rmxycomplete  39379  jm2.17a  39422  jm2.17b  39423  rmygeid  39426  jm2.22  39457  rmxdiophlem  39477  hbtlem5  39593  hbt  39595  fperiodmullem  41435  dvnxpaek  42092  stoweidlem17  42168  wallispilem3  42218  stirlinglem5  42229  stirlinglem7  42231  fourierdlem16  42274  fourierdlem21  42279  fourierdlem22  42280  fourierdlem83  42340  fourierdlem112  42369  elaa2lem  42384  etransclem23  42408  zm1nn  43368  nn0resubcl  43374  fz0addge0  43385  elfzlble  43386  subsubelfzo0  43392  2ffzoeq  43394  iccpartigtl  43415  lswn0  43436  sqrtpwpw2p  43532  fmtnodvds  43538  goldbachth  43541  odz2prm2pw  43557  flsqrt  43588  nn0e  43694  nn0sumltlt  44230  ply1mulgsumlem2  44273  nn0eo  44420  flnn0div2ge  44425  fllog2  44460  dignn0fr  44493  digexp  44499  dig2nn0  44503  0dig2nn0e  44504  dig2bits  44506
  Copyright terms: Public domain W3C validator