Theorem nnnn0d 12510

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℕcn 12193  ℕ₀cn0 12449

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3922  df-ss 3934  df-n0 12450

This theorem is referenced by:  nn0ge2m1nn0  12520  nnzd  12563  eluzge2nn0  12858  expgt1  14072  expaddzlem  14077  expaddz  14078  expmulz  14080  expmulnbnd  14207  exp11nnd  14233  facwordi  14261  faclbnd  14262  facavg  14273  bcm1k  14287  wrdeqs1cat  14692  cshwcsh2id  14801  relexpsucnnr  14998  isercolllem2  15639  bcxmas  15808  climcndslem1  15822  climcndslem2  15823  climcnds  15824  pwdif  15841  geo2sum  15846  mertenslem1  15857  prodmolem3  15906  prodmolem2a  15907  bpolydiflem  16027  eftabs  16048  efcllem  16050  eftlub  16084  eirrlem  16179  rpnnen2lem9  16197  rpnnen2lem11  16199  dvdsfac  16303  pwp1fsum  16368  oddpwp1fsum  16369  bitsfzo  16412  bitsfi  16414  sadcaddlem  16434  smumullem  16469  gcdcl  16483  dvdsgcdidd  16514  mulgcd  16525  rplpwr  16535  rprpwr  16536  rppwr  16537  nn0rppwr  16538  expgcd  16540  lcmcl  16578  lcmgcdnn  16588  lcmfcl  16605  nprmdvds1  16683  rpexp  16699  prmdvdsbc  16703  zsqrtelqelz  16735  phiprmpw  16753  eulerthlem2  16759  eulerth  16760  fermltl  16761  odzcllem  16770  odzdvds  16773  odzphi  16774  prm23lt5  16792  pythagtriplem6  16799  pythagtriplem7  16800  pcprmpw2  16860  dvdsprmpweqle  16864  pcprod  16873  pcfac  16877  pcbc  16878  expnprm  16880  pockthlem  16883  pockthg  16884  prmunb  16892  prmreclem2  16895  prmreclem3  16896  prmreclem4  16897  prmreclem5  16898  prmreclem6  16899  mul4sqlem  16931  4sqlem11  16933  4sqlem17  16939  vdwlem1  16959  vdwlem5  16963  vdwlem6  16964  vdwlem8  16966  vdwlem9  16967  vdwlem11  16969  vdwlem12  16970  vdwnnlem3  16975  ramz2  17002  ramub1lem1  17004  ramub1lem2  17005  ramub1  17006  prmgaplem3  17031  2expltfac  17070  psgnunilem3  19433  odfval  19469  mndodconglem  19478  gexcl3  19524  pgpfi1  19532  sylow1lem1  19535  gexexlem  19789  prmcyg  19831  gsumval3  19844  ablfacrplem  20004  ablfacrp  20005  ablfacrp2  20006  ablfac1eu  20012  prmgrpsimpgd  20053  srgbinomlem3  20144  srgbinomlem4  20145  fermltlchr  21446  freshmansdream  21491  chfacfscmulgsum  22754  chfacfpmmulgsum  22758  cpmadugsumlemF  22770  ovoliunlem1  25410  mbfi1fseqlem1  25623  mbfi1fseqlem3  25625  mbfi1fseqlem5  25627  itg2cnlem2  25670  dvply1  26198  aalioulem2  26248  aalioulem5  26251  aaliou3lem1  26257  aaliou3lem2  26258  aaliou3lem8  26260  aaliou3lem6  26263  taylthlem1  26288  taylthlem2  26289  taylthlem2OLD  26290  pserdvlem2  26345  cxpeq  26674  zrtelqelz  26675  dmgmdivn0  26945  lgamgulmlem5  26950  lgamcvg2  26972  wilthlem1  26985  ftalem1  26990  ftalem2  26991  ftalem4  26993  ftalem5  26994  basellem2  26999  basellem3  27000  basellem4  27001  basellem5  27002  isppw2  27032  mpodvdsmulf1o  27111  dvdsmulf1o  27113  sgmmul  27119  fsumvma2  27132  chpchtsum  27137  logfacubnd  27139  mersenne  27145  perfect1  27146  perfectlem1  27147  perfectlem2  27148  perfect  27149  dchrelbas3  27156  dchrelbasd  27157  dchrzrh1  27162  dchrzrhmul  27164  dchrmulcl  27167  dchrn0  27168  dchrfi  27173  dchrghm  27174  dchrabs  27178  dchrinv  27179  dchrptlem1  27182  dchrptlem2  27183  dchrptlem3  27184  dchrpt  27185  dchrsum2  27186  sum2dchr  27192  pcbcctr  27194  bcmono  27195  bclbnd  27198  bposlem1  27202  bposlem3  27204  bposlem5  27206  bposlem6  27207  lgslem1  27215  lgsval2lem  27225  lgsvalmod  27234  lgsmod  27241  lgsdirprm  27249  lgsne0  27253  lgsqrlem1  27264  lgsqrlem2  27265  lgsqrlem3  27266  lgsqrlem4  27267  gausslemma2dlem0b  27275  gausslemma2dlem0c  27276  gausslemma2dlem1  27284  gausslemma2dlem7  27291  gausslemma2d  27292  lgseisenlem1  27293  lgseisenlem2  27294  lgseisenlem3  27295  lgseisenlem4  27296  lgseisen  27297  lgsquadlem2  27299  lgsquadlem3  27300  m1lgs  27306  2lgslem1a  27309  2sqlem3  27338  2sqblem  27349  chebbnd1lem1  27387  chebbnd1lem3  27389  rplogsumlem2  27403  rpvmasumlem  27405  dchrisumlem1  27407  dchrisumlem2  27408  dchrmusum2  27412  dchrvmasumlem3  27417  dchrisum0ff  27425  dchrisum0flblem1  27426  rpvmasum2  27430  dchrisum0re  27431  dchrisum0lem2a  27435  dirith  27447  mudivsum  27448  pntpbnd1a  27503  pntlemq  27519  pntlemr  27520  pntlemj  27521  ostth2lem1  27536  ostth2lem2  27552  ostth2lem3  27553  ostth2  27555  crctcshwlkn0lem6  29752  hashecclwwlkn1  30013  umgrhashecclwwlk  30014  clwwlknon  30026  eucrctshift  30179  numclwlk1lem2  30306  nrt2irr  30409  dipcl  30648  dipcn  30656  bcm1n  32725  expgt0b  32748  nexple  32776  2exple2exp  32777  oexpled  32779  wrdpmtrlast  33057  psgnfzto1st  33069  isarchi2  33146  submarchi  33147  znfermltl  33344  fldextrspundgdvdslem  33682  fldextrspundgdvds  33683  fldext2rspun  33684  constrext2chnlem  33747  cos9thpiminplylem2  33780  submateqlem1  33804  madjusmdetlem2  33825  madjusmdetlem4  33827  mdetlap  33829  oddpwdc  34352  eulerpartlemsv2  34356  eulerpartlemsf  34357  eulerpartlems  34358  eulerpartlemv  34362  eulerpartlemb  34366  plymulx0  34545  signsvtn0  34568  fsum2dsub  34605  reprinfz1  34620  reprpmtf1o  34624  circlemeth  34638  circlemethnat  34639  hgt750lemb  34654  hgt750lema  34655  hgt750leme  34656  tgoldbachgtde  34658  tgoldbachgtda  34659  lpadleft  34681  subfacp1lem1  35173  subfacp1lem6  35179  subfaclim  35182  erdszelem8  35192  erdszelem10  35194  cvmliftlem10  35288  faclim2  35742  poimirlem7  37628  poimirlem17  37638  poimirlem18  37639  poimirlem20  37641  poimirlem21  37642  poimirlem22  37643  poimirlem25  37646  poimirlem26  37647  poimirlem27  37648  poimirlem28  37649  poimirlem32  37653  nninfnub  37752  bfplem1  37823  zndvdchrrhm  41967  lcmineqlem1  42024  lcmineqlem2  42025  lcmineqlem8  42031  lcmineqlem10  42033  lcmineqlem11  42034  lcmineqlem15  42038  lcmineqlem16  42039  lcmineqlem18  42041  lcmineqlem19  42042  lcmineqlem20  42043  lcmineqlem21  42044  lcmineqlem22  42045  3lexlogpow2ineq2  42054  dvrelogpow2b  42063  aks4d1p1p2  42065  aks4d1p1p4  42066  aks4d1p1  42071  aks4d1p3  42073  aks4d1p7d1  42077  aks4d1p7  42078  aks4d1p8  42082  aks4d1p9  42083  isprimroot2  42089  primrootsunit1  42092  primrootscoprmpow  42094  posbezout  42095  primrootscoprbij  42097  primrootlekpowne0  42100  primrootspoweq0  42101  aks6d1c1p2  42104  aks6d1c1p3  42105  aks6d1c1p4  42106  aks6d1c1p5  42107  aks6d1c1p7  42108  aks6d1c1p6  42109  aks6d1c1p8  42110  aks6d1c2p2  42114  hashscontpowcl  42115  hashscontpow1  42116  hashscontpow  42117  aks6d1c4  42119  aks6d1c2lem3  42121  aks6d1c2lem4  42122  aks6d1c2  42125  sticksstones6  42146  sticksstones7  42147  sticksstones10  42150  sticksstones12a  42152  sticksstones12  42153  sticksstones20  42161  sticksstones22  42163  aks6d1c6lem2  42166  aks6d1c6lem3  42167  aks6d1c6lem4  42168  aks6d1c6isolem1  42169  aks6d1c6isolem2  42170  aks6d1c6lem5  42172  bcled  42173  bcle2d  42174  aks6d1c7lem1  42175  aks6d1c7  42179  aks5lem2  42182  aks5lem3a  42184  aks5lem5a  42186  grpods  42189  unitscyglem2  42191  unitscyglem4  42193  aks5lem7  42195  aks5  42199  sumcubes  42308  oexpreposd  42317  exp11d  42321  dvdsexpb  42330  fiabv  42531  fsuppind  42585  dffltz  42629  fltdvdsabdvdsc  42633  fltne  42639  flt4lem4  42644  flt4lem7  42654  fltltc  42656  fltnltalem  42657  fltnlta  42658  3rexfrabdioph  42792  4rexfrabdioph  42793  6rexfrabdioph  42794  7rexfrabdioph  42795  irrapxlem5  42821  pellexlem2  42825  pellexlem6  42829  pell14qrgt0  42854  pell1qrge1  42865  pellfundgt1  42878  ltrmxnn0  42945  jm2.26lem3  42997  jm2.27a  43001  jm2.27c  43003  rmxdiophlem  43011  jm3.1lem1  43013  jm3.1lem2  43014  jm3.1lem3  43015  jm3.1  43016  dgrsub2  43131  mpaaeu  43146  idomsubgmo  43189  relexpxpmin  43713  nzprmdif  44315  binomcxplemwb  44344  fperiodmul  45309  xralrple4  45376  fsumnncl  45577  dvsinexp  45916  dvxpaek  45945  itgsinexplem1  45959  stoweidlem1  46006  stoweidlem17  46022  stoweidlem25  46030  stoweidlem34  46039  stoweidlem38  46043  stoweidlem40  46045  stoweidlem42  46047  stoweidlem45  46050  stirlinglem4  46082  stirlinglem5  46083  stirlinglem10  46088  stirlinglem13  46091  dirkertrigeq  46106  fourierdlem21  46133  fourierdlem25  46137  fourierdlem48  46159  fourierdlem54  46165  fourierdlem64  46175  fourierdlem65  46176  fourierdlem73  46184  fourierdlem81  46192  fourierdlem83  46194  fourierdlem92  46203  fourierdlem103  46214  fourierdlem104  46215  fourierdlem112  46223  fourierdlem113  46224  etransclem1  46240  etransclem4  46243  etransclem8  46247  etransclem15  46254  etransclem17  46256  etransclem18  46257  etransclem19  46258  etransclem20  46259  etransclem21  46260  etransclem22  46261  etransclem23  46262  etransclem24  46263  etransclem25  46264  etransclem27  46266  etransclem32  46271  etransclem35  46274  etransclem41  46280  etransclem44  46283  etransclem46  46285  modmknepk  47367  iccpartigtl  47428  iccpartgt  47432  iccpartgel  47434  iccelpart  47438  odz2prm2pw  47568  fmtnoprmfac1  47570  fmtnoprmfac2  47572  2pwp1prm  47594  sfprmdvdsmersenne  47608  lighneallem4a  47613  proththdlem  47618  proththd  47619  perfectALTVlem1  47726  perfectALTVlem2  47727  perfectALTV  47728  fpprwpprb  47745  gpgedgvtx1  48057  logbpw2m1  48560  nnpw2blenfzo  48574  nnolog2flm1  48583  dignn0fr  48594  nn0sumshdiglemA  48612  nn0sumshdiglemB  48613