Theorem nnnn0d 12503

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℕcn 12186  ℕ₀cn0 12442

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 3449  df-un 3919  df-ss 3931  df-n0 12443

This theorem is referenced by:  nn0ge2m1nn0  12513  nnzd  12556  eluzge2nn0  12851  expgt1  14065  expaddzlem  14070  expaddz  14071  expmulz  14073  expmulnbnd  14200  exp11nnd  14226  facwordi  14254  faclbnd  14255  facavg  14266  bcm1k  14280  wrdeqs1cat  14685  cshwcsh2id  14794  relexpsucnnr  14991  isercolllem2  15632  bcxmas  15801  climcndslem1  15815  climcndslem2  15816  climcnds  15817  pwdif  15834  geo2sum  15839  mertenslem1  15850  prodmolem3  15899  prodmolem2a  15900  bpolydiflem  16020  eftabs  16041  efcllem  16043  eftlub  16077  eirrlem  16172  rpnnen2lem9  16190  rpnnen2lem11  16192  dvdsfac  16296  pwp1fsum  16361  oddpwp1fsum  16362  bitsfzo  16405  bitsfi  16407  sadcaddlem  16427  smumullem  16462  gcdcl  16476  dvdsgcdidd  16507  mulgcd  16518  rplpwr  16528  rprpwr  16529  rppwr  16530  nn0rppwr  16531  expgcd  16533  lcmcl  16571  lcmgcdnn  16581  lcmfcl  16598  nprmdvds1  16676  rpexp  16692  prmdvdsbc  16696  zsqrtelqelz  16728  phiprmpw  16746  eulerthlem2  16752  eulerth  16753  fermltl  16754  odzcllem  16763  odzdvds  16766  odzphi  16767  prm23lt5  16785  pythagtriplem6  16792  pythagtriplem7  16793  pcprmpw2  16853  dvdsprmpweqle  16857  pcprod  16866  pcfac  16870  pcbc  16871  expnprm  16873  pockthlem  16876  pockthg  16877  prmunb  16885  prmreclem2  16888  prmreclem3  16889  prmreclem4  16890  prmreclem5  16891  prmreclem6  16892  mul4sqlem  16924  4sqlem11  16926  4sqlem17  16932  vdwlem1  16952  vdwlem5  16956  vdwlem6  16957  vdwlem8  16959  vdwlem9  16960  vdwlem11  16962  vdwlem12  16963  vdwnnlem3  16968  ramz2  16995  ramub1lem1  16997  ramub1lem2  16998  ramub1  16999  prmgaplem3  17024  2expltfac  17063  psgnunilem3  19426  odfval  19462  mndodconglem  19471  gexcl3  19517  pgpfi1  19525  sylow1lem1  19528  gexexlem  19782  prmcyg  19824  gsumval3  19837  ablfacrplem  19997  ablfacrp  19998  ablfacrp2  19999  ablfac1eu  20005  prmgrpsimpgd  20046  srgbinomlem3  20137  srgbinomlem4  20138  fermltlchr  21439  freshmansdream  21484  chfacfscmulgsum  22747  chfacfpmmulgsum  22751  cpmadugsumlemF  22763  ovoliunlem1  25403  mbfi1fseqlem1  25616  mbfi1fseqlem3  25618  mbfi1fseqlem5  25620  itg2cnlem2  25663  dvply1  26191  aalioulem2  26241  aalioulem5  26244  aaliou3lem1  26250  aaliou3lem2  26251  aaliou3lem8  26253  aaliou3lem6  26256  taylthlem1  26281  taylthlem2  26282  taylthlem2OLD  26283  pserdvlem2  26338  cxpeq  26667  zrtelqelz  26668  dmgmdivn0  26938  lgamgulmlem5  26943  lgamcvg2  26965  wilthlem1  26978  ftalem1  26983  ftalem2  26984  ftalem4  26986  ftalem5  26987  basellem2  26992  basellem3  26993  basellem4  26994  basellem5  26995  isppw2  27025  mpodvdsmulf1o  27104  dvdsmulf1o  27106  sgmmul  27112  fsumvma2  27125  chpchtsum  27130  logfacubnd  27132  mersenne  27138  perfect1  27139  perfectlem1  27140  perfectlem2  27141  perfect  27142  dchrelbas3  27149  dchrelbasd  27150  dchrzrh1  27155  dchrzrhmul  27157  dchrmulcl  27160  dchrn0  27161  dchrfi  27166  dchrghm  27167  dchrabs  27171  dchrinv  27172  dchrptlem1  27175  dchrptlem2  27176  dchrptlem3  27177  dchrpt  27178  dchrsum2  27179  sum2dchr  27185  pcbcctr  27187  bcmono  27188  bclbnd  27191  bposlem1  27195  bposlem3  27197  bposlem5  27199  bposlem6  27200  lgslem1  27208  lgsval2lem  27218  lgsvalmod  27227  lgsmod  27234  lgsdirprm  27242  lgsne0  27246  lgsqrlem1  27257  lgsqrlem2  27258  lgsqrlem3  27259  lgsqrlem4  27260  gausslemma2dlem0b  27268  gausslemma2dlem0c  27269  gausslemma2dlem1  27277  gausslemma2dlem7  27284  gausslemma2d  27285  lgseisenlem1  27286  lgseisenlem2  27287  lgseisenlem3  27288  lgseisenlem4  27289  lgseisen  27290  lgsquadlem2  27292  lgsquadlem3  27293  m1lgs  27299  2lgslem1a  27302  2sqlem3  27331  2sqblem  27342  chebbnd1lem1  27380  chebbnd1lem3  27382  rplogsumlem2  27396  rpvmasumlem  27398  dchrisumlem1  27400  dchrisumlem2  27401  dchrmusum2  27405  dchrvmasumlem3  27410  dchrisum0ff  27418  dchrisum0flblem1  27419  rpvmasum2  27423  dchrisum0re  27424  dchrisum0lem2a  27428  dirith  27440  mudivsum  27441  pntpbnd1a  27496  pntlemq  27512  pntlemr  27513  pntlemj  27514  ostth2lem1  27529  ostth2lem2  27545  ostth2lem3  27546  ostth2  27548  crctcshwlkn0lem6  29745  hashecclwwlkn1  30006  umgrhashecclwwlk  30007  clwwlknon  30019  eucrctshift  30172  numclwlk1lem2  30299  nrt2irr  30402  dipcl  30641  dipcn  30649  bcm1n  32718  expgt0b  32741  nexple  32769  2exple2exp  32770  oexpled  32772  wrdpmtrlast  33050  psgnfzto1st  33062  isarchi2  33139  submarchi  33140  znfermltl  33337  fldextrspundgdvdslem  33675  fldextrspundgdvds  33676  fldext2rspun  33677  constrext2chnlem  33740  cos9thpiminplylem2  33773  submateqlem1  33797  madjusmdetlem2  33818  madjusmdetlem4  33820  mdetlap  33822  oddpwdc  34345  eulerpartlemsv2  34349  eulerpartlemsf  34350  eulerpartlems  34351  eulerpartlemv  34355  eulerpartlemb  34359  plymulx0  34538  signsvtn0  34561  fsum2dsub  34598  reprinfz1  34613  reprpmtf1o  34617  circlemeth  34631  circlemethnat  34632  hgt750lemb  34647  hgt750lema  34648  hgt750leme  34649  tgoldbachgtde  34651  tgoldbachgtda  34652  lpadleft  34674  subfacp1lem1  35166  subfacp1lem6  35172  subfaclim  35175  erdszelem8  35185  erdszelem10  35187  cvmliftlem10  35281  faclim2  35735  poimirlem7  37621  poimirlem17  37631  poimirlem18  37632  poimirlem20  37634  poimirlem21  37635  poimirlem22  37636  poimirlem25  37639  poimirlem26  37640  poimirlem27  37641  poimirlem28  37642  poimirlem32  37646  nninfnub  37745  bfplem1  37816  zndvdchrrhm  41960  lcmineqlem1  42017  lcmineqlem2  42018  lcmineqlem8  42024  lcmineqlem10  42026  lcmineqlem11  42027  lcmineqlem15  42031  lcmineqlem16  42032  lcmineqlem18  42034  lcmineqlem19  42035  lcmineqlem20  42036  lcmineqlem21  42037  lcmineqlem22  42038  3lexlogpow2ineq2  42047  dvrelogpow2b  42056  aks4d1p1p2  42058  aks4d1p1p4  42059  aks4d1p1  42064  aks4d1p3  42066  aks4d1p7d1  42070  aks4d1p7  42071  aks4d1p8  42075  aks4d1p9  42076  isprimroot2  42082  primrootsunit1  42085  primrootscoprmpow  42087  posbezout  42088  primrootscoprbij  42090  primrootlekpowne0  42093  primrootspoweq0  42094  aks6d1c1p2  42097  aks6d1c1p3  42098  aks6d1c1p4  42099  aks6d1c1p5  42100  aks6d1c1p7  42101  aks6d1c1p6  42102  aks6d1c1p8  42103  aks6d1c2p2  42107  hashscontpowcl  42108  hashscontpow1  42109  hashscontpow  42110  aks6d1c4  42112  aks6d1c2lem3  42114  aks6d1c2lem4  42115  aks6d1c2  42118  sticksstones6  42139  sticksstones7  42140  sticksstones10  42143  sticksstones12a  42145  sticksstones12  42146  sticksstones20  42154  sticksstones22  42156  aks6d1c6lem2  42159  aks6d1c6lem3  42160  aks6d1c6lem4  42161  aks6d1c6isolem1  42162  aks6d1c6isolem2  42163  aks6d1c6lem5  42165  bcled  42166  bcle2d  42167  aks6d1c7lem1  42168  aks6d1c7  42172  aks5lem2  42175  aks5lem3a  42177  aks5lem5a  42179  grpods  42182  unitscyglem2  42184  unitscyglem4  42186  aks5lem7  42188  aks5  42192  sumcubes  42301  oexpreposd  42310  exp11d  42314  dvdsexpb  42323  fiabv  42524  fsuppind  42578  dffltz  42622  fltdvdsabdvdsc  42626  fltne  42632  flt4lem4  42637  flt4lem7  42647  fltltc  42649  fltnltalem  42650  fltnlta  42651  3rexfrabdioph  42785  4rexfrabdioph  42786  6rexfrabdioph  42787  7rexfrabdioph  42788  irrapxlem5  42814  pellexlem2  42818  pellexlem6  42822  pell14qrgt0  42847  pell1qrge1  42858  pellfundgt1  42871  ltrmxnn0  42938  jm2.26lem3  42990  jm2.27a  42994  jm2.27c  42996  rmxdiophlem  43004  jm3.1lem1  43006  jm3.1lem2  43007  jm3.1lem3  43008  jm3.1  43009  dgrsub2  43124  mpaaeu  43139  idomsubgmo  43182  relexpxpmin  43706  nzprmdif  44308  binomcxplemwb  44337  fperiodmul  45302  xralrple4  45369  fsumnncl  45570  dvsinexp  45909  dvxpaek  45938  itgsinexplem1  45952  stoweidlem1  45999  stoweidlem17  46015  stoweidlem25  46023  stoweidlem34  46032  stoweidlem38  46036  stoweidlem40  46038  stoweidlem42  46040  stoweidlem45  46043  stirlinglem4  46075  stirlinglem5  46076  stirlinglem10  46081  stirlinglem13  46084  dirkertrigeq  46099  fourierdlem21  46126  fourierdlem25  46130  fourierdlem48  46152  fourierdlem54  46158  fourierdlem64  46168  fourierdlem65  46169  fourierdlem73  46177  fourierdlem81  46185  fourierdlem83  46187  fourierdlem92  46196  fourierdlem103  46207  fourierdlem104  46208  fourierdlem112  46216  fourierdlem113  46217  etransclem1  46233  etransclem4  46236  etransclem8  46240  etransclem15  46247  etransclem17  46249  etransclem18  46250  etransclem19  46251  etransclem20  46252  etransclem21  46253  etransclem22  46254  etransclem23  46255  etransclem24  46256  etransclem25  46257  etransclem27  46259  etransclem32  46264  etransclem35  46267  etransclem41  46273  etransclem44  46276  etransclem46  46278  modmknepk  47363  iccpartigtl  47424  iccpartgt  47428  iccpartgel  47430  iccelpart  47434  odz2prm2pw  47564  fmtnoprmfac1  47566  fmtnoprmfac2  47568  2pwp1prm  47590  sfprmdvdsmersenne  47604  lighneallem4a  47609  proththdlem  47614  proththd  47615  perfectALTVlem1  47722  perfectALTVlem2  47723  perfectALTV  47724  fpprwpprb  47741  gpgedgvtx1  48053  logbpw2m1  48556  nnpw2blenfzo  48570  nnolog2flm1  48579  dignn0fr  48590  nn0sumshdiglemA  48608  nn0sumshdiglemB  48609