Theorem nnnn0d 12039

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℕcn 11719  ℕ₀cn0 11979

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2711

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2718  df-cleq 2731  df-clel 2812  df-v 3401  df-un 3849  df-in 3851  df-ss 3861  df-n0 11980

This theorem is referenced by:  nn0ge2m1nn0  12049  nnzd  12170  eluzge2nn0  12372  expgt1  13562  expaddzlem  13567  expaddz  13568  expmulz  13570  expmulnbnd  13691  facwordi  13744  faclbnd  13745  facavg  13756  bcm1k  13770  wrdeqs1cat  14174  cshwcsh2id  14282  relexpsucnnr  14477  isercolllem2  15118  bcxmas  15286  climcndslem1  15300  climcndslem2  15301  climcnds  15302  pwdif  15319  geo2sum  15324  mertenslem1  15335  prodmolem3  15382  prodmolem2a  15383  bpolydiflem  15503  eftabs  15524  efcllem  15526  eftlub  15557  eirrlem  15652  rpnnen2lem9  15670  rpnnen2lem11  15672  dvdsfac  15774  pwp1fsum  15839  oddpwp1fsum  15840  bitsfzo  15881  bitsfi  15883  sadcaddlem  15903  smumullem  15938  gcdcl  15952  dvdsgcdidd  15984  mulgcd  15995  rplpwr  16006  rprpwr  16007  rppwr  16008  lcmcl  16045  lcmgcdnn  16055  lcmfcl  16072  nprmdvds1  16150  rpexp  16166  zsqrtelqelz  16201  phiprmpw  16216  eulerthlem2  16222  eulerth  16223  fermltl  16224  odzcllem  16232  odzdvds  16235  odzphi  16236  prm23lt5  16254  pythagtriplem6  16261  pythagtriplem7  16262  pcprmpw2  16321  dvdsprmpweqle  16325  pcprod  16334  pcfac  16338  pcbc  16339  expnprm  16341  pockthlem  16344  pockthg  16345  prmunb  16353  prmreclem2  16356  prmreclem3  16357  prmreclem4  16358  prmreclem5  16359  prmreclem6  16360  mul4sqlem  16392  4sqlem11  16394  4sqlem17  16400  vdwlem1  16420  vdwlem5  16424  vdwlem6  16425  vdwlem8  16427  vdwlem9  16428  vdwlem11  16430  vdwlem12  16431  vdwnnlem3  16436  ramz2  16463  ramub1lem1  16465  ramub1lem2  16466  ramub1  16467  prmgaplem3  16492  2expltfac  16532  psgnunilem3  18745  odfval  18781  mndodconglem  18790  gexcl3  18833  pgpfi1  18841  sylow1lem1  18844  gexexlem  19094  prmcyg  19136  gsumval3  19149  ablfacrplem  19309  ablfacrp  19310  ablfacrp2  19311  ablfac1eu  19317  prmgrpsimpgd  19358  srgbinomlem3  19414  srgbinomlem4  19415  chfacfscmulgsum  21614  chfacfpmmulgsum  21618  cpmadugsumlemF  21630  ovoliunlem1  24257  mbfi1fseqlem1  24471  mbfi1fseqlem3  24473  mbfi1fseqlem5  24475  itg2cnlem2  24518  dvply1  25035  aalioulem2  25084  aalioulem5  25087  aaliou3lem1  25093  aaliou3lem2  25094  aaliou3lem8  25096  aaliou3lem6  25099  taylthlem1  25123  taylthlem2  25124  pserdvlem2  25178  cxpeq  25501  dmgmdivn0  25768  lgamgulmlem5  25773  lgamcvg2  25795  wilthlem1  25808  ftalem1  25813  ftalem2  25814  ftalem4  25816  ftalem5  25817  basellem2  25822  basellem3  25823  basellem4  25824  basellem5  25825  isppw2  25855  dvdsmulf1o  25934  sgmmul  25940  fsumvma2  25953  chpchtsum  25958  logfacubnd  25960  mersenne  25966  perfect1  25967  perfectlem1  25968  perfectlem2  25969  perfect  25970  dchrelbas3  25977  dchrelbasd  25978  dchrzrh1  25983  dchrzrhmul  25985  dchrmulcl  25988  dchrn0  25989  dchrfi  25994  dchrghm  25995  dchrabs  25999  dchrinv  26000  dchrptlem1  26003  dchrptlem2  26004  dchrptlem3  26005  dchrpt  26006  dchrsum2  26007  sum2dchr  26013  pcbcctr  26015  bcmono  26016  bclbnd  26019  bposlem1  26023  bposlem3  26025  bposlem5  26027  bposlem6  26028  lgslem1  26036  lgsval2lem  26046  lgsvalmod  26055  lgsmod  26062  lgsdirprm  26070  lgsne0  26074  lgsqrlem1  26085  lgsqrlem2  26086  lgsqrlem3  26087  lgsqrlem4  26088  gausslemma2dlem0b  26096  gausslemma2dlem0c  26097  gausslemma2dlem1  26105  gausslemma2dlem7  26112  gausslemma2d  26113  lgseisenlem1  26114  lgseisenlem2  26115  lgseisenlem3  26116  lgseisenlem4  26117  lgseisen  26118  lgsquadlem2  26120  lgsquadlem3  26121  m1lgs  26127  2lgslem1a  26130  2sqlem3  26159  2sqblem  26170  chebbnd1lem1  26208  chebbnd1lem3  26210  rplogsumlem2  26224  rpvmasumlem  26226  dchrisumlem1  26228  dchrisumlem2  26229  dchrmusum2  26233  dchrvmasumlem3  26238  dchrisum0ff  26246  dchrisum0flblem1  26247  rpvmasum2  26251  dchrisum0re  26252  dchrisum0lem2a  26256  dirith  26268  mudivsum  26269  pntpbnd1a  26324  pntlemq  26340  pntlemr  26341  pntlemj  26342  ostth2lem1  26357  ostth2lem2  26373  ostth2lem3  26374  ostth2  26376  crctcshwlkn0lem6  27756  hashecclwwlkn1  28017  umgrhashecclwwlk  28018  clwwlknon  28030  eucrctshift  28183  numclwlk1lem2  28310  dipcl  28650  dipcn  28658  bcm1n  30694  prmdvdsbc  30708  psgnfzto1st  30952  isarchi2  31019  submarchi  31020  freshmansdream  31064  znfermltl  31137  submateqlem1  31332  madjusmdetlem2  31353  madjusmdetlem4  31355  mdetlap  31357  nexple  31550  oddpwdc  31894  eulerpartlemsv2  31898  eulerpartlemsf  31899  eulerpartlems  31900  eulerpartlemv  31904  eulerpartlemb  31908  plymulx0  32099  signsvtn0  32122  fsum2dsub  32160  reprinfz1  32175  reprpmtf1o  32179  circlemeth  32193  circlemethnat  32194  hgt750lemb  32209  hgt750lema  32210  hgt750leme  32211  tgoldbachgtde  32213  tgoldbachgtda  32214  lpadleft  32236  subfacp1lem1  32715  subfacp1lem6  32721  subfaclim  32724  erdszelem8  32734  erdszelem10  32736  cvmliftlem10  32830  faclim2  33290  poimirlem7  35430  poimirlem17  35440  poimirlem18  35441  poimirlem20  35443  poimirlem21  35444  poimirlem22  35445  poimirlem25  35448  poimirlem26  35449  poimirlem27  35450  poimirlem28  35451  poimirlem32  35455  nninfnub  35555  bfplem1  35626  lcmineqlem1  39680  lcmineqlem2  39681  lcmineqlem8  39687  lcmineqlem10  39689  lcmineqlem11  39690  lcmineqlem15  39694  lcmineqlem16  39695  lcmineqlem18  39697  lcmineqlem19  39698  lcmineqlem20  39699  lcmineqlem21  39700  lcmineqlem22  39701  3lexlogpow2ineq2  39710  dvrelogpow2b  39718  aks4d1p1p2  39720  aks4d1p1p4  39721  aks4d1p1  39726  sticksstones6  39736  sticksstones7  39737  metakunt2  39740  fsuppind  39881  oexpreposd  39920  exp11nnd  39924  exp11d  39925  nn0rppwr  39933  expgcd  39934  dvdsexpb  39942  zrtelqelz  39945  dffltz  40066  fltdvdsabdvdsc  40070  fltne  40076  flt4lem4  40081  flt4lem7  40091  fltltc  40093  fltnltalem  40094  fltnlta  40095  3rexfrabdioph  40214  4rexfrabdioph  40215  6rexfrabdioph  40216  7rexfrabdioph  40217  irrapxlem5  40243  pellexlem2  40247  pellexlem6  40251  pell14qrgt0  40276  pell1qrge1  40287  pellfundgt1  40300  ltrmxnn0  40366  jm2.26lem3  40418  jm2.27a  40422  jm2.27c  40424  rmxdiophlem  40432  jm3.1lem1  40434  jm3.1lem2  40435  jm3.1lem3  40436  jm3.1  40437  dgrsub2  40555  mpaaeu  40570  idomsubgmo  40618  relexpxpmin  40894  nzprmdif  41498  binomcxplemwb  41527  fperiodmul  42404  xralrple4  42473  fsumnncl  42677  dvsinexp  43017  dvxpaek  43046  itgsinexplem1  43060  stoweidlem1  43107  stoweidlem17  43123  stoweidlem25  43131  stoweidlem34  43140  stoweidlem38  43144  stoweidlem40  43146  stoweidlem42  43148  stoweidlem45  43151  stirlinglem4  43183  stirlinglem5  43184  stirlinglem10  43189  stirlinglem13  43192  dirkertrigeq  43207  fourierdlem21  43234  fourierdlem25  43238  fourierdlem48  43260  fourierdlem54  43266  fourierdlem64  43276  fourierdlem65  43277  fourierdlem73  43285  fourierdlem81  43293  fourierdlem83  43295  fourierdlem92  43304  fourierdlem103  43315  fourierdlem104  43316  fourierdlem112  43324  fourierdlem113  43325  etransclem1  43341  etransclem4  43344  etransclem8  43348  etransclem15  43355  etransclem17  43357  etransclem18  43358  etransclem19  43359  etransclem20  43360  etransclem21  43361  etransclem22  43362  etransclem23  43363  etransclem24  43364  etransclem25  43365  etransclem27  43367  etransclem32  43372  etransclem35  43375  etransclem41  43381  etransclem44  43384  etransclem46  43386  iccpartigtl  44439  iccpartgt  44443  iccpartgel  44445  iccelpart  44449  odz2prm2pw  44579  fmtnoprmfac1  44581  fmtnoprmfac2  44583  2pwp1prm  44605  sfprmdvdsmersenne  44619  lighneallem4a  44624  proththdlem  44629  proththd  44630  perfectALTVlem1  44737  perfectALTVlem2  44738  perfectALTV  44739  fpprwpprb  44756  logbpw2m1  45477  nnpw2blenfzo  45491  nnolog2flm1  45500  dignn0fr  45511  nn0sumshdiglemA  45529  nn0sumshdiglemB  45530