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

Theorem nnnn0 11907
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 11903 . 2 ℕ ⊆ ℕ0
21sseli 3965 1 (𝐴 ∈ ℕ → 𝐴 ∈ ℕ0)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2114  cn 11640  0cn0 11900
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-un 3943  df-in 3945  df-ss 3954  df-n0 11901
This theorem is referenced by:  nnnn0i  11908  elnnnn0b  11944  elnnnn0c  11945  elz2  12002  nn0ind-raph  12085  zindd  12086  fzo1fzo0n0  13091  ubmelfzo  13105  elfzom1elp1fzo  13107  fzo0sn0fzo1  13129  quoremnn0ALT  13228  modmulnn  13260  modsumfzodifsn  13315  addmodlteq  13317  expneg  13440  expcllem  13443  expcl2lem  13444  expeq0  13462  mulexpz  13472  expmordi  13534  rpexpmord  13535  expnlbnd  13597  expmulnbnd  13599  digit2  13600  digit1  13601  facmapnn  13648  facdiv  13650  faclbnd  13653  faclbnd3  13655  faclbnd4lem3  13658  faclbnd4lem4  13659  faclbnd5  13661  faclbnd6  13662  bcval5  13681  ishashinf  13824  iswrdi  13868  pfxn0  14050  repswfsts  14145  repswlsw  14146  repswcshw  14176  relexpnnrn  14406  relexpaddg  14414  absexpz  14667  isercoll  15026  summolem3  15073  summolem2a  15074  climcndslem2  15207  climcnds  15208  harmonic  15216  arisum  15217  expcnv  15221  geo2sum  15231  geo2lim  15233  geoisum1  15237  geoisum1c  15238  0.999...  15239  mertenslem2  15243  fallfacfwd  15392  0fallfac  15393  0risefac  15394  ef0lem  15434  ege2le3  15445  efaddlem  15448  efexp  15456  rpnnen2lem2  15570  rpnnen2lem4  15572  ruclem12  15596  dvdsmodexp  15617  nn0enne  15730  nnehalf  15732  nno  15735  nn0o  15736  pwp1fsum  15744  divalg2  15758  ndvdssub  15762  gcdmultiplez  15885  gcddiv  15901  gcdmultipleOLD  15902  gcdmultiplezOLD  15903  rpmulgcd  15908  rplpwr  15909  dvdssqlem  15912  eucalgf  15929  lcmflefac  15994  1nprm  16025  2mulprm  16039  isprm5  16053  isprm6  16060  prmdvdsexp  16061  phicl2  16107  phibndlem  16109  phiprmpw  16115  crth  16117  eulerthlem2  16121  hashgcdlem  16127  phisum  16129  pythagtriplem10  16159  pythagtriplem6  16160  pythagtriplem7  16161  pythagtriplem12  16165  pythagtriplem14  16167  pclem  16177  pcexp  16198  pcid  16211  pcprod  16233  pcbc  16238  prmpwdvds  16242  infpnlem1  16248  infpnlem2  16249  prmunb  16252  prmreclem6  16259  1arith  16265  vdwapf  16310  0hashbc  16345  ram0  16360  prmdvdsprmo  16380  prmdvdsprmop  16381  prmolefac  16384  prmgaplem1  16387  prmgaplem2  16388  prmgapprmolem  16399  prmgapprmo  16400  cshwrepswhash1  16438  smndex1n0mnd  18079  ghmmulg  18372  odmodnn0  18670  dfod2  18693  submod  18696  cply1mul  20464  cply1coe0  20469  cply1coe0bi  20470  prmirredlem  20642  prmirred  20644  znf1o  20700  znhash  20707  znfi  20708  znfld  20709  znidomb  20710  znunithash  20713  znrrg  20714  cpmatmcllem  21328  m2cpm  21351  m2cpminvid2lem  21364  fvmptnn04ifa  21460  chfacfisf  21464  chfacfisfcpmat  21465  chfacffsupp  21466  chfacfscmul0  21468  chfacfscmulfsupp  21469  chfacfscmulgsum  21470  chfacfpmmul0  21472  chfacfpmmulfsupp  21473  chfacfpmmulgsum  21474  chfacfpmmulgsum2  21475  cayhamlem1  21476  cpmadugsumlemF  21486  tgpmulg  22703  cmodscexp  23727  cphipval  23848  ovollb2lem  24091  ovoliunlem1  24105  ovoliunlem3  24107  uniioombllem3  24188  uniioombllem4  24189  opnmbllem  24204  mbfi1fseqlem1  24318  mbfi1fseqlem3  24320  mbfi1fseqlem4  24321  mbfi1fseqlem5  24322  mbfi1fseqlem6  24323  dvexp  24552  dvexp3  24577  plyco  24833  dgrcolem1  24865  plydivex  24888  aaliou3lem2  24934  aaliou3lem3  24935  aaliou3lem5  24938  aaliou3lem6  24939  aaliou3lem7  24940  aaliou3lem9  24941  radcnvlem2  25004  dvradcnv  25011  pserdv2  25020  abelthlem6  25026  abelthlem9  25030  logtayllem  25244  logtayl  25245  logtaylsum  25246  logtayl2  25247  cxproot  25275  root1id  25337  logbgcd1irr  25374  atantayl  25517  atantayl2  25518  leibpilem2  25521  leibpi  25522  birthdaylem2  25532  birthdaylem3  25533  dfef2  25550  basellem2  25661  basellem4  25663  basellem5  25664  basellem6  25665  basellem8  25667  isppw2  25694  vmappw  25695  sqf11  25718  vma1  25745  1sgm2ppw  25778  chtublem  25789  fsumvma2  25792  vmasum  25794  dchrelbas4  25821  dchrzrhcl  25823  dchrfi  25833  dchrhash  25849  pcbcctr  25854  bclbnd  25858  bposlem1  25862  lgsval4a  25897  lgsdchrval  25932  lgsdchr  25933  gausslemma2dlem0c  25936  gausslemma2dlem0d  25937  gausslemma2dlem6  25950  2lgslem1a1  25967  2lgslem1c  25971  2lgslem3a1  25978  2lgslem3b1  25979  2lgslem3c1  25980  2lgslem3d1  25981  2sqreunnlem1  26027  2sqreunnltblem  26029  rplogsumlem2  26063  dchrisumlem2  26068  ostth2lem1  26196  ostth2lem3  26213  ostth3  26216  cusgrsize2inds  27237  pthdivtx  27512  crctcshwlkn0lem4  27593  crctcshwlkn0lem5  27594  crctcshwlkn0lem7  27596  0enwwlksnge1  27644  rusgr0edg  27754  clwlkclwwlkf1lem2  27785  clwlkclwwlkf1lem3  27786  clwwisshclwwslem  27794  clwwlkinwwlk  27820  clwwlknfiOLD  27826  clwwlkel  27827  clwwlkf  27828  clwwlkf1  27830  clwwlknwwlksnb  27836  wwlksubclwwlk  27839  erclwwlknref  27850  clwwlknonwwlknonb  27887  numclwwlkqhash  28156  numclwwlk2lem1  28157  numclwlk2lem2f  28158  numclwlk2lem2f1o  28160  ipval2  28486  ipasslem3  28612  ipasslem4  28613  nn0min  30538  esumcst  31324  eulerpartlemb  31628  fibp1  31661  ballotlem1  31746  subfacp1lem6  32434  subfaclim  32437  subfacval3  32438  snmlff  32578  bcprod  32972  faclim2  32982  dvdspw  32984  nn0prpwlem  33672  knoppndvlem18  33870  opnmbllem0  34930  nnubfi  35027  nninfnub  35028  geomcau  35036  heiborlem5  35095  heiborlem6  35096  heiborlem7  35097  heiborlem8  35098  bfplem1  35102  nn0expgcd  39191  dffltz  39278  fltnltalem  39281  irrapxlem2  39427  pellexlem1  39433  pellexlem5  39437  pellqrex  39483  monotoddzzfi  39546  jm2.17c  39566  acongeq  39587  jm2.18  39592  jm2.23  39600  jm2.26lem3  39605  jm3.1  39624  expdiophlem1  39625  idomrootle  39802  idomodle  39803  proot1ex  39808  rp-isfinite6  39891  cnvtrclfv  40076  cotrclrcl  40094  inductionexd  40512  binomcxplemnotnn0  40695  nnne1ge2  41565  dvnmptconst  42233  stoweidlem3  42295  stoweidlem7  42299  stoweidlem34  42326  wallispilem4  42360  wallispilem5  42361  wallispi2lem1  42363  wallispi2lem2  42364  stirlinglem2  42367  stirlinglem3  42368  stirlinglem4  42369  stirlinglem5  42370  stirlinglem7  42372  stirlinglem11  42376  stirlinglem14  42379  stirlinglem15  42380  stirlingr  42382  fourierdlem15  42414  fourierdlem21  42420  fourierdlem22  42421  fourierdlem92  42490  fourierdlem112  42510  fouriersw  42523  sge0rpcpnf  42710  sge0ad2en  42720  ovnsubaddlem1  42859  ovnsubaddlem2  42860  ovolval5lem1  42941  ovolval5lem2  42942  iccpartiltu  43589  iccpartigtl  43590  iccpartlt  43591  iccpartleu  43595  iccpartrn  43597  iccelpart  43600  iccpartiun  43601  iccpartdisj  43604  sqrtpwpw2p  43707  fmtnosqrt  43708  odz2prm2pw  43732  fmtnoprmfac1lem  43733  fmtnoprmfac1  43734  2pwp1prm  43758  lighneallem1  43777  lighneallem2  43778  lighneallem3  43779  lighneallem4a  43780  lighneallem4  43782  nnpw2evenALTV  43874  dfwppr  43910  cznabel  44232  cznrng  44233  ztprmneprm  44402  altgsumbc  44407  altgsumbcALT  44408  pw2m1lepw2m1  44582  nneom  44594  logbpw2m1  44634  blennn  44642  blenpw2m1  44646  blengt1fldiv2p1  44660  dignn0ldlem  44669  dignnld  44670  dig2nn1st  44672  dignn0flhalflem1  44682  nn0sumshdiglemA  44686  nn0sumshdiglemB  44687  eenglngeehlnm  44733
  Copyright terms: Public domain W3C validator