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

Theorem nnnn0d 11389
Description: A positive integer is a nonnegative integer. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
nnnn0d.1 (𝜑𝐴 ∈ ℕ)
Assertion
Ref Expression
nnnn0d (𝜑𝐴 ∈ ℕ0)

Proof of Theorem nnnn0d
StepHypRef Expression
1 nnssnn0 11333 . 2 ℕ ⊆ ℕ0
2 nnnn0d.1 . 2 (𝜑𝐴 ∈ ℕ)
31, 2sseldi 3634 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:  nn0ge2m1nn0  11399  nnzd  11519  eluzge2nn0  11765  expgt1  12938  expaddzlem  12943  expaddz  12944  expmulz  12946  expmulnbnd  13036  facwordi  13116  faclbnd  13117  facavg  13128  bcm1k  13142  wrdeqs1cat  13520  cshwcsh2id  13620  relexpsucnnr  13809  isercolllem2  14440  bcxmas  14611  climcndslem1  14625  climcndslem2  14626  climcnds  14627  geo2sum  14648  mertenslem1  14660  prodmolem3  14707  prodmolem2a  14708  bpolydiflem  14829  eftabs  14850  efcllem  14852  eftlub  14883  eirrlem  14976  rpnnen2lem9  14995  rpnnen2lem11  14997  dvdsfac  15095  oddpwp1fsum  15162  bitsfzo  15204  bitsfi  15206  sadcaddlem  15226  smumullem  15261  gcdcl  15275  mulgcd  15312  rplpwr  15323  rppwr  15324  lcmcl  15361  lcmgcdnn  15371  lcmfcl  15388  nprmdvds1  15465  rpexp  15479  zsqrtelqelz  15513  phiprmpw  15528  eulerthlem2  15534  eulerth  15535  fermltl  15536  odzcllem  15544  odzdvds  15547  odzphi  15548  prm23lt5  15566  pythagtriplem6  15573  pythagtriplem7  15574  pcprmpw2  15633  dvdsprmpweqle  15637  pcprod  15646  pcfac  15650  pcbc  15651  expnprm  15653  pockthlem  15656  pockthg  15657  prmunb  15665  prmreclem2  15668  prmreclem3  15669  prmreclem4  15670  prmreclem5  15671  prmreclem6  15672  mul4sqlem  15704  4sqlem11  15706  4sqlem17  15712  vdwlem1  15732  vdwlem5  15736  vdwlem6  15737  vdwlem8  15739  vdwlem9  15740  vdwlem11  15742  vdwlem12  15743  vdwnnlem3  15748  ramz2  15775  ramub1lem1  15777  ramub1lem2  15778  ramub1  15779  prmgaplem3  15804  2expltfac  15846  psgnunilem3  17962  mndodconglem  18006  gexcl3  18048  pgpfi1  18056  sylow1lem1  18059  gexexlem  18301  prmcyg  18341  gsumval3  18354  ablfacrplem  18510  ablfacrp  18511  ablfacrp2  18512  ablfac1eu  18518  srgbinomlem3  18588  srgbinomlem4  18589  chfacfscmulgsum  20713  chfacfpmmulgsum  20717  cpmadugsumlemF  20729  ovoliunlem1  23316  mbfi1fseqlem1  23527  mbfi1fseqlem3  23529  mbfi1fseqlem5  23531  itg2cnlem2  23574  dvply1  24084  aalioulem2  24133  aalioulem5  24136  aaliou3lem1  24142  aaliou3lem2  24143  aaliou3lem8  24145  aaliou3lem6  24148  taylthlem1  24172  taylthlem2  24173  pserdvlem2  24227  cxpeq  24543  dmgmdivn0  24799  lgamgulmlem5  24804  lgamcvg2  24826  wilthlem1  24839  ftalem1  24844  ftalem2  24845  ftalem4  24847  ftalem5  24848  basellem2  24853  basellem3  24854  basellem4  24855  basellem5  24856  isppw2  24886  dvdsmulf1o  24965  sgmmul  24971  chpchtsum  24989  logfacubnd  24991  mersenne  24997  perfect1  24998  perfectlem1  24999  perfectlem2  25000  perfect  25001  dchrelbas3  25008  dchrelbasd  25009  dchrzrh1  25014  dchrzrhmul  25016  dchrmulcl  25019  dchrn0  25020  dchrfi  25025  dchrghm  25026  dchrabs  25030  dchrinv  25031  dchrptlem1  25034  dchrptlem2  25035  dchrptlem3  25036  dchrpt  25037  dchrsum2  25038  sum2dchr  25044  pcbcctr  25046  bcmono  25047  bclbnd  25050  bposlem1  25054  bposlem3  25056  bposlem5  25058  bposlem6  25059  lgslem1  25067  lgsval2lem  25077  lgsvalmod  25086  lgsmod  25093  lgsdirprm  25101  lgsne0  25105  lgsqrlem1  25116  lgsqrlem2  25117  lgsqrlem3  25118  lgsqrlem4  25119  gausslemma2dlem0b  25127  gausslemma2dlem0c  25128  gausslemma2dlem1  25136  gausslemma2dlem7  25143  gausslemma2d  25144  lgseisenlem1  25145  lgseisenlem2  25146  lgseisenlem3  25147  lgseisenlem4  25148  lgseisen  25149  lgsquadlem2  25151  lgsquadlem3  25152  m1lgs  25158  2lgslem1a  25161  2sqlem3  25190  2sqblem  25201  chebbnd1lem1  25203  chebbnd1lem3  25205  rplogsumlem2  25219  rpvmasumlem  25221  dchrisumlem1  25223  dchrisumlem2  25224  dchrmusum2  25228  dchrvmasumlem3  25233  dchrisum0ff  25241  dchrisum0flblem1  25242  rpvmasum2  25246  dchrisum0re  25247  dchrisum0lem2a  25251  dirith  25263  mudivsum  25264  pntpbnd1a  25319  pntlemq  25335  pntlemr  25336  pntlemj  25337  ostth2lem2  25368  ostth2lem3  25369  ostth2  25371  crctcshwlkn0lem6  26763  hashecclwwlkn1  27041  umgrhashecclwwlk  27042  clwlksfclwwlk  27049  clwwlknon  27063  eucrctshift  27221  2clwwlk2clwwlklem2lem1  27328  2clwwlk2clwwlklem2lem2  27329  dipcl  27695  dipcn  27703  bcm1n  29682  isarchi2  29867  submarchi  29868  psgnfzto1st  29983  submateqlem1  30001  madjusmdetlem2  30022  madjusmdetlem4  30024  mdetlap  30026  nexple  30199  oddpwdc  30544  eulerpartlemsv2  30548  eulerpartlemsf  30549  eulerpartlems  30550  eulerpartlemv  30554  eulerpartlemb  30558  plymulx0  30752  signsvtn0  30775  fsum2dsub  30813  reprinfz1  30828  reprpmtf1o  30832  circlemeth  30846  circlemethnat  30847  hgt750lemb  30862  hgt750lema  30863  hgt750leme  30864  tgoldbachgtde  30866  tgoldbachgtda  30867  subfacp1lem1  31287  subfacp1lem6  31293  subfaclim  31296  erdszelem8  31306  erdszelem10  31308  cvmliftlem10  31402  faclim2  31760  poimirlem7  33546  poimirlem17  33556  poimirlem18  33557  poimirlem20  33559  poimirlem21  33560  poimirlem22  33561  poimirlem25  33564  poimirlem26  33565  poimirlem27  33566  poimirlem28  33567  poimirlem32  33571  nninfnub  33677  bfplem1  33751  3rexfrabdioph  37678  4rexfrabdioph  37679  6rexfrabdioph  37680  7rexfrabdioph  37681  irrapxlem5  37707  pellexlem2  37711  pellexlem6  37715  pell14qrgt0  37740  pell1qrge1  37751  pellfundgt1  37764  ltrmxnn0  37833  jm2.26lem3  37885  jm2.27a  37889  jm2.27c  37891  rmxdiophlem  37899  jm3.1lem1  37901  jm3.1lem2  37902  jm3.1lem3  37903  jm3.1  37904  dgrsub2  38022  mpaaeu  38037  idomsubgmo  38093  relexpxpmin  38326  nzprmdif  38835  binomcxplemwb  38864  fperiodmul  39832  xralrple4  39902  fsumnncl  40121  dvsinexp  40443  dvxpaek  40473  itgsinexplem1  40487  stoweidlem1  40536  stoweidlem17  40552  stoweidlem25  40560  stoweidlem34  40569  stoweidlem38  40573  stoweidlem40  40575  stoweidlem42  40577  stoweidlem45  40580  stirlinglem4  40612  stirlinglem5  40613  stirlinglem10  40618  stirlinglem13  40621  dirkertrigeq  40636  fourierdlem21  40663  fourierdlem25  40667  fourierdlem48  40689  fourierdlem54  40695  fourierdlem64  40705  fourierdlem65  40706  fourierdlem73  40714  fourierdlem81  40722  fourierdlem83  40724  fourierdlem92  40733  fourierdlem103  40744  fourierdlem104  40745  fourierdlem112  40753  fourierdlem113  40754  etransclem1  40770  etransclem4  40773  etransclem8  40777  etransclem15  40784  etransclem17  40786  etransclem18  40787  etransclem19  40788  etransclem20  40789  etransclem21  40790  etransclem22  40791  etransclem23  40792  etransclem24  40793  etransclem25  40794  etransclem27  40796  etransclem32  40801  etransclem35  40804  etransclem41  40810  etransclem44  40813  etransclem46  40815  iccpartigtl  41684  iccpartgt  41688  iccpartgel  41690  iccelpart  41694  odz2prm2pw  41800  fmtnoprmfac1  41802  fmtnoprmfac2  41804  pwdif  41826  2pwp1prm  41828  sfprmdvdsmersenne  41845  lighneallem4a  41850  proththdlem  41855  proththd  41856  perfectALTVlem1  41955  perfectALTVlem2  41956  perfectALTV  41957  logbpw2m1  42686  nnpw2blenfzo  42700  nnolog2flm1  42709  dignn0fr  42720  nn0sumshdiglemA  42738  nn0sumshdiglemB  42739
  Copyright terms: Public domain W3C validator