Theorem nnnn0d 12223

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℕcn 11903  ℕ₀cn0 12163

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-un 3888  df-in 3890  df-ss 3900  df-n0 12164

This theorem is referenced by:  nn0ge2m1nn0  12233  nnzd  12354  eluzge2nn0  12556  expgt1  13749  expaddzlem  13754  expaddz  13755  expmulz  13757  expmulnbnd  13878  facwordi  13931  faclbnd  13932  facavg  13943  bcm1k  13957  wrdeqs1cat  14361  cshwcsh2id  14469  relexpsucnnr  14664  isercolllem2  15305  bcxmas  15475  climcndslem1  15489  climcndslem2  15490  climcnds  15491  pwdif  15508  geo2sum  15513  mertenslem1  15524  prodmolem3  15571  prodmolem2a  15572  bpolydiflem  15692  eftabs  15713  efcllem  15715  eftlub  15746  eirrlem  15841  rpnnen2lem9  15859  rpnnen2lem11  15861  dvdsfac  15963  pwp1fsum  16028  oddpwp1fsum  16029  bitsfzo  16070  bitsfi  16072  sadcaddlem  16092  smumullem  16127  gcdcl  16141  dvdsgcdidd  16173  mulgcd  16184  rplpwr  16195  rprpwr  16196  rppwr  16197  lcmcl  16234  lcmgcdnn  16244  lcmfcl  16261  nprmdvds1  16339  rpexp  16355  zsqrtelqelz  16390  phiprmpw  16405  eulerthlem2  16411  eulerth  16412  fermltl  16413  odzcllem  16421  odzdvds  16424  odzphi  16425  prm23lt5  16443  pythagtriplem6  16450  pythagtriplem7  16451  pcprmpw2  16511  dvdsprmpweqle  16515  pcprod  16524  pcfac  16528  pcbc  16529  expnprm  16531  pockthlem  16534  pockthg  16535  prmunb  16543  prmreclem2  16546  prmreclem3  16547  prmreclem4  16548  prmreclem5  16549  prmreclem6  16550  mul4sqlem  16582  4sqlem11  16584  4sqlem17  16590  vdwlem1  16610  vdwlem5  16614  vdwlem6  16615  vdwlem8  16617  vdwlem9  16618  vdwlem11  16620  vdwlem12  16621  vdwnnlem3  16626  ramz2  16653  ramub1lem1  16655  ramub1lem2  16656  ramub1  16657  prmgaplem3  16682  2expltfac  16722  psgnunilem3  19019  odfval  19055  mndodconglem  19064  gexcl3  19107  pgpfi1  19115  sylow1lem1  19118  gexexlem  19368  prmcyg  19410  gsumval3  19423  ablfacrplem  19583  ablfacrp  19584  ablfacrp2  19585  ablfac1eu  19591  prmgrpsimpgd  19632  srgbinomlem3  19693  srgbinomlem4  19694  chfacfscmulgsum  21917  chfacfpmmulgsum  21921  cpmadugsumlemF  21933  ovoliunlem1  24571  mbfi1fseqlem1  24785  mbfi1fseqlem3  24787  mbfi1fseqlem5  24789  itg2cnlem2  24832  dvply1  25349  aalioulem2  25398  aalioulem5  25401  aaliou3lem1  25407  aaliou3lem2  25408  aaliou3lem8  25410  aaliou3lem6  25413  taylthlem1  25437  taylthlem2  25438  pserdvlem2  25492  cxpeq  25815  dmgmdivn0  26082  lgamgulmlem5  26087  lgamcvg2  26109  wilthlem1  26122  ftalem1  26127  ftalem2  26128  ftalem4  26130  ftalem5  26131  basellem2  26136  basellem3  26137  basellem4  26138  basellem5  26139  isppw2  26169  dvdsmulf1o  26248  sgmmul  26254  fsumvma2  26267  chpchtsum  26272  logfacubnd  26274  mersenne  26280  perfect1  26281  perfectlem1  26282  perfectlem2  26283  perfect  26284  dchrelbas3  26291  dchrelbasd  26292  dchrzrh1  26297  dchrzrhmul  26299  dchrmulcl  26302  dchrn0  26303  dchrfi  26308  dchrghm  26309  dchrabs  26313  dchrinv  26314  dchrptlem1  26317  dchrptlem2  26318  dchrptlem3  26319  dchrpt  26320  dchrsum2  26321  sum2dchr  26327  pcbcctr  26329  bcmono  26330  bclbnd  26333  bposlem1  26337  bposlem3  26339  bposlem5  26341  bposlem6  26342  lgslem1  26350  lgsval2lem  26360  lgsvalmod  26369  lgsmod  26376  lgsdirprm  26384  lgsne0  26388  lgsqrlem1  26399  lgsqrlem2  26400  lgsqrlem3  26401  lgsqrlem4  26402  gausslemma2dlem0b  26410  gausslemma2dlem0c  26411  gausslemma2dlem1  26419  gausslemma2dlem7  26426  gausslemma2d  26427  lgseisenlem1  26428  lgseisenlem2  26429  lgseisenlem3  26430  lgseisenlem4  26431  lgseisen  26432  lgsquadlem2  26434  lgsquadlem3  26435  m1lgs  26441  2lgslem1a  26444  2sqlem3  26473  2sqblem  26484  chebbnd1lem1  26522  chebbnd1lem3  26524  rplogsumlem2  26538  rpvmasumlem  26540  dchrisumlem1  26542  dchrisumlem2  26543  dchrmusum2  26547  dchrvmasumlem3  26552  dchrisum0ff  26560  dchrisum0flblem1  26561  rpvmasum2  26565  dchrisum0re  26566  dchrisum0lem2a  26570  dirith  26582  mudivsum  26583  pntpbnd1a  26638  pntlemq  26654  pntlemr  26655  pntlemj  26656  ostth2lem1  26671  ostth2lem2  26687  ostth2lem3  26688  ostth2  26690  crctcshwlkn0lem6  28081  hashecclwwlkn1  28342  umgrhashecclwwlk  28343  clwwlknon  28355  eucrctshift  28508  numclwlk1lem2  28635  dipcl  28975  dipcn  28983  bcm1n  31018  prmdvdsbc  31032  psgnfzto1st  31274  isarchi2  31341  submarchi  31342  freshmansdream  31386  znfermltl  31464  submateqlem1  31659  madjusmdetlem2  31680  madjusmdetlem4  31682  mdetlap  31684  nexple  31877  oddpwdc  32221  eulerpartlemsv2  32225  eulerpartlemsf  32226  eulerpartlems  32227  eulerpartlemv  32231  eulerpartlemb  32235  plymulx0  32426  signsvtn0  32449  fsum2dsub  32487  reprinfz1  32502  reprpmtf1o  32506  circlemeth  32520  circlemethnat  32521  hgt750lemb  32536  hgt750lema  32537  hgt750leme  32538  tgoldbachgtde  32540  tgoldbachgtda  32541  lpadleft  32563  subfacp1lem1  33041  subfacp1lem6  33047  subfaclim  33050  erdszelem8  33060  erdszelem10  33062  cvmliftlem10  33156  faclim2  33620  poimirlem7  35711  poimirlem17  35721  poimirlem18  35722  poimirlem20  35724  poimirlem21  35725  poimirlem22  35726  poimirlem25  35729  poimirlem26  35730  poimirlem27  35731  poimirlem28  35732  poimirlem32  35736  nninfnub  35836  bfplem1  35907  lcmineqlem1  39965  lcmineqlem2  39966  lcmineqlem8  39972  lcmineqlem10  39974  lcmineqlem11  39975  lcmineqlem15  39979  lcmineqlem16  39980  lcmineqlem18  39982  lcmineqlem19  39983  lcmineqlem20  39984  lcmineqlem21  39985  lcmineqlem22  39986  3lexlogpow2ineq2  39995  dvrelogpow2b  40004  aks4d1p1p2  40006  aks4d1p1p4  40007  aks4d1p1  40012  aks4d1p3  40014  aks4d1p7d1  40018  aks4d1p7  40019  aks4d1p8  40023  aks4d1p9  40024  sticksstones6  40035  sticksstones7  40036  sticksstones10  40039  sticksstones12a  40041  sticksstones12  40042  sticksstones20  40050  sticksstones22  40052  metakunt2  40054  fsuppind  40202  oexpreposd  40242  exp11nnd  40245  exp11d  40246  nn0rppwr  40254  expgcd  40255  dvdsexpb  40263  zrtelqelz  40266  dffltz  40387  fltdvdsabdvdsc  40391  fltne  40397  flt4lem4  40402  flt4lem7  40412  fltltc  40414  fltnltalem  40415  fltnlta  40416  3rexfrabdioph  40535  4rexfrabdioph  40536  6rexfrabdioph  40537  7rexfrabdioph  40538  irrapxlem5  40564  pellexlem2  40568  pellexlem6  40572  pell14qrgt0  40597  pell1qrge1  40608  pellfundgt1  40621  ltrmxnn0  40687  jm2.26lem3  40739  jm2.27a  40743  jm2.27c  40745  rmxdiophlem  40753  jm3.1lem1  40755  jm3.1lem2  40756  jm3.1lem3  40757  jm3.1  40758  dgrsub2  40876  mpaaeu  40891  idomsubgmo  40939  relexpxpmin  41214  nzprmdif  41826  binomcxplemwb  41855  fperiodmul  42733  xralrple4  42802  fsumnncl  43003  dvsinexp  43342  dvxpaek  43371  itgsinexplem1  43385  stoweidlem1  43432  stoweidlem17  43448  stoweidlem25  43456  stoweidlem34  43465  stoweidlem38  43469  stoweidlem40  43471  stoweidlem42  43473  stoweidlem45  43476  stirlinglem4  43508  stirlinglem5  43509  stirlinglem10  43514  stirlinglem13  43517  dirkertrigeq  43532  fourierdlem21  43559  fourierdlem25  43563  fourierdlem48  43585  fourierdlem54  43591  fourierdlem64  43601  fourierdlem65  43602  fourierdlem73  43610  fourierdlem81  43618  fourierdlem83  43620  fourierdlem92  43629  fourierdlem103  43640  fourierdlem104  43641  fourierdlem112  43649  fourierdlem113  43650  etransclem1  43666  etransclem4  43669  etransclem8  43673  etransclem15  43680  etransclem17  43682  etransclem18  43683  etransclem19  43684  etransclem20  43685  etransclem21  43686  etransclem22  43687  etransclem23  43688  etransclem24  43689  etransclem25  43690  etransclem27  43692  etransclem32  43697  etransclem35  43700  etransclem41  43706  etransclem44  43709  etransclem46  43711  iccpartigtl  44763  iccpartgt  44767  iccpartgel  44769  iccelpart  44773  odz2prm2pw  44903  fmtnoprmfac1  44905  fmtnoprmfac2  44907  2pwp1prm  44929  sfprmdvdsmersenne  44943  lighneallem4a  44948  proththdlem  44953  proththd  44954  perfectALTVlem1  45061  perfectALTVlem2  45062  perfectALTV  45063  fpprwpprb  45080  logbpw2m1  45801  nnpw2blenfzo  45815  nnolog2flm1  45824  dignn0fr  45835  nn0sumshdiglemA  45853  nn0sumshdiglemB  45854