Theorem nnnn0d 12528

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

Syntax hints:   → wi 4   ∈ wcel 2106  ℕcn 12208  ℕ₀cn0 12468

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-un 3952  df-in 3954  df-ss 3964  df-n0 12469

This theorem is referenced by:  nn0ge2m1nn0  12538  nnzd  12581  eluzge2nn0  12867  expgt1  14062  expaddzlem  14067  expaddz  14068  expmulz  14070  expmulnbnd  14194  facwordi  14245  faclbnd  14246  facavg  14257  bcm1k  14271  wrdeqs1cat  14666  cshwcsh2id  14775  relexpsucnnr  14968  isercolllem2  15608  bcxmas  15777  climcndslem1  15791  climcndslem2  15792  climcnds  15793  pwdif  15810  geo2sum  15815  mertenslem1  15826  prodmolem3  15873  prodmolem2a  15874  bpolydiflem  15994  eftabs  16015  efcllem  16017  eftlub  16048  eirrlem  16143  rpnnen2lem9  16161  rpnnen2lem11  16163  dvdsfac  16265  pwp1fsum  16330  oddpwp1fsum  16331  bitsfzo  16372  bitsfi  16374  sadcaddlem  16394  smumullem  16429  gcdcl  16443  dvdsgcdidd  16475  mulgcd  16486  rplpwr  16495  rprpwr  16496  rppwr  16497  lcmcl  16534  lcmgcdnn  16544  lcmfcl  16561  nprmdvds1  16639  rpexp  16655  zsqrtelqelz  16690  phiprmpw  16705  eulerthlem2  16711  eulerth  16712  fermltl  16713  odzcllem  16721  odzdvds  16724  odzphi  16725  prm23lt5  16743  pythagtriplem6  16750  pythagtriplem7  16751  pcprmpw2  16811  dvdsprmpweqle  16815  pcprod  16824  pcfac  16828  pcbc  16829  expnprm  16831  pockthlem  16834  pockthg  16835  prmunb  16843  prmreclem2  16846  prmreclem3  16847  prmreclem4  16848  prmreclem5  16849  prmreclem6  16850  mul4sqlem  16882  4sqlem11  16884  4sqlem17  16890  vdwlem1  16910  vdwlem5  16914  vdwlem6  16915  vdwlem8  16917  vdwlem9  16918  vdwlem11  16920  vdwlem12  16921  vdwnnlem3  16926  ramz2  16953  ramub1lem1  16955  ramub1lem2  16956  ramub1  16957  prmgaplem3  16982  2expltfac  17022  psgnunilem3  19358  odfval  19394  mndodconglem  19403  gexcl3  19449  pgpfi1  19457  sylow1lem1  19460  gexexlem  19714  prmcyg  19756  gsumval3  19769  ablfacrplem  19929  ablfacrp  19930  ablfacrp2  19931  ablfac1eu  19937  prmgrpsimpgd  19978  srgbinomlem3  20044  srgbinomlem4  20045  chfacfscmulgsum  22353  chfacfpmmulgsum  22357  cpmadugsumlemF  22369  ovoliunlem1  25010  mbfi1fseqlem1  25224  mbfi1fseqlem3  25226  mbfi1fseqlem5  25228  itg2cnlem2  25271  dvply1  25788  aalioulem2  25837  aalioulem5  25840  aaliou3lem1  25846  aaliou3lem2  25847  aaliou3lem8  25849  aaliou3lem6  25852  taylthlem1  25876  taylthlem2  25877  pserdvlem2  25931  cxpeq  26254  dmgmdivn0  26521  lgamgulmlem5  26526  lgamcvg2  26548  wilthlem1  26561  ftalem1  26566  ftalem2  26567  ftalem4  26569  ftalem5  26570  basellem2  26575  basellem3  26576  basellem4  26577  basellem5  26578  isppw2  26608  dvdsmulf1o  26687  sgmmul  26693  fsumvma2  26706  chpchtsum  26711  logfacubnd  26713  mersenne  26719  perfect1  26720  perfectlem1  26721  perfectlem2  26722  perfect  26723  dchrelbas3  26730  dchrelbasd  26731  dchrzrh1  26736  dchrzrhmul  26738  dchrmulcl  26741  dchrn0  26742  dchrfi  26747  dchrghm  26748  dchrabs  26752  dchrinv  26753  dchrptlem1  26756  dchrptlem2  26757  dchrptlem3  26758  dchrpt  26759  dchrsum2  26760  sum2dchr  26766  pcbcctr  26768  bcmono  26769  bclbnd  26772  bposlem1  26776  bposlem3  26778  bposlem5  26780  bposlem6  26781  lgslem1  26789  lgsval2lem  26799  lgsvalmod  26808  lgsmod  26815  lgsdirprm  26823  lgsne0  26827  lgsqrlem1  26838  lgsqrlem2  26839  lgsqrlem3  26840  lgsqrlem4  26841  gausslemma2dlem0b  26849  gausslemma2dlem0c  26850  gausslemma2dlem1  26858  gausslemma2dlem7  26865  gausslemma2d  26866  lgseisenlem1  26867  lgseisenlem2  26868  lgseisenlem3  26869  lgseisenlem4  26870  lgseisen  26871  lgsquadlem2  26873  lgsquadlem3  26874  m1lgs  26880  2lgslem1a  26883  2sqlem3  26912  2sqblem  26923  chebbnd1lem1  26961  chebbnd1lem3  26963  rplogsumlem2  26977  rpvmasumlem  26979  dchrisumlem1  26981  dchrisumlem2  26982  dchrmusum2  26986  dchrvmasumlem3  26991  dchrisum0ff  26999  dchrisum0flblem1  27000  rpvmasum2  27004  dchrisum0re  27005  dchrisum0lem2a  27009  dirith  27021  mudivsum  27022  pntpbnd1a  27077  pntlemq  27093  pntlemr  27094  pntlemj  27095  ostth2lem1  27110  ostth2lem2  27126  ostth2lem3  27127  ostth2  27129  crctcshwlkn0lem6  29058  hashecclwwlkn1  29319  umgrhashecclwwlk  29320  clwwlknon  29332  eucrctshift  29485  numclwlk1lem2  29612  dipcl  29952  dipcn  29960  bcm1n  31993  prmdvdsbc  32009  psgnfzto1st  32251  isarchi2  32318  submarchi  32319  freshmansdream  32369  fermltlchr  32466  znfermltl  32467  submateqlem1  32775  madjusmdetlem2  32796  madjusmdetlem4  32798  mdetlap  32800  nexple  32995  oddpwdc  33341  eulerpartlemsv2  33345  eulerpartlemsf  33346  eulerpartlems  33347  eulerpartlemv  33351  eulerpartlemb  33355  plymulx0  33546  signsvtn0  33569  fsum2dsub  33607  reprinfz1  33622  reprpmtf1o  33626  circlemeth  33640  circlemethnat  33641  hgt750lemb  33656  hgt750lema  33657  hgt750leme  33658  tgoldbachgtde  33660  tgoldbachgtda  33661  lpadleft  33683  subfacp1lem1  34158  subfacp1lem6  34164  subfaclim  34167  erdszelem8  34177  erdszelem10  34179  cvmliftlem10  34273  faclim2  34706  poimirlem7  36483  poimirlem17  36493  poimirlem18  36494  poimirlem20  36496  poimirlem21  36497  poimirlem22  36498  poimirlem25  36501  poimirlem26  36502  poimirlem27  36503  poimirlem28  36504  poimirlem32  36508  nninfnub  36607  bfplem1  36678  lcmineqlem1  40882  lcmineqlem2  40883  lcmineqlem8  40889  lcmineqlem10  40891  lcmineqlem11  40892  lcmineqlem15  40896  lcmineqlem16  40897  lcmineqlem18  40899  lcmineqlem19  40900  lcmineqlem20  40901  lcmineqlem21  40902  lcmineqlem22  40903  3lexlogpow2ineq2  40912  dvrelogpow2b  40921  aks4d1p1p2  40923  aks4d1p1p4  40924  aks4d1p1  40929  aks4d1p3  40931  aks4d1p7d1  40935  aks4d1p7  40936  aks4d1p8  40940  aks4d1p9  40941  aks6d1c2p2  40945  sticksstones6  40955  sticksstones7  40956  sticksstones10  40959  sticksstones12a  40961  sticksstones12  40962  sticksstones20  40970  sticksstones22  40972  metakunt2  40974  fsuppind  41159  sumcubes  41206  oexpreposd  41207  exp11nnd  41210  exp11d  41211  nn0rppwr  41219  expgcd  41220  dvdsexpb  41228  zrtelqelz  41231  dffltz  41372  fltdvdsabdvdsc  41376  fltne  41382  flt4lem4  41387  flt4lem7  41397  fltltc  41399  fltnltalem  41400  fltnlta  41401  3rexfrabdioph  41520  4rexfrabdioph  41521  6rexfrabdioph  41522  7rexfrabdioph  41523  irrapxlem5  41549  pellexlem2  41553  pellexlem6  41557  pell14qrgt0  41582  pell1qrge1  41593  pellfundgt1  41606  ltrmxnn0  41673  jm2.26lem3  41725  jm2.27a  41729  jm2.27c  41731  rmxdiophlem  41739  jm3.1lem1  41741  jm3.1lem2  41742  jm3.1lem3  41743  jm3.1  41744  dgrsub2  41862  mpaaeu  41877  idomsubgmo  41925  relexpxpmin  42453  nzprmdif  43063  binomcxplemwb  43092  fperiodmul  44000  xralrple4  44069  fsumnncl  44274  dvsinexp  44613  dvxpaek  44642  itgsinexplem1  44656  stoweidlem1  44703  stoweidlem17  44719  stoweidlem25  44727  stoweidlem34  44736  stoweidlem38  44740  stoweidlem40  44742  stoweidlem42  44744  stoweidlem45  44747  stirlinglem4  44779  stirlinglem5  44780  stirlinglem10  44785  stirlinglem13  44788  dirkertrigeq  44803  fourierdlem21  44830  fourierdlem25  44834  fourierdlem48  44856  fourierdlem54  44862  fourierdlem64  44872  fourierdlem65  44873  fourierdlem73  44881  fourierdlem81  44889  fourierdlem83  44891  fourierdlem92  44900  fourierdlem103  44911  fourierdlem104  44912  fourierdlem112  44920  fourierdlem113  44921  etransclem1  44937  etransclem4  44940  etransclem8  44944  etransclem15  44951  etransclem17  44953  etransclem18  44954  etransclem19  44955  etransclem20  44956  etransclem21  44957  etransclem22  44958  etransclem23  44959  etransclem24  44960  etransclem25  44961  etransclem27  44963  etransclem32  44968  etransclem35  44971  etransclem41  44977  etransclem44  44980  etransclem46  44982  iccpartigtl  46077  iccpartgt  46081  iccpartgel  46083  iccelpart  46087  odz2prm2pw  46217  fmtnoprmfac1  46219  fmtnoprmfac2  46221  2pwp1prm  46243  sfprmdvdsmersenne  46257  lighneallem4a  46262  proththdlem  46267  proththd  46268  perfectALTVlem1  46375  perfectALTVlem2  46376  perfectALTV  46377  fpprwpprb  46394  logbpw2m1  47206  nnpw2blenfzo  47220  nnolog2flm1  47229  dignn0fr  47240  nn0sumshdiglemA  47258  nn0sumshdiglemB  47259