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

Theorem nnnn0 11337
Description: A positive integer is a nonnegative integer. (Contributed by NM, 9-May-2004.)
Assertion
Ref Expression
nnnn0 (𝐴 ∈ ℕ → 𝐴 ∈ ℕ0)

Proof of Theorem nnnn0
StepHypRef Expression
1 nnssnn0 11333 . 2 ℕ ⊆ ℕ0
21sseli 3632 1 (𝐴 ∈ ℕ → 𝐴 ∈ ℕ0)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2030  cn 11058  0cn0 11330
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-un 3612  df-in 3614  df-ss 3621  df-n0 11331
This theorem is referenced by:  nnnn0i  11338  elnnnn0b  11375  elnnnn0c  11376  elz2  11432  nn0ind-raph  11515  zindd  11516  fzo1fzo0n0  12558  ubmelfzo  12572  elfzom1elp1fzo  12574  fzo0sn0fzo1  12597  quoremnn0ALT  12696  modmulnn  12728  modsumfzodifsn  12783  addmodlteq  12785  expneg  12908  expcllem  12911  expcl2lem  12912  expeq0  12930  mulexpz  12940  expnlbnd  13034  expmulnbnd  13036  digit2  13037  digit1  13038  facmapnn  13112  facdiv  13114  faclbnd  13117  faclbnd3  13119  faclbnd4lem3  13122  faclbnd4lem4  13123  faclbnd5  13125  faclbnd6  13126  bcval5  13145  ishashinf  13285  iswrdi  13341  swrdn0  13476  swrdtrcfv  13487  swrdccatwrd  13514  repswfsts  13574  repswlsw  13575  repswcshw  13604  relexpnnrn  13829  relexpaddg  13837  absexpz  14089  isercoll  14442  summolem3  14489  summolem2a  14490  climcndslem2  14626  climcnds  14627  harmonic  14635  arisum  14636  expcnv  14640  geo2sum  14648  geo2lim  14650  geoisum1  14654  geoisum1c  14655  0.999...  14656  0.999...OLD  14657  mertenslem2  14661  fallfacfwd  14811  0fallfac  14812  0risefac  14813  ef0lem  14853  ege2le3  14864  efaddlem  14867  efexp  14875  rpnnen2lem2  14988  rpnnen2lem4  14990  ruclem12  15014  dvdsmodexp  15035  nn0enne  15141  nnehalf  15143  nno  15145  nn0o  15146  pwp1fsum  15161  divalg2  15175  ndvdssub  15180  gcddiv  15315  gcdmultiple  15316  gcdmultiplez  15317  rpmulgcd  15322  rplpwr  15323  dvdssqlem  15326  eucalgf  15343  lcmflefac  15408  1nprm  15439  isprm5  15466  isprm6  15473  prmdvdsexp  15474  phicl2  15520  phibndlem  15522  phiprmpw  15528  crth  15530  eulerthlem2  15534  hashgcdlem  15540  phisum  15542  pythagtriplem10  15572  pythagtriplem6  15573  pythagtriplem7  15574  pythagtriplem12  15578  pythagtriplem14  15580  pclem  15590  pcexp  15611  pcid  15624  pcprod  15646  pcbc  15651  prmpwdvds  15655  infpnlem1  15661  infpnlem2  15662  prmunb  15665  prmreclem6  15672  1arith  15678  vdwapf  15723  0hashbc  15758  ram0  15773  prmdvdsprmo  15793  prmdvdsprmop  15794  prmolefac  15797  prmgaplem1  15800  prmgaplem2  15801  prmgapprmolem  15812  prmgapprmo  15813  cshwrepswhash1  15856  ghmmulg  17719  odmodnn0  18005  dfod2  18027  submod  18030  cply1mul  19712  cply1coe0  19717  cply1coe0bi  19718  prmirredlem  19889  prmirred  19891  znf1o  19948  znhash  19955  znfi  19956  znfld  19957  znidomb  19958  znunithash  19961  znrrg  19962  cpmatmcllem  20571  m2cpm  20594  m2cpminvid2lem  20607  fvmptnn04ifa  20703  chfacfisf  20707  chfacfisfcpmat  20708  chfacffsupp  20709  chfacfscmul0  20711  chfacfscmulfsupp  20712  chfacfscmulgsum  20713  chfacfpmmul0  20715  chfacfpmmulfsupp  20716  chfacfpmmulgsum  20717  chfacfpmmulgsum2  20718  cayhamlem1  20719  cpmadugsumlemF  20729  tgpmulg  21944  cmodscexp  22967  cphipval  23088  ovollb2lem  23302  ovoliunlem1  23316  ovoliunlem3  23318  uniioombllem3  23399  uniioombllem4  23400  opnmbllem  23415  mbfi1fseqlem1  23527  mbfi1fseqlem3  23529  mbfi1fseqlem4  23530  mbfi1fseqlem5  23531  mbfi1fseqlem6  23532  dvexp  23761  dvexp3  23786  plyco  24042  dgrcolem1  24074  plydivex  24097  aaliou3lem2  24143  aaliou3lem3  24144  aaliou3lem5  24147  aaliou3lem6  24148  aaliou3lem7  24149  aaliou3lem9  24150  radcnvlem2  24213  dvradcnv  24220  pserdv2  24229  abelthlem6  24235  abelthlem9  24239  logtayllem  24450  logtayl  24451  logtaylsum  24452  logtayl2  24453  cxproot  24481  root1id  24540  atantayl  24709  atantayl2  24710  leibpilem2  24713  leibpi  24714  birthdaylem2  24724  birthdaylem3  24725  dfef2  24742  basellem2  24853  basellem4  24855  basellem5  24856  basellem6  24857  basellem8  24859  isppw2  24886  vmappw  24887  sqf11  24910  vma1  24937  1sgm2ppw  24970  chtublem  24981  fsumvma2  24984  vmasum  24986  dchrelbas4  25013  dchrzrhcl  25015  dchrfi  25025  dchrhash  25041  pcbcctr  25046  bclbnd  25050  bposlem1  25054  lgsval4a  25089  lgsdchrval  25124  lgsdchr  25125  gausslemma2dlem0c  25128  gausslemma2dlem0d  25129  gausslemma2dlem6  25142  2lgslem1a1  25159  2lgslem1c  25163  2lgslem3a1  25170  2lgslem3b1  25171  2lgslem3c1  25172  2lgslem3d1  25173  rplogsumlem2  25219  dchrisumlem2  25224  ostth2lem1  25352  ostth2lem3  25369  ostth3  25372  cusgrsize2inds  26405  pthdivtx  26681  crctcshwlkn0lem4  26761  crctcshwlkn0lem5  26762  crctcshwlkn0lem7  26764  0enwwlksnge1  26818  rusgr0edg  26940  clwwlknclwwlkdifnumOLD  26948  clwwisshclwwslem  26971  clwwlkinwwlk  27003  clwwlknfi  27008  clwwlkel  27009  clwwlkf  27010  clwwlkf1  27012  clwwlknwwlksnb  27019  wwlksubclwwlk  27023  erclwwlknref  27033  clwlksf1clwwlklem  27055  clwwlknonelOLD  27071  clwwlknonwwlknonb  27080  clwwlknonwwlknonbOLD  27081  numclwwlkqhash  27355  numclwwlk2lem1  27356  numclwlk2lem2f  27357  numclwlk2lem2f1o  27359  numclwwlk2lem1OLD  27363  numclwlk2lem2fOLD  27364  ipval2  27690  ipasslem3  27816  ipasslem4  27817  nn0min  29695  esumcst  30253  eulerpartlemb  30558  fibp1  30591  ballotlem1  30676  subfacp1lem6  31293  subfaclim  31296  subfacval3  31297  snmlff  31437  bcprod  31750  faclim2  31760  dvdspw  31762  nn0prpwlem  32442  knoppndvlem18  32645  opnmbllem0  33575  nnubfi  33676  nninfnub  33677  geomcau  33685  heiborlem5  33744  heiborlem6  33745  heiborlem7  33746  heiborlem8  33747  bfplem1  33751  irrapxlem2  37704  pellexlem1  37710  pellexlem5  37714  pellqrex  37760  monotoddzzfi  37824  expmordi  37829  rpexpmord  37830  jm2.17c  37846  acongeq  37867  jm2.18  37872  jm2.23  37880  jm2.26lem3  37885  jm3.1  37904  expdiophlem1  37905  idomrootle  38090  idomodle  38091  proot1ex  38096  rp-isfinite6  38181  cnvtrclfv  38333  cotrclrcl  38351  inductionexd  38770  binomcxplemnotnn0  38872  nnne1ge2  39818  dvnmptconst  40474  stoweidlem3  40538  stoweidlem7  40542  stoweidlem34  40569  wallispilem4  40603  wallispilem5  40604  wallispi2lem1  40606  wallispi2lem2  40607  stirlinglem2  40610  stirlinglem3  40611  stirlinglem4  40612  stirlinglem5  40613  stirlinglem7  40615  stirlinglem11  40619  stirlinglem14  40622  stirlinglem15  40623  stirlingr  40625  fourierdlem15  40657  fourierdlem21  40663  fourierdlem22  40664  fourierdlem92  40733  fourierdlem112  40753  fouriersw  40766  sge0rpcpnf  40956  sge0ad2en  40966  ovnsubaddlem1  41105  ovnsubaddlem2  41106  ovolval5lem1  41187  ovolval5lem2  41188  iccpartiltu  41683  iccpartigtl  41684  iccpartlt  41685  iccpartleu  41689  iccpartrn  41691  iccelpart  41694  iccpartiun  41695  iccpartdisj  41698  pfxn0  41719  sqrtpwpw2p  41775  fmtnosqrt  41776  odz2prm2pw  41800  fmtnoprmfac1lem  41801  fmtnoprmfac1  41802  2pwp1prm  41828  lighneallem1  41847  lighneallem2  41848  lighneallem3  41849  lighneallem4a  41850  lighneallem4  41852  nnpw2evenALTV  41936  cznabel  42279  cznrng  42280  ztprmneprm  42450  altgsumbc  42455  altgsumbcALT  42456  pw2m1lepw2m1  42635  nneom  42646  logbpw2m1  42686  blennn  42694  blenpw2m1  42698  blengt1fldiv2p1  42712  dignn0ldlem  42721  dignnld  42722  dig2nn1st  42724  dignn0flhalflem1  42734  nn0sumshdiglemA  42738  nn0sumshdiglemB  42739
  Copyright terms: Public domain W3C validator