Theorem nnnn0d 11943

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 11888	. 2 ⊢ ℕ ⊆ ℕ0
2		nnnn0d.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ)
3	1, 2	sseldi 3913	1 ⊢ (𝜑 → 𝐴 ∈ ℕ0)

Syntax hints:   → wi 4   ∈ wcel 2111  ℕcn 11625  ℕ₀cn0 11885

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-n0 11886

This theorem is referenced by:  nn0ge2m1nn0  11953  nnzd  12074  eluzge2nn0  12275  expgt1  13463  expaddzlem  13468  expaddz  13469  expmulz  13471  expmulnbnd  13592  facwordi  13645  faclbnd  13646  facavg  13657  bcm1k  13671  wrdeqs1cat  14073  cshwcsh2id  14181  relexpsucnnr  14376  isercolllem2  15014  bcxmas  15182  climcndslem1  15196  climcndslem2  15197  climcnds  15198  pwdif  15215  geo2sum  15221  mertenslem1  15232  prodmolem3  15279  prodmolem2a  15280  bpolydiflem  15400  eftabs  15421  efcllem  15423  eftlub  15454  eirrlem  15549  rpnnen2lem9  15567  rpnnen2lem11  15569  dvdsfac  15668  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  16418  psgnunilem3  18616  odfval  18652  mndodconglem  18661  gexcl3  18704  pgpfi1  18712  sylow1lem1  18715  gexexlem  18965  prmcyg  19007  gsumval3  19020  ablfacrplem  19180  ablfacrp  19181  ablfacrp2  19182  ablfac1eu  19188  prmgrpsimpgd  19229  srgbinomlem3  19285  srgbinomlem4  19286  chfacfscmulgsum  21465  chfacfpmmulgsum  21469  cpmadugsumlemF  21481  ovoliunlem1  24106  mbfi1fseqlem1  24319  mbfi1fseqlem3  24321  mbfi1fseqlem5  24323  itg2cnlem2  24366  dvply1  24880  aalioulem2  24929  aalioulem5  24932  aaliou3lem1  24938  aaliou3lem2  24939  aaliou3lem8  24941  aaliou3lem6  24944  taylthlem1  24968  taylthlem2  24969  pserdvlem2  25023  cxpeq  25346  dmgmdivn0  25613  lgamgulmlem5  25618  lgamcvg2  25640  wilthlem1  25653  ftalem1  25658  ftalem2  25659  ftalem4  25661  ftalem5  25662  basellem2  25667  basellem3  25668  basellem4  25669  basellem5  25670  isppw2  25700  dvdsmulf1o  25779  sgmmul  25785  fsumvma2  25798  chpchtsum  25803  logfacubnd  25805  mersenne  25811  perfect1  25812  perfectlem1  25813  perfectlem2  25814  perfect  25815  dchrelbas3  25822  dchrelbasd  25823  dchrzrh1  25828  dchrzrhmul  25830  dchrmulcl  25833  dchrn0  25834  dchrfi  25839  dchrghm  25840  dchrabs  25844  dchrinv  25845  dchrptlem1  25848  dchrptlem2  25849  dchrptlem3  25850  dchrpt  25851  dchrsum2  25852  sum2dchr  25858  pcbcctr  25860  bcmono  25861  bclbnd  25864  bposlem1  25868  bposlem3  25870  bposlem5  25872  bposlem6  25873  lgslem1  25881  lgsval2lem  25891  lgsvalmod  25900  lgsmod  25907  lgsdirprm  25915  lgsne0  25919  lgsqrlem1  25930  lgsqrlem2  25931  lgsqrlem3  25932  lgsqrlem4  25933  gausslemma2dlem0b  25941  gausslemma2dlem0c  25942  gausslemma2dlem1  25950  gausslemma2dlem7  25957  gausslemma2d  25958  lgseisenlem1  25959  lgseisenlem2  25960  lgseisenlem3  25961  lgseisenlem4  25962  lgseisen  25963  lgsquadlem2  25965  lgsquadlem3  25966  m1lgs  25972  2lgslem1a  25975  2sqlem3  26004  2sqblem  26015  chebbnd1lem1  26053  chebbnd1lem3  26055  rplogsumlem2  26069  rpvmasumlem  26071  dchrisumlem1  26073  dchrisumlem2  26074  dchrmusum2  26078  dchrvmasumlem3  26083  dchrisum0ff  26091  dchrisum0flblem1  26092  rpvmasum2  26096  dchrisum0re  26097  dchrisum0lem2a  26101  dirith  26113  mudivsum  26114  pntpbnd1a  26169  pntlemq  26185  pntlemr  26186  pntlemj  26187  ostth2lem1  26202  ostth2lem2  26218  ostth2lem3  26219  ostth2  26221  crctcshwlkn0lem6  27601  hashecclwwlkn1  27862  umgrhashecclwwlk  27863  clwwlknon  27875  eucrctshift  28028  numclwlk1lem2  28155  dipcl  28495  dipcn  28503  bcm1n  30544  prmdvdsbc  30558  psgnfzto1st  30797  isarchi2  30864  submarchi  30865  freshmansdream  30909  submateqlem1  31160  madjusmdetlem2  31181  madjusmdetlem4  31183  mdetlap  31185  nexple  31378  oddpwdc  31722  eulerpartlemsv2  31726  eulerpartlemsf  31727  eulerpartlems  31728  eulerpartlemv  31732  eulerpartlemb  31736  plymulx0  31927  signsvtn0  31950  fsum2dsub  31988  reprinfz1  32003  reprpmtf1o  32007  circlemeth  32021  circlemethnat  32022  hgt750lemb  32037  hgt750lema  32038  hgt750leme  32039  tgoldbachgtde  32041  tgoldbachgtda  32042  lpadleft  32064  subfacp1lem1  32539  subfacp1lem6  32545  subfaclim  32548  erdszelem8  32558  erdszelem10  32560  cvmliftlem10  32654  faclim2  33093  poimirlem7  35064  poimirlem17  35074  poimirlem18  35075  poimirlem20  35077  poimirlem21  35078  poimirlem22  35079  poimirlem25  35082  poimirlem26  35083  poimirlem27  35084  poimirlem28  35085  poimirlem32  35089  nninfnub  35189  bfplem1  35260  lcmineqlem1  39317  lcmineqlem2  39318  lcmineqlem8  39324  lcmineqlem10  39326  lcmineqlem11  39327  lcmineqlem15  39331  lcmineqlem16  39332  lcmineqlem18  39334  lcmineqlem19  39335  lcmineqlem20  39336  lcmineqlem21  39337  lcmineqlem22  39338  metakunt2  39351  fsuppind  39456  oexpreposd  39487  nn0rppwr  39490  expgcd  39491  zrtelqelz  39500  dffltz  39615  fltne  39616  fltltc  39617  fltnltalem  39618  fltnlta  39619  3rexfrabdioph  39738  4rexfrabdioph  39739  6rexfrabdioph  39740  7rexfrabdioph  39741  irrapxlem5  39767  pellexlem2  39771  pellexlem6  39775  pell14qrgt0  39800  pell1qrge1  39811  pellfundgt1  39824  ltrmxnn0  39890  jm2.26lem3  39942  jm2.27a  39946  jm2.27c  39948  rmxdiophlem  39956  jm3.1lem1  39958  jm3.1lem2  39959  jm3.1lem3  39960  jm3.1  39961  dgrsub2  40079  mpaaeu  40094  idomsubgmo  40142  relexpxpmin  40418  nzprmdif  41023  binomcxplemwb  41052  fperiodmul  41936  xralrple4  42005  fsumnncl  42213  dvsinexp  42553  dvxpaek  42582  itgsinexplem1  42596  stoweidlem1  42643  stoweidlem17  42659  stoweidlem25  42667  stoweidlem34  42676  stoweidlem38  42680  stoweidlem40  42682  stoweidlem42  42684  stoweidlem45  42687  stirlinglem4  42719  stirlinglem5  42720  stirlinglem10  42725  stirlinglem13  42728  dirkertrigeq  42743  fourierdlem21  42770  fourierdlem25  42774  fourierdlem48  42796  fourierdlem54  42802  fourierdlem64  42812  fourierdlem65  42813  fourierdlem73  42821  fourierdlem81  42829  fourierdlem83  42831  fourierdlem92  42840  fourierdlem103  42851  fourierdlem104  42852  fourierdlem112  42860  fourierdlem113  42861  etransclem1  42877  etransclem4  42880  etransclem8  42884  etransclem15  42891  etransclem17  42893  etransclem18  42894  etransclem19  42895  etransclem20  42896  etransclem21  42897  etransclem22  42898  etransclem23  42899  etransclem24  42900  etransclem25  42901  etransclem27  42903  etransclem32  42908  etransclem35  42911  etransclem41  42917  etransclem44  42920  etransclem46  42922  iccpartigtl  43940  iccpartgt  43944  iccpartgel  43946  iccelpart  43950  odz2prm2pw  44080  fmtnoprmfac1  44082  fmtnoprmfac2  44084  2pwp1prm  44106  sfprmdvdsmersenne  44121  lighneallem4a  44126  proththdlem  44131  proththd  44132  perfectALTVlem1  44239  perfectALTVlem2  44240  perfectALTV  44241  fpprwpprb  44258  logbpw2m1  44981  nnpw2blenfzo  44995  nnolog2flm1  45004  dignn0fr  45015  nn0sumshdiglemA  45033  nn0sumshdiglemB  45034