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

Theorem nnnn0 11893
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 11889 . 2 ℕ ⊆ ℕ0
21sseli 3962 1 (𝐴 ∈ ℕ → 𝐴 ∈ ℕ0)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  cn 11627  0cn0 11886
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3497  df-un 3940  df-in 3942  df-ss 3951  df-n0 11887
This theorem is referenced by:  nnnn0i  11894  elnnnn0b  11930  elnnnn0c  11931  elz2  11988  nn0ind-raph  12071  zindd  12072  fzo1fzo0n0  13078  ubmelfzo  13092  elfzom1elp1fzo  13094  fzo0sn0fzo1  13116  quoremnn0ALT  13215  modmulnn  13247  modsumfzodifsn  13302  addmodlteq  13304  expneg  13427  expcllem  13430  expcl2lem  13431  expeq0  13449  mulexpz  13459  expmordi  13521  rpexpmord  13522  expnlbnd  13584  expmulnbnd  13586  digit2  13587  digit1  13588  facmapnn  13635  facdiv  13637  faclbnd  13640  faclbnd3  13642  faclbnd4lem3  13645  faclbnd4lem4  13646  faclbnd5  13648  faclbnd6  13649  bcval5  13668  ishashinf  13811  iswrdi  13855  pfxn0  14038  repswfsts  14133  repswlsw  14134  repswcshw  14164  relexpnnrn  14394  relexpaddg  14402  absexpz  14655  isercoll  15014  summolem3  15061  summolem2a  15062  climcndslem2  15195  climcnds  15196  harmonic  15204  arisum  15205  expcnv  15209  geo2sum  15219  geo2lim  15221  geoisum1  15225  geoisum1c  15226  0.999...  15227  mertenslem2  15231  fallfacfwd  15380  0fallfac  15381  0risefac  15382  ef0lem  15422  ege2le3  15433  efaddlem  15436  efexp  15444  rpnnen2lem2  15558  rpnnen2lem4  15560  ruclem12  15584  dvdsmodexp  15605  nn0enne  15718  nnehalf  15720  nno  15723  nn0o  15724  pwp1fsum  15732  divalg2  15746  ndvdssub  15750  gcdmultiplez  15873  gcddiv  15889  gcdmultipleOLD  15890  gcdmultiplezOLD  15891  rpmulgcd  15896  rplpwr  15897  dvdssqlem  15900  eucalgf  15917  lcmflefac  15982  1nprm  16013  2mulprm  16027  isprm5  16041  isprm6  16048  prmdvdsexp  16049  phicl2  16095  phibndlem  16097  phiprmpw  16103  crth  16105  eulerthlem2  16109  hashgcdlem  16115  phisum  16117  pythagtriplem10  16147  pythagtriplem6  16148  pythagtriplem7  16149  pythagtriplem12  16153  pythagtriplem14  16155  pclem  16165  pcexp  16186  pcid  16199  pcprod  16221  pcbc  16226  prmpwdvds  16230  infpnlem1  16236  infpnlem2  16237  prmunb  16240  prmreclem6  16247  1arith  16253  vdwapf  16298  0hashbc  16333  ram0  16348  prmdvdsprmo  16368  prmdvdsprmop  16369  prmolefac  16372  prmgaplem1  16375  prmgaplem2  16376  prmgapprmolem  16387  prmgapprmo  16388  cshwrepswhash1  16426  ghmmulg  18310  odmodnn0  18599  dfod2  18622  submod  18625  cply1mul  20392  cply1coe0  20397  cply1coe0bi  20398  prmirredlem  20570  prmirred  20572  znf1o  20628  znhash  20635  znfi  20636  znfld  20637  znidomb  20638  znunithash  20641  znrrg  20642  cpmatmcllem  21256  m2cpm  21279  m2cpminvid2lem  21292  fvmptnn04ifa  21388  chfacfisf  21392  chfacfisfcpmat  21393  chfacffsupp  21394  chfacfscmul0  21396  chfacfscmulfsupp  21397  chfacfscmulgsum  21398  chfacfpmmul0  21400  chfacfpmmulfsupp  21401  chfacfpmmulgsum  21402  chfacfpmmulgsum2  21403  cayhamlem1  21404  cpmadugsumlemF  21414  tgpmulg  22631  cmodscexp  23654  cphipval  23775  ovollb2lem  24018  ovoliunlem1  24032  ovoliunlem3  24034  uniioombllem3  24115  uniioombllem4  24116  opnmbllem  24131  mbfi1fseqlem1  24245  mbfi1fseqlem3  24247  mbfi1fseqlem4  24248  mbfi1fseqlem5  24249  mbfi1fseqlem6  24250  dvexp  24479  dvexp3  24504  plyco  24760  dgrcolem1  24792  plydivex  24815  aaliou3lem2  24861  aaliou3lem3  24862  aaliou3lem5  24865  aaliou3lem6  24866  aaliou3lem7  24867  aaliou3lem9  24868  radcnvlem2  24931  dvradcnv  24938  pserdv2  24947  abelthlem6  24953  abelthlem9  24957  logtayllem  25169  logtayl  25170  logtaylsum  25171  logtayl2  25172  cxproot  25200  root1id  25262  logbgcd1irr  25299  atantayl  25442  atantayl2  25443  leibpilem2  25447  leibpi  25448  birthdaylem2  25458  birthdaylem3  25459  dfef2  25476  basellem2  25587  basellem4  25589  basellem5  25590  basellem6  25591  basellem8  25593  isppw2  25620  vmappw  25621  sqf11  25644  vma1  25671  1sgm2ppw  25704  chtublem  25715  fsumvma2  25718  vmasum  25720  dchrelbas4  25747  dchrzrhcl  25749  dchrfi  25759  dchrhash  25775  pcbcctr  25780  bclbnd  25784  bposlem1  25788  lgsval4a  25823  lgsdchrval  25858  lgsdchr  25859  gausslemma2dlem0c  25862  gausslemma2dlem0d  25863  gausslemma2dlem6  25876  2lgslem1a1  25893  2lgslem1c  25897  2lgslem3a1  25904  2lgslem3b1  25905  2lgslem3c1  25906  2lgslem3d1  25907  2sqreunnlem1  25953  2sqreunnltblem  25955  rplogsumlem2  25989  dchrisumlem2  25994  ostth2lem1  26122  ostth2lem3  26139  ostth3  26142  cusgrsize2inds  27163  pthdivtx  27438  crctcshwlkn0lem4  27519  crctcshwlkn0lem5  27520  crctcshwlkn0lem7  27522  0enwwlksnge1  27570  rusgr0edg  27680  clwlkclwwlkf1lem2  27711  clwlkclwwlkf1lem3  27712  clwwisshclwwslem  27720  clwwlkinwwlk  27746  clwwlknfiOLD  27752  clwwlkel  27753  clwwlkf  27754  clwwlkf1  27756  clwwlknwwlksnb  27762  wwlksubclwwlk  27765  erclwwlknref  27776  clwwlknonwwlknonb  27813  numclwwlkqhash  28082  numclwwlk2lem1  28083  numclwlk2lem2f  28084  numclwlk2lem2f1o  28086  ipval2  28412  ipasslem3  28538  ipasslem4  28539  nn0min  30464  esumcst  31222  eulerpartlemb  31526  fibp1  31559  ballotlem1  31644  subfacp1lem6  32330  subfaclim  32333  subfacval3  32334  snmlff  32474  bcprod  32868  faclim2  32878  dvdspw  32880  nn0prpwlem  33568  knoppndvlem18  33766  opnmbllem0  34810  nnubfi  34908  nninfnub  34909  geomcau  34917  heiborlem5  34976  heiborlem6  34977  heiborlem7  34978  heiborlem8  34979  bfplem1  34983  nn0expgcd  39064  dffltz  39151  fltnltalem  39154  irrapxlem2  39300  pellexlem1  39306  pellexlem5  39310  pellqrex  39356  monotoddzzfi  39419  jm2.17c  39439  acongeq  39460  jm2.18  39465  jm2.23  39473  jm2.26lem3  39478  jm3.1  39497  expdiophlem1  39498  idomrootle  39675  idomodle  39676  proot1ex  39681  rp-isfinite6  39764  cnvtrclfv  39949  cotrclrcl  39967  inductionexd  40385  binomcxplemnotnn0  40568  nnne1ge2  41438  dvnmptconst  42106  stoweidlem3  42169  stoweidlem7  42173  stoweidlem34  42200  wallispilem4  42234  wallispilem5  42235  wallispi2lem1  42237  wallispi2lem2  42238  stirlinglem2  42241  stirlinglem3  42242  stirlinglem4  42243  stirlinglem5  42244  stirlinglem7  42246  stirlinglem11  42250  stirlinglem14  42253  stirlinglem15  42254  stirlingr  42256  fourierdlem15  42288  fourierdlem21  42294  fourierdlem22  42295  fourierdlem92  42364  fourierdlem112  42384  fouriersw  42397  sge0rpcpnf  42584  sge0ad2en  42594  ovnsubaddlem1  42733  ovnsubaddlem2  42734  ovolval5lem1  42815  ovolval5lem2  42816  iccpartiltu  43429  iccpartigtl  43430  iccpartlt  43431  iccpartleu  43435  iccpartrn  43437  iccelpart  43440  iccpartiun  43441  iccpartdisj  43444  sqrtpwpw2p  43547  fmtnosqrt  43548  odz2prm2pw  43572  fmtnoprmfac1lem  43573  fmtnoprmfac1  43574  2pwp1prm  43598  lighneallem1  43617  lighneallem2  43618  lighneallem3  43619  lighneallem4a  43620  lighneallem4  43622  nnpw2evenALTV  43714  dfwppr  43750  smndex1n0mnd  43982  cznabel  44123  cznrng  44124  ztprmneprm  44293  altgsumbc  44298  altgsumbcALT  44299  pw2m1lepw2m1  44473  nneom  44485  logbpw2m1  44525  blennn  44533  blenpw2m1  44537  blengt1fldiv2p1  44551  dignn0ldlem  44560  dignnld  44561  dig2nn1st  44563  dignn0flhalflem1  44573  nn0sumshdiglemA  44577  nn0sumshdiglemB  44578  eenglngeehlnm  44624
  Copyright terms: Public domain W3C validator