Theorem nnnn0d 12464

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℕcn 12147  ℕ₀cn0 12403

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 3440  df-un 3910  df-ss 3922  df-n0 12404

This theorem is referenced by:  nn0ge2m1nn0  12474  nnzd  12517  eluzge2nn0  12812  expgt1  14026  expaddzlem  14031  expaddz  14032  expmulz  14034  expmulnbnd  14161  exp11nnd  14187  facwordi  14215  faclbnd  14216  facavg  14227  bcm1k  14241  wrdeqs1cat  14645  cshwcsh2id  14754  relexpsucnnr  14951  isercolllem2  15592  bcxmas  15761  climcndslem1  15775  climcndslem2  15776  climcnds  15777  pwdif  15794  geo2sum  15799  mertenslem1  15810  prodmolem3  15859  prodmolem2a  15860  bpolydiflem  15980  eftabs  16001  efcllem  16003  eftlub  16037  eirrlem  16132  rpnnen2lem9  16150  rpnnen2lem11  16152  dvdsfac  16256  pwp1fsum  16321  oddpwp1fsum  16322  bitsfzo  16365  bitsfi  16367  sadcaddlem  16387  smumullem  16422  gcdcl  16436  dvdsgcdidd  16467  mulgcd  16478  rplpwr  16488  rprpwr  16489  rppwr  16490  nn0rppwr  16491  expgcd  16493  lcmcl  16531  lcmgcdnn  16541  lcmfcl  16558  nprmdvds1  16636  rpexp  16652  prmdvdsbc  16656  zsqrtelqelz  16688  phiprmpw  16706  eulerthlem2  16712  eulerth  16713  fermltl  16714  odzcllem  16723  odzdvds  16726  odzphi  16727  prm23lt5  16745  pythagtriplem6  16752  pythagtriplem7  16753  pcprmpw2  16813  dvdsprmpweqle  16817  pcprod  16826  pcfac  16830  pcbc  16831  expnprm  16833  pockthlem  16836  pockthg  16837  prmunb  16845  prmreclem2  16848  prmreclem3  16849  prmreclem4  16850  prmreclem5  16851  prmreclem6  16852  mul4sqlem  16884  4sqlem11  16886  4sqlem17  16892  vdwlem1  16912  vdwlem5  16916  vdwlem6  16917  vdwlem8  16919  vdwlem9  16920  vdwlem11  16922  vdwlem12  16923  vdwnnlem3  16928  ramz2  16955  ramub1lem1  16957  ramub1lem2  16958  ramub1  16959  prmgaplem3  16984  2expltfac  17023  psgnunilem3  19394  odfval  19430  mndodconglem  19439  gexcl3  19485  pgpfi1  19493  sylow1lem1  19496  gexexlem  19750  prmcyg  19792  gsumval3  19805  ablfacrplem  19965  ablfacrp  19966  ablfacrp2  19967  ablfac1eu  19973  prmgrpsimpgd  20014  srgbinomlem3  20132  srgbinomlem4  20133  fermltlchr  21455  freshmansdream  21500  chfacfscmulgsum  22764  chfacfpmmulgsum  22768  cpmadugsumlemF  22780  ovoliunlem1  25420  mbfi1fseqlem1  25633  mbfi1fseqlem3  25635  mbfi1fseqlem5  25637  itg2cnlem2  25680  dvply1  26208  aalioulem2  26258  aalioulem5  26261  aaliou3lem1  26267  aaliou3lem2  26268  aaliou3lem8  26270  aaliou3lem6  26273  taylthlem1  26298  taylthlem2  26299  taylthlem2OLD  26300  pserdvlem2  26355  cxpeq  26684  zrtelqelz  26685  dmgmdivn0  26955  lgamgulmlem5  26960  lgamcvg2  26982  wilthlem1  26995  ftalem1  27000  ftalem2  27001  ftalem4  27003  ftalem5  27004  basellem2  27009  basellem3  27010  basellem4  27011  basellem5  27012  isppw2  27042  mpodvdsmulf1o  27121  dvdsmulf1o  27123  sgmmul  27129  fsumvma2  27142  chpchtsum  27147  logfacubnd  27149  mersenne  27155  perfect1  27156  perfectlem1  27157  perfectlem2  27158  perfect  27159  dchrelbas3  27166  dchrelbasd  27167  dchrzrh1  27172  dchrzrhmul  27174  dchrmulcl  27177  dchrn0  27178  dchrfi  27183  dchrghm  27184  dchrabs  27188  dchrinv  27189  dchrptlem1  27192  dchrptlem2  27193  dchrptlem3  27194  dchrpt  27195  dchrsum2  27196  sum2dchr  27202  pcbcctr  27204  bcmono  27205  bclbnd  27208  bposlem1  27212  bposlem3  27214  bposlem5  27216  bposlem6  27217  lgslem1  27225  lgsval2lem  27235  lgsvalmod  27244  lgsmod  27251  lgsdirprm  27259  lgsne0  27263  lgsqrlem1  27274  lgsqrlem2  27275  lgsqrlem3  27276  lgsqrlem4  27277  gausslemma2dlem0b  27285  gausslemma2dlem0c  27286  gausslemma2dlem1  27294  gausslemma2dlem7  27301  gausslemma2d  27302  lgseisenlem1  27303  lgseisenlem2  27304  lgseisenlem3  27305  lgseisenlem4  27306  lgseisen  27307  lgsquadlem2  27309  lgsquadlem3  27310  m1lgs  27316  2lgslem1a  27319  2sqlem3  27348  2sqblem  27359  chebbnd1lem1  27397  chebbnd1lem3  27399  rplogsumlem2  27413  rpvmasumlem  27415  dchrisumlem1  27417  dchrisumlem2  27418  dchrmusum2  27422  dchrvmasumlem3  27427  dchrisum0ff  27435  dchrisum0flblem1  27436  rpvmasum2  27440  dchrisum0re  27441  dchrisum0lem2a  27445  dirith  27457  mudivsum  27458  pntpbnd1a  27513  pntlemq  27529  pntlemr  27530  pntlemj  27531  ostth2lem1  27546  ostth2lem2  27562  ostth2lem3  27563  ostth2  27565  crctcshwlkn0lem6  29779  hashecclwwlkn1  30040  umgrhashecclwwlk  30041  clwwlknon  30053  eucrctshift  30206  numclwlk1lem2  30333  nrt2irr  30436  dipcl  30675  dipcn  30683  bcm1n  32757  expgt0b  32780  nexple  32808  2exple2exp  32809  oexpled  32811  wrdpmtrlast  33054  psgnfzto1st  33066  isarchi2  33146  submarchi  33147  znfermltl  33322  fldextrspundgdvdslem  33666  fldextrspundgdvds  33667  fldext2rspun  33668  constrext2chnlem  33736  cos9thpiminplylem2  33769  submateqlem1  33793  madjusmdetlem2  33814  madjusmdetlem4  33816  mdetlap  33818  oddpwdc  34341  eulerpartlemsv2  34345  eulerpartlemsf  34346  eulerpartlems  34347  eulerpartlemv  34351  eulerpartlemb  34355  plymulx0  34534  signsvtn0  34557  fsum2dsub  34594  reprinfz1  34609  reprpmtf1o  34613  circlemeth  34627  circlemethnat  34628  hgt750lemb  34643  hgt750lema  34644  hgt750leme  34645  tgoldbachgtde  34647  tgoldbachgtda  34648  lpadleft  34670  subfacp1lem1  35171  subfacp1lem6  35177  subfaclim  35180  erdszelem8  35190  erdszelem10  35192  cvmliftlem10  35286  faclim2  35740  poimirlem7  37626  poimirlem17  37636  poimirlem18  37637  poimirlem20  37639  poimirlem21  37640  poimirlem22  37641  poimirlem25  37644  poimirlem26  37645  poimirlem27  37646  poimirlem28  37647  poimirlem32  37651  nninfnub  37750  bfplem1  37821  zndvdchrrhm  41965  lcmineqlem1  42022  lcmineqlem2  42023  lcmineqlem8  42029  lcmineqlem10  42031  lcmineqlem11  42032  lcmineqlem15  42036  lcmineqlem16  42037  lcmineqlem18  42039  lcmineqlem19  42040  lcmineqlem20  42041  lcmineqlem21  42042  lcmineqlem22  42043  3lexlogpow2ineq2  42052  dvrelogpow2b  42061  aks4d1p1p2  42063  aks4d1p1p4  42064  aks4d1p1  42069  aks4d1p3  42071  aks4d1p7d1  42075  aks4d1p7  42076  aks4d1p8  42080  aks4d1p9  42081  isprimroot2  42087  primrootsunit1  42090  primrootscoprmpow  42092  posbezout  42093  primrootscoprbij  42095  primrootlekpowne0  42098  primrootspoweq0  42099  aks6d1c1p2  42102  aks6d1c1p3  42103  aks6d1c1p4  42104  aks6d1c1p5  42105  aks6d1c1p7  42106  aks6d1c1p6  42107  aks6d1c1p8  42108  aks6d1c2p2  42112  hashscontpowcl  42113  hashscontpow1  42114  hashscontpow  42115  aks6d1c4  42117  aks6d1c2lem3  42119  aks6d1c2lem4  42120  aks6d1c2  42123  sticksstones6  42144  sticksstones7  42145  sticksstones10  42148  sticksstones12a  42150  sticksstones12  42151  sticksstones20  42159  sticksstones22  42161  aks6d1c6lem2  42164  aks6d1c6lem3  42165  aks6d1c6lem4  42166  aks6d1c6isolem1  42167  aks6d1c6isolem2  42168  aks6d1c6lem5  42170  bcled  42171  bcle2d  42172  aks6d1c7lem1  42173  aks6d1c7  42177  aks5lem2  42180  aks5lem3a  42182  aks5lem5a  42184  grpods  42187  unitscyglem2  42189  unitscyglem4  42191  aks5lem7  42193  aks5  42197  sumcubes  42306  oexpreposd  42315  exp11d  42319  dvdsexpb  42328  fiabv  42529  fsuppind  42583  dffltz  42627  fltdvdsabdvdsc  42631  fltne  42637  flt4lem4  42642  flt4lem7  42652  fltltc  42654  fltnltalem  42655  fltnlta  42656  3rexfrabdioph  42790  4rexfrabdioph  42791  6rexfrabdioph  42792  7rexfrabdioph  42793  irrapxlem5  42819  pellexlem2  42823  pellexlem6  42827  pell14qrgt0  42852  pell1qrge1  42863  pellfundgt1  42876  ltrmxnn0  42942  jm2.26lem3  42994  jm2.27a  42998  jm2.27c  43000  rmxdiophlem  43008  jm3.1lem1  43010  jm3.1lem2  43011  jm3.1lem3  43012  jm3.1  43013  dgrsub2  43128  mpaaeu  43143  idomsubgmo  43186  relexpxpmin  43710  nzprmdif  44312  binomcxplemwb  44341  fperiodmul  45306  xralrple4  45372  fsumnncl  45573  dvsinexp  45912  dvxpaek  45941  itgsinexplem1  45955  stoweidlem1  46002  stoweidlem17  46018  stoweidlem25  46026  stoweidlem34  46035  stoweidlem38  46039  stoweidlem40  46041  stoweidlem42  46043  stoweidlem45  46046  stirlinglem4  46078  stirlinglem5  46079  stirlinglem10  46084  stirlinglem13  46087  dirkertrigeq  46102  fourierdlem21  46129  fourierdlem25  46133  fourierdlem48  46155  fourierdlem54  46161  fourierdlem64  46171  fourierdlem65  46172  fourierdlem73  46180  fourierdlem81  46188  fourierdlem83  46190  fourierdlem92  46199  fourierdlem103  46210  fourierdlem104  46211  fourierdlem112  46219  fourierdlem113  46220  etransclem1  46236  etransclem4  46239  etransclem8  46243  etransclem15  46250  etransclem17  46252  etransclem18  46253  etransclem19  46254  etransclem20  46255  etransclem21  46256  etransclem22  46257  etransclem23  46258  etransclem24  46259  etransclem25  46260  etransclem27  46262  etransclem32  46267  etransclem35  46270  etransclem41  46276  etransclem44  46279  etransclem46  46281  modmknepk  47366  iccpartigtl  47427  iccpartgt  47431  iccpartgel  47433  iccelpart  47437  odz2prm2pw  47567  fmtnoprmfac1  47569  fmtnoprmfac2  47571  2pwp1prm  47593  sfprmdvdsmersenne  47607  lighneallem4a  47612  proththdlem  47617  proththd  47618  perfectALTVlem1  47725  perfectALTVlem2  47726  perfectALTV  47727  fpprwpprb  47744  gpgedgvtx1  48066  logbpw2m1  48572  nnpw2blenfzo  48586  nnolog2flm1  48595  dignn0fr  48606  nn0sumshdiglemA  48624  nn0sumshdiglemB  48625