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

Theorem nnnn0 11892
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 11888 . 2 ℕ ⊆ ℕ0
21sseli 3960 1 (𝐴 ∈ ℕ → 𝐴 ∈ ℕ0)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  cn 11626  0cn0 11885
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 2790
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 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-v 3494  df-un 3938  df-in 3940  df-ss 3949  df-n0 11886
This theorem is referenced by:  nnnn0i  11893  elnnnn0b  11929  elnnnn0c  11930  elz2  11987  nn0ind-raph  12070  zindd  12071  fzo1fzo0n0  13076  ubmelfzo  13090  elfzom1elp1fzo  13092  fzo0sn0fzo1  13114  quoremnn0ALT  13213  modmulnn  13245  modsumfzodifsn  13300  addmodlteq  13302  expneg  13425  expcllem  13428  expcl2lem  13429  expeq0  13447  mulexpz  13457  expmordi  13519  rpexpmord  13520  expnlbnd  13582  expmulnbnd  13584  digit2  13585  digit1  13586  facmapnn  13633  facdiv  13635  faclbnd  13638  faclbnd3  13640  faclbnd4lem3  13643  faclbnd4lem4  13644  faclbnd5  13646  faclbnd6  13647  bcval5  13666  ishashinf  13809  iswrdi  13853  pfxn0  14036  repswfsts  14131  repswlsw  14132  repswcshw  14162  relexpnnrn  14392  relexpaddg  14400  absexpz  14653  isercoll  15012  summolem3  15059  summolem2a  15060  climcndslem2  15193  climcnds  15194  harmonic  15202  arisum  15203  expcnv  15207  geo2sum  15217  geo2lim  15219  geoisum1  15223  geoisum1c  15224  0.999...  15225  mertenslem2  15229  fallfacfwd  15378  0fallfac  15379  0risefac  15380  ef0lem  15420  ege2le3  15431  efaddlem  15434  efexp  15442  rpnnen2lem2  15556  rpnnen2lem4  15558  ruclem12  15582  dvdsmodexp  15603  nn0enne  15716  nnehalf  15718  nno  15721  nn0o  15722  pwp1fsum  15730  divalg2  15744  ndvdssub  15748  gcdmultiplez  15871  gcddiv  15887  gcdmultipleOLD  15888  gcdmultiplezOLD  15889  rpmulgcd  15894  rplpwr  15895  dvdssqlem  15898  eucalgf  15915  lcmflefac  15980  1nprm  16011  2mulprm  16025  isprm5  16039  isprm6  16046  prmdvdsexp  16047  phicl2  16093  phibndlem  16095  phiprmpw  16101  crth  16103  eulerthlem2  16107  hashgcdlem  16113  phisum  16115  pythagtriplem10  16145  pythagtriplem6  16146  pythagtriplem7  16147  pythagtriplem12  16151  pythagtriplem14  16153  pclem  16163  pcexp  16184  pcid  16197  pcprod  16219  pcbc  16224  prmpwdvds  16228  infpnlem1  16234  infpnlem2  16235  prmunb  16238  prmreclem6  16245  1arith  16251  vdwapf  16296  0hashbc  16331  ram0  16346  prmdvdsprmo  16366  prmdvdsprmop  16367  prmolefac  16370  prmgaplem1  16373  prmgaplem2  16374  prmgapprmolem  16385  prmgapprmo  16386  cshwrepswhash1  16424  ghmmulg  18308  odmodnn0  18597  dfod2  18620  submod  18623  cply1mul  20390  cply1coe0  20395  cply1coe0bi  20396  prmirredlem  20568  prmirred  20570  znf1o  20626  znhash  20633  znfi  20634  znfld  20635  znidomb  20636  znunithash  20639  znrrg  20640  cpmatmcllem  21254  m2cpm  21277  m2cpminvid2lem  21290  fvmptnn04ifa  21386  chfacfisf  21390  chfacfisfcpmat  21391  chfacffsupp  21392  chfacfscmul0  21394  chfacfscmulfsupp  21395  chfacfscmulgsum  21396  chfacfpmmul0  21398  chfacfpmmulfsupp  21399  chfacfpmmulgsum  21400  chfacfpmmulgsum2  21401  cayhamlem1  21402  cpmadugsumlemF  21412  tgpmulg  22629  cmodscexp  23652  cphipval  23773  ovollb2lem  24016  ovoliunlem1  24030  ovoliunlem3  24032  uniioombllem3  24113  uniioombllem4  24114  opnmbllem  24129  mbfi1fseqlem1  24243  mbfi1fseqlem3  24245  mbfi1fseqlem4  24246  mbfi1fseqlem5  24247  mbfi1fseqlem6  24248  dvexp  24477  dvexp3  24502  plyco  24758  dgrcolem1  24790  plydivex  24813  aaliou3lem2  24859  aaliou3lem3  24860  aaliou3lem5  24863  aaliou3lem6  24864  aaliou3lem7  24865  aaliou3lem9  24866  radcnvlem2  24929  dvradcnv  24936  pserdv2  24945  abelthlem6  24951  abelthlem9  24955  logtayllem  25169  logtayl  25170  logtaylsum  25171  logtayl2  25172  cxproot  25200  root1id  25262  logbgcd1irr  25299  atantayl  25442  atantayl2  25443  leibpilem2  25446  leibpi  25447  birthdaylem2  25457  birthdaylem3  25458  dfef2  25475  basellem2  25586  basellem4  25588  basellem5  25589  basellem6  25590  basellem8  25592  isppw2  25619  vmappw  25620  sqf11  25643  vma1  25670  1sgm2ppw  25703  chtublem  25714  fsumvma2  25717  vmasum  25719  dchrelbas4  25746  dchrzrhcl  25748  dchrfi  25758  dchrhash  25774  pcbcctr  25779  bclbnd  25783  bposlem1  25787  lgsval4a  25822  lgsdchrval  25857  lgsdchr  25858  gausslemma2dlem0c  25861  gausslemma2dlem0d  25862  gausslemma2dlem6  25875  2lgslem1a1  25892  2lgslem1c  25896  2lgslem3a1  25903  2lgslem3b1  25904  2lgslem3c1  25905  2lgslem3d1  25906  2sqreunnlem1  25952  2sqreunnltblem  25954  rplogsumlem2  25988  dchrisumlem2  25993  ostth2lem1  26121  ostth2lem3  26138  ostth3  26141  cusgrsize2inds  27162  pthdivtx  27437  crctcshwlkn0lem4  27518  crctcshwlkn0lem5  27519  crctcshwlkn0lem7  27521  0enwwlksnge1  27569  rusgr0edg  27679  clwlkclwwlkf1lem2  27710  clwlkclwwlkf1lem3  27711  clwwisshclwwslem  27719  clwwlkinwwlk  27745  clwwlknfiOLD  27751  clwwlkel  27752  clwwlkf  27753  clwwlkf1  27755  clwwlknwwlksnb  27761  wwlksubclwwlk  27764  erclwwlknref  27775  clwwlknonwwlknonb  27812  numclwwlkqhash  28081  numclwwlk2lem1  28082  numclwlk2lem2f  28083  numclwlk2lem2f1o  28085  ipval2  28411  ipasslem3  28537  ipasslem4  28538  nn0min  30463  esumcst  31221  eulerpartlemb  31525  fibp1  31558  ballotlem1  31643  subfacp1lem6  32329  subfaclim  32332  subfacval3  32333  snmlff  32473  bcprod  32867  faclim2  32877  dvdspw  32879  nn0prpwlem  33567  knoppndvlem18  33765  opnmbllem0  34809  nnubfi  34906  nninfnub  34907  geomcau  34915  heiborlem5  34974  heiborlem6  34975  heiborlem7  34976  heiborlem8  34977  bfplem1  34981  nn0expgcd  39062  dffltz  39149  fltnltalem  39152  irrapxlem2  39298  pellexlem1  39304  pellexlem5  39308  pellqrex  39354  monotoddzzfi  39417  jm2.17c  39437  acongeq  39458  jm2.18  39463  jm2.23  39471  jm2.26lem3  39476  jm3.1  39495  expdiophlem1  39496  idomrootle  39673  idomodle  39674  proot1ex  39679  rp-isfinite6  39762  cnvtrclfv  39947  cotrclrcl  39965  inductionexd  40383  binomcxplemnotnn0  40565  nnne1ge2  41434  dvnmptconst  42102  stoweidlem3  42165  stoweidlem7  42169  stoweidlem34  42196  wallispilem4  42230  wallispilem5  42231  wallispi2lem1  42233  wallispi2lem2  42234  stirlinglem2  42237  stirlinglem3  42238  stirlinglem4  42239  stirlinglem5  42240  stirlinglem7  42242  stirlinglem11  42246  stirlinglem14  42249  stirlinglem15  42250  stirlingr  42252  fourierdlem15  42284  fourierdlem21  42290  fourierdlem22  42291  fourierdlem92  42360  fourierdlem112  42380  fouriersw  42393  sge0rpcpnf  42580  sge0ad2en  42590  ovnsubaddlem1  42729  ovnsubaddlem2  42730  ovolval5lem1  42811  ovolval5lem2  42812  iccpartiltu  43459  iccpartigtl  43460  iccpartlt  43461  iccpartleu  43465  iccpartrn  43467  iccelpart  43470  iccpartiun  43471  iccpartdisj  43474  sqrtpwpw2p  43577  fmtnosqrt  43578  odz2prm2pw  43602  fmtnoprmfac1lem  43603  fmtnoprmfac1  43604  2pwp1prm  43628  lighneallem1  43647  lighneallem2  43648  lighneallem3  43649  lighneallem4a  43650  lighneallem4  43652  nnpw2evenALTV  43744  dfwppr  43780  smndex1n0mnd  44012  cznabel  44153  cznrng  44154  ztprmneprm  44323  altgsumbc  44328  altgsumbcALT  44329  pw2m1lepw2m1  44503  nneom  44515  logbpw2m1  44555  blennn  44563  blenpw2m1  44567  blengt1fldiv2p1  44581  dignn0ldlem  44590  dignnld  44591  dig2nn1st  44593  dignn0flhalflem1  44603  nn0sumshdiglemA  44607  nn0sumshdiglemB  44608  eenglngeehlnm  44654
  Copyright terms: Public domain W3C validator