Theorem nnnn0d 12489

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℕcn 12165  ℕ₀cn0 12428

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 2709

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 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-un 3895  df-ss 3907  df-n0 12429

This theorem is referenced by:  nn0ge2m1nn0  12499  nnzd  12541  eluzge2nn0  12833  expgt1  14053  expaddzlem  14058  expaddz  14059  expmulz  14061  expmulnbnd  14188  exp11nnd  14214  facwordi  14242  faclbnd  14243  facavg  14254  bcm1k  14268  wrdeqs1cat  14673  cshwcsh2id  14781  relexpsucnnr  14978  isercolllem2  15619  bcxmas  15791  climcndslem1  15805  climcndslem2  15806  climcnds  15807  pwdif  15824  geo2sum  15829  mertenslem1  15840  prodmolem3  15889  prodmolem2a  15890  bpolydiflem  16010  eftabs  16031  efcllem  16033  eftlub  16067  eirrlem  16162  rpnnen2lem9  16180  rpnnen2lem11  16182  dvdsfac  16286  pwp1fsum  16351  oddpwp1fsum  16352  bitsfzo  16395  bitsfi  16397  sadcaddlem  16417  smumullem  16452  gcdcl  16466  dvdsgcdidd  16497  mulgcd  16508  rplpwr  16518  rprpwr  16519  rppwr  16520  nn0rppwr  16521  expgcd  16523  lcmcl  16561  lcmgcdnn  16571  lcmfcl  16588  nprmdvds1  16667  rpexp  16683  prmdvdsbc  16687  zsqrtelqelz  16719  phiprmpw  16737  eulerthlem2  16743  eulerth  16744  fermltl  16745  odzcllem  16754  odzdvds  16757  odzphi  16758  prm23lt5  16776  pythagtriplem6  16783  pythagtriplem7  16784  pcprmpw2  16844  dvdsprmpweqle  16848  pcprod  16857  pcfac  16861  pcbc  16862  expnprm  16864  pockthlem  16867  pockthg  16868  prmunb  16876  prmreclem2  16879  prmreclem3  16880  prmreclem4  16881  prmreclem5  16882  prmreclem6  16883  mul4sqlem  16915  4sqlem11  16917  4sqlem17  16923  vdwlem1  16943  vdwlem5  16947  vdwlem6  16948  vdwlem8  16950  vdwlem9  16951  vdwlem11  16953  vdwlem12  16954  vdwnnlem3  16959  ramz2  16986  ramub1lem1  16988  ramub1lem2  16989  ramub1  16990  prmgaplem3  17015  2expltfac  17054  psgnunilem3  19462  odfval  19498  mndodconglem  19507  gexcl3  19553  pgpfi1  19561  sylow1lem1  19564  gexexlem  19818  prmcyg  19860  gsumval3  19873  ablfacrplem  20033  ablfacrp  20034  ablfacrp2  20035  ablfac1eu  20041  prmgrpsimpgd  20082  srgbinomlem3  20200  srgbinomlem4  20201  fermltlchr  21519  freshmansdream  21564  chfacfscmulgsum  22835  chfacfpmmulgsum  22839  cpmadugsumlemF  22851  ovoliunlem1  25479  mbfi1fseqlem1  25692  mbfi1fseqlem3  25694  mbfi1fseqlem5  25696  itg2cnlem2  25739  dvply1  26260  aalioulem2  26310  aalioulem5  26313  aaliou3lem1  26319  aaliou3lem2  26320  aaliou3lem8  26322  aaliou3lem6  26325  taylthlem1  26350  taylthlem2  26351  taylthlem2OLD  26352  pserdvlem2  26406  cxpeq  26734  zrtelqelz  26735  dmgmdivn0  27005  lgamgulmlem5  27010  lgamcvg2  27032  wilthlem1  27045  ftalem1  27050  ftalem2  27051  ftalem4  27053  ftalem5  27054  basellem2  27059  basellem3  27060  basellem4  27061  basellem5  27062  isppw2  27092  mpodvdsmulf1o  27171  dvdsmulf1o  27173  sgmmul  27178  fsumvma2  27191  chpchtsum  27196  logfacubnd  27198  mersenne  27204  perfect1  27205  perfectlem1  27206  perfectlem2  27207  perfect  27208  dchrelbas3  27215  dchrelbasd  27216  dchrzrh1  27221  dchrzrhmul  27223  dchrmulcl  27226  dchrn0  27227  dchrfi  27232  dchrghm  27233  dchrabs  27237  dchrinv  27238  dchrptlem1  27241  dchrptlem2  27242  dchrptlem3  27243  dchrpt  27244  dchrsum2  27245  sum2dchr  27251  pcbcctr  27253  bcmono  27254  bclbnd  27257  bposlem1  27261  bposlem3  27263  bposlem5  27265  bposlem6  27266  lgslem1  27274  lgsval2lem  27284  lgsvalmod  27293  lgsmod  27300  lgsdirprm  27308  lgsne0  27312  lgsqrlem1  27323  lgsqrlem2  27324  lgsqrlem3  27325  lgsqrlem4  27326  gausslemma2dlem0b  27334  gausslemma2dlem0c  27335  gausslemma2dlem1  27343  gausslemma2dlem7  27350  gausslemma2d  27351  lgseisenlem1  27352  lgseisenlem2  27353  lgseisenlem3  27354  lgseisenlem4  27355  lgseisen  27356  lgsquadlem2  27358  lgsquadlem3  27359  m1lgs  27365  2lgslem1a  27368  2sqlem3  27397  2sqblem  27408  chebbnd1lem1  27446  chebbnd1lem3  27448  rplogsumlem2  27462  rpvmasumlem  27464  dchrisumlem1  27466  dchrisumlem2  27467  dchrmusum2  27471  dchrvmasumlem3  27476  dchrisum0ff  27484  dchrisum0flblem1  27485  rpvmasum2  27489  dchrisum0re  27490  dchrisum0lem2a  27494  dirith  27506  mudivsum  27507  pntpbnd1a  27562  pntlemq  27578  pntlemr  27579  pntlemj  27580  ostth2lem1  27595  ostth2lem2  27611  ostth2lem3  27612  ostth2  27614  crctcshwlkn0lem6  29898  hashecclwwlkn1  30162  umgrhashecclwwlk  30163  clwwlknon  30175  eucrctshift  30328  numclwlk1lem2  30455  nrt2irr  30558  dipcl  30798  dipcn  30806  bcm1n  32883  expgt0b  32905  nexple  32932  2exple2exp  32933  oexpled  32935  wrdpmtrlast  33169  psgnfzto1st  33181  isarchi2  33261  submarchi  33262  znfermltl  33441  fldextrspundgdvdslem  33840  fldextrspundgdvds  33841  fldext2rspun  33842  constrext2chnlem  33910  cos9thpiminplylem2  33943  submateqlem1  33967  madjusmdetlem2  33988  madjusmdetlem4  33990  mdetlap  33992  oddpwdc  34514  eulerpartlemsv2  34518  eulerpartlemsf  34519  eulerpartlems  34520  eulerpartlemv  34524  eulerpartlemb  34528  plymulx0  34707  signsvtn0  34730  fsum2dsub  34767  reprinfz1  34782  reprpmtf1o  34786  circlemeth  34800  circlemethnat  34801  hgt750lemb  34816  hgt750lema  34817  hgt750leme  34818  tgoldbachgtde  34820  tgoldbachgtda  34821  lpadleft  34843  subfacp1lem1  35377  subfacp1lem6  35383  subfaclim  35386  erdszelem8  35396  erdszelem10  35398  cvmliftlem10  35492  faclim2  35946  poimirlem7  37962  poimirlem17  37972  poimirlem18  37973  poimirlem20  37975  poimirlem21  37976  poimirlem22  37977  poimirlem25  37980  poimirlem26  37981  poimirlem27  37982  poimirlem28  37983  poimirlem32  37987  nninfnub  38086  bfplem1  38157  zndvdchrrhm  42426  lcmineqlem1  42482  lcmineqlem2  42483  lcmineqlem8  42489  lcmineqlem10  42491  lcmineqlem11  42492  lcmineqlem15  42496  lcmineqlem16  42497  lcmineqlem18  42499  lcmineqlem19  42500  lcmineqlem20  42501  lcmineqlem21  42502  lcmineqlem22  42503  3lexlogpow2ineq2  42512  dvrelogpow2b  42521  aks4d1p1p2  42523  aks4d1p1p4  42524  aks4d1p1  42529  aks4d1p3  42531  aks4d1p7d1  42535  aks4d1p7  42536  aks4d1p8  42540  aks4d1p9  42541  isprimroot2  42547  primrootsunit1  42550  primrootscoprmpow  42552  posbezout  42553  primrootscoprbij  42555  primrootlekpowne0  42558  primrootspoweq0  42559  aks6d1c1p2  42562  aks6d1c1p3  42563  aks6d1c1p4  42564  aks6d1c1p5  42565  aks6d1c1p7  42566  aks6d1c1p6  42567  aks6d1c1p8  42568  aks6d1c2p2  42572  hashscontpowcl  42573  hashscontpow1  42574  hashscontpow  42575  aks6d1c4  42577  aks6d1c2lem3  42579  aks6d1c2lem4  42580  aks6d1c2  42583  sticksstones6  42604  sticksstones7  42605  sticksstones10  42608  sticksstones12a  42610  sticksstones12  42611  sticksstones20  42619  sticksstones22  42621  aks6d1c6lem2  42624  aks6d1c6lem3  42625  aks6d1c6lem4  42626  aks6d1c6isolem1  42627  aks6d1c6isolem2  42628  aks6d1c6lem5  42630  bcled  42631  bcle2d  42632  aks6d1c7lem1  42633  aks6d1c7  42637  aks5lem2  42640  aks5lem3a  42642  aks5lem5a  42644  grpods  42647  unitscyglem2  42649  unitscyglem4  42651  aks5lem7  42653  aks5  42657  sumcubes  42759  oexpreposd  42768  exp11d  42772  dvdsexpb  42781  fiabv  42995  fsuppind  43037  dffltz  43081  fltdvdsabdvdsc  43085  fltne  43091  flt4lem4  43096  flt4lem7  43106  fltltc  43108  fltnltalem  43109  fltnlta  43110  3rexfrabdioph  43243  4rexfrabdioph  43244  6rexfrabdioph  43245  7rexfrabdioph  43246  irrapxlem5  43272  pellexlem2  43276  pellexlem6  43280  pell14qrgt0  43305  pell1qrge1  43316  pellfundgt1  43329  ltrmxnn0  43395  jm2.26lem3  43447  jm2.27a  43451  jm2.27c  43453  rmxdiophlem  43461  jm3.1lem1  43463  jm3.1lem2  43464  jm3.1lem3  43465  jm3.1  43466  dgrsub2  43581  mpaaeu  43596  idomsubgmo  43639  relexpxpmin  44162  nzprmdif  44764  binomcxplemwb  44793  fperiodmul  45755  xralrple4  45820  fsumnncl  46020  dvsinexp  46357  dvxpaek  46386  itgsinexplem1  46400  stoweidlem1  46447  stoweidlem17  46463  stoweidlem25  46471  stoweidlem34  46480  stoweidlem38  46484  stoweidlem40  46486  stoweidlem42  46488  stoweidlem45  46491  stirlinglem4  46523  stirlinglem5  46524  stirlinglem10  46529  stirlinglem13  46532  dirkertrigeq  46547  fourierdlem21  46574  fourierdlem25  46578  fourierdlem48  46600  fourierdlem54  46606  fourierdlem64  46616  fourierdlem65  46617  fourierdlem73  46625  fourierdlem81  46633  fourierdlem83  46635  fourierdlem92  46644  fourierdlem103  46655  fourierdlem104  46656  fourierdlem112  46664  fourierdlem113  46665  etransclem1  46681  etransclem4  46684  etransclem8  46688  etransclem15  46695  etransclem17  46697  etransclem18  46698  etransclem19  46699  etransclem20  46700  etransclem21  46701  etransclem22  46702  etransclem23  46703  etransclem24  46704  etransclem25  46705  etransclem27  46707  etransclem32  46712  etransclem35  46715  etransclem41  46721  etransclem44  46724  etransclem46  46726  modmknepk  47828  iccpartigtl  47895  iccpartgt  47899  iccpartgel  47901  iccelpart  47905  odz2prm2pw  48038  fmtnoprmfac1  48040  fmtnoprmfac2  48042  2pwp1prm  48064  sfprmdvdsmersenne  48078  lighneallem4a  48083  proththdlem  48088  proththd  48089  perfectALTVlem1  48209  perfectALTVlem2  48210  perfectALTV  48211  fpprwpprb  48228  gpgedgvtx1  48550  logbpw2m1  49055  nnpw2blenfzo  49069  nnolog2flm1  49078  dignn0fr  49089  nn0sumshdiglemA  49107  nn0sumshdiglemB  49108