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

Theorem nnnn0 11176
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 11172 . 2 ℕ ⊆ ℕ0
21sseli 3564 1 (𝐴 ∈ ℕ → 𝐴 ∈ ℕ0)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1977  cn 10897  0cn0 11169
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-un 3545  df-in 3547  df-ss 3554  df-n0 11170
This theorem is referenced by:  nnnn0i  11177  elnnnn0b  11214  elnnnn0c  11215  elz2  11271  nn0ind-raph  11353  zindd  11354  fzo1fzo0n0  12386  ubmelfzo  12400  elfzom1elp1fzo  12402  fzo0sn0fzo1  12424  quoremnn0ALT  12518  modmulnn  12550  modsumfzodifsn  12605  addmodlteq  12607  expneg  12730  expcllem  12733  expcl2lem  12734  expeq0  12752  mulexpz  12762  expnlbnd  12856  expmulnbnd  12858  digit2  12859  digit1  12860  facmapnn  12934  facdiv  12936  faclbnd  12939  faclbnd3  12941  faclbnd4lem3  12944  faclbnd4lem4  12945  faclbnd5  12947  faclbnd6  12948  bcval5  12967  ishashinf  13104  iswrdi  13164  swrdn0  13282  swrdtrcfv  13293  swrdccatwrd  13320  repswfsts  13379  repswlsw  13380  repswcshw  13409  relexpnnrn  13633  relexpaddg  13641  absexpz  13893  isercoll  14246  summolem3  14292  summolem2a  14293  climcndslem2  14421  climcnds  14422  harmonic  14430  arisum  14431  expcnv  14435  geo2sum  14443  geo2lim  14445  geoisum1  14449  geoisum1c  14450  0.999...  14451  0.999...OLD  14452  mertenslem2  14456  fallfacfwd  14606  0fallfac  14607  0risefac  14608  ef0lem  14648  ege2le3  14659  efaddlem  14662  efexp  14670  rpnnen2lem2  14783  rpnnen2lem4  14785  ruclem12  14809  nn0enne  14932  nnehalf  14934  nno  14936  nn0o  14937  pwp1fsum  14952  divalg2  14966  ndvdssub  14971  gcddiv  15106  gcdmultiple  15107  gcdmultiplez  15108  rpmulgcd  15113  rplpwr  15114  dvdssqlem  15117  eucalgf  15134  lcmflefac  15199  1nprm  15230  isprm5  15257  isprm6  15264  prmdvdsexp  15265  phicl2  15311  phibndlem  15313  phiprmpw  15319  crth  15321  eulerthlem2  15325  hashgcdlem  15331  phisum  15333  pythagtriplem10  15363  pythagtriplem6  15364  pythagtriplem7  15365  pythagtriplem12  15369  pythagtriplem14  15371  pclem  15381  pcexp  15402  pcid  15415  pcprod  15437  pcbc  15442  prmpwdvds  15446  infpnlem1  15452  infpnlem2  15453  prmunb  15456  prmreclem6  15463  1arith  15469  vdwapf  15514  0hashbc  15549  ram0  15564  prmdvdsprmo  15584  prmdvdsprmop  15585  prmolefac  15588  prmgaplem1  15591  prmgaplem2  15592  prmgapprmolem  15603  prmgapprmo  15604  cshwrepswhash1  15647  ghmmulg  17495  odmodnn0  17782  dfod2  17804  submod  17807  cply1mul  19485  cply1coe0  19490  cply1coe0bi  19491  prmirredlem  19660  prmirred  19662  znf1o  19719  znhash  19726  znfi  19727  znfld  19728  znidomb  19729  znunithash  19732  znrrg  19733  cpmatmcllem  20342  m2cpm  20365  m2cpminvid2lem  20378  fvmptnn04ifa  20474  chfacfisf  20478  chfacfisfcpmat  20479  chfacffsupp  20480  chfacfscmul0  20482  chfacfscmulfsupp  20483  chfacfscmulgsum  20484  chfacfpmmul0  20486  chfacfpmmulfsupp  20487  chfacfpmmulgsum  20488  chfacfpmmulgsum2  20489  cayhamlem1  20490  cpmadugsumlemF  20500  tgpmulg  21707  cmodscexp  22729  cphipval  22850  ovollb2lem  23063  ovoliunlem1  23077  ovoliunlem3  23079  uniioombllem3  23159  uniioombllem4  23160  opnmbllem  23175  mbfi1fseqlem1  23288  mbfi1fseqlem3  23290  mbfi1fseqlem4  23291  mbfi1fseqlem5  23292  mbfi1fseqlem6  23293  dvexp  23522  dvexp3  23545  plyco  23801  dgrcolem1  23833  plydivex  23856  aaliou3lem2  23902  aaliou3lem3  23903  aaliou3lem5  23906  aaliou3lem6  23907  aaliou3lem7  23908  aaliou3lem9  23909  radcnvlem2  23972  dvradcnv  23979  pserdv2  23988  abelthlem6  23994  abelthlem9  23998  logtayllem  24205  logtayl  24206  logtaylsum  24207  logtayl2  24208  cxproot  24236  root1id  24295  atantayl  24464  atantayl2  24465  leibpilem2  24468  leibpi  24469  birthdaylem2  24479  birthdaylem3  24480  dfef2  24497  basellem2  24608  basellem4  24610  basellem5  24611  basellem6  24612  basellem8  24614  isppw2  24641  vmappw  24642  sqf11  24665  vma1  24692  1sgm2ppw  24725  chtublem  24736  fsumvma2  24739  vmasum  24741  dchrelbas4  24768  dchrzrhcl  24770  dchrfi  24780  dchrhash  24796  pcbcctr  24801  bclbnd  24805  bposlem1  24809  lgsval4a  24844  lgsdchrval  24879  lgsdchr  24880  gausslemma2dlem0c  24883  gausslemma2dlem0d  24884  gausslemma2dlem6  24897  2lgslem1a1  24914  2lgslem1c  24918  2lgslem3a1  24925  2lgslem3b1  24926  2lgslem3c1  24927  2lgslem3d1  24928  rplogsumlem2  24974  dchrisumlem2  24979  ostth2lem1  25107  ostth2lem3  25124  ostth3  25127  cusgrasize2inds  26005  cyclnspth  26159  clwwlkel  26321  clwwlkf  26322  clwwlkf1  26324  wwlksubclwwlk  26332  clwwisshclwwlem  26334  clwlkf1clwwlklem  26376  rusgra0edg  26482  clwlknclwlkdifnum  26488  clwwlkextfrlem1  26603  numclwwlkqhash  26627  numclwwlk2lem1  26629  numclwlk2lem2f  26630  numclwlk2lem2f1o  26632  ipval2  26946  ipasslem3  27072  ipasslem4  27073  nn0min  28954  esumcst  29452  eulerpartlemb  29757  fibp1  29790  ballotlem1  29875  subfacp1lem6  30421  subfaclim  30424  subfacval3  30425  snmlff  30565  bcprod  30877  faclim2  30887  dvdspw  30889  nn0prpwlem  31487  knoppndvlem18  31690  opnmbllem0  32615  nnubfi  32716  nninfnub  32717  geomcau  32725  heiborlem5  32784  heiborlem6  32785  heiborlem7  32786  heiborlem8  32787  bfplem1  32791  irrapxlem2  36405  pellexlem1  36411  pellexlem5  36415  pellqrex  36461  monotoddzzfi  36525  expmordi  36530  rpexpmord  36531  jm2.17c  36547  acongeq  36568  jm2.18  36573  jm2.23  36581  jm2.26lem3  36586  jm3.1  36605  expdiophlem1  36606  idomrootle  36792  idomodle  36793  proot1ex  36798  rp-isfinite6  36883  cnvtrclfv  37035  cotrclrcl  37053  inductionexd  37473  binomcxplemnotnn0  37577  nnne1ge2  38445  dvnmptconst  38831  stoweidlem3  38896  stoweidlem7  38900  stoweidlem34  38927  wallispilem4  38961  wallispilem5  38962  wallispi2lem1  38964  wallispi2lem2  38965  stirlinglem2  38968  stirlinglem3  38969  stirlinglem4  38970  stirlinglem5  38971  stirlinglem7  38973  stirlinglem11  38977  stirlinglem14  38980  stirlinglem15  38981  stirlingr  38983  fourierdlem15  39015  fourierdlem21  39021  fourierdlem22  39022  fourierdlem92  39091  fourierdlem112  39111  fouriersw  39124  sge0rpcpnf  39314  sge0ad2en  39324  ovnsubaddlem1  39460  ovnsubaddlem2  39461  ovolval5lem1  39542  ovolval5lem2  39543  iccpartiltu  39960  iccpartigtl  39961  iccpartlt  39962  iccpartleu  39966  iccpartrn  39968  iccelpart  39971  iccpartiun  39972  iccpartdisj  39975  sqrtpwpw2p  39988  fmtnosqrt  39989  odz2prm2pw  40013  fmtnoprmfac1lem  40014  fmtnoprmfac1  40015  2pwp1prm  40041  lighneallem1  40060  lighneallem2  40061  lighneallem3  40062  lighneallem4a  40063  lighneallem4  40065  nnpw2evenALTV  40149  pfxn0  40257  cusgrsize2inds  40669  pthdivtx  40935  crctcsh1wlkn0lem4  41016  crctcsh1wlkn0lem5  41017  crctcsh1wlkn0lem7  41019  0enwwlksnge1  41060  wspniunwspnon  41130  rusgr0edg  41176  clwwlknclwwlkdifnum  41182  clwwlksnfi  41220  clwwlksel  41221  clwwlksf  41222  clwwlksf1  41224  wwlksubclwwlks  41232  clwwisshclwwslem  41234  erclwwlksnref  41253  clwlksf1clwwlklem  41275  av-numclwwlk2lem1  41532  av-numclwlk2lem2f  41533  av-numclwwlk4  41540  cznabel  41746  cznrng  41747  ztprmneprm  41918  altgsumbc  41923  altgsumbcALT  41924  pw2m1lepw2m1  42104  nneom  42115  logbpw2m1  42159  blennn  42167  blenpw2m1  42171  blengt1fldiv2p1  42185  dignn0ldlem  42194  dignnld  42195  dig2nn1st  42197  dignn0flhalflem1  42207  nn0sumshdiglemA  42211  nn0sumshdiglemB  42212
  Copyright terms: Public domain W3C validator