Theorem nnnn0d 12433

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℕcn 12116  ℕ₀cn0 12372

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3435  df-un 3904  df-ss 3916  df-n0 12373

This theorem is referenced by:  nn0ge2m1nn0  12443  nnzd  12486  eluzge2nn0  12781  expgt1  13995  expaddzlem  14000  expaddz  14001  expmulz  14003  expmulnbnd  14130  exp11nnd  14156  facwordi  14184  faclbnd  14185  facavg  14196  bcm1k  14210  wrdeqs1cat  14614  cshwcsh2id  14722  relexpsucnnr  14919  isercolllem2  15560  bcxmas  15729  climcndslem1  15743  climcndslem2  15744  climcnds  15745  pwdif  15762  geo2sum  15767  mertenslem1  15778  prodmolem3  15827  prodmolem2a  15828  bpolydiflem  15948  eftabs  15969  efcllem  15971  eftlub  16005  eirrlem  16100  rpnnen2lem9  16118  rpnnen2lem11  16120  dvdsfac  16224  pwp1fsum  16289  oddpwp1fsum  16290  bitsfzo  16333  bitsfi  16335  sadcaddlem  16355  smumullem  16390  gcdcl  16404  dvdsgcdidd  16435  mulgcd  16446  rplpwr  16456  rprpwr  16457  rppwr  16458  nn0rppwr  16459  expgcd  16461  lcmcl  16499  lcmgcdnn  16509  lcmfcl  16526  nprmdvds1  16604  rpexp  16620  prmdvdsbc  16624  zsqrtelqelz  16656  phiprmpw  16674  eulerthlem2  16680  eulerth  16681  fermltl  16682  odzcllem  16691  odzdvds  16694  odzphi  16695  prm23lt5  16713  pythagtriplem6  16720  pythagtriplem7  16721  pcprmpw2  16781  dvdsprmpweqle  16785  pcprod  16794  pcfac  16798  pcbc  16799  expnprm  16801  pockthlem  16804  pockthg  16805  prmunb  16813  prmreclem2  16816  prmreclem3  16817  prmreclem4  16818  prmreclem5  16819  prmreclem6  16820  mul4sqlem  16852  4sqlem11  16854  4sqlem17  16860  vdwlem1  16880  vdwlem5  16884  vdwlem6  16885  vdwlem8  16887  vdwlem9  16888  vdwlem11  16890  vdwlem12  16891  vdwnnlem3  16896  ramz2  16923  ramub1lem1  16925  ramub1lem2  16926  ramub1  16927  prmgaplem3  16952  2expltfac  16991  psgnunilem3  19362  odfval  19398  mndodconglem  19407  gexcl3  19453  pgpfi1  19461  sylow1lem1  19464  gexexlem  19718  prmcyg  19760  gsumval3  19773  ablfacrplem  19933  ablfacrp  19934  ablfacrp2  19935  ablfac1eu  19941  prmgrpsimpgd  19982  srgbinomlem3  20100  srgbinomlem4  20101  fermltlchr  21420  freshmansdream  21465  chfacfscmulgsum  22729  chfacfpmmulgsum  22733  cpmadugsumlemF  22745  ovoliunlem1  25384  mbfi1fseqlem1  25597  mbfi1fseqlem3  25599  mbfi1fseqlem5  25601  itg2cnlem2  25644  dvply1  26172  aalioulem2  26222  aalioulem5  26225  aaliou3lem1  26231  aaliou3lem2  26232  aaliou3lem8  26234  aaliou3lem6  26237  taylthlem1  26262  taylthlem2  26263  taylthlem2OLD  26264  pserdvlem2  26319  cxpeq  26648  zrtelqelz  26649  dmgmdivn0  26919  lgamgulmlem5  26924  lgamcvg2  26946  wilthlem1  26959  ftalem1  26964  ftalem2  26965  ftalem4  26967  ftalem5  26968  basellem2  26973  basellem3  26974  basellem4  26975  basellem5  26976  isppw2  27006  mpodvdsmulf1o  27085  dvdsmulf1o  27087  sgmmul  27093  fsumvma2  27106  chpchtsum  27111  logfacubnd  27113  mersenne  27119  perfect1  27120  perfectlem1  27121  perfectlem2  27122  perfect  27123  dchrelbas3  27130  dchrelbasd  27131  dchrzrh1  27136  dchrzrhmul  27138  dchrmulcl  27141  dchrn0  27142  dchrfi  27147  dchrghm  27148  dchrabs  27152  dchrinv  27153  dchrptlem1  27156  dchrptlem2  27157  dchrptlem3  27158  dchrpt  27159  dchrsum2  27160  sum2dchr  27166  pcbcctr  27168  bcmono  27169  bclbnd  27172  bposlem1  27176  bposlem3  27178  bposlem5  27180  bposlem6  27181  lgslem1  27189  lgsval2lem  27199  lgsvalmod  27208  lgsmod  27215  lgsdirprm  27223  lgsne0  27227  lgsqrlem1  27238  lgsqrlem2  27239  lgsqrlem3  27240  lgsqrlem4  27241  gausslemma2dlem0b  27249  gausslemma2dlem0c  27250  gausslemma2dlem1  27258  gausslemma2dlem7  27265  gausslemma2d  27266  lgseisenlem1  27267  lgseisenlem2  27268  lgseisenlem3  27269  lgseisenlem4  27270  lgseisen  27271  lgsquadlem2  27273  lgsquadlem3  27274  m1lgs  27280  2lgslem1a  27283  2sqlem3  27312  2sqblem  27323  chebbnd1lem1  27361  chebbnd1lem3  27363  rplogsumlem2  27377  rpvmasumlem  27379  dchrisumlem1  27381  dchrisumlem2  27382  dchrmusum2  27386  dchrvmasumlem3  27391  dchrisum0ff  27399  dchrisum0flblem1  27400  rpvmasum2  27404  dchrisum0re  27405  dchrisum0lem2a  27409  dirith  27421  mudivsum  27422  pntpbnd1a  27477  pntlemq  27493  pntlemr  27494  pntlemj  27495  ostth2lem1  27510  ostth2lem2  27526  ostth2lem3  27527  ostth2  27529  crctcshwlkn0lem6  29747  hashecclwwlkn1  30008  umgrhashecclwwlk  30009  clwwlknon  30021  eucrctshift  30174  numclwlk1lem2  30301  nrt2irr  30404  dipcl  30643  dipcn  30651  bcm1n  32730  expgt0b  32754  nexple  32782  2exple2exp  32783  oexpled  32785  wrdpmtrlast  33030  psgnfzto1st  33042  isarchi2  33122  submarchi  33123  znfermltl  33299  fldextrspundgdvdslem  33661  fldextrspundgdvds  33662  fldext2rspun  33663  constrext2chnlem  33731  cos9thpiminplylem2  33764  submateqlem1  33788  madjusmdetlem2  33809  madjusmdetlem4  33811  mdetlap  33813  oddpwdc  34335  eulerpartlemsv2  34339  eulerpartlemsf  34340  eulerpartlems  34341  eulerpartlemv  34345  eulerpartlemb  34349  plymulx0  34528  signsvtn0  34551  fsum2dsub  34588  reprinfz1  34603  reprpmtf1o  34607  circlemeth  34621  circlemethnat  34622  hgt750lemb  34637  hgt750lema  34638  hgt750leme  34639  tgoldbachgtde  34641  tgoldbachgtda  34642  lpadleft  34664  subfacp1lem1  35169  subfacp1lem6  35175  subfaclim  35178  erdszelem8  35188  erdszelem10  35190  cvmliftlem10  35284  faclim2  35738  poimirlem7  37624  poimirlem17  37634  poimirlem18  37635  poimirlem20  37637  poimirlem21  37638  poimirlem22  37639  poimirlem25  37642  poimirlem26  37643  poimirlem27  37644  poimirlem28  37645  poimirlem32  37649  nninfnub  37748  bfplem1  37819  zndvdchrrhm  41962  lcmineqlem1  42019  lcmineqlem2  42020  lcmineqlem8  42026  lcmineqlem10  42028  lcmineqlem11  42029  lcmineqlem15  42033  lcmineqlem16  42034  lcmineqlem18  42036  lcmineqlem19  42037  lcmineqlem20  42038  lcmineqlem21  42039  lcmineqlem22  42040  3lexlogpow2ineq2  42049  dvrelogpow2b  42058  aks4d1p1p2  42060  aks4d1p1p4  42061  aks4d1p1  42066  aks4d1p3  42068  aks4d1p7d1  42072  aks4d1p7  42073  aks4d1p8  42077  aks4d1p9  42078  isprimroot2  42084  primrootsunit1  42087  primrootscoprmpow  42089  posbezout  42090  primrootscoprbij  42092  primrootlekpowne0  42095  primrootspoweq0  42096  aks6d1c1p2  42099  aks6d1c1p3  42100  aks6d1c1p4  42101  aks6d1c1p5  42102  aks6d1c1p7  42103  aks6d1c1p6  42104  aks6d1c1p8  42105  aks6d1c2p2  42109  hashscontpowcl  42110  hashscontpow1  42111  hashscontpow  42112  aks6d1c4  42114  aks6d1c2lem3  42116  aks6d1c2lem4  42117  aks6d1c2  42120  sticksstones6  42141  sticksstones7  42142  sticksstones10  42145  sticksstones12a  42147  sticksstones12  42148  sticksstones20  42156  sticksstones22  42158  aks6d1c6lem2  42161  aks6d1c6lem3  42162  aks6d1c6lem4  42163  aks6d1c6isolem1  42164  aks6d1c6isolem2  42165  aks6d1c6lem5  42167  bcled  42168  bcle2d  42169  aks6d1c7lem1  42170  aks6d1c7  42174  aks5lem2  42177  aks5lem3a  42179  aks5lem5a  42181  grpods  42184  unitscyglem2  42186  unitscyglem4  42188  aks5lem7  42190  aks5  42194  sumcubes  42303  oexpreposd  42312  exp11d  42316  dvdsexpb  42325  fiabv  42526  fsuppind  42580  dffltz  42624  fltdvdsabdvdsc  42628  fltne  42634  flt4lem4  42639  flt4lem7  42649  fltltc  42651  fltnltalem  42652  fltnlta  42653  3rexfrabdioph  42787  4rexfrabdioph  42788  6rexfrabdioph  42789  7rexfrabdioph  42790  irrapxlem5  42816  pellexlem2  42820  pellexlem6  42824  pell14qrgt0  42849  pell1qrge1  42860  pellfundgt1  42873  ltrmxnn0  42939  jm2.26lem3  42991  jm2.27a  42995  jm2.27c  42997  rmxdiophlem  43005  jm3.1lem1  43007  jm3.1lem2  43008  jm3.1lem3  43009  jm3.1  43010  dgrsub2  43125  mpaaeu  43140  idomsubgmo  43183  relexpxpmin  43707  nzprmdif  44309  binomcxplemwb  44338  fperiodmul  45302  xralrple4  45368  fsumnncl  45569  dvsinexp  45906  dvxpaek  45935  itgsinexplem1  45949  stoweidlem1  45996  stoweidlem17  46012  stoweidlem25  46020  stoweidlem34  46029  stoweidlem38  46033  stoweidlem40  46035  stoweidlem42  46037  stoweidlem45  46040  stirlinglem4  46072  stirlinglem5  46073  stirlinglem10  46078  stirlinglem13  46081  dirkertrigeq  46096  fourierdlem21  46123  fourierdlem25  46127  fourierdlem48  46149  fourierdlem54  46155  fourierdlem64  46165  fourierdlem65  46166  fourierdlem73  46174  fourierdlem81  46182  fourierdlem83  46184  fourierdlem92  46193  fourierdlem103  46204  fourierdlem104  46205  fourierdlem112  46213  fourierdlem113  46214  etransclem1  46230  etransclem4  46233  etransclem8  46237  etransclem15  46244  etransclem17  46246  etransclem18  46247  etransclem19  46248  etransclem20  46249  etransclem21  46250  etransclem22  46251  etransclem23  46252  etransclem24  46253  etransclem25  46254  etransclem27  46256  etransclem32  46261  etransclem35  46264  etransclem41  46270  etransclem44  46273  etransclem46  46275  modmknepk  47360  iccpartigtl  47421  iccpartgt  47425  iccpartgel  47427  iccelpart  47431  odz2prm2pw  47561  fmtnoprmfac1  47563  fmtnoprmfac2  47565  2pwp1prm  47587  sfprmdvdsmersenne  47601  lighneallem4a  47606  proththdlem  47611  proththd  47612  perfectALTVlem1  47719  perfectALTVlem2  47720  perfectALTV  47721  fpprwpprb  47738  gpgedgvtx1  48060  logbpw2m1  48566  nnpw2blenfzo  48580  nnolog2flm1  48589  dignn0fr  48600  nn0sumshdiglemA  48618  nn0sumshdiglemB  48619