Theorem nnnn0d 11351

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

Syntax hints:   → wi 4   ∈ wcel 1990  ℕcn 11020  ℕ₀cn0 11292

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-un 3579  df-in 3581  df-ss 3588  df-n0 11293

This theorem is referenced by:  nn0ge2m1nn0  11361  nnzd  11481  eluzge2nn0  11727  expgt1  12898  expaddzlem  12903  expaddz  12904  expmulz  12906  expmulnbnd  12996  facwordi  13076  faclbnd  13077  facavg  13088  bcm1k  13102  wrdeqs1cat  13474  cshwcsh2id  13574  relexpsucnnr  13765  isercolllem2  14396  bcxmas  14567  climcndslem1  14581  climcndslem2  14582  climcnds  14583  geo2sum  14604  mertenslem1  14616  prodmolem3  14663  prodmolem2a  14664  bpolydiflem  14785  eftabs  14806  efcllem  14808  eftlub  14839  eirrlem  14932  rpnnen2lem9  14951  rpnnen2lem11  14953  dvdsfac  15048  oddpwp1fsum  15115  bitsfzo  15157  bitsfi  15159  sadcaddlem  15179  smumullem  15214  gcdcl  15228  mulgcd  15265  rplpwr  15276  rppwr  15277  lcmcl  15314  lcmgcdnn  15324  lcmfcl  15341  nprmdvds1  15418  rpexp  15432  zsqrtelqelz  15466  phiprmpw  15481  eulerthlem2  15487  eulerth  15488  fermltl  15489  odzcllem  15497  odzdvds  15500  odzphi  15501  prm23lt5  15519  pythagtriplem6  15526  pythagtriplem7  15527  pcprmpw2  15586  dvdsprmpweqle  15590  pcprod  15599  pcfac  15603  pcbc  15604  expnprm  15606  pockthlem  15609  pockthg  15610  prmunb  15618  prmreclem2  15621  prmreclem3  15622  prmreclem4  15623  prmreclem5  15624  prmreclem6  15625  mul4sqlem  15657  4sqlem11  15659  4sqlem17  15665  vdwlem1  15685  vdwlem5  15689  vdwlem6  15690  vdwlem8  15692  vdwlem9  15693  vdwlem11  15695  vdwlem12  15696  vdwnnlem3  15701  ramz2  15728  ramub1lem1  15730  ramub1lem2  15731  ramub1  15732  prmgaplem3  15757  2expltfac  15799  psgnunilem3  17916  mndodconglem  17960  gexcl3  18002  pgpfi1  18010  sylow1lem1  18013  gexexlem  18255  prmcyg  18295  gsumval3  18308  ablfacrplem  18464  ablfacrp  18465  ablfacrp2  18466  ablfac1eu  18472  srgbinomlem3  18542  srgbinomlem4  18543  chfacfscmulgsum  20665  chfacfpmmulgsum  20669  cpmadugsumlemF  20681  ovoliunlem1  23270  mbfi1fseqlem1  23482  mbfi1fseqlem3  23484  mbfi1fseqlem5  23486  itg2cnlem2  23529  dvply1  24039  aalioulem2  24088  aalioulem5  24091  aaliou3lem1  24097  aaliou3lem2  24098  aaliou3lem8  24100  aaliou3lem6  24103  taylthlem1  24127  taylthlem2  24128  pserdvlem2  24182  cxpeq  24498  dmgmdivn0  24754  lgamgulmlem5  24759  lgamcvg2  24781  wilthlem1  24794  ftalem1  24799  ftalem2  24800  ftalem4  24802  ftalem5  24803  basellem2  24808  basellem3  24809  basellem4  24810  basellem5  24811  isppw2  24841  dvdsmulf1o  24920  sgmmul  24926  chpchtsum  24944  logfacubnd  24946  mersenne  24952  perfect1  24953  perfectlem1  24954  perfectlem2  24955  perfect  24956  dchrelbas3  24963  dchrelbasd  24964  dchrzrh1  24969  dchrzrhmul  24971  dchrmulcl  24974  dchrn0  24975  dchrfi  24980  dchrghm  24981  dchrabs  24985  dchrinv  24986  dchrptlem1  24989  dchrptlem2  24990  dchrptlem3  24991  dchrpt  24992  dchrsum2  24993  sum2dchr  24999  pcbcctr  25001  bcmono  25002  bclbnd  25005  bposlem1  25009  bposlem3  25011  bposlem5  25013  bposlem6  25014  lgslem1  25022  lgslem4  25025  lgsval2lem  25032  lgsvalmod  25041  lgsmod  25048  lgsdirprm  25056  lgsne0  25060  lgsqrlem1  25071  lgsqrlem2  25072  lgsqrlem3  25073  lgsqrlem4  25074  gausslemma2dlem0b  25082  gausslemma2dlem0c  25083  gausslemma2dlem1  25091  gausslemma2dlem7  25098  gausslemma2d  25099  lgseisenlem1  25100  lgseisenlem2  25101  lgseisenlem3  25102  lgseisenlem4  25103  lgseisen  25104  lgsquadlem2  25106  lgsquadlem3  25107  m1lgs  25113  2lgslem1a  25116  2sqlem3  25145  2sqblem  25156  chebbnd1lem1  25158  chebbnd1lem3  25160  rplogsumlem2  25174  rpvmasumlem  25176  dchrisumlem1  25178  dchrisumlem2  25179  dchrmusum2  25183  dchrvmasumlem3  25188  dchrisum0ff  25196  dchrisum0flblem1  25197  rpvmasum2  25201  dchrisum0re  25202  dchrisum0lem2a  25206  dirith  25218  mudivsum  25219  pntpbnd1a  25274  pntlemq  25290  pntlemr  25291  pntlemj  25292  ostth2lem2  25323  ostth2lem3  25324  ostth2  25326  crctcshwlkn0lem6  26707  hashecclwwlksn1  26954  umgrhashecclwwlk  26955  clwlksfclwwlk  26962  eucrctshift  27103  dipcl  27567  dipcn  27575  bcm1n  29554  isarchi2  29739  submarchi  29740  psgnfzto1st  29855  submateqlem1  29873  madjusmdetlem2  29894  madjusmdetlem4  29896  mdetlap  29898  nexple  30071  oddpwdc  30416  eulerpartlemsv2  30420  eulerpartlemsf  30421  eulerpartlems  30422  eulerpartlemv  30426  eulerpartlemb  30430  plymulx0  30624  signsvtn0  30647  fsum2dsub  30685  reprinfz1  30700  reprpmtf1o  30704  circlemeth  30718  circlemethnat  30719  hgt750lemb  30734  hgt750lema  30735  hgt750leme  30736  tgoldbachgtde  30738  tgoldbachgtda  30739  subfacp1lem1  31161  subfacp1lem6  31167  subfaclim  31170  erdszelem8  31180  erdszelem10  31182  cvmliftlem10  31276  faclim2  31634  poimirlem7  33416  poimirlem17  33426  poimirlem18  33427  poimirlem20  33429  poimirlem21  33430  poimirlem22  33431  poimirlem25  33434  poimirlem26  33435  poimirlem27  33436  poimirlem28  33437  poimirlem32  33441  nninfnub  33547  bfplem1  33621  3rexfrabdioph  37361  4rexfrabdioph  37362  6rexfrabdioph  37363  7rexfrabdioph  37364  irrapxlem5  37390  pellexlem2  37394  pellexlem6  37398  pell14qrgt0  37423  pell1qrge1  37434  pellfundgt1  37447  ltrmxnn0  37516  jm2.26lem3  37568  jm2.27a  37572  jm2.27c  37574  rmxdiophlem  37582  jm3.1lem1  37584  jm3.1lem2  37585  jm3.1lem3  37586  jm3.1  37587  dgrsub2  37705  mpaaeu  37720  idomsubgmo  37776  relexpxpmin  38009  nzprmdif  38518  binomcxplemwb  38547  fperiodmul  39518  xralrple4  39589  fsumnncl  39803  dvsinexp  40125  dvxpaek  40155  itgsinexplem1  40169  stoweidlem1  40218  stoweidlem17  40234  stoweidlem25  40242  stoweidlem34  40251  stoweidlem38  40255  stoweidlem40  40257  stoweidlem42  40259  stoweidlem45  40262  stirlinglem4  40294  stirlinglem5  40295  stirlinglem10  40300  stirlinglem13  40303  dirkertrigeq  40318  fourierdlem21  40345  fourierdlem25  40349  fourierdlem48  40371  fourierdlem54  40377  fourierdlem64  40387  fourierdlem65  40388  fourierdlem73  40396  fourierdlem81  40404  fourierdlem83  40406  fourierdlem92  40415  fourierdlem103  40426  fourierdlem104  40427  fourierdlem112  40435  fourierdlem113  40436  etransclem1  40452  etransclem4  40455  etransclem8  40459  etransclem15  40466  etransclem17  40468  etransclem18  40469  etransclem19  40470  etransclem20  40471  etransclem21  40472  etransclem22  40473  etransclem23  40474  etransclem24  40475  etransclem25  40476  etransclem27  40478  etransclem32  40483  etransclem35  40486  etransclem41  40492  etransclem44  40495  etransclem46  40497  iccpartigtl  41359  iccpartgt  41363  iccpartgel  41365  iccelpart  41369  odz2prm2pw  41475  fmtnoprmfac1  41477  fmtnoprmfac2  41479  pwdif  41501  2pwp1prm  41503  sfprmdvdsmersenne  41520  lighneallem4a  41525  proththdlem  41530  proththd  41531  perfectALTVlem1  41630  perfectALTVlem2  41631  perfectALTV  41632  logbpw2m1  42361  nnpw2blenfzo  42375  nnolog2flm1  42384  dignn0fr  42395  nn0sumshdiglemA  42413  nn0sumshdiglemB  42414