Theorem nnnn0d 12674

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  ℕcn 12342  ℕ₀cn0 12613

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3897  df-un 4150  df-n0 12614

This theorem is used by:  nn0ge2m1nn0  12684  nnzd  12726  eluzge2nn0  13026  expgt1  14250  expaddzlem  14255  expaddz  14256  expmulz  14258  expmulnbnd  14386  exp11nnd  14412  facwordi  14440  faclbnd  14441  facavg  14452  bcm1k  14466  wrdeqs1cat  14877  cshwcsh2id  14987  relexpsucnnr  15187  isercolllem2  15842  bcxmas  16013  climcndslem1  16027  climcndslem2  16028  climcnds  16029  pwdif  16046  geo2sum  16051  mertenslem1  16062  prodmolem3  16109  prodmolem2a  16110  bpolydiflem  16229  eftabs  16250  efcllem  16252  eftlub  16286  eirrlem  16381  rpnnen2lem9  16399  rpnnen2lem11  16401  dvdsfac  16505  pwp1fsum  16570  oddpwp1fsum  16571  bitsfzo  16614  bitsfi  16616  sadcaddlem  16636  smumullem  16671  gcdcl  16685  dvdsgcdidd  16719  mulgcd  16730  rplpwr  16741  rprpwr  16742  rppwr  16743  nn0rppwr  16744  expgcd  16746  lcmcl  16785  lcmgcdnn  16795  lcmfcl  16812  nprmdvds1  16891  rpexp  16907  prmdvdsbc  16911  zsqrtelqelz  16943  phiprmpw  16962  eulerthlem2  16968  eulerth  16969  fermltl  16970  odzcllem  16979  odzdvds  16982  odzphi  16983  prm23lt5  17001  pythagtriplem6  17008  pythagtriplem7  17009  pcprmpw2  17069  dvdsprmpweqle  17073  pcprod  17082  pcfac  17086  pcbc  17087  expnprm  17089  pockthlem  17092  pockthg  17093  prmunb  17101  prmreclem2  17104  prmreclem3  17105  prmreclem4  17106  prmreclem5  17107  prmreclem6  17108  mul4sqlem  17140  4sqlem11  17142  4sqlem17  17148  vdwlem1  17168  vdwlem5  17172  vdwlem6  17173  vdwlem8  17175  vdwlem9  17176  vdwlem11  17178  vdwlem12  17179  vdwnnlem3  17184  ramz2  17211  ramub1lem1  17213  ramub1lem2  17214  ramub1  17215  prmgaplem3  17240  2expltfac  17279  psgnunilem3  19719  odfval  19755  mndodconglem  19764  gexcl3  19810  pgpfi1  19818  sylow1lem1  19821  gexexlem  20075  prmcyg  20117  gsumval3  20130  ablfacrplem  20290  ablfacrp  20291  ablfacrp2  20292  ablfac1eu  20298  prmgrpsimpgd  20339  srgbinomlem3  20463  srgbinomlem4  20464  fermltlchr  21844  freshmansdream  21889  chfacfscmulgsum  23187  chfacfpmmulgsum  23191  cpmadugsumlemF  23203  ovoliunlem1  25832  mbfi1fseqlem1  26045  mbfi1fseqlem3  26047  mbfi1fseqlem5  26049  itg2cnlem2  26092  plyn0mulidp  26611  dvply1  26614  aalioulem2  26669  aalioulem5  26672  aaliou3lem1  26678  aaliou3lem2  26679  aaliou3lem8  26681  aaliou3lem6  26684  taylthlem1  26709  taylthlem2  26710  pserdvlem2  26764  cxpeq  27094  zrtelqelz  27095  dmgmdivn0  27364  lgamgulmlem5  27369  lgamcvg2  27391  wilthlem1  27404  ftalem1  27409  ftalem2  27410  ftalem4  27412  ftalem5  27413  basellem2  27418  basellem3  27419  basellem4  27420  basellem5  27421  isppw2  27451  mpodvdsmulf1o  27530  dvdsmulf1o  27532  sgmmul  27537  fsumvma2  27550  chpchtsum  27555  logfacubnd  27557  mersenne  27563  perfect1  27564  perfectlem1  27565  perfectlem2  27566  perfect  27567  dchrelbas3  27574  dchrelbasd  27575  dchrzrh1  27580  dchrzrhmul  27582  dchrmulcl  27585  dchrn0  27586  dchrfi  27591  dchrghm  27592  dchrabs  27596  dchrinv  27597  dchrptlem1  27600  dchrptlem2  27601  dchrptlem3  27602  dchrpt  27603  dchrsum2  27604  sum2dchr  27610  pcbcctr  27612  bcmono  27613  bclbnd  27616  bposlem1  27620  bposlem3  27622  bposlem5  27624  bposlem6  27625  lgslem1  27633  lgsval2lem  27643  lgsvalmod  27652  lgsmod  27659  lgsdirprm  27667  lgsne0  27671  lgsqrlem1  27682  lgsqrlem2  27683  lgsqrlem3  27684  lgsqrlem4  27685  gausslemma2dlem0b  27693  gausslemma2dlem0c  27694  gausslemma2dlem1  27702  gausslemma2dlem7  27709  gausslemma2d  27710  lgseisenlem1  27711  lgseisenlem2  27712  lgseisenlem3  27713  lgseisenlem4  27714  lgseisen  27715  lgsquadlem2  27717  lgsquadlem3  27718  m1lgs  27724  2lgslem1a  27727  2sqlem3  27756  2sqblem  27767  chebbnd1lem1  27805  chebbnd1lem3  27807  rplogsumlem2  27821  rpvmasumlem  27823  dchrisumlem1  27825  dchrisumlem2  27826  dchrmusum2  27830  dchrvmasumlem3  27835  dchrisum0ff  27843  dchrisum0flblem1  27844  rpvmasum2  27848  dchrisum0re  27849  dchrisum0lem2a  27853  dirith  27865  mudivsum  27866  pntpbnd1a  27921  pntlemq  27937  pntlemr  27938  pntlemj  27939  ostth2lem1  27954  ostth2lem2  27970  ostth2lem3  27971  ostth2  27973  fltdvdsabdvdsc  27979  fltne  27984  flt4lem4  27988  flt4lem7  27998  fltoprm  28004  crctcshwlkn0lem6  30413  hashecclwwlkn1  30677  umgrhashecclwwlk  30678  clwwlknon  30690  eucrctshift  30853  numclwlk1lem2  30980  nrt2irr  31083  dipcl  31323  dipcn  31331  bcm1n  33437  expgt0b  33458  nexple  33474  2exple2exp  33475  oexpled  33477  wrdpmtrlast  33704  psgnfzto1st  33716  isarchi2  33796  submarchi  33797  znfermltl  33972  fldextrspundgdvdslem  34362  fldextrspundgdvds  34363  fldext2rspun  34364  constrext2chnlem  34432  cos9thpiminplylem2  34465  submateqlem1  34489  madjusmdetlem2  34510  madjusmdetlem4  34512  mdetlap  34514  oddpwdc  35036  eulerpartlemsv2  35040  eulerpartlemsf  35041  eulerpartlems  35042  eulerpartlemv  35046  eulerpartlemb  35050  signsvtn0  35249  fsum2dsub  35286  reprinfz1  35301  reprpmtf1o  35305  circlemeth  35319  circlemethnat  35320  hgt750lemb  35335  hgt750lema  35336  hgt750leme  35337  tgoldbachgtde  35339  tgoldbachgtda  35340  lpadleft  35365  subfacp1lem1  36062  subfacp1lem6  36068  subfaclim  36071  erdszelem8  36081  erdszelem10  36083  cvmliftlem10  36177  faclim2  36637  poimirlem7  38682  poimirlem17  38692  poimirlem18  38693  poimirlem20  38695  poimirlem21  38696  poimirlem22  38697  poimirlem25  38700  poimirlem26  38701  poimirlem27  38702  poimirlem28  38703  poimirlem32  38707  nninfnub  38822  bfplem1  38893  zndvdchrrhm  43160  lcmineqlem1  43216  lcmineqlem2  43217  lcmineqlem8  43223  lcmineqlem10  43225  lcmineqlem11  43226  lcmineqlem15  43230  lcmineqlem16  43231  lcmineqlem18  43233  lcmineqlem19  43234  lcmineqlem20  43235  lcmineqlem21  43236  lcmineqlem22  43237  3lexlogpow2ineq2  43246  dvrelogpow2b  43255  aks4d1p1p2  43257  aks4d1p1p4  43258  aks4d1p1  43263  aks4d1p3  43265  aks4d1p7d1  43269  aks4d1p7  43270  aks4d1p8  43274  aks4d1p9  43275  isprimroot2  43281  primrootsunit1  43284  primrootscoprmpow  43286  posbezout  43287  primrootscoprbij  43289  primrootlekpowne0  43292  primrootspoweq0  43293  aks6d1c1p2  43296  aks6d1c1p3  43297  aks6d1c1p4  43298  aks6d1c1p5  43299  aks6d1c1p7  43300  aks6d1c1p6  43301  aks6d1c1p8  43302  aks6d1c2p2  43306  hashscontpowcl  43307  hashscontpow1  43308  hashscontpow  43309  aks6d1c4  43311  aks6d1c2lem3  43313  aks6d1c2lem4  43314  aks6d1c2  43317  sticksstones6  43338  sticksstones7  43339  sticksstones10  43342  sticksstones12a  43344  sticksstones12  43345  sticksstones20  43353  sticksstones22  43355  aks6d1c6lem2  43358  aks6d1c6lem3  43359  aks6d1c6lem4  43360  aks6d1c6isolem1  43361  aks6d1c6isolem2  43362  aks6d1c6lem5  43364  bcled  43365  bcle2d  43366  aks6d1c7lem1  43367  aks6d1c7  43371  aks5lem2  43374  aks5lem3a  43376  aks5lem5a  43378  grpods  43381  unitscyglem2  43383  unitscyglem4  43385  aks5lem7  43387  aks5  43391  sumcubes  43507  oexpreposd  43516  exp11d  43520  dvdsexpb  43524  fiabv  43737  fsuppind  43755  dffltz  43807  fltltc  43809  fltnltalem  43810  fltnlta  43811  3rexfrabdioph  43941  4rexfrabdioph  43942  6rexfrabdioph  43943  7rexfrabdioph  43944  irrapxlem5  43970  pellexlem2  43974  pellexlem6  43978  pell14qrgt0  44003  pell1qrge1  44014  pellfundgt1  44027  ltrmxnn0  44093  jm2.26lem3  44145  jm2.27a  44149  jm2.27c  44151  rmxdiophlem  44159  jm3.1lem1  44161  jm3.1lem2  44162  jm3.1lem3  44163  jm3.1  44164  dgrsub2  44274  mpaaeu  44289  idomsubgmo  44332  relexpxpmin  44854  nzprmdif  45440  binomcxplemwb  45469  fperiodmul  46456  xralrple4  46520  fsumnncl  46720  dvsinexp  47057  dvxpaek  47086  itgsinexplem1  47100  stoweidlem1  47147  stoweidlem17  47163  stoweidlem25  47171  stoweidlem34  47180  stoweidlem38  47184  stoweidlem40  47186  stoweidlem42  47188  stoweidlem45  47191  stirlinglem4  47223  stirlinglem5  47224  stirlinglem10  47229  stirlinglem13  47232  dirkertrigeq  47247  fourierdlem21  47274  fourierdlem25  47278  fourierdlem48  47300  fourierdlem54  47306  fourierdlem64  47316  fourierdlem65  47317  fourierdlem73  47325  fourierdlem81  47333  fourierdlem83  47335  fourierdlem92  47344  fourierdlem103  47355  fourierdlem104  47356  fourierdlem112  47364  fourierdlem113  47365  etransclem1  47381  etransclem4  47384  etransclem8  47388  etransclem15  47395  etransclem17  47397  etransclem18  47398  etransclem19  47399  etransclem20  47400  etransclem21  47401  etransclem22  47402  etransclem23  47403  etransclem24  47404  etransclem25  47405  etransclem27  47407  etransclem32  47412  etransclem35  47415  etransclem41  47421  etransclem44  47424  etransclem46  47426  modmknepk  48574  iccpartigtl  48641  iccpartgt  48645  iccpartgel  48647  iccelpart  48651  odz2prm2pw  48784  fmtnoprmfac1  48786  fmtnoprmfac2  48788  2pwp1prm  48810  sfprmdvdsmersenne  48824  lighneallem4a  48829  proththdlem  48834  proththd  48835  perfectALTVlem1  48955  perfectALTVlem2  48956  perfectALTV  48957  fpprwpprb  48974  gpgedgvtx1  49296  logbpw2m1  49815  nnpw2blenfzo  49829  nnolog2flm1  49838  dignn0fr  49849  nn0sumshdiglemA  49867  nn0sumshdiglemB  49868