Theorem nnnn0d 12580

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ℕcn 12248  ℕ₀cn0 12519

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3911  df-ss 3923  df-n0 12520

This theorem is used by:  nn0ge2m1nn0  12590  nnzd  12632  eluzge2nn0  12932  expgt1  14154  expaddzlem  14159  expaddz  14160  expmulz  14162  expmulnbnd  14289  exp11nnd  14315  facwordi  14343  faclbnd  14344  facavg  14355  bcm1k  14369  wrdeqs1cat  14779  cshwcsh2id  14889  relexpsucnnr  15086  isercolllem2  15741  bcxmas  15912  climcndslem1  15926  climcndslem2  15927  climcnds  15928  pwdif  15945  geo2sum  15950  mertenslem1  15961  prodmolem3  16010  prodmolem2a  16011  bpolydiflem  16130  eftabs  16151  efcllem  16153  eftlub  16187  eirrlem  16282  rpnnen2lem9  16300  rpnnen2lem11  16302  dvdsfac  16406  pwp1fsum  16471  oddpwp1fsum  16472  bitsfzo  16515  bitsfi  16517  sadcaddlem  16537  smumullem  16572  gcdcl  16586  dvdsgcdidd  16617  mulgcd  16628  rplpwr  16638  rprpwr  16639  rppwr  16640  nn0rppwr  16641  expgcd  16643  lcmcl  16681  lcmgcdnn  16691  lcmfcl  16708  nprmdvds1  16787  rpexp  16803  prmdvdsbc  16807  zsqrtelqelz  16839  phiprmpw  16857  eulerthlem2  16863  eulerth  16864  fermltl  16865  odzcllem  16874  odzdvds  16877  odzphi  16878  prm23lt5  16896  pythagtriplem6  16903  pythagtriplem7  16904  pcprmpw2  16964  dvdsprmpweqle  16968  pcprod  16977  pcfac  16981  pcbc  16982  expnprm  16984  pockthlem  16987  pockthg  16988  prmunb  16996  prmreclem2  16999  prmreclem3  17000  prmreclem4  17001  prmreclem5  17002  prmreclem6  17003  mul4sqlem  17035  4sqlem11  17037  4sqlem17  17043  vdwlem1  17063  vdwlem5  17067  vdwlem6  17068  vdwlem8  17070  vdwlem9  17071  vdwlem11  17073  vdwlem12  17074  vdwnnlem3  17079  ramz2  17106  ramub1lem1  17108  ramub1lem2  17109  ramub1  17110  prmgaplem3  17135  2expltfac  17174  psgnunilem3  19610  odfval  19646  mndodconglem  19655  gexcl3  19701  pgpfi1  19709  sylow1lem1  19712  gexexlem  19966  prmcyg  20008  gsumval3  20021  ablfacrplem  20181  ablfacrp  20182  ablfacrp2  20183  ablfac1eu  20189  prmgrpsimpgd  20230  srgbinomlem3  20354  srgbinomlem4  20355  fermltlchr  21729  freshmansdream  21774  chfacfscmulgsum  23067  chfacfpmmulgsum  23071  cpmadugsumlemF  23083  ovoliunlem1  25712  mbfi1fseqlem1  25925  mbfi1fseqlem3  25927  mbfi1fseqlem5  25929  itg2cnlem2  25972  plyn0mulidp  26493  dvply1  26496  aalioulem2  26547  aalioulem5  26550  aaliou3lem1  26556  aaliou3lem2  26557  aaliou3lem8  26559  aaliou3lem6  26562  taylthlem1  26587  taylthlem2  26588  pserdvlem2  26642  cxpeq  26973  zrtelqelz  26974  dmgmdivn0  27243  lgamgulmlem5  27248  lgamcvg2  27270  wilthlem1  27283  ftalem1  27288  ftalem2  27289  ftalem4  27291  ftalem5  27292  basellem2  27297  basellem3  27298  basellem4  27299  basellem5  27300  isppw2  27330  mpodvdsmulf1o  27409  dvdsmulf1o  27411  sgmmul  27416  fsumvma2  27429  chpchtsum  27434  logfacubnd  27436  mersenne  27442  perfect1  27443  perfectlem1  27444  perfectlem2  27445  perfect  27446  dchrelbas3  27453  dchrelbasd  27454  dchrzrh1  27459  dchrzrhmul  27461  dchrmulcl  27464  dchrn0  27465  dchrfi  27470  dchrghm  27471  dchrabs  27475  dchrinv  27476  dchrptlem1  27479  dchrptlem2  27480  dchrptlem3  27481  dchrpt  27482  dchrsum2  27483  sum2dchr  27489  pcbcctr  27491  bcmono  27492  bclbnd  27495  bposlem1  27499  bposlem3  27501  bposlem5  27503  bposlem6  27504  lgslem1  27512  lgsval2lem  27522  lgsvalmod  27531  lgsmod  27538  lgsdirprm  27546  lgsne0  27550  lgsqrlem1  27561  lgsqrlem2  27562  lgsqrlem3  27563  lgsqrlem4  27564  gausslemma2dlem0b  27572  gausslemma2dlem0c  27573  gausslemma2dlem1  27581  gausslemma2dlem7  27588  gausslemma2d  27589  lgseisenlem1  27590  lgseisenlem2  27591  lgseisenlem3  27592  lgseisenlem4  27593  lgseisen  27594  lgsquadlem2  27596  lgsquadlem3  27597  m1lgs  27603  2lgslem1a  27606  2sqlem3  27635  2sqblem  27646  chebbnd1lem1  27684  chebbnd1lem3  27686  rplogsumlem2  27700  rpvmasumlem  27702  dchrisumlem1  27704  dchrisumlem2  27705  dchrmusum2  27709  dchrvmasumlem3  27714  dchrisum0ff  27722  dchrisum0flblem1  27723  rpvmasum2  27727  dchrisum0re  27728  dchrisum0lem2a  27732  dirith  27744  mudivsum  27745  pntpbnd1a  27800  pntlemq  27816  pntlemr  27817  pntlemj  27818  ostth2lem1  27833  ostth2lem2  27849  ostth2lem3  27850  ostth2  27852  crctcshwlkn0lem6  30231  hashecclwwlkn1  30495  umgrhashecclwwlk  30496  clwwlknon  30508  eucrctshift  30665  numclwlk1lem2  30792  nrt2irr  30895  dipcl  31135  dipcn  31143  bcm1n  33210  expgt0b  33231  nexple  33247  2exple2exp  33248  oexpled  33250  wrdpmtrlast  33477  psgnfzto1st  33489  isarchi2  33569  submarchi  33570  znfermltl  33745  fldextrspundgdvdslem  34134  fldextrspundgdvds  34135  fldext2rspun  34136  constrext2chnlem  34204  cos9thpiminplylem2  34237  submateqlem1  34261  madjusmdetlem2  34282  madjusmdetlem4  34284  mdetlap  34286  oddpwdc  34809  eulerpartlemsv2  34813  eulerpartlemsf  34814  eulerpartlems  34815  eulerpartlemv  34819  eulerpartlemb  34823  signsvtn0  35022  fsum2dsub  35059  reprinfz1  35074  reprpmtf1o  35078  circlemeth  35092  circlemethnat  35093  hgt750lemb  35108  hgt750lema  35109  hgt750leme  35110  tgoldbachgtde  35112  tgoldbachgtda  35113  lpadleft  35138  subfacp1lem1  35708  subfacp1lem6  35714  subfaclim  35717  erdszelem8  35727  erdszelem10  35729  cvmliftlem10  35823  faclim2  36277  poimirlem7  38335  poimirlem17  38345  poimirlem18  38346  poimirlem20  38348  poimirlem21  38349  poimirlem22  38350  poimirlem25  38353  poimirlem26  38354  poimirlem27  38355  poimirlem28  38356  poimirlem32  38360  nninfnub  38460  bfplem1  38531  zndvdchrrhm  42798  lcmineqlem1  42854  lcmineqlem2  42855  lcmineqlem8  42861  lcmineqlem10  42863  lcmineqlem11  42864  lcmineqlem15  42868  lcmineqlem16  42869  lcmineqlem18  42871  lcmineqlem19  42872  lcmineqlem20  42873  lcmineqlem21  42874  lcmineqlem22  42875  3lexlogpow2ineq2  42884  dvrelogpow2b  42893  aks4d1p1p2  42895  aks4d1p1p4  42896  aks4d1p1  42901  aks4d1p3  42903  aks4d1p7d1  42907  aks4d1p7  42908  aks4d1p8  42912  aks4d1p9  42913  isprimroot2  42919  primrootsunit1  42922  primrootscoprmpow  42924  posbezout  42925  primrootscoprbij  42927  primrootlekpowne0  42930  primrootspoweq0  42931  aks6d1c1p2  42934  aks6d1c1p3  42935  aks6d1c1p4  42936  aks6d1c1p5  42937  aks6d1c1p7  42938  aks6d1c1p6  42939  aks6d1c1p8  42940  aks6d1c2p2  42944  hashscontpowcl  42945  hashscontpow1  42946  hashscontpow  42947  aks6d1c4  42949  aks6d1c2lem3  42951  aks6d1c2lem4  42952  aks6d1c2  42955  sticksstones6  42976  sticksstones7  42977  sticksstones10  42980  sticksstones12a  42982  sticksstones12  42983  sticksstones20  42991  sticksstones22  42993  aks6d1c6lem2  42996  aks6d1c6lem3  42997  aks6d1c6lem4  42998  aks6d1c6isolem1  42999  aks6d1c6isolem2  43000  aks6d1c6lem5  43002  bcled  43003  bcle2d  43004  aks6d1c7lem1  43005  aks6d1c7  43009  aks5lem2  43012  aks5lem3a  43014  aks5lem5a  43016  grpods  43019  unitscyglem2  43021  unitscyglem4  43023  aks5lem7  43025  aks5  43029  sumcubes  43132  oexpreposd  43141  exp11d  43145  dvdsexpb  43154  fiabv  43362  fsuppind  43380  dffltz  43424  fltdvdsabdvdsc  43428  fltne  43434  flt4lem4  43439  flt4lem7  43449  fltltc  43451  fltnltalem  43452  fltnlta  43453  3rexfrabdioph  43582  4rexfrabdioph  43583  6rexfrabdioph  43584  7rexfrabdioph  43585  irrapxlem5  43611  pellexlem2  43615  pellexlem6  43619  pell14qrgt0  43644  pell1qrge1  43655  pellfundgt1  43668  ltrmxnn0  43734  jm2.26lem3  43786  jm2.27a  43790  jm2.27c  43792  rmxdiophlem  43800  jm3.1lem1  43802  jm3.1lem2  43803  jm3.1lem3  43804  jm3.1  43805  dgrsub2  43920  mpaaeu  43935  idomsubgmo  43978  relexpxpmin  44501  nzprmdif  45087  binomcxplemwb  45116  fperiodmul  46081  xralrple4  46146  fsumnncl  46346  dvsinexp  46683  dvxpaek  46712  itgsinexplem1  46726  stoweidlem1  46773  stoweidlem17  46789  stoweidlem25  46797  stoweidlem34  46806  stoweidlem38  46810  stoweidlem40  46812  stoweidlem42  46814  stoweidlem45  46817  stirlinglem4  46849  stirlinglem5  46850  stirlinglem10  46855  stirlinglem13  46858  dirkertrigeq  46873  fourierdlem21  46900  fourierdlem25  46904  fourierdlem48  46926  fourierdlem54  46932  fourierdlem64  46942  fourierdlem65  46943  fourierdlem73  46951  fourierdlem81  46959  fourierdlem83  46961  fourierdlem92  46970  fourierdlem103  46981  fourierdlem104  46982  fourierdlem112  46990  fourierdlem113  46991  etransclem1  47007  etransclem4  47010  etransclem8  47014  etransclem15  47021  etransclem17  47023  etransclem18  47024  etransclem19  47025  etransclem20  47026  etransclem21  47027  etransclem22  47028  etransclem23  47029  etransclem24  47030  etransclem25  47031  etransclem27  47033  etransclem32  47038  etransclem35  47041  etransclem41  47047  etransclem44  47050  etransclem46  47052  modmknepk  48163  iccpartigtl  48230  iccpartgt  48234  iccpartgel  48236  iccelpart  48240  odz2prm2pw  48373  fmtnoprmfac1  48375  fmtnoprmfac2  48377  2pwp1prm  48399  sfprmdvdsmersenne  48413  lighneallem4a  48418  proththdlem  48423  proththd  48424  perfectALTVlem1  48544  perfectALTVlem2  48545  perfectALTV  48546  fpprwpprb  48563  gpgedgvtx1  48885  logbpw2m1  49404  nnpw2blenfzo  49418  nnolog2flm1  49427  dignn0fr  49438  nn0sumshdiglemA  49456  nn0sumshdiglemB  49457