Theorem nnnn0d 12587

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℕcn 12266  ℕ₀cn0 12526

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-un 3956  df-ss 3968  df-n0 12527

This theorem is referenced by:  nn0ge2m1nn0  12597  nnzd  12640  eluzge2nn0  12929  expgt1  14141  expaddzlem  14146  expaddz  14147  expmulz  14149  expmulnbnd  14274  exp11nnd  14300  facwordi  14328  faclbnd  14329  facavg  14340  bcm1k  14354  wrdeqs1cat  14758  cshwcsh2id  14867  relexpsucnnr  15064  isercolllem2  15702  bcxmas  15871  climcndslem1  15885  climcndslem2  15886  climcnds  15887  pwdif  15904  geo2sum  15909  mertenslem1  15920  prodmolem3  15969  prodmolem2a  15970  bpolydiflem  16090  eftabs  16111  efcllem  16113  eftlub  16145  eirrlem  16240  rpnnen2lem9  16258  rpnnen2lem11  16260  dvdsfac  16363  pwp1fsum  16428  oddpwp1fsum  16429  bitsfzo  16472  bitsfi  16474  sadcaddlem  16494  smumullem  16529  gcdcl  16543  dvdsgcdidd  16574  mulgcd  16585  rplpwr  16595  rprpwr  16596  rppwr  16597  nn0rppwr  16598  expgcd  16600  lcmcl  16638  lcmgcdnn  16648  lcmfcl  16665  nprmdvds1  16743  rpexp  16759  prmdvdsbc  16763  zsqrtelqelz  16795  phiprmpw  16813  eulerthlem2  16819  eulerth  16820  fermltl  16821  odzcllem  16830  odzdvds  16833  odzphi  16834  prm23lt5  16852  pythagtriplem6  16859  pythagtriplem7  16860  pcprmpw2  16920  dvdsprmpweqle  16924  pcprod  16933  pcfac  16937  pcbc  16938  expnprm  16940  pockthlem  16943  pockthg  16944  prmunb  16952  prmreclem2  16955  prmreclem3  16956  prmreclem4  16957  prmreclem5  16958  prmreclem6  16959  mul4sqlem  16991  4sqlem11  16993  4sqlem17  16999  vdwlem1  17019  vdwlem5  17023  vdwlem6  17024  vdwlem8  17026  vdwlem9  17027  vdwlem11  17029  vdwlem12  17030  vdwnnlem3  17035  ramz2  17062  ramub1lem1  17064  ramub1lem2  17065  ramub1  17066  prmgaplem3  17091  2expltfac  17130  psgnunilem3  19514  odfval  19550  mndodconglem  19559  gexcl3  19605  pgpfi1  19613  sylow1lem1  19616  gexexlem  19870  prmcyg  19912  gsumval3  19925  ablfacrplem  20085  ablfacrp  20086  ablfacrp2  20087  ablfac1eu  20093  prmgrpsimpgd  20134  srgbinomlem3  20225  srgbinomlem4  20226  fermltlchr  21544  freshmansdream  21593  chfacfscmulgsum  22866  chfacfpmmulgsum  22870  cpmadugsumlemF  22882  ovoliunlem1  25537  mbfi1fseqlem1  25750  mbfi1fseqlem3  25752  mbfi1fseqlem5  25754  itg2cnlem2  25797  dvply1  26325  aalioulem2  26375  aalioulem5  26378  aaliou3lem1  26384  aaliou3lem2  26385  aaliou3lem8  26387  aaliou3lem6  26390  taylthlem1  26415  taylthlem2  26416  taylthlem2OLD  26417  pserdvlem2  26472  cxpeq  26800  zrtelqelz  26801  dmgmdivn0  27071  lgamgulmlem5  27076  lgamcvg2  27098  wilthlem1  27111  ftalem1  27116  ftalem2  27117  ftalem4  27119  ftalem5  27120  basellem2  27125  basellem3  27126  basellem4  27127  basellem5  27128  isppw2  27158  mpodvdsmulf1o  27237  dvdsmulf1o  27239  sgmmul  27245  fsumvma2  27258  chpchtsum  27263  logfacubnd  27265  mersenne  27271  perfect1  27272  perfectlem1  27273  perfectlem2  27274  perfect  27275  dchrelbas3  27282  dchrelbasd  27283  dchrzrh1  27288  dchrzrhmul  27290  dchrmulcl  27293  dchrn0  27294  dchrfi  27299  dchrghm  27300  dchrabs  27304  dchrinv  27305  dchrptlem1  27308  dchrptlem2  27309  dchrptlem3  27310  dchrpt  27311  dchrsum2  27312  sum2dchr  27318  pcbcctr  27320  bcmono  27321  bclbnd  27324  bposlem1  27328  bposlem3  27330  bposlem5  27332  bposlem6  27333  lgslem1  27341  lgsval2lem  27351  lgsvalmod  27360  lgsmod  27367  lgsdirprm  27375  lgsne0  27379  lgsqrlem1  27390  lgsqrlem2  27391  lgsqrlem3  27392  lgsqrlem4  27393  gausslemma2dlem0b  27401  gausslemma2dlem0c  27402  gausslemma2dlem1  27410  gausslemma2dlem7  27417  gausslemma2d  27418  lgseisenlem1  27419  lgseisenlem2  27420  lgseisenlem3  27421  lgseisenlem4  27422  lgseisen  27423  lgsquadlem2  27425  lgsquadlem3  27426  m1lgs  27432  2lgslem1a  27435  2sqlem3  27464  2sqblem  27475  chebbnd1lem1  27513  chebbnd1lem3  27515  rplogsumlem2  27529  rpvmasumlem  27531  dchrisumlem1  27533  dchrisumlem2  27534  dchrmusum2  27538  dchrvmasumlem3  27543  dchrisum0ff  27551  dchrisum0flblem1  27552  rpvmasum2  27556  dchrisum0re  27557  dchrisum0lem2a  27561  dirith  27573  mudivsum  27574  pntpbnd1a  27629  pntlemq  27645  pntlemr  27646  pntlemj  27647  ostth2lem1  27662  ostth2lem2  27678  ostth2lem3  27679  ostth2  27681  crctcshwlkn0lem6  29835  hashecclwwlkn1  30096  umgrhashecclwwlk  30097  clwwlknon  30109  eucrctshift  30262  numclwlk1lem2  30389  nrt2irr  30492  dipcl  30731  dipcn  30739  bcm1n  32797  expgt0b  32818  nexple  32833  2exple2exp  32834  wrdpmtrlast  33113  psgnfzto1st  33125  isarchi2  33192  submarchi  33193  znfermltl  33394  fldextrspundgdvdslem  33730  fldextrspundgdvds  33731  fldext2rspun  33732  submateqlem1  33806  madjusmdetlem2  33827  madjusmdetlem4  33829  mdetlap  33831  oddpwdc  34356  eulerpartlemsv2  34360  eulerpartlemsf  34361  eulerpartlems  34362  eulerpartlemv  34366  eulerpartlemb  34370  plymulx0  34562  signsvtn0  34585  fsum2dsub  34622  reprinfz1  34637  reprpmtf1o  34641  circlemeth  34655  circlemethnat  34656  hgt750lemb  34671  hgt750lema  34672  hgt750leme  34673  tgoldbachgtde  34675  tgoldbachgtda  34676  lpadleft  34698  subfacp1lem1  35184  subfacp1lem6  35190  subfaclim  35193  erdszelem8  35203  erdszelem10  35205  cvmliftlem10  35299  faclim2  35748  poimirlem7  37634  poimirlem17  37644  poimirlem18  37645  poimirlem20  37647  poimirlem21  37648  poimirlem22  37649  poimirlem25  37652  poimirlem26  37653  poimirlem27  37654  poimirlem28  37655  poimirlem32  37659  nninfnub  37758  bfplem1  37829  zndvdchrrhm  41972  lcmineqlem1  42030  lcmineqlem2  42031  lcmineqlem8  42037  lcmineqlem10  42039  lcmineqlem11  42040  lcmineqlem15  42044  lcmineqlem16  42045  lcmineqlem18  42047  lcmineqlem19  42048  lcmineqlem20  42049  lcmineqlem21  42050  lcmineqlem22  42051  3lexlogpow2ineq2  42060  dvrelogpow2b  42069  aks4d1p1p2  42071  aks4d1p1p4  42072  aks4d1p1  42077  aks4d1p3  42079  aks4d1p7d1  42083  aks4d1p7  42084  aks4d1p8  42088  aks4d1p9  42089  isprimroot2  42095  primrootsunit1  42098  primrootscoprmpow  42100  posbezout  42101  primrootscoprbij  42103  primrootlekpowne0  42106  primrootspoweq0  42107  aks6d1c1p2  42110  aks6d1c1p3  42111  aks6d1c1p4  42112  aks6d1c1p5  42113  aks6d1c1p7  42114  aks6d1c1p6  42115  aks6d1c1p8  42116  aks6d1c2p2  42120  hashscontpowcl  42121  hashscontpow1  42122  hashscontpow  42123  aks6d1c4  42125  aks6d1c2lem3  42127  aks6d1c2lem4  42128  aks6d1c2  42131  sticksstones6  42152  sticksstones7  42153  sticksstones10  42156  sticksstones12a  42158  sticksstones12  42159  sticksstones20  42167  sticksstones22  42169  aks6d1c6lem2  42172  aks6d1c6lem3  42173  aks6d1c6lem4  42174  aks6d1c6isolem1  42175  aks6d1c6isolem2  42176  aks6d1c6lem5  42178  bcled  42179  bcle2d  42180  aks6d1c7lem1  42181  aks6d1c7  42185  aks5lem2  42188  aks5lem3a  42190  aks5lem5a  42192  grpods  42195  unitscyglem2  42197  unitscyglem4  42199  aks5lem7  42201  aks5  42205  metakunt2  42207  sumcubes  42347  oexpreposd  42357  exp11d  42361  dvdsexpb  42370  fiabv  42546  fsuppind  42600  dffltz  42644  fltdvdsabdvdsc  42648  fltne  42654  flt4lem4  42659  flt4lem7  42669  fltltc  42671  fltnltalem  42672  fltnlta  42673  3rexfrabdioph  42808  4rexfrabdioph  42809  6rexfrabdioph  42810  7rexfrabdioph  42811  irrapxlem5  42837  pellexlem2  42841  pellexlem6  42845  pell14qrgt0  42870  pell1qrge1  42881  pellfundgt1  42894  ltrmxnn0  42961  jm2.26lem3  43013  jm2.27a  43017  jm2.27c  43019  rmxdiophlem  43027  jm3.1lem1  43029  jm3.1lem2  43030  jm3.1lem3  43031  jm3.1  43032  dgrsub2  43147  mpaaeu  43162  idomsubgmo  43205  relexpxpmin  43730  nzprmdif  44338  binomcxplemwb  44367  fperiodmul  45316  xralrple4  45384  fsumnncl  45587  dvsinexp  45926  dvxpaek  45955  itgsinexplem1  45969  stoweidlem1  46016  stoweidlem17  46032  stoweidlem25  46040  stoweidlem34  46049  stoweidlem38  46053  stoweidlem40  46055  stoweidlem42  46057  stoweidlem45  46060  stirlinglem4  46092  stirlinglem5  46093  stirlinglem10  46098  stirlinglem13  46101  dirkertrigeq  46116  fourierdlem21  46143  fourierdlem25  46147  fourierdlem48  46169  fourierdlem54  46175  fourierdlem64  46185  fourierdlem65  46186  fourierdlem73  46194  fourierdlem81  46202  fourierdlem83  46204  fourierdlem92  46213  fourierdlem103  46224  fourierdlem104  46225  fourierdlem112  46233  fourierdlem113  46234  etransclem1  46250  etransclem4  46253  etransclem8  46257  etransclem15  46264  etransclem17  46266  etransclem18  46267  etransclem19  46268  etransclem20  46269  etransclem21  46270  etransclem22  46271  etransclem23  46272  etransclem24  46273  etransclem25  46274  etransclem27  46276  etransclem32  46281  etransclem35  46284  etransclem41  46290  etransclem44  46293  etransclem46  46295  iccpartigtl  47410  iccpartgt  47414  iccpartgel  47416  iccelpart  47420  odz2prm2pw  47550  fmtnoprmfac1  47552  fmtnoprmfac2  47554  2pwp1prm  47576  sfprmdvdsmersenne  47590  lighneallem4a  47595  proththdlem  47600  proththd  47601  perfectALTVlem1  47708  perfectALTVlem2  47709  perfectALTV  47710  fpprwpprb  47727  gpgedgvtx1  48020  gpg3nbgrvtxlem  48023  logbpw2m1  48488  nnpw2blenfzo  48502  nnolog2flm1  48511  dignn0fr  48522  nn0sumshdiglemA  48540  nn0sumshdiglemB  48541