Theorem nnnn0d 12589

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ℕcn 12257  ℕ₀cn0 12528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 3904  df-ss 3916  df-n0 12529

This theorem is used by:  nn0ge2m1nn0  12599  nnzd  12641  eluzge2nn0  12941  expgt1  14164  expaddzlem  14169  expaddz  14170  expmulz  14172  expmulnbnd  14299  exp11nnd  14325  facwordi  14353  faclbnd  14354  facavg  14365  bcm1k  14379  wrdeqs1cat  14789  cshwcsh2id  14899  relexpsucnnr  15098  isercolllem2  15753  bcxmas  15924  climcndslem1  15938  climcndslem2  15939  climcnds  15940  pwdif  15957  geo2sum  15962  mertenslem1  15973  prodmolem3  16020  prodmolem2a  16021  bpolydiflem  16140  eftabs  16161  efcllem  16163  eftlub  16197  eirrlem  16292  rpnnen2lem9  16310  rpnnen2lem11  16312  dvdsfac  16416  pwp1fsum  16481  oddpwp1fsum  16482  bitsfzo  16525  bitsfi  16527  sadcaddlem  16547  smumullem  16582  gcdcl  16596  dvdsgcdidd  16627  mulgcd  16638  rplpwr  16648  rprpwr  16649  rppwr  16650  nn0rppwr  16651  expgcd  16653  lcmcl  16691  lcmgcdnn  16701  lcmfcl  16718  nprmdvds1  16797  rpexp  16813  prmdvdsbc  16817  zsqrtelqelz  16849  phiprmpw  16867  eulerthlem2  16873  eulerth  16874  fermltl  16875  odzcllem  16884  odzdvds  16887  odzphi  16888  prm23lt5  16906  pythagtriplem6  16913  pythagtriplem7  16914  pcprmpw2  16974  dvdsprmpweqle  16978  pcprod  16987  pcfac  16991  pcbc  16992  expnprm  16994  pockthlem  16997  pockthg  16998  prmunb  17006  prmreclem2  17009  prmreclem3  17010  prmreclem4  17011  prmreclem5  17012  prmreclem6  17013  mul4sqlem  17045  4sqlem11  17047  4sqlem17  17053  vdwlem1  17073  vdwlem5  17077  vdwlem6  17078  vdwlem8  17080  vdwlem9  17081  vdwlem11  17083  vdwlem12  17084  vdwnnlem3  17089  ramz2  17116  ramub1lem1  17118  ramub1lem2  17119  ramub1  17120  prmgaplem3  17145  2expltfac  17184  psgnunilem3  19623  odfval  19659  mndodconglem  19668  gexcl3  19714  pgpfi1  19722  sylow1lem1  19725  gexexlem  19979  prmcyg  20021  gsumval3  20034  ablfacrplem  20194  ablfacrp  20195  ablfacrp2  20196  ablfac1eu  20202  prmgrpsimpgd  20243  srgbinomlem3  20367  srgbinomlem4  20368  fermltlchr  21742  freshmansdream  21787  chfacfscmulgsum  23085  chfacfpmmulgsum  23089  cpmadugsumlemF  23101  ovoliunlem1  25730  mbfi1fseqlem1  25943  mbfi1fseqlem3  25945  mbfi1fseqlem5  25947  itg2cnlem2  25990  plyn0mulidp  26511  dvply1  26514  aalioulem2  26569  aalioulem5  26572  aaliou3lem1  26578  aaliou3lem2  26579  aaliou3lem8  26581  aaliou3lem6  26584  taylthlem1  26609  taylthlem2  26610  pserdvlem2  26664  cxpeq  26994  zrtelqelz  26995  dmgmdivn0  27264  lgamgulmlem5  27269  lgamcvg2  27291  wilthlem1  27304  ftalem1  27309  ftalem2  27310  ftalem4  27312  ftalem5  27313  basellem2  27318  basellem3  27319  basellem4  27320  basellem5  27321  isppw2  27351  mpodvdsmulf1o  27430  dvdsmulf1o  27432  sgmmul  27437  fsumvma2  27450  chpchtsum  27455  logfacubnd  27457  mersenne  27463  perfect1  27464  perfectlem1  27465  perfectlem2  27466  perfect  27467  dchrelbas3  27474  dchrelbasd  27475  dchrzrh1  27480  dchrzrhmul  27482  dchrmulcl  27485  dchrn0  27486  dchrfi  27491  dchrghm  27492  dchrabs  27496  dchrinv  27497  dchrptlem1  27500  dchrptlem2  27501  dchrptlem3  27502  dchrpt  27503  dchrsum2  27504  sum2dchr  27510  pcbcctr  27512  bcmono  27513  bclbnd  27516  bposlem1  27520  bposlem3  27522  bposlem5  27524  bposlem6  27525  lgslem1  27533  lgsval2lem  27543  lgsvalmod  27552  lgsmod  27559  lgsdirprm  27567  lgsne0  27571  lgsqrlem1  27582  lgsqrlem2  27583  lgsqrlem3  27584  lgsqrlem4  27585  gausslemma2dlem0b  27593  gausslemma2dlem0c  27594  gausslemma2dlem1  27602  gausslemma2dlem7  27609  gausslemma2d  27610  lgseisenlem1  27611  lgseisenlem2  27612  lgseisenlem3  27613  lgseisenlem4  27614  lgseisen  27615  lgsquadlem2  27617  lgsquadlem3  27618  m1lgs  27624  2lgslem1a  27627  2sqlem3  27656  2sqblem  27667  chebbnd1lem1  27705  chebbnd1lem3  27707  rplogsumlem2  27721  rpvmasumlem  27723  dchrisumlem1  27725  dchrisumlem2  27726  dchrmusum2  27730  dchrvmasumlem3  27735  dchrisum0ff  27743  dchrisum0flblem1  27744  rpvmasum2  27748  dchrisum0re  27749  dchrisum0lem2a  27753  dirith  27765  mudivsum  27766  pntpbnd1a  27821  pntlemq  27837  pntlemr  27838  pntlemj  27839  ostth2lem1  27854  ostth2lem2  27870  ostth2lem3  27871  ostth2  27873  crctcshwlkn0lem6  30283  hashecclwwlkn1  30547  umgrhashecclwwlk  30548  clwwlknon  30560  eucrctshift  30723  numclwlk1lem2  30850  nrt2irr  30953  dipcl  31193  dipcn  31201  bcm1n  33266  expgt0b  33287  nexple  33303  2exple2exp  33304  oexpled  33306  wrdpmtrlast  33533  psgnfzto1st  33545  isarchi2  33625  submarchi  33626  znfermltl  33801  fldextrspundgdvdslem  34190  fldextrspundgdvds  34191  fldext2rspun  34192  constrext2chnlem  34260  cos9thpiminplylem2  34293  submateqlem1  34317  madjusmdetlem2  34338  madjusmdetlem4  34340  mdetlap  34342  oddpwdc  34865  eulerpartlemsv2  34869  eulerpartlemsf  34870  eulerpartlems  34871  eulerpartlemv  34875  eulerpartlemb  34879  signsvtn0  35078  fsum2dsub  35115  reprinfz1  35130  reprpmtf1o  35134  circlemeth  35148  circlemethnat  35149  hgt750lemb  35164  hgt750lema  35165  hgt750leme  35166  tgoldbachgtde  35168  tgoldbachgtda  35169  lpadleft  35194  subfacp1lem1  35758  subfacp1lem6  35764  subfaclim  35767  erdszelem8  35777  erdszelem10  35779  cvmliftlem10  35873  faclim2  36327  poimirlem7  38376  poimirlem17  38386  poimirlem18  38387  poimirlem20  38389  poimirlem21  38390  poimirlem22  38391  poimirlem25  38394  poimirlem26  38395  poimirlem27  38396  poimirlem28  38397  poimirlem32  38401  nninfnub  38501  bfplem1  38572  zndvdchrrhm  42839  lcmineqlem1  42895  lcmineqlem2  42896  lcmineqlem8  42902  lcmineqlem10  42904  lcmineqlem11  42905  lcmineqlem15  42909  lcmineqlem16  42910  lcmineqlem18  42912  lcmineqlem19  42913  lcmineqlem20  42914  lcmineqlem21  42915  lcmineqlem22  42916  3lexlogpow2ineq2  42925  dvrelogpow2b  42934  aks4d1p1p2  42936  aks4d1p1p4  42937  aks4d1p1  42942  aks4d1p3  42944  aks4d1p7d1  42948  aks4d1p7  42949  aks4d1p8  42953  aks4d1p9  42954  isprimroot2  42960  primrootsunit1  42963  primrootscoprmpow  42965  posbezout  42966  primrootscoprbij  42968  primrootlekpowne0  42971  primrootspoweq0  42972  aks6d1c1p2  42975  aks6d1c1p3  42976  aks6d1c1p4  42977  aks6d1c1p5  42978  aks6d1c1p7  42979  aks6d1c1p6  42980  aks6d1c1p8  42981  aks6d1c2p2  42985  hashscontpowcl  42986  hashscontpow1  42987  hashscontpow  42988  aks6d1c4  42990  aks6d1c2lem3  42992  aks6d1c2lem4  42993  aks6d1c2  42996  sticksstones6  43017  sticksstones7  43018  sticksstones10  43021  sticksstones12a  43023  sticksstones12  43024  sticksstones20  43032  sticksstones22  43034  aks6d1c6lem2  43037  aks6d1c6lem3  43038  aks6d1c6lem4  43039  aks6d1c6isolem1  43040  aks6d1c6isolem2  43041  aks6d1c6lem5  43043  bcled  43044  bcle2d  43045  aks6d1c7lem1  43046  aks6d1c7  43050  aks5lem2  43053  aks5lem3a  43055  aks5lem5a  43057  grpods  43060  unitscyglem2  43062  unitscyglem4  43064  aks5lem7  43066  aks5  43070  sumcubes  43188  oexpreposd  43197  exp11d  43201  dvdsexpb  43210  fiabv  43418  fsuppind  43436  dffltz  43480  fltdvdsabdvdsc  43484  fltne  43490  flt4lem4  43495  flt4lem7  43505  fltltc  43507  fltnltalem  43508  fltnlta  43509  3rexfrabdioph  43638  4rexfrabdioph  43639  6rexfrabdioph  43640  7rexfrabdioph  43641  irrapxlem5  43667  pellexlem2  43671  pellexlem6  43675  pell14qrgt0  43700  pell1qrge1  43711  pellfundgt1  43724  ltrmxnn0  43790  jm2.26lem3  43842  jm2.27a  43846  jm2.27c  43848  rmxdiophlem  43856  jm3.1lem1  43858  jm3.1lem2  43859  jm3.1lem3  43860  jm3.1  43861  dgrsub2  43976  mpaaeu  43991  idomsubgmo  44034  relexpxpmin  44557  nzprmdif  45143  binomcxplemwb  45172  fperiodmul  46137  xralrple4  46202  fsumnncl  46402  dvsinexp  46739  dvxpaek  46768  itgsinexplem1  46782  stoweidlem1  46829  stoweidlem17  46845  stoweidlem25  46853  stoweidlem34  46862  stoweidlem38  46866  stoweidlem40  46868  stoweidlem42  46870  stoweidlem45  46873  stirlinglem4  46905  stirlinglem5  46906  stirlinglem10  46911  stirlinglem13  46914  dirkertrigeq  46929  fourierdlem21  46956  fourierdlem25  46960  fourierdlem48  46982  fourierdlem54  46988  fourierdlem64  46998  fourierdlem65  46999  fourierdlem73  47007  fourierdlem81  47015  fourierdlem83  47017  fourierdlem92  47026  fourierdlem103  47037  fourierdlem104  47038  fourierdlem112  47046  fourierdlem113  47047  etransclem1  47063  etransclem4  47066  etransclem8  47070  etransclem15  47077  etransclem17  47079  etransclem18  47080  etransclem19  47081  etransclem20  47082  etransclem21  47083  etransclem22  47084  etransclem23  47085  etransclem24  47086  etransclem25  47087  etransclem27  47089  etransclem32  47094  etransclem35  47097  etransclem41  47103  etransclem44  47106  etransclem46  47108  modmknepk  48256  iccpartigtl  48323  iccpartgt  48327  iccpartgel  48329  iccelpart  48333  odz2prm2pw  48466  fmtnoprmfac1  48468  fmtnoprmfac2  48470  2pwp1prm  48492  sfprmdvdsmersenne  48506  lighneallem4a  48511  proththdlem  48516  proththd  48517  perfectALTVlem1  48637  perfectALTVlem2  48638  perfectALTV  48639  fpprwpprb  48656  gpgedgvtx1  48978  logbpw2m1  49497  nnpw2blenfzo  49511  nnolog2flm1  49520  dignn0fr  49531  nn0sumshdiglemA  49549  nn0sumshdiglemB  49550