Theorem nnnn0d 12707

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  ℕcn 12375  ℕ₀cn0 12646

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-un 4154  df-n0 12647

This theorem is used by:  nn0ge2m1nn0  12717  nnzd  12759  eluzge2nn0  13059  expgt1  14283  expaddzlem  14288  expaddz  14289  expmulz  14291  expmulnbnd  14420  exp11nnd  14446  facwordi  14474  faclbnd  14475  facavg  14486  bcm1k  14500  wrdeqs1cat  14911  cshwcsh2id  15021  relexpsucnnr  15221  isercolllem2  15877  bcxmas  16048  climcndslem1  16062  climcndslem2  16063  climcnds  16064  pwdif  16081  geo2sum  16086  mertenslem1  16097  prodmolem3  16144  prodmolem2a  16145  bpolydiflem  16264  eftabs  16285  efcllem  16287  eftlub  16321  eirrlem  16416  rpnnen2lem9  16434  rpnnen2lem11  16436  dvdsfac  16540  pwp1fsum  16605  oddpwp1fsum  16606  bitsfzo  16649  bitsfi  16651  sadcaddlem  16671  smumullem  16706  gcdcl  16720  dvdsgcdidd  16754  mulgcd  16765  rplpwr  16776  rprpwr  16777  rppwr  16778  nn0rppwr  16779  expgcd  16781  lcmcl  16820  lcmgcdnn  16830  lcmfcl  16847  nprmdvds1  16926  rpexp  16942  prmdvdsbc  16946  zsqrtelqelz  16978  phiprmpw  16997  eulerthlem2  17003  eulerth  17004  fermltl  17005  odzcllem  17014  odzdvds  17017  odzphi  17018  prm23lt5  17036  pythagtriplem6  17043  pythagtriplem7  17044  pcprmpw2  17104  dvdsprmpweqle  17108  pcprod  17117  pcfac  17121  pcbc  17122  expnprm  17124  pockthlem  17127  pockthg  17128  prmunb  17136  prmreclem2  17139  prmreclem3  17140  prmreclem4  17141  prmreclem5  17142  prmreclem6  17143  mul4sqlem  17175  4sqlem11  17177  4sqlem17  17183  vdwlem1  17203  vdwlem5  17207  vdwlem6  17208  vdwlem8  17210  vdwlem9  17211  vdwlem11  17213  vdwlem12  17214  vdwnnlem3  17219  ramz2  17246  ramub1lem1  17248  ramub1lem2  17249  ramub1  17250  prmgaplem3  17275  2expltfac  17314  psgnunilem3  19761  odfval  19797  mndodconglem  19806  gexcl3  19852  pgpfi1  19860  sylow1lem1  19863  gexexlem  20117  prmcyg  20159  gsumval3  20172  ablfacrplem  20332  ablfacrp  20333  ablfacrp2  20334  ablfac1eu  20340  prmgrpsimpgd  20381  srgbinomlem3  20505  srgbinomlem4  20506  fermltlchr  21890  freshmansdream  21935  chfacfscmulgsum  23233  chfacfpmmulgsum  23237  cpmadugsumlemF  23249  ovoliunlem1  25878  mbfi1fseqlem1  26091  mbfi1fseqlem3  26093  mbfi1fseqlem5  26095  itg2cnlem2  26138  plyn0mulidp  26657  dvply1  26660  aalioulem2  26717  aalioulem5  26720  aaliou3lem1  26726  aaliou3lem2  26727  aaliou3lem8  26729  aaliou3lem6  26732  taylthlem1  26757  taylthlem2  26758  pserdvlem2  26812  cxpeq  27142  zrtelqelz  27143  dmgmdivn0  27412  lgamgulmlem5  27417  lgamcvg2  27439  wilthlem1  27452  ftalem1  27457  ftalem2  27458  ftalem4  27460  ftalem5  27461  basellem2  27466  basellem3  27467  basellem4  27468  basellem5  27469  isppw2  27499  mpodvdsmulf1o  27578  dvdsmulf1o  27580  sgmmul  27585  fsumvma2  27598  chpchtsum  27603  logfacubnd  27605  mersenne  27611  perfect1  27612  perfectlem1  27613  perfectlem2  27614  perfect  27615  dchrelbas3  27622  dchrelbasd  27623  dchrzrh1  27628  dchrzrhmul  27630  dchrmulcl  27633  dchrn0  27634  dchrfi  27639  dchrghm  27640  dchrabs  27644  dchrinv  27645  dchrptlem1  27648  dchrptlem2  27649  dchrptlem3  27650  dchrpt  27651  dchrsum2  27652  sum2dchr  27658  pcbcctr  27660  bcmono  27661  bclbnd  27664  bposlem1  27668  bposlem3  27670  bposlem5  27672  bposlem6  27673  lgslem1  27681  lgsval2lem  27691  lgsvalmod  27700  lgsmod  27707  lgsdirprm  27715  lgsne0  27719  lgsqrlem1  27730  lgsqrlem2  27731  lgsqrlem3  27732  lgsqrlem4  27733  gausslemma2dlem0b  27741  gausslemma2dlem0c  27742  gausslemma2dlem1  27750  gausslemma2dlem7  27757  gausslemma2d  27758  lgseisenlem1  27759  lgseisenlem2  27760  lgseisenlem3  27761  lgseisenlem4  27762  lgseisen  27763  lgsquadlem2  27765  lgsquadlem3  27766  m1lgs  27772  2lgslem1a  27775  2sqlem3  27804  2sqblem  27815  chebbnd1lem1  27853  chebbnd1lem3  27855  rplogsumlem2  27869  rpvmasumlem  27871  dchrisumlem1  27873  dchrisumlem2  27874  dchrmusum2  27878  dchrvmasumlem3  27883  dchrisum0ff  27891  dchrisum0flblem1  27892  rpvmasum2  27896  dchrisum0re  27897  dchrisum0lem2a  27901  dirith  27913  mudivsum  27914  pntpbnd1a  27969  pntlemq  27985  pntlemr  27986  pntlemj  27987  ostth2lem1  28002  ostth2lem2  28018  ostth2lem3  28019  ostth2  28021  fltdvdsabdvdsc  28027  fltne  28032  flt4lem4  28036  flt4lem7  28046  fltoprm  28052  crctcshwlkn0lem6  30461  hashecclwwlkn1  30725  umgrhashecclwwlk  30726  clwwlknon  30738  eucrctshift  30901  numclwlk1lem2  31028  nrt2irr  31131  dipcl  31371  dipcn  31379  bcm1n  33483  expgt0b  33504  nexple  33520  2exple2exp  33521  oexpled  33523  wrdpmtrlast  33753  psgnfzto1st  33765  isarchi2  33845  submarchi  33846  znfermltl  34026  fldextrspundgdvdslem  34423  fldextrspundgdvds  34424  fldext2rspun  34425  constrext2chnlem  34493  cos9thpiminplylem2  34526  submateqlem1  34550  madjusmdetlem2  34571  madjusmdetlem4  34573  mdetlap  34575  oddpwdc  35097  eulerpartlemsv2  35101  eulerpartlemsf  35102  eulerpartlems  35103  eulerpartlemv  35107  eulerpartlemb  35111  signsvtn0  35310  fsum2dsub  35347  reprinfz1  35362  reprpmtf1o  35366  circlemeth  35380  circlemethnat  35381  hgt750lemb  35396  hgt750lema  35397  hgt750leme  35398  tgoldbachgtde  35400  tgoldbachgtda  35401  lpadleft  35426  subfacp1lem1  36152  subfacp1lem6  36158  subfaclim  36161  erdszelem8  36171  erdszelem10  36173  cvmliftlem10  36267  faclim2  36728  poimirlem7  38813  poimirlem17  38823  poimirlem18  38824  poimirlem20  38826  poimirlem21  38827  poimirlem22  38828  poimirlem25  38831  poimirlem26  38832  poimirlem27  38833  poimirlem28  38834  poimirlem32  38838  nninfnub  38951  bfplem1  39022  zndvdchrrhm  43289  lcmineqlem1  43345  lcmineqlem2  43346  lcmineqlem8  43352  lcmineqlem10  43354  lcmineqlem11  43355  lcmineqlem15  43359  lcmineqlem16  43360  lcmineqlem18  43362  lcmineqlem19  43363  lcmineqlem20  43364  lcmineqlem21  43365  lcmineqlem22  43366  3lexlogpow2ineq2  43375  dvrelogpow2b  43384  aks4d1p1p2  43386  aks4d1p1p4  43387  aks4d1p1  43392  aks4d1p3  43394  aks4d1p7d1  43398  aks4d1p7  43399  aks4d1p8  43403  aks4d1p9  43404  isprimroot2  43410  primrootsunit1  43413  primrootscoprmpow  43415  posbezout  43416  primrootscoprbij  43418  primrootlekpowne0  43421  primrootspoweq0  43422  aks6d1c1p2  43425  aks6d1c1p3  43426  aks6d1c1p4  43427  aks6d1c1p5  43428  aks6d1c1p7  43429  aks6d1c1p6  43430  aks6d1c1p8  43431  aks6d1c2p2  43435  hashscontpowcl  43436  hashscontpow1  43437  hashscontpow  43438  aks6d1c4  43440  aks6d1c2lem3  43442  aks6d1c2lem4  43443  aks6d1c2  43446  sticksstones6  43467  sticksstones7  43468  sticksstones10  43471  sticksstones12a  43473  sticksstones12  43474  sticksstones20  43482  sticksstones22  43484  aks6d1c6lem2  43487  aks6d1c6lem3  43488  aks6d1c6lem4  43489  aks6d1c6isolem1  43490  aks6d1c6isolem2  43491  aks6d1c6lem5  43493  bcled  43494  bcle2d  43495  aks6d1c7lem1  43496  aks6d1c7  43500  aks5lem2  43503  aks5lem3a  43505  aks5lem5a  43507  grpods  43510  unitscyglem2  43512  unitscyglem4  43514  aks5lem7  43516  aks5  43520  sumcubes  43636  oexpreposd  43645  exp11d  43649  dvdsexpb  43653  fiabv  43866  fsuppind  43884  dffltz  43936  fltltc  43938  fltnltalem  43939  fltnlta  43940  3rexfrabdioph  44070  4rexfrabdioph  44071  6rexfrabdioph  44072  7rexfrabdioph  44073  irrapxlem5  44099  pellexlem2  44103  pellexlem6  44107  pell14qrgt0  44132  pell1qrge1  44143  pellfundgt1  44156  ltrmxnn0  44222  jm2.26lem3  44274  jm2.27a  44278  jm2.27c  44280  rmxdiophlem  44288  jm3.1lem1  44290  jm3.1lem2  44291  jm3.1lem3  44292  jm3.1  44293  dgrsub2  44402  mpaaeu  44417  idomsubgmo  44456  relexpxpmin  44978  nzprmdif  45564  binomcxplemwb  45593  fperiodmul  46593  xralrple4  46657  fsumnncl  46857  dvsinexp  47194  dvxpaek  47223  itgsinexplem1  47237  stoweidlem1  47284  stoweidlem17  47300  stoweidlem25  47308  stoweidlem34  47317  stoweidlem38  47321  stoweidlem40  47323  stoweidlem42  47325  stoweidlem45  47328  stirlinglem4  47360  stirlinglem5  47361  stirlinglem10  47366  stirlinglem13  47369  dirkertrigeq  47384  fourierdlem21  47411  fourierdlem25  47415  fourierdlem48  47437  fourierdlem54  47443  fourierdlem64  47453  fourierdlem65  47454  fourierdlem73  47462  fourierdlem81  47470  fourierdlem83  47472  fourierdlem92  47481  fourierdlem103  47492  fourierdlem104  47493  fourierdlem112  47501  fourierdlem113  47502  etransclem1  47518  etransclem4  47521  etransclem8  47525  etransclem15  47532  etransclem17  47534  etransclem18  47535  etransclem19  47536  etransclem20  47537  etransclem21  47538  etransclem22  47539  etransclem23  47540  etransclem24  47541  etransclem25  47542  etransclem27  47544  etransclem32  47549  etransclem35  47552  etransclem41  47558  etransclem44  47561  etransclem46  47563  modmknepk  48711  iccpartigtl  48778  iccpartgt  48782  iccpartgel  48784  iccelpart  48788  odz2prm2pw  48921  fmtnoprmfac1  48923  fmtnoprmfac2  48925  2pwp1prm  48947  sfprmdvdsmersenne  48961  lighneallem4a  48966  proththdlem  48971  proththd  48972  perfectALTVlem1  49092  perfectALTVlem2  49093  perfectALTV  49094  fpprwpprb  49111  gpgedgvtx1  49433  logbpw2m1  50010  nnpw2blenfzo  50024  nnolog2flm1  50033  dignn0fr  50044  nn0sumshdiglemA  50062  nn0sumshdiglemB  50063