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

Theorem nnnn0d 11598
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 11541 . 2 ℕ ⊆ ℕ0
2 nnnn0d.1 . 2 (𝜑𝐴 ∈ ℕ)
31, 2sseldi 3759 1 (𝜑𝐴 ∈ ℕ0)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2155  cn 11274  0cn0 11538
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-v 3352  df-un 3737  df-in 3739  df-ss 3746  df-n0 11539
This theorem is referenced by:  nn0ge2m1nn0  11608  nnzd  11728  eluzge2nn0  11927  expgt1  13105  expaddzlem  13110  expaddz  13111  expmulz  13113  expmulnbnd  13203  facwordi  13280  faclbnd  13281  facavg  13292  bcm1k  13306  wrdeqs1cat  13717  wrdeqs1catOLD  13718  cshwcsh2id  13857  relexpsucnnr  14050  isercolllem2  14681  bcxmas  14851  climcndslem1  14865  climcndslem2  14866  climcnds  14867  geo2sum  14888  mertenslem1  14899  prodmolem3  14946  prodmolem2a  14947  bpolydiflem  15067  eftabs  15088  efcllem  15090  eftlub  15121  eirrlem  15214  rpnnen2lem9  15233  rpnnen2lem11  15235  dvdsfac  15333  oddpwp1fsum  15397  bitsfzo  15438  bitsfi  15440  sadcaddlem  15460  smumullem  15495  gcdcl  15509  mulgcd  15546  rplpwr  15557  rppwr  15558  lcmcl  15595  lcmgcdnn  15605  lcmfcl  15622  nprmdvds1  15697  rpexp  15711  zsqrtelqelz  15745  phiprmpw  15760  eulerthlem2  15766  eulerth  15767  fermltl  15768  odzcllem  15776  odzdvds  15779  odzphi  15780  prm23lt5  15798  pythagtriplem6  15805  pythagtriplem7  15806  pcprmpw2  15865  dvdsprmpweqle  15869  pcprod  15878  pcfac  15882  pcbc  15883  expnprm  15885  pockthlem  15888  pockthg  15889  prmunb  15897  prmreclem2  15900  prmreclem3  15901  prmreclem4  15902  prmreclem5  15903  prmreclem6  15904  mul4sqlem  15936  4sqlem11  15938  4sqlem17  15944  vdwlem1  15964  vdwlem5  15968  vdwlem6  15969  vdwlem8  15971  vdwlem9  15972  vdwlem11  15974  vdwlem12  15975  vdwnnlem3  15980  ramz2  16007  ramub1lem1  16009  ramub1lem2  16010  ramub1  16011  prmgaplem3  16036  2expltfac  16073  psgnunilem3  18180  mndodconglem  18224  gexcl3  18266  pgpfi1  18274  sylow1lem1  18277  gexexlem  18521  prmcyg  18561  gsumval3  18574  ablfacrplem  18731  ablfacrp  18732  ablfacrp2  18733  ablfac1eu  18739  srgbinomlem3  18809  srgbinomlem4  18810  chfacfscmulgsum  20944  chfacfpmmulgsum  20948  cpmadugsumlemF  20960  ovoliunlem1  23560  mbfi1fseqlem1  23773  mbfi1fseqlem3  23775  mbfi1fseqlem5  23777  itg2cnlem2  23820  dvply1  24330  aalioulem2  24379  aalioulem5  24382  aaliou3lem1  24388  aaliou3lem2  24389  aaliou3lem8  24391  aaliou3lem6  24394  taylthlem1  24418  taylthlem2  24419  pserdvlem2  24473  cxpeq  24789  dmgmdivn0  25045  lgamgulmlem5  25050  lgamcvg2  25072  wilthlem1  25085  ftalem1  25090  ftalem2  25091  ftalem4  25093  ftalem5  25094  basellem2  25099  basellem3  25100  basellem4  25101  basellem5  25102  isppw2  25132  dvdsmulf1o  25211  sgmmul  25217  chpchtsum  25235  logfacubnd  25237  mersenne  25243  perfect1  25244  perfectlem1  25245  perfectlem2  25246  perfect  25247  dchrelbas3  25254  dchrelbasd  25255  dchrzrh1  25260  dchrzrhmul  25262  dchrmulcl  25265  dchrn0  25266  dchrfi  25271  dchrghm  25272  dchrabs  25276  dchrinv  25277  dchrptlem1  25280  dchrptlem2  25281  dchrptlem3  25282  dchrpt  25283  dchrsum2  25284  sum2dchr  25290  pcbcctr  25292  bcmono  25293  bclbnd  25296  bposlem1  25300  bposlem3  25302  bposlem5  25304  bposlem6  25305  lgslem1  25313  lgsval2lem  25323  lgsvalmod  25332  lgsmod  25339  lgsdirprm  25347  lgsne0  25351  lgsqrlem1  25362  lgsqrlem2  25363  lgsqrlem3  25364  lgsqrlem4  25365  gausslemma2dlem0b  25373  gausslemma2dlem0c  25374  gausslemma2dlem1  25382  gausslemma2dlem7  25389  gausslemma2d  25390  lgseisenlem1  25391  lgseisenlem2  25392  lgseisenlem3  25393  lgseisenlem4  25394  lgseisen  25395  lgsquadlem2  25397  lgsquadlem3  25398  m1lgs  25404  2lgslem1a  25407  2sqlem3  25436  2sqblem  25447  chebbnd1lem1  25449  chebbnd1lem3  25451  rplogsumlem2  25465  rpvmasumlem  25467  dchrisumlem1  25469  dchrisumlem2  25470  dchrmusum2  25474  dchrvmasumlem3  25479  dchrisum0ff  25487  dchrisum0flblem1  25488  rpvmasum2  25492  dchrisum0re  25493  dchrisum0lem2a  25497  dirith  25509  mudivsum  25510  pntpbnd1a  25565  pntlemq  25581  pntlemr  25582  pntlemj  25583  ostth2lem2  25614  ostth2lem3  25615  ostth2  25617  crctcshwlkn0lem6  27000  hashecclwwlkn1  27329  umgrhashecclwwlk  27330  clwlksfclwwlkOLD  27337  clwwlknon  27360  eucrctshift  27521  numclwlk1lem2  27674  dipcl  28023  dipcn  28031  bcm1n  30003  isarchi2  30186  submarchi  30187  psgnfzto1st  30302  submateqlem1  30320  madjusmdetlem2  30341  madjusmdetlem4  30343  mdetlap  30345  nexple  30518  oddpwdc  30863  eulerpartlemsv2  30867  eulerpartlemsf  30868  eulerpartlems  30869  eulerpartlemv  30873  eulerpartlemb  30877  plymulx0  31073  signsvtn0  31096  signsvtn0OLD  31097  fsum2dsub  31136  reprinfz1  31151  reprpmtf1o  31155  circlemeth  31169  circlemethnat  31170  hgt750lemb  31185  hgt750lema  31186  hgt750leme  31187  tgoldbachgtde  31189  tgoldbachgtda  31190  subfacp1lem1  31609  subfacp1lem6  31615  subfaclim  31618  erdszelem8  31628  erdszelem10  31630  cvmliftlem10  31724  faclim2  32079  poimirlem7  33840  poimirlem17  33850  poimirlem18  33851  poimirlem20  33853  poimirlem21  33854  poimirlem22  33855  poimirlem25  33858  poimirlem26  33859  poimirlem27  33860  poimirlem28  33861  poimirlem32  33865  nninfnub  33969  bfplem1  34043  3rexfrabdioph  38039  4rexfrabdioph  38040  6rexfrabdioph  38041  7rexfrabdioph  38042  irrapxlem5  38068  pellexlem2  38072  pellexlem6  38076  pell14qrgt0  38101  pell1qrge1  38112  pellfundgt1  38125  ltrmxnn0  38193  jm2.26lem3  38245  jm2.27a  38249  jm2.27c  38251  rmxdiophlem  38259  jm3.1lem1  38261  jm3.1lem2  38262  jm3.1lem3  38263  jm3.1  38264  dgrsub2  38382  mpaaeu  38397  idomsubgmo  38453  relexpxpmin  38684  nzprmdif  39192  binomcxplemwb  39221  fperiodmul  40157  xralrple4  40227  fsumnncl  40441  dvsinexp  40763  dvxpaek  40793  itgsinexplem1  40807  stoweidlem1  40855  stoweidlem17  40871  stoweidlem25  40879  stoweidlem34  40888  stoweidlem38  40892  stoweidlem40  40894  stoweidlem42  40896  stoweidlem45  40899  stirlinglem4  40931  stirlinglem5  40932  stirlinglem10  40937  stirlinglem13  40940  dirkertrigeq  40955  fourierdlem21  40982  fourierdlem25  40986  fourierdlem48  41008  fourierdlem54  41014  fourierdlem64  41024  fourierdlem65  41025  fourierdlem73  41033  fourierdlem81  41041  fourierdlem83  41043  fourierdlem92  41052  fourierdlem103  41063  fourierdlem104  41064  fourierdlem112  41072  fourierdlem113  41073  etransclem1  41089  etransclem4  41092  etransclem8  41096  etransclem15  41103  etransclem17  41105  etransclem18  41106  etransclem19  41107  etransclem20  41108  etransclem21  41109  etransclem22  41110  etransclem23  41111  etransclem24  41112  etransclem25  41113  etransclem27  41115  etransclem32  41120  etransclem35  41123  etransclem41  41129  etransclem44  41132  etransclem46  41134  iccpartigtl  42093  iccpartgt  42097  iccpartgel  42099  iccelpart  42103  odz2prm2pw  42151  fmtnoprmfac1  42153  fmtnoprmfac2  42155  pwdif  42177  2pwp1prm  42179  sfprmdvdsmersenne  42196  lighneallem4a  42201  proththdlem  42206  proththd  42207  perfectALTVlem1  42306  perfectALTVlem2  42307  perfectALTV  42308  logbpw2m1  43030  nnpw2blenfzo  43044  nnolog2flm1  43053  dignn0fr  43064  nn0sumshdiglemA  43082  nn0sumshdiglemB  43083
  Copyright terms: Public domain W3C validator