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

Theorem nnnn0d 11944
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 11889 . 2 ℕ ⊆ ℕ0
2 nnnn0d.1 . 2 (𝜑𝐴 ∈ ℕ)
31, 2sseldi 3969 1 (𝜑𝐴 ∈ ℕ0)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  cn 11627  0cn0 11886
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-v 3502  df-un 3945  df-in 3947  df-ss 3956  df-n0 11887
This theorem is referenced by:  nn0ge2m1nn0  11954  nnzd  12075  eluzge2nn0  12276  expgt1  13457  expaddzlem  13462  expaddz  13463  expmulz  13465  expmulnbnd  13586  facwordi  13639  faclbnd  13640  facavg  13651  bcm1k  13665  wrdeqs1cat  14072  cshwcsh2id  14180  relexpsucnnr  14374  isercolllem2  15012  bcxmas  15180  climcndslem1  15194  climcndslem2  15195  climcnds  15196  pwdif  15213  geo2sum  15219  mertenslem1  15230  prodmolem3  15277  prodmolem2a  15278  bpolydiflem  15398  eftabs  15419  efcllem  15421  eftlub  15452  eirrlem  15547  rpnnen2lem9  15565  rpnnen2lem11  15567  dvdsfac  15666  pwp1fsum  15732  oddpwp1fsum  15733  bitsfzo  15774  bitsfi  15776  sadcaddlem  15796  smumullem  15831  gcdcl  15845  dvdsgcdidd  15875  mulgcd  15886  rplpwr  15897  rppwr  15898  lcmcl  15935  lcmgcdnn  15945  lcmfcl  15962  nprmdvds1  16040  rpexp  16054  zsqrtelqelz  16088  phiprmpw  16103  eulerthlem2  16109  eulerth  16110  fermltl  16111  odzcllem  16119  odzdvds  16122  odzphi  16123  prm23lt5  16141  pythagtriplem6  16148  pythagtriplem7  16149  pcprmpw2  16208  dvdsprmpweqle  16212  pcprod  16221  pcfac  16225  pcbc  16226  expnprm  16228  pockthlem  16231  pockthg  16232  prmunb  16240  prmreclem2  16243  prmreclem3  16244  prmreclem4  16245  prmreclem5  16246  prmreclem6  16247  mul4sqlem  16279  4sqlem11  16281  4sqlem17  16287  vdwlem1  16307  vdwlem5  16311  vdwlem6  16312  vdwlem8  16314  vdwlem9  16315  vdwlem11  16317  vdwlem12  16318  vdwnnlem3  16323  ramz2  16350  ramub1lem1  16352  ramub1lem2  16353  ramub1  16354  prmgaplem3  16379  2expltfac  16416  psgnunilem3  18544  odfval  18580  mndodconglem  18589  gexcl3  18632  pgpfi1  18640  sylow1lem1  18643  gexexlem  18892  prmcyg  18934  gsumval3  18947  ablfacrplem  19107  ablfacrp  19108  ablfacrp2  19109  ablfac1eu  19115  prmgrpsimpgd  19156  srgbinomlem3  19212  srgbinomlem4  19213  chfacfscmulgsum  21384  chfacfpmmulgsum  21388  cpmadugsumlemF  21400  ovoliunlem1  24018  mbfi1fseqlem1  24231  mbfi1fseqlem3  24233  mbfi1fseqlem5  24235  itg2cnlem2  24278  dvply1  24788  aalioulem2  24837  aalioulem5  24840  aaliou3lem1  24846  aaliou3lem2  24847  aaliou3lem8  24849  aaliou3lem6  24852  taylthlem1  24876  taylthlem2  24877  pserdvlem2  24931  cxpeq  25251  dmgmdivn0  25519  lgamgulmlem5  25524  lgamcvg2  25546  wilthlem1  25559  ftalem1  25564  ftalem2  25565  ftalem4  25567  ftalem5  25568  basellem2  25573  basellem3  25574  basellem4  25575  basellem5  25576  isppw2  25606  dvdsmulf1o  25685  sgmmul  25691  fsumvma2  25704  chpchtsum  25709  logfacubnd  25711  mersenne  25717  perfect1  25718  perfectlem1  25719  perfectlem2  25720  perfect  25721  dchrelbas3  25728  dchrelbasd  25729  dchrzrh1  25734  dchrzrhmul  25736  dchrmulcl  25739  dchrn0  25740  dchrfi  25745  dchrghm  25746  dchrabs  25750  dchrinv  25751  dchrptlem1  25754  dchrptlem2  25755  dchrptlem3  25756  dchrpt  25757  dchrsum2  25758  sum2dchr  25764  pcbcctr  25766  bcmono  25767  bclbnd  25770  bposlem1  25774  bposlem3  25776  bposlem5  25778  bposlem6  25779  lgslem1  25787  lgsval2lem  25797  lgsvalmod  25806  lgsmod  25813  lgsdirprm  25821  lgsne0  25825  lgsqrlem1  25836  lgsqrlem2  25837  lgsqrlem3  25838  lgsqrlem4  25839  gausslemma2dlem0b  25847  gausslemma2dlem0c  25848  gausslemma2dlem1  25856  gausslemma2dlem7  25863  gausslemma2d  25864  lgseisenlem1  25865  lgseisenlem2  25866  lgseisenlem3  25867  lgseisenlem4  25868  lgseisen  25869  lgsquadlem2  25871  lgsquadlem3  25872  m1lgs  25878  2lgslem1a  25881  2sqlem3  25910  2sqblem  25921  chebbnd1lem1  25959  chebbnd1lem3  25961  rplogsumlem2  25975  rpvmasumlem  25977  dchrisumlem1  25979  dchrisumlem2  25980  dchrmusum2  25984  dchrvmasumlem3  25989  dchrisum0ff  25997  dchrisum0flblem1  25998  rpvmasum2  26002  dchrisum0re  26003  dchrisum0lem2a  26007  dirith  26019  mudivsum  26020  pntpbnd1a  26075  pntlemq  26091  pntlemr  26092  pntlemj  26093  ostth2lem1  26108  ostth2lem2  26124  ostth2lem3  26125  ostth2  26127  crctcshwlkn0lem6  27507  hashecclwwlkn1  27770  umgrhashecclwwlk  27771  clwwlknon  27783  eucrctshift  27936  numclwlk1lem2  28063  dipcl  28403  dipcn  28411  bcm1n  30431  prmdvdsbc  30445  psgnfzto1st  30661  isarchi2  30728  submarchi  30729  freshmansdream  30773  submateqlem1  30958  madjusmdetlem2  30979  madjusmdetlem4  30981  mdetlap  30983  nexple  31154  oddpwdc  31498  eulerpartlemsv2  31502  eulerpartlemsf  31503  eulerpartlems  31504  eulerpartlemv  31508  eulerpartlemb  31512  plymulx0  31703  signsvtn0  31726  fsum2dsub  31764  reprinfz1  31779  reprpmtf1o  31783  circlemeth  31797  circlemethnat  31798  hgt750lemb  31813  hgt750lema  31814  hgt750leme  31815  tgoldbachgtde  31817  tgoldbachgtda  31818  lpadleft  31840  subfacp1lem1  32310  subfacp1lem6  32316  subfaclim  32319  erdszelem8  32329  erdszelem10  32331  cvmliftlem10  32425  faclim2  32864  poimirlem7  34766  poimirlem17  34776  poimirlem18  34777  poimirlem20  34779  poimirlem21  34780  poimirlem22  34781  poimirlem25  34784  poimirlem26  34785  poimirlem27  34786  poimirlem28  34787  poimirlem32  34791  nninfnub  34894  bfplem1  34968  oexpreposd  39044  nn0rppwr  39047  expgcd  39048  zrtelqelz  39057  dffltz  39136  fltne  39137  fltltc  39138  fltnltalem  39139  fltnlta  39140  3rexfrabdioph  39259  4rexfrabdioph  39260  6rexfrabdioph  39261  7rexfrabdioph  39262  irrapxlem5  39288  pellexlem2  39292  pellexlem6  39296  pell14qrgt0  39321  pell1qrge1  39332  pellfundgt1  39345  ltrmxnn0  39411  jm2.26lem3  39463  jm2.27a  39467  jm2.27c  39469  rmxdiophlem  39477  jm3.1lem1  39479  jm3.1lem2  39480  jm3.1lem3  39481  jm3.1  39482  dgrsub2  39600  mpaaeu  39615  idomsubgmo  39663  relexpxpmin  39927  nzprmdif  40516  binomcxplemwb  40545  fperiodmul  41436  xralrple4  41506  fsumnncl  41717  dvsinexp  42060  dvxpaek  42090  itgsinexplem1  42104  stoweidlem1  42152  stoweidlem17  42168  stoweidlem25  42176  stoweidlem34  42185  stoweidlem38  42189  stoweidlem40  42191  stoweidlem42  42193  stoweidlem45  42196  stirlinglem4  42228  stirlinglem5  42229  stirlinglem10  42234  stirlinglem13  42237  dirkertrigeq  42252  fourierdlem21  42279  fourierdlem25  42283  fourierdlem48  42305  fourierdlem54  42311  fourierdlem64  42321  fourierdlem65  42322  fourierdlem73  42330  fourierdlem81  42338  fourierdlem83  42340  fourierdlem92  42349  fourierdlem103  42360  fourierdlem104  42361  fourierdlem112  42369  fourierdlem113  42370  etransclem1  42386  etransclem4  42389  etransclem8  42393  etransclem15  42400  etransclem17  42402  etransclem18  42403  etransclem19  42404  etransclem20  42405  etransclem21  42406  etransclem22  42407  etransclem23  42408  etransclem24  42409  etransclem25  42410  etransclem27  42412  etransclem32  42417  etransclem35  42420  etransclem41  42426  etransclem44  42429  etransclem46  42431  iccpartigtl  43415  iccpartgt  43419  iccpartgel  43421  iccelpart  43425  odz2prm2pw  43557  fmtnoprmfac1  43559  fmtnoprmfac2  43561  2pwp1prm  43583  sfprmdvdsmersenne  43600  lighneallem4a  43605  proththdlem  43610  proththd  43611  perfectALTVlem1  43718  perfectALTVlem2  43719  perfectALTV  43720  fpprwpprb  43737  logbpw2m1  44459  nnpw2blenfzo  44473  nnolog2flm1  44482  dignn0fr  44493  nn0sumshdiglemA  44511  nn0sumshdiglemB  44512
  Copyright terms: Public domain W3C validator