Theorem nnnn0d 12564

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

Syntax hints:   → wi 4   ∈ wcel 2149  ℕcn 12232  ℕ₀cn0 12503

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-un 3918  df-ss 3930  df-n0 12504

This theorem is referenced by:  nn0ge2m1nn0  12574  nnzd  12616  eluzge2nn0  12915  expgt1  14135  expaddzlem  14140  expaddz  14141  expmulz  14143  expmulnbnd  14270  exp11nnd  14296  facwordi  14324  faclbnd  14325  facavg  14336  bcm1k  14350  wrdeqs1cat  14756  cshwcsh2id  14864  relexpsucnnr  15061  isercolllem2  15716  bcxmas  15888  climcndslem1  15902  climcndslem2  15903  climcnds  15904  pwdif  15921  geo2sum  15926  mertenslem1  15937  prodmolem3  15986  prodmolem2a  15987  bpolydiflem  16107  eftabs  16128  efcllem  16130  eftlub  16164  eirrlem  16259  rpnnen2lem9  16277  rpnnen2lem11  16279  dvdsfac  16383  pwp1fsum  16448  oddpwp1fsum  16449  bitsfzo  16492  bitsfi  16494  sadcaddlem  16514  smumullem  16549  gcdcl  16563  dvdsgcdidd  16594  mulgcd  16605  rplpwr  16615  rprpwr  16616  rppwr  16617  nn0rppwr  16618  expgcd  16620  lcmcl  16658  lcmgcdnn  16668  lcmfcl  16685  nprmdvds1  16764  rpexp  16780  prmdvdsbc  16784  zsqrtelqelz  16816  phiprmpw  16834  eulerthlem2  16840  eulerth  16841  fermltl  16842  odzcllem  16851  odzdvds  16854  odzphi  16855  prm23lt5  16873  pythagtriplem6  16880  pythagtriplem7  16881  pcprmpw2  16941  dvdsprmpweqle  16945  pcprod  16954  pcfac  16958  pcbc  16959  expnprm  16961  pockthlem  16964  pockthg  16965  prmunb  16973  prmreclem2  16976  prmreclem3  16977  prmreclem4  16978  prmreclem5  16979  prmreclem6  16980  mul4sqlem  17012  4sqlem11  17014  4sqlem17  17020  vdwlem1  17040  vdwlem5  17044  vdwlem6  17045  vdwlem8  17047  vdwlem9  17048  vdwlem11  17050  vdwlem12  17051  vdwnnlem3  17056  ramz2  17083  ramub1lem1  17085  ramub1lem2  17086  ramub1  17087  prmgaplem3  17112  2expltfac  17151  psgnunilem3  19565  odfval  19601  mndodconglem  19610  gexcl3  19656  pgpfi1  19664  sylow1lem1  19667  gexexlem  19921  prmcyg  19963  gsumval3  19976  ablfacrplem  20136  ablfacrp  20137  ablfacrp2  20138  ablfac1eu  20144  prmgrpsimpgd  20185  srgbinomlem3  20309  srgbinomlem4  20310  fermltlchr  21647  freshmansdream  21692  chfacfscmulgsum  22985  chfacfpmmulgsum  22989  cpmadugsumlemF  23001  ovoliunlem1  25629  mbfi1fseqlem1  25842  mbfi1fseqlem3  25844  mbfi1fseqlem5  25846  itg2cnlem2  25889  plyn0mulidp  26410  dvply1  26413  aalioulem2  26462  aalioulem5  26465  aaliou3lem1  26471  aaliou3lem2  26472  aaliou3lem8  26474  aaliou3lem6  26477  taylthlem1  26501  taylthlem2  26502  pserdvlem2  26556  cxpeq  26887  zrtelqelz  26888  dmgmdivn0  27157  lgamgulmlem5  27162  lgamcvg2  27184  wilthlem1  27197  ftalem1  27202  ftalem2  27203  ftalem4  27205  ftalem5  27206  basellem2  27211  basellem3  27212  basellem4  27213  basellem5  27214  isppw2  27244  mpodvdsmulf1o  27323  dvdsmulf1o  27325  sgmmul  27330  fsumvma2  27343  chpchtsum  27348  logfacubnd  27350  mersenne  27356  perfect1  27357  perfectlem1  27358  perfectlem2  27359  perfect  27360  dchrelbas3  27367  dchrelbasd  27368  dchrzrh1  27373  dchrzrhmul  27375  dchrmulcl  27378  dchrn0  27379  dchrfi  27384  dchrghm  27385  dchrabs  27389  dchrinv  27390  dchrptlem1  27393  dchrptlem2  27394  dchrptlem3  27395  dchrpt  27396  dchrsum2  27397  sum2dchr  27403  pcbcctr  27405  bcmono  27406  bclbnd  27409  bposlem1  27413  bposlem3  27415  bposlem5  27417  bposlem6  27418  lgslem1  27426  lgsval2lem  27436  lgsvalmod  27445  lgsmod  27452  lgsdirprm  27460  lgsne0  27464  lgsqrlem1  27475  lgsqrlem2  27476  lgsqrlem3  27477  lgsqrlem4  27478  gausslemma2dlem0b  27486  gausslemma2dlem0c  27487  gausslemma2dlem1  27495  gausslemma2dlem7  27502  gausslemma2d  27503  lgseisenlem1  27504  lgseisenlem2  27505  lgseisenlem3  27506  lgseisenlem4  27507  lgseisen  27508  lgsquadlem2  27510  lgsquadlem3  27511  m1lgs  27517  2lgslem1a  27520  2sqlem3  27549  2sqblem  27560  chebbnd1lem1  27598  chebbnd1lem3  27600  rplogsumlem2  27614  rpvmasumlem  27616  dchrisumlem1  27618  dchrisumlem2  27619  dchrmusum2  27623  dchrvmasumlem3  27628  dchrisum0ff  27636  dchrisum0flblem1  27637  rpvmasum2  27641  dchrisum0re  27642  dchrisum0lem2a  27646  dirith  27658  mudivsum  27659  pntpbnd1a  27714  pntlemq  27730  pntlemr  27731  pntlemj  27732  ostth2lem1  27747  ostth2lem2  27763  ostth2lem3  27764  ostth2  27766  crctcshwlkn0lem6  30104  hashecclwwlkn1  30368  umgrhashecclwwlk  30369  clwwlknon  30381  eucrctshift  30534  numclwlk1lem2  30661  nrt2irr  30764  dipcl  31004  dipcn  31012  bcm1n  33080  expgt0b  33101  nexple  33117  2exple2exp  33118  oexpled  33120  wrdpmtrlast  33353  psgnfzto1st  33365  isarchi2  33445  submarchi  33446  znfermltl  33623  fldextrspundgdvdslem  34014  fldextrspundgdvds  34015  fldext2rspun  34016  constrext2chnlem  34084  cos9thpiminplylem2  34117  submateqlem1  34141  madjusmdetlem2  34162  madjusmdetlem4  34164  mdetlap  34166  oddpwdc  34688  eulerpartlemsv2  34692  eulerpartlemsf  34693  eulerpartlems  34694  eulerpartlemv  34698  eulerpartlemb  34702  signsvtn0  34901  fsum2dsub  34938  reprinfz1  34953  reprpmtf1o  34957  circlemeth  34971  circlemethnat  34972  hgt750lemb  34987  hgt750lema  34988  hgt750leme  34989  tgoldbachgtde  34991  tgoldbachgtda  34992  lpadleft  35017  subfacp1lem1  35569  subfacp1lem6  35575  subfaclim  35578  erdszelem8  35588  erdszelem10  35590  cvmliftlem10  35684  faclim2  36138  poimirlem7  38165  poimirlem17  38175  poimirlem18  38176  poimirlem20  38178  poimirlem21  38179  poimirlem22  38180  poimirlem25  38183  poimirlem26  38184  poimirlem27  38185  poimirlem28  38186  poimirlem32  38190  nninfnub  38289  bfplem1  38360  zndvdchrrhm  42629  lcmineqlem1  42685  lcmineqlem2  42686  lcmineqlem8  42692  lcmineqlem10  42694  lcmineqlem11  42695  lcmineqlem15  42699  lcmineqlem16  42700  lcmineqlem18  42702  lcmineqlem19  42703  lcmineqlem20  42704  lcmineqlem21  42705  lcmineqlem22  42706  3lexlogpow2ineq2  42715  dvrelogpow2b  42724  aks4d1p1p2  42726  aks4d1p1p4  42727  aks4d1p1  42732  aks4d1p3  42734  aks4d1p7d1  42738  aks4d1p7  42739  aks4d1p8  42743  aks4d1p9  42744  isprimroot2  42750  primrootsunit1  42753  primrootscoprmpow  42755  posbezout  42756  primrootscoprbij  42758  primrootlekpowne0  42761  primrootspoweq0  42762  aks6d1c1p2  42765  aks6d1c1p3  42766  aks6d1c1p4  42767  aks6d1c1p5  42768  aks6d1c1p7  42769  aks6d1c1p6  42770  aks6d1c1p8  42771  aks6d1c2p2  42775  hashscontpowcl  42776  hashscontpow1  42777  hashscontpow  42778  aks6d1c4  42780  aks6d1c2lem3  42782  aks6d1c2lem4  42783  aks6d1c2  42786  sticksstones6  42807  sticksstones7  42808  sticksstones10  42811  sticksstones12a  42813  sticksstones12  42814  sticksstones20  42822  sticksstones22  42824  aks6d1c6lem2  42827  aks6d1c6lem3  42828  aks6d1c6lem4  42829  aks6d1c6isolem1  42830  aks6d1c6isolem2  42831  aks6d1c6lem5  42833  bcled  42834  bcle2d  42835  aks6d1c7lem1  42836  aks6d1c7  42840  aks5lem2  42843  aks5lem3a  42845  aks5lem5a  42847  grpods  42850  unitscyglem2  42852  unitscyglem4  42854  aks5lem7  42856  aks5  42860  sumcubes  42963  oexpreposd  42972  exp11d  42976  dvdsexpb  42985  fiabv  43195  fsuppind  43213  dffltz  43257  fltdvdsabdvdsc  43261  fltne  43267  flt4lem4  43272  flt4lem7  43282  fltltc  43284  fltnltalem  43285  fltnlta  43286  3rexfrabdioph  43415  4rexfrabdioph  43416  6rexfrabdioph  43417  7rexfrabdioph  43418  irrapxlem5  43444  pellexlem2  43448  pellexlem6  43452  pell14qrgt0  43477  pell1qrge1  43488  pellfundgt1  43501  ltrmxnn0  43567  jm2.26lem3  43619  jm2.27a  43623  jm2.27c  43625  rmxdiophlem  43633  jm3.1lem1  43635  jm3.1lem2  43636  jm3.1lem3  43637  jm3.1  43638  dgrsub2  43753  mpaaeu  43768  idomsubgmo  43811  relexpxpmin  44334  nzprmdif  44920  binomcxplemwb  44949  fperiodmul  45914  xralrple4  45979  fsumnncl  46179  dvsinexp  46516  dvxpaek  46545  itgsinexplem1  46559  stoweidlem1  46606  stoweidlem17  46622  stoweidlem25  46630  stoweidlem34  46639  stoweidlem38  46643  stoweidlem40  46645  stoweidlem42  46647  stoweidlem45  46650  stirlinglem4  46682  stirlinglem5  46683  stirlinglem10  46688  stirlinglem13  46691  dirkertrigeq  46706  fourierdlem21  46733  fourierdlem25  46737  fourierdlem48  46759  fourierdlem54  46765  fourierdlem64  46775  fourierdlem65  46776  fourierdlem73  46784  fourierdlem81  46792  fourierdlem83  46794  fourierdlem92  46803  fourierdlem103  46814  fourierdlem104  46815  fourierdlem112  46823  fourierdlem113  46824  etransclem1  46840  etransclem4  46843  etransclem8  46847  etransclem15  46854  etransclem17  46856  etransclem18  46857  etransclem19  46858  etransclem20  46859  etransclem21  46860  etransclem22  46861  etransclem23  46862  etransclem24  46863  etransclem25  46864  etransclem27  46866  etransclem32  46871  etransclem35  46874  etransclem41  46880  etransclem44  46883  etransclem46  46885  modmknepk  47993  iccpartigtl  48060  iccpartgt  48064  iccpartgel  48066  iccelpart  48070  odz2prm2pw  48203  fmtnoprmfac1  48205  fmtnoprmfac2  48207  2pwp1prm  48229  sfprmdvdsmersenne  48243  lighneallem4a  48248  proththdlem  48253  proththd  48254  perfectALTVlem1  48374  perfectALTVlem2  48375  perfectALTV  48376  fpprwpprb  48393  gpgedgvtx1  48715  logbpw2m1  49231  nnpw2blenfzo  49245  nnolog2flm1  49254  dignn0fr  49265  nn0sumshdiglemA  49283  nn0sumshdiglemB  49284