Theorem nnnn0d 12531

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

Syntax hints:   → wi 4   ∈ wcel 2106  ℕcn 12211  ℕ₀cn0 12471

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-un 3953  df-in 3955  df-ss 3965  df-n0 12472

This theorem is referenced by:  nn0ge2m1nn0  12541  nnzd  12584  eluzge2nn0  12870  expgt1  14065  expaddzlem  14070  expaddz  14071  expmulz  14073  expmulnbnd  14197  facwordi  14248  faclbnd  14249  facavg  14260  bcm1k  14274  wrdeqs1cat  14669  cshwcsh2id  14778  relexpsucnnr  14971  isercolllem2  15611  bcxmas  15780  climcndslem1  15794  climcndslem2  15795  climcnds  15796  pwdif  15813  geo2sum  15818  mertenslem1  15829  prodmolem3  15876  prodmolem2a  15877  bpolydiflem  15997  eftabs  16018  efcllem  16020  eftlub  16051  eirrlem  16146  rpnnen2lem9  16164  rpnnen2lem11  16166  dvdsfac  16268  pwp1fsum  16333  oddpwp1fsum  16334  bitsfzo  16375  bitsfi  16377  sadcaddlem  16397  smumullem  16432  gcdcl  16446  dvdsgcdidd  16478  mulgcd  16489  rplpwr  16498  rprpwr  16499  rppwr  16500  lcmcl  16537  lcmgcdnn  16547  lcmfcl  16564  nprmdvds1  16642  rpexp  16658  zsqrtelqelz  16693  phiprmpw  16708  eulerthlem2  16714  eulerth  16715  fermltl  16716  odzcllem  16724  odzdvds  16727  odzphi  16728  prm23lt5  16746  pythagtriplem6  16753  pythagtriplem7  16754  pcprmpw2  16814  dvdsprmpweqle  16818  pcprod  16827  pcfac  16831  pcbc  16832  expnprm  16834  pockthlem  16837  pockthg  16838  prmunb  16846  prmreclem2  16849  prmreclem3  16850  prmreclem4  16851  prmreclem5  16852  prmreclem6  16853  mul4sqlem  16885  4sqlem11  16887  4sqlem17  16893  vdwlem1  16913  vdwlem5  16917  vdwlem6  16918  vdwlem8  16920  vdwlem9  16921  vdwlem11  16923  vdwlem12  16924  vdwnnlem3  16929  ramz2  16956  ramub1lem1  16958  ramub1lem2  16959  ramub1  16960  prmgaplem3  16985  2expltfac  17025  psgnunilem3  19363  odfval  19399  mndodconglem  19408  gexcl3  19454  pgpfi1  19462  sylow1lem1  19465  gexexlem  19719  prmcyg  19761  gsumval3  19774  ablfacrplem  19934  ablfacrp  19935  ablfacrp2  19936  ablfac1eu  19942  prmgrpsimpgd  19983  srgbinomlem3  20050  srgbinomlem4  20051  chfacfscmulgsum  22361  chfacfpmmulgsum  22365  cpmadugsumlemF  22377  ovoliunlem1  25018  mbfi1fseqlem1  25232  mbfi1fseqlem3  25234  mbfi1fseqlem5  25236  itg2cnlem2  25279  dvply1  25796  aalioulem2  25845  aalioulem5  25848  aaliou3lem1  25854  aaliou3lem2  25855  aaliou3lem8  25857  aaliou3lem6  25860  taylthlem1  25884  taylthlem2  25885  pserdvlem2  25939  cxpeq  26262  dmgmdivn0  26529  lgamgulmlem5  26534  lgamcvg2  26556  wilthlem1  26569  ftalem1  26574  ftalem2  26575  ftalem4  26577  ftalem5  26578  basellem2  26583  basellem3  26584  basellem4  26585  basellem5  26586  isppw2  26616  dvdsmulf1o  26695  sgmmul  26701  fsumvma2  26714  chpchtsum  26719  logfacubnd  26721  mersenne  26727  perfect1  26728  perfectlem1  26729  perfectlem2  26730  perfect  26731  dchrelbas3  26738  dchrelbasd  26739  dchrzrh1  26744  dchrzrhmul  26746  dchrmulcl  26749  dchrn0  26750  dchrfi  26755  dchrghm  26756  dchrabs  26760  dchrinv  26761  dchrptlem1  26764  dchrptlem2  26765  dchrptlem3  26766  dchrpt  26767  dchrsum2  26768  sum2dchr  26774  pcbcctr  26776  bcmono  26777  bclbnd  26780  bposlem1  26784  bposlem3  26786  bposlem5  26788  bposlem6  26789  lgslem1  26797  lgsval2lem  26807  lgsvalmod  26816  lgsmod  26823  lgsdirprm  26831  lgsne0  26835  lgsqrlem1  26846  lgsqrlem2  26847  lgsqrlem3  26848  lgsqrlem4  26849  gausslemma2dlem0b  26857  gausslemma2dlem0c  26858  gausslemma2dlem1  26866  gausslemma2dlem7  26873  gausslemma2d  26874  lgseisenlem1  26875  lgseisenlem2  26876  lgseisenlem3  26877  lgseisenlem4  26878  lgseisen  26879  lgsquadlem2  26881  lgsquadlem3  26882  m1lgs  26888  2lgslem1a  26891  2sqlem3  26920  2sqblem  26931  chebbnd1lem1  26969  chebbnd1lem3  26971  rplogsumlem2  26985  rpvmasumlem  26987  dchrisumlem1  26989  dchrisumlem2  26990  dchrmusum2  26994  dchrvmasumlem3  26999  dchrisum0ff  27007  dchrisum0flblem1  27008  rpvmasum2  27012  dchrisum0re  27013  dchrisum0lem2a  27017  dirith  27029  mudivsum  27030  pntpbnd1a  27085  pntlemq  27101  pntlemr  27102  pntlemj  27103  ostth2lem1  27118  ostth2lem2  27134  ostth2lem3  27135  ostth2  27137  crctcshwlkn0lem6  29066  hashecclwwlkn1  29327  umgrhashecclwwlk  29328  clwwlknon  29340  eucrctshift  29493  numclwlk1lem2  29620  dipcl  29960  dipcn  29968  bcm1n  32001  prmdvdsbc  32017  psgnfzto1st  32259  isarchi2  32326  submarchi  32327  freshmansdream  32376  fermltlchr  32473  znfermltl  32474  submateqlem1  32782  madjusmdetlem2  32803  madjusmdetlem4  32805  mdetlap  32807  nexple  33002  oddpwdc  33348  eulerpartlemsv2  33352  eulerpartlemsf  33353  eulerpartlems  33354  eulerpartlemv  33358  eulerpartlemb  33362  plymulx0  33553  signsvtn0  33576  fsum2dsub  33614  reprinfz1  33629  reprpmtf1o  33633  circlemeth  33647  circlemethnat  33648  hgt750lemb  33663  hgt750lema  33664  hgt750leme  33665  tgoldbachgtde  33667  tgoldbachgtda  33668  lpadleft  33690  subfacp1lem1  34165  subfacp1lem6  34171  subfaclim  34174  erdszelem8  34184  erdszelem10  34186  cvmliftlem10  34280  faclim2  34713  poimirlem7  36490  poimirlem17  36500  poimirlem18  36501  poimirlem20  36503  poimirlem21  36504  poimirlem22  36505  poimirlem25  36508  poimirlem26  36509  poimirlem27  36510  poimirlem28  36511  poimirlem32  36515  nninfnub  36614  bfplem1  36685  lcmineqlem1  40889  lcmineqlem2  40890  lcmineqlem8  40896  lcmineqlem10  40898  lcmineqlem11  40899  lcmineqlem15  40903  lcmineqlem16  40904  lcmineqlem18  40906  lcmineqlem19  40907  lcmineqlem20  40908  lcmineqlem21  40909  lcmineqlem22  40910  3lexlogpow2ineq2  40919  dvrelogpow2b  40928  aks4d1p1p2  40930  aks4d1p1p4  40931  aks4d1p1  40936  aks4d1p3  40938  aks4d1p7d1  40942  aks4d1p7  40943  aks4d1p8  40947  aks4d1p9  40948  aks6d1c2p2  40952  sticksstones6  40962  sticksstones7  40963  sticksstones10  40966  sticksstones12a  40968  sticksstones12  40969  sticksstones20  40977  sticksstones22  40979  metakunt2  40981  fsuppind  41164  sumcubes  41211  oexpreposd  41212  exp11nnd  41215  exp11d  41216  nn0rppwr  41224  expgcd  41225  dvdsexpb  41233  zrtelqelz  41236  dffltz  41377  fltdvdsabdvdsc  41381  fltne  41387  flt4lem4  41392  flt4lem7  41402  fltltc  41404  fltnltalem  41405  fltnlta  41406  3rexfrabdioph  41525  4rexfrabdioph  41526  6rexfrabdioph  41527  7rexfrabdioph  41528  irrapxlem5  41554  pellexlem2  41558  pellexlem6  41562  pell14qrgt0  41587  pell1qrge1  41598  pellfundgt1  41611  ltrmxnn0  41678  jm2.26lem3  41730  jm2.27a  41734  jm2.27c  41736  rmxdiophlem  41744  jm3.1lem1  41746  jm3.1lem2  41747  jm3.1lem3  41748  jm3.1  41749  dgrsub2  41867  mpaaeu  41882  idomsubgmo  41930  relexpxpmin  42458  nzprmdif  43068  binomcxplemwb  43097  fperiodmul  44004  xralrple4  44073  fsumnncl  44278  dvsinexp  44617  dvxpaek  44646  itgsinexplem1  44660  stoweidlem1  44707  stoweidlem17  44723  stoweidlem25  44731  stoweidlem34  44740  stoweidlem38  44744  stoweidlem40  44746  stoweidlem42  44748  stoweidlem45  44751  stirlinglem4  44783  stirlinglem5  44784  stirlinglem10  44789  stirlinglem13  44792  dirkertrigeq  44807  fourierdlem21  44834  fourierdlem25  44838  fourierdlem48  44860  fourierdlem54  44866  fourierdlem64  44876  fourierdlem65  44877  fourierdlem73  44885  fourierdlem81  44893  fourierdlem83  44895  fourierdlem92  44904  fourierdlem103  44915  fourierdlem104  44916  fourierdlem112  44924  fourierdlem113  44925  etransclem1  44941  etransclem4  44944  etransclem8  44948  etransclem15  44955  etransclem17  44957  etransclem18  44958  etransclem19  44959  etransclem20  44960  etransclem21  44961  etransclem22  44962  etransclem23  44963  etransclem24  44964  etransclem25  44965  etransclem27  44967  etransclem32  44972  etransclem35  44975  etransclem41  44981  etransclem44  44984  etransclem46  44986  iccpartigtl  46081  iccpartgt  46085  iccpartgel  46087  iccelpart  46091  odz2prm2pw  46221  fmtnoprmfac1  46223  fmtnoprmfac2  46225  2pwp1prm  46247  sfprmdvdsmersenne  46261  lighneallem4a  46266  proththdlem  46271  proththd  46272  perfectALTVlem1  46379  perfectALTVlem2  46380  perfectALTV  46381  fpprwpprb  46398  logbpw2m1  47243  nnpw2blenfzo  47257  nnolog2flm1  47266  dignn0fr  47277  nn0sumshdiglemA  47295  nn0sumshdiglemB  47296