Theorem nnnn0d 11228

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

Step	Hyp	Ref	Expression
1		nnssnn0 11172	. 2 ⊢ ℕ ⊆ ℕ0
2		nnnn0d.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ)
3	1, 2	sseldi 3566	1 ⊢ (𝜑 → 𝐴 ∈ ℕ0)

Syntax hints:   → wi 4   ∈ wcel 1977  ℕcn 10897  ℕ₀cn0 11169

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-un 3545  df-in 3547  df-ss 3554  df-n0 11170

This theorem is referenced by:  nn0ge2m1nn0  11238  nnzd  11357  eluzge2nn0  11603  expgt1  12760  expaddzlem  12765  expaddz  12766  expmulz  12768  expmulnbnd  12858  facwordi  12938  faclbnd  12939  facavg  12950  bcm1k  12964  wrdeqs1cat  13326  cshwcsh2id  13425  relexpsucnnr  13613  isercolllem2  14244  bcxmas  14406  climcndslem1  14420  climcndslem2  14421  climcnds  14422  geo2sum  14443  mertenslem1  14455  prodmolem3  14502  prodmolem2a  14503  bpolydiflem  14624  eftabs  14645  efcllem  14647  eftlub  14678  eirrlem  14771  rpnnen2lem9  14790  rpnnen2lem11  14792  dvdsfac  14886  oddpwp1fsum  14953  bitsfzo  14995  bitsfi  14997  sadcaddlem  15017  smumullem  15052  gcdcl  15066  mulgcd  15103  rplpwr  15114  rppwr  15115  lcmcl  15152  lcmgcdnn  15162  lcmfcl  15179  nprmdvds1  15256  rpexp  15270  zsqrtelqelz  15304  phiprmpw  15319  eulerthlem2  15325  eulerth  15326  fermltl  15327  odzcllem  15335  odzdvds  15338  odzphi  15339  prm23lt5  15357  pythagtriplem6  15364  pythagtriplem7  15365  pcprmpw2  15424  dvdsprmpweqle  15428  pcprod  15437  pcfac  15441  pcbc  15442  expnprm  15444  pockthlem  15447  pockthg  15448  prmunb  15456  prmreclem2  15459  prmreclem3  15460  prmreclem4  15461  prmreclem5  15462  prmreclem6  15463  mul4sqlem  15495  4sqlem11  15497  4sqlem17  15503  vdwlem1  15523  vdwlem5  15527  vdwlem6  15528  vdwlem8  15530  vdwlem9  15531  vdwlem11  15533  vdwlem12  15534  vdwnnlem3  15539  ramz2  15566  ramub1lem1  15568  ramub1lem2  15569  ramub1  15570  prmgaplem3  15595  2expltfac  15637  psgnunilem3  17739  mndodconglem  17783  gexcl3  17825  pgpfi1  17833  sylow1lem1  17836  gexexlem  18078  prmcyg  18118  gsumval3  18131  ablfacrplem  18287  ablfacrp  18288  ablfacrp2  18289  ablfac1eu  18295  srgbinomlem3  18365  srgbinomlem4  18366  chfacfscmulgsum  20484  chfacfpmmulgsum  20488  cpmadugsumlemF  20500  ovoliunlem1  23077  mbfi1fseqlem1  23288  mbfi1fseqlem3  23290  mbfi1fseqlem5  23292  itg2cnlem2  23335  dvply1  23843  aalioulem2  23892  aalioulem5  23895  aaliou3lem1  23901  aaliou3lem2  23902  aaliou3lem8  23904  aaliou3lem6  23907  taylthlem1  23931  taylthlem2  23932  pserdvlem2  23986  cxpeq  24298  dmgmdivn0  24554  lgamgulmlem5  24559  lgamcvg2  24581  wilthlem1  24594  ftalem1  24599  ftalem2  24600  ftalem4  24602  ftalem5  24603  basellem2  24608  basellem3  24609  basellem4  24610  basellem5  24611  isppw2  24641  dvdsmulf1o  24720  sgmmul  24726  chpchtsum  24744  logfacubnd  24746  mersenne  24752  perfect1  24753  perfectlem1  24754  perfectlem2  24755  perfect  24756  dchrelbas3  24763  dchrelbasd  24764  dchrzrh1  24769  dchrzrhmul  24771  dchrmulcl  24774  dchrn0  24775  dchrfi  24780  dchrghm  24781  dchrabs  24785  dchrinv  24786  dchrptlem1  24789  dchrptlem2  24790  dchrptlem3  24791  dchrpt  24792  dchrsum2  24793  sum2dchr  24799  pcbcctr  24801  bcmono  24802  bclbnd  24805  bposlem1  24809  bposlem3  24811  bposlem5  24813  bposlem6  24814  lgslem1  24822  lgslem4  24825  lgsval2lem  24832  lgsvalmod  24841  lgsmod  24848  lgsdirprm  24856  lgsne0  24860  lgsqrlem1  24871  lgsqrlem2  24872  lgsqrlem3  24873  lgsqrlem4  24874  gausslemma2dlem0b  24882  gausslemma2dlem0c  24883  gausslemma2dlem1  24891  gausslemma2dlem7  24898  gausslemma2d  24899  lgseisenlem1  24900  lgseisenlem2  24901  lgseisenlem3  24902  lgseisenlem4  24903  lgseisen  24904  lgsquadlem2  24906  lgsquadlem3  24907  m1lgs  24913  2lgslem1a  24916  2sqlem3  24945  2sqblem  24956  chebbnd1lem1  24958  chebbnd1lem3  24960  rplogsumlem2  24974  rpvmasumlem  24976  dchrisumlem1  24978  dchrisumlem2  24979  dchrmusum2  24983  dchrvmasumlem3  24988  dchrisum0ff  24996  dchrisum0flblem1  24997  rpvmasum2  25001  dchrisum0re  25002  dchrisum0lem2a  25006  dirith  25018  mudivsum  25019  pntpbnd1a  25074  pntlemq  25090  pntlemr  25091  pntlemj  25092  ostth2lem2  25123  ostth2lem3  25124  ostth2  25126  hashecclwwlkn1  26361  usghashecclwwlk  26362  hashclwwlkn  26363  clwwlkndivn  26364  clwlkfclwwlk  26371  numclwwlk3  26636  numclwwlk6  26640  numclwwlk7  26641  dipcl  26951  dipcn  26959  bcm1n  28941  isarchi2  29070  submarchi  29071  psgnfzto1st  29186  submateqlem1  29201  madjusmdetlem2  29222  madjusmdetlem4  29224  mdetlap  29226  nexple  29399  oddpwdc  29743  eulerpartlemsv2  29747  eulerpartlemsf  29748  eulerpartlems  29749  eulerpartlemv  29753  eulerpartlemb  29757  plymulx0  29950  signsvtn0  29973  subfacp1lem1  30415  subfacp1lem6  30421  subfaclim  30424  erdszelem8  30434  erdszelem10  30436  cvmliftlem10  30530  faclim2  30887  poimirlem7  32586  poimirlem17  32596  poimirlem18  32597  poimirlem20  32599  poimirlem21  32600  poimirlem22  32601  poimirlem25  32604  poimirlem26  32605  poimirlem27  32606  poimirlem28  32607  poimirlem32  32611  nninfnub  32717  bfplem1  32791  3rexfrabdioph  36379  4rexfrabdioph  36380  6rexfrabdioph  36381  7rexfrabdioph  36382  irrapxlem5  36408  pellexlem2  36412  pellexlem6  36416  pell14qrgt0  36441  pell1qrge1  36452  pellfundgt1  36465  ltrmxnn0  36534  jm2.26lem3  36586  jm2.27a  36590  jm2.27c  36592  rmxdiophlem  36600  jm3.1lem1  36602  jm3.1lem2  36603  jm3.1lem3  36604  jm3.1  36605  dgrsub2  36724  mpaaeu  36739  idomsubgmo  36795  relexpxpmin  37028  nzprmdif  37540  binomcxplemwb  37569  fperiodmul  38459  xralrple4  38530  fsumnncl  38638  dvsinexp  38798  dvxpaek  38830  itgsinexplem1  38845  stoweidlem1  38894  stoweidlem17  38910  stoweidlem25  38918  stoweidlem34  38927  stoweidlem38  38931  stoweidlem40  38933  stoweidlem42  38935  stoweidlem45  38938  stirlinglem4  38970  stirlinglem5  38971  stirlinglem10  38976  stirlinglem13  38979  dirkertrigeq  38994  fourierdlem21  39021  fourierdlem25  39025  fourierdlem48  39047  fourierdlem54  39053  fourierdlem64  39063  fourierdlem65  39064  fourierdlem73  39072  fourierdlem81  39080  fourierdlem83  39082  fourierdlem92  39091  fourierdlem103  39102  fourierdlem104  39103  fourierdlem112  39111  fourierdlem113  39112  etransclem1  39128  etransclem4  39131  etransclem8  39135  etransclem15  39142  etransclem17  39144  etransclem18  39145  etransclem19  39146  etransclem20  39147  etransclem21  39148  etransclem22  39149  etransclem23  39150  etransclem24  39151  etransclem25  39152  etransclem27  39154  etransclem32  39159  etransclem35  39162  etransclem41  39168  etransclem44  39171  etransclem46  39173  iccpartigtl  39961  iccpartgt  39965  iccpartgel  39967  iccelpart  39971  odz2prm2pw  40013  fmtnoprmfac1  40015  fmtnoprmfac2  40017  pwdif  40039  2pwp1prm  40041  sfprmdvdsmersenne  40058  lighneallem4a  40063  proththdlem  40068  proththd  40069  perfectALTVlem1  40164  perfectALTVlem2  40165  perfectALTV  40166  crctcsh1wlkn0lem6  41018  hashecclwwlksn1  41261  umgrhashecclwwlk  41262  clwlksfclwwlk  41269  eucrctshift  41411  logbpw2m1  42159  nnpw2blenfzo  42173  nnolog2flm1  42182  dignn0fr  42193  nn0sumshdiglemA  42211  nn0sumshdiglemB  42212