Theorem nnnn0d 12498

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℕcn 12174  ℕ₀cn0 12437

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894  df-ss 3906  df-n0 12438

This theorem is referenced by:  nn0ge2m1nn0  12508  nnzd  12550  eluzge2nn0  12842  expgt1  14062  expaddzlem  14067  expaddz  14068  expmulz  14070  expmulnbnd  14197  exp11nnd  14223  facwordi  14251  faclbnd  14252  facavg  14263  bcm1k  14277  wrdeqs1cat  14682  cshwcsh2id  14790  relexpsucnnr  14987  isercolllem2  15628  bcxmas  15800  climcndslem1  15814  climcndslem2  15815  climcnds  15816  pwdif  15833  geo2sum  15838  mertenslem1  15849  prodmolem3  15898  prodmolem2a  15899  bpolydiflem  16019  eftabs  16040  efcllem  16042  eftlub  16076  eirrlem  16171  rpnnen2lem9  16189  rpnnen2lem11  16191  dvdsfac  16295  pwp1fsum  16360  oddpwp1fsum  16361  bitsfzo  16404  bitsfi  16406  sadcaddlem  16426  smumullem  16461  gcdcl  16475  dvdsgcdidd  16506  mulgcd  16517  rplpwr  16527  rprpwr  16528  rppwr  16529  nn0rppwr  16530  expgcd  16532  lcmcl  16570  lcmgcdnn  16580  lcmfcl  16597  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  19471  odfval  19507  mndodconglem  19516  gexcl3  19562  pgpfi1  19570  sylow1lem1  19573  gexexlem  19827  prmcyg  19869  gsumval3  19882  ablfacrplem  20042  ablfacrp  20043  ablfacrp2  20044  ablfac1eu  20050  prmgrpsimpgd  20091  srgbinomlem3  20209  srgbinomlem4  20210  fermltlchr  21509  freshmansdream  21554  chfacfscmulgsum  22825  chfacfpmmulgsum  22829  cpmadugsumlemF  22841  ovoliunlem1  25469  mbfi1fseqlem1  25682  mbfi1fseqlem3  25684  mbfi1fseqlem5  25686  itg2cnlem2  25729  dvply1  26250  aalioulem2  26299  aalioulem5  26302  aaliou3lem1  26308  aaliou3lem2  26309  aaliou3lem8  26311  aaliou3lem6  26314  taylthlem1  26338  taylthlem2  26339  pserdvlem2  26393  cxpeq  26721  zrtelqelz  26722  dmgmdivn0  26991  lgamgulmlem5  26996  lgamcvg2  27018  wilthlem1  27031  ftalem1  27036  ftalem2  27037  ftalem4  27039  ftalem5  27040  basellem2  27045  basellem3  27046  basellem4  27047  basellem5  27048  isppw2  27078  mpodvdsmulf1o  27157  dvdsmulf1o  27159  sgmmul  27164  fsumvma2  27177  chpchtsum  27182  logfacubnd  27184  mersenne  27190  perfect1  27191  perfectlem1  27192  perfectlem2  27193  perfect  27194  dchrelbas3  27201  dchrelbasd  27202  dchrzrh1  27207  dchrzrhmul  27209  dchrmulcl  27212  dchrn0  27213  dchrfi  27218  dchrghm  27219  dchrabs  27223  dchrinv  27224  dchrptlem1  27227  dchrptlem2  27228  dchrptlem3  27229  dchrpt  27230  dchrsum2  27231  sum2dchr  27237  pcbcctr  27239  bcmono  27240  bclbnd  27243  bposlem1  27247  bposlem3  27249  bposlem5  27251  bposlem6  27252  lgslem1  27260  lgsval2lem  27270  lgsvalmod  27279  lgsmod  27286  lgsdirprm  27294  lgsne0  27298  lgsqrlem1  27309  lgsqrlem2  27310  lgsqrlem3  27311  lgsqrlem4  27312  gausslemma2dlem0b  27320  gausslemma2dlem0c  27321  gausslemma2dlem1  27329  gausslemma2dlem7  27336  gausslemma2d  27337  lgseisenlem1  27338  lgseisenlem2  27339  lgseisenlem3  27340  lgseisenlem4  27341  lgseisen  27342  lgsquadlem2  27344  lgsquadlem3  27345  m1lgs  27351  2lgslem1a  27354  2sqlem3  27383  2sqblem  27394  chebbnd1lem1  27432  chebbnd1lem3  27434  rplogsumlem2  27448  rpvmasumlem  27450  dchrisumlem1  27452  dchrisumlem2  27453  dchrmusum2  27457  dchrvmasumlem3  27462  dchrisum0ff  27470  dchrisum0flblem1  27471  rpvmasum2  27475  dchrisum0re  27476  dchrisum0lem2a  27480  dirith  27492  mudivsum  27493  pntpbnd1a  27548  pntlemq  27564  pntlemr  27565  pntlemj  27566  ostth2lem1  27581  ostth2lem2  27597  ostth2lem3  27598  ostth2  27600  crctcshwlkn0lem6  29883  hashecclwwlkn1  30147  umgrhashecclwwlk  30148  clwwlknon  30160  eucrctshift  30313  numclwlk1lem2  30440  nrt2irr  30543  dipcl  30783  dipcn  30791  bcm1n  32868  expgt0b  32890  nexple  32917  2exple2exp  32918  oexpled  32920  wrdpmtrlast  33154  psgnfzto1st  33166  isarchi2  33246  submarchi  33247  znfermltl  33426  fldextrspundgdvdslem  33824  fldextrspundgdvds  33825  fldext2rspun  33826  constrext2chnlem  33894  cos9thpiminplylem2  33927  submateqlem1  33951  madjusmdetlem2  33972  madjusmdetlem4  33974  mdetlap  33976  oddpwdc  34498  eulerpartlemsv2  34502  eulerpartlemsf  34503  eulerpartlems  34504  eulerpartlemv  34508  eulerpartlemb  34512  plymulx0  34691  signsvtn0  34714  fsum2dsub  34751  reprinfz1  34766  reprpmtf1o  34770  circlemeth  34784  circlemethnat  34785  hgt750lemb  34800  hgt750lema  34801  hgt750leme  34802  tgoldbachgtde  34804  tgoldbachgtda  34805  lpadleft  34827  subfacp1lem1  35361  subfacp1lem6  35367  subfaclim  35370  erdszelem8  35380  erdszelem10  35382  cvmliftlem10  35476  faclim2  35930  poimirlem7  37948  poimirlem17  37958  poimirlem18  37959  poimirlem20  37961  poimirlem21  37962  poimirlem22  37963  poimirlem25  37966  poimirlem26  37967  poimirlem27  37968  poimirlem28  37969  poimirlem32  37973  nninfnub  38072  bfplem1  38143  zndvdchrrhm  42412  lcmineqlem1  42468  lcmineqlem2  42469  lcmineqlem8  42475  lcmineqlem10  42477  lcmineqlem11  42478  lcmineqlem15  42482  lcmineqlem16  42483  lcmineqlem18  42485  lcmineqlem19  42486  lcmineqlem20  42487  lcmineqlem21  42488  lcmineqlem22  42489  3lexlogpow2ineq2  42498  dvrelogpow2b  42507  aks4d1p1p2  42509  aks4d1p1p4  42510  aks4d1p1  42515  aks4d1p3  42517  aks4d1p7d1  42521  aks4d1p7  42522  aks4d1p8  42526  aks4d1p9  42527  isprimroot2  42533  primrootsunit1  42536  primrootscoprmpow  42538  posbezout  42539  primrootscoprbij  42541  primrootlekpowne0  42544  primrootspoweq0  42545  aks6d1c1p2  42548  aks6d1c1p3  42549  aks6d1c1p4  42550  aks6d1c1p5  42551  aks6d1c1p7  42552  aks6d1c1p6  42553  aks6d1c1p8  42554  aks6d1c2p2  42558  hashscontpowcl  42559  hashscontpow1  42560  hashscontpow  42561  aks6d1c4  42563  aks6d1c2lem3  42565  aks6d1c2lem4  42566  aks6d1c2  42569  sticksstones6  42590  sticksstones7  42591  sticksstones10  42594  sticksstones12a  42596  sticksstones12  42597  sticksstones20  42605  sticksstones22  42607  aks6d1c6lem2  42610  aks6d1c6lem3  42611  aks6d1c6lem4  42612  aks6d1c6isolem1  42613  aks6d1c6isolem2  42614  aks6d1c6lem5  42616  bcled  42617  bcle2d  42618  aks6d1c7lem1  42619  aks6d1c7  42623  aks5lem2  42626  aks5lem3a  42628  aks5lem5a  42630  grpods  42633  unitscyglem2  42635  unitscyglem4  42637  aks5lem7  42639  aks5  42643  sumcubes  42745  oexpreposd  42754  exp11d  42758  dvdsexpb  42767  fiabv  42981  fsuppind  43023  dffltz  43067  fltdvdsabdvdsc  43071  fltne  43077  flt4lem4  43082  flt4lem7  43092  fltltc  43094  fltnltalem  43095  fltnlta  43096  3rexfrabdioph  43225  4rexfrabdioph  43226  6rexfrabdioph  43227  7rexfrabdioph  43228  irrapxlem5  43254  pellexlem2  43258  pellexlem6  43262  pell14qrgt0  43287  pell1qrge1  43298  pellfundgt1  43311  ltrmxnn0  43377  jm2.26lem3  43429  jm2.27a  43433  jm2.27c  43435  rmxdiophlem  43443  jm3.1lem1  43445  jm3.1lem2  43446  jm3.1lem3  43447  jm3.1  43448  dgrsub2  43563  mpaaeu  43578  idomsubgmo  43621  relexpxpmin  44144  nzprmdif  44746  binomcxplemwb  44775  fperiodmul  45737  xralrple4  45802  fsumnncl  46002  dvsinexp  46339  dvxpaek  46368  itgsinexplem1  46382  stoweidlem1  46429  stoweidlem17  46445  stoweidlem25  46453  stoweidlem34  46462  stoweidlem38  46466  stoweidlem40  46468  stoweidlem42  46470  stoweidlem45  46473  stirlinglem4  46505  stirlinglem5  46506  stirlinglem10  46511  stirlinglem13  46514  dirkertrigeq  46529  fourierdlem21  46556  fourierdlem25  46560  fourierdlem48  46582  fourierdlem54  46588  fourierdlem64  46598  fourierdlem65  46599  fourierdlem73  46607  fourierdlem81  46615  fourierdlem83  46617  fourierdlem92  46626  fourierdlem103  46637  fourierdlem104  46638  fourierdlem112  46646  fourierdlem113  46647  etransclem1  46663  etransclem4  46666  etransclem8  46670  etransclem15  46677  etransclem17  46679  etransclem18  46680  etransclem19  46681  etransclem20  46682  etransclem21  46683  etransclem22  46684  etransclem23  46685  etransclem24  46686  etransclem25  46687  etransclem27  46689  etransclem32  46694  etransclem35  46697  etransclem41  46703  etransclem44  46706  etransclem46  46708  modmknepk  47816  iccpartigtl  47883  iccpartgt  47887  iccpartgel  47889  iccelpart  47893  odz2prm2pw  48026  fmtnoprmfac1  48028  fmtnoprmfac2  48030  2pwp1prm  48052  sfprmdvdsmersenne  48066  lighneallem4a  48071  proththdlem  48076  proththd  48077  perfectALTVlem1  48197  perfectALTVlem2  48198  perfectALTV  48199  fpprwpprb  48216  gpgedgvtx1  48538  logbpw2m1  49043  nnpw2blenfzo  49057  nnolog2flm1  49066  dignn0fr  49077  nn0sumshdiglemA  49095  nn0sumshdiglemB  49096