Theorem nnnn0d 12302

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

Syntax hints:   → wi 4   ∈ wcel 2107  ℕcn 11982  ℕ₀cn0 12242

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-un 3893  df-in 3895  df-ss 3905  df-n0 12243

This theorem is referenced by:  nn0ge2m1nn0  12312  nnzd  12434  eluzge2nn0  12636  expgt1  13830  expaddzlem  13835  expaddz  13836  expmulz  13838  expmulnbnd  13959  facwordi  14012  faclbnd  14013  facavg  14024  bcm1k  14038  wrdeqs1cat  14442  cshwcsh2id  14550  relexpsucnnr  14745  isercolllem2  15386  bcxmas  15556  climcndslem1  15570  climcndslem2  15571  climcnds  15572  pwdif  15589  geo2sum  15594  mertenslem1  15605  prodmolem3  15652  prodmolem2a  15653  bpolydiflem  15773  eftabs  15794  efcllem  15796  eftlub  15827  eirrlem  15922  rpnnen2lem9  15940  rpnnen2lem11  15942  dvdsfac  16044  pwp1fsum  16109  oddpwp1fsum  16110  bitsfzo  16151  bitsfi  16153  sadcaddlem  16173  smumullem  16208  gcdcl  16222  dvdsgcdidd  16254  mulgcd  16265  rplpwr  16276  rprpwr  16277  rppwr  16278  lcmcl  16315  lcmgcdnn  16325  lcmfcl  16342  nprmdvds1  16420  rpexp  16436  zsqrtelqelz  16471  phiprmpw  16486  eulerthlem2  16492  eulerth  16493  fermltl  16494  odzcllem  16502  odzdvds  16505  odzphi  16506  prm23lt5  16524  pythagtriplem6  16531  pythagtriplem7  16532  pcprmpw2  16592  dvdsprmpweqle  16596  pcprod  16605  pcfac  16609  pcbc  16610  expnprm  16612  pockthlem  16615  pockthg  16616  prmunb  16624  prmreclem2  16627  prmreclem3  16628  prmreclem4  16629  prmreclem5  16630  prmreclem6  16631  mul4sqlem  16663  4sqlem11  16665  4sqlem17  16671  vdwlem1  16691  vdwlem5  16695  vdwlem6  16696  vdwlem8  16698  vdwlem9  16699  vdwlem11  16701  vdwlem12  16702  vdwnnlem3  16707  ramz2  16734  ramub1lem1  16736  ramub1lem2  16737  ramub1  16738  prmgaplem3  16763  2expltfac  16803  psgnunilem3  19113  odfval  19149  mndodconglem  19158  gexcl3  19201  pgpfi1  19209  sylow1lem1  19212  gexexlem  19462  prmcyg  19504  gsumval3  19517  ablfacrplem  19677  ablfacrp  19678  ablfacrp2  19679  ablfac1eu  19685  prmgrpsimpgd  19726  srgbinomlem3  19787  srgbinomlem4  19788  chfacfscmulgsum  22018  chfacfpmmulgsum  22022  cpmadugsumlemF  22034  ovoliunlem1  24675  mbfi1fseqlem1  24889  mbfi1fseqlem3  24891  mbfi1fseqlem5  24893  itg2cnlem2  24936  dvply1  25453  aalioulem2  25502  aalioulem5  25505  aaliou3lem1  25511  aaliou3lem2  25512  aaliou3lem8  25514  aaliou3lem6  25517  taylthlem1  25541  taylthlem2  25542  pserdvlem2  25596  cxpeq  25919  dmgmdivn0  26186  lgamgulmlem5  26191  lgamcvg2  26213  wilthlem1  26226  ftalem1  26231  ftalem2  26232  ftalem4  26234  ftalem5  26235  basellem2  26240  basellem3  26241  basellem4  26242  basellem5  26243  isppw2  26273  dvdsmulf1o  26352  sgmmul  26358  fsumvma2  26371  chpchtsum  26376  logfacubnd  26378  mersenne  26384  perfect1  26385  perfectlem1  26386  perfectlem2  26387  perfect  26388  dchrelbas3  26395  dchrelbasd  26396  dchrzrh1  26401  dchrzrhmul  26403  dchrmulcl  26406  dchrn0  26407  dchrfi  26412  dchrghm  26413  dchrabs  26417  dchrinv  26418  dchrptlem1  26421  dchrptlem2  26422  dchrptlem3  26423  dchrpt  26424  dchrsum2  26425  sum2dchr  26431  pcbcctr  26433  bcmono  26434  bclbnd  26437  bposlem1  26441  bposlem3  26443  bposlem5  26445  bposlem6  26446  lgslem1  26454  lgsval2lem  26464  lgsvalmod  26473  lgsmod  26480  lgsdirprm  26488  lgsne0  26492  lgsqrlem1  26503  lgsqrlem2  26504  lgsqrlem3  26505  lgsqrlem4  26506  gausslemma2dlem0b  26514  gausslemma2dlem0c  26515  gausslemma2dlem1  26523  gausslemma2dlem7  26530  gausslemma2d  26531  lgseisenlem1  26532  lgseisenlem2  26533  lgseisenlem3  26534  lgseisenlem4  26535  lgseisen  26536  lgsquadlem2  26538  lgsquadlem3  26539  m1lgs  26545  2lgslem1a  26548  2sqlem3  26577  2sqblem  26588  chebbnd1lem1  26626  chebbnd1lem3  26628  rplogsumlem2  26642  rpvmasumlem  26644  dchrisumlem1  26646  dchrisumlem2  26647  dchrmusum2  26651  dchrvmasumlem3  26656  dchrisum0ff  26664  dchrisum0flblem1  26665  rpvmasum2  26669  dchrisum0re  26670  dchrisum0lem2a  26674  dirith  26686  mudivsum  26687  pntpbnd1a  26742  pntlemq  26758  pntlemr  26759  pntlemj  26760  ostth2lem1  26775  ostth2lem2  26791  ostth2lem3  26792  ostth2  26794  crctcshwlkn0lem6  28189  hashecclwwlkn1  28450  umgrhashecclwwlk  28451  clwwlknon  28463  eucrctshift  28616  numclwlk1lem2  28743  dipcl  29083  dipcn  29091  bcm1n  31125  prmdvdsbc  31139  psgnfzto1st  31381  isarchi2  31448  submarchi  31449  freshmansdream  31493  znfermltl  31571  submateqlem1  31766  madjusmdetlem2  31787  madjusmdetlem4  31789  mdetlap  31791  nexple  31986  oddpwdc  32330  eulerpartlemsv2  32334  eulerpartlemsf  32335  eulerpartlems  32336  eulerpartlemv  32340  eulerpartlemb  32344  plymulx0  32535  signsvtn0  32558  fsum2dsub  32596  reprinfz1  32611  reprpmtf1o  32615  circlemeth  32629  circlemethnat  32630  hgt750lemb  32645  hgt750lema  32646  hgt750leme  32647  tgoldbachgtde  32649  tgoldbachgtda  32650  lpadleft  32672  subfacp1lem1  33150  subfacp1lem6  33156  subfaclim  33159  erdszelem8  33169  erdszelem10  33171  cvmliftlem10  33265  faclim2  33723  poimirlem7  35793  poimirlem17  35803  poimirlem18  35804  poimirlem20  35806  poimirlem21  35807  poimirlem22  35808  poimirlem25  35811  poimirlem26  35812  poimirlem27  35813  poimirlem28  35814  poimirlem32  35818  nninfnub  35918  bfplem1  35989  lcmineqlem1  40044  lcmineqlem2  40045  lcmineqlem8  40051  lcmineqlem10  40053  lcmineqlem11  40054  lcmineqlem15  40058  lcmineqlem16  40059  lcmineqlem18  40061  lcmineqlem19  40062  lcmineqlem20  40063  lcmineqlem21  40064  lcmineqlem22  40065  3lexlogpow2ineq2  40074  dvrelogpow2b  40083  aks4d1p1p2  40085  aks4d1p1p4  40086  aks4d1p1  40091  aks4d1p3  40093  aks4d1p7d1  40097  aks4d1p7  40098  aks4d1p8  40102  aks4d1p9  40103  sticksstones6  40114  sticksstones7  40115  sticksstones10  40118  sticksstones12a  40120  sticksstones12  40121  sticksstones20  40129  sticksstones22  40131  metakunt2  40133  fsuppind  40286  oexpreposd  40328  exp11nnd  40331  exp11d  40332  nn0rppwr  40340  expgcd  40341  dvdsexpb  40349  zrtelqelz  40352  dffltz  40478  fltdvdsabdvdsc  40482  fltne  40488  flt4lem4  40493  flt4lem7  40503  fltltc  40505  fltnltalem  40506  fltnlta  40507  3rexfrabdioph  40626  4rexfrabdioph  40627  6rexfrabdioph  40628  7rexfrabdioph  40629  irrapxlem5  40655  pellexlem2  40659  pellexlem6  40663  pell14qrgt0  40688  pell1qrge1  40699  pellfundgt1  40712  ltrmxnn0  40778  jm2.26lem3  40830  jm2.27a  40834  jm2.27c  40836  rmxdiophlem  40844  jm3.1lem1  40846  jm3.1lem2  40847  jm3.1lem3  40848  jm3.1  40849  dgrsub2  40967  mpaaeu  40982  idomsubgmo  41030  relexpxpmin  41332  nzprmdif  41944  binomcxplemwb  41973  fperiodmul  42850  xralrple4  42919  fsumnncl  43120  dvsinexp  43459  dvxpaek  43488  itgsinexplem1  43502  stoweidlem1  43549  stoweidlem17  43565  stoweidlem25  43573  stoweidlem34  43582  stoweidlem38  43586  stoweidlem40  43588  stoweidlem42  43590  stoweidlem45  43593  stirlinglem4  43625  stirlinglem5  43626  stirlinglem10  43631  stirlinglem13  43634  dirkertrigeq  43649  fourierdlem21  43676  fourierdlem25  43680  fourierdlem48  43702  fourierdlem54  43708  fourierdlem64  43718  fourierdlem65  43719  fourierdlem73  43727  fourierdlem81  43735  fourierdlem83  43737  fourierdlem92  43746  fourierdlem103  43757  fourierdlem104  43758  fourierdlem112  43766  fourierdlem113  43767  etransclem1  43783  etransclem4  43786  etransclem8  43790  etransclem15  43797  etransclem17  43799  etransclem18  43800  etransclem19  43801  etransclem20  43802  etransclem21  43803  etransclem22  43804  etransclem23  43805  etransclem24  43806  etransclem25  43807  etransclem27  43809  etransclem32  43814  etransclem35  43817  etransclem41  43823  etransclem44  43826  etransclem46  43828  iccpartigtl  44886  iccpartgt  44890  iccpartgel  44892  iccelpart  44896  odz2prm2pw  45026  fmtnoprmfac1  45028  fmtnoprmfac2  45030  2pwp1prm  45052  sfprmdvdsmersenne  45066  lighneallem4a  45071  proththdlem  45076  proththd  45077  perfectALTVlem1  45184  perfectALTVlem2  45185  perfectALTV  45186  fpprwpprb  45203  logbpw2m1  45924  nnpw2blenfzo  45938  nnolog2flm1  45947  dignn0fr  45958  nn0sumshdiglemA  45976  nn0sumshdiglemB  45977