Theorem nn0addcld 12468

Description: Closure of addition of nonnegative integers, inference form. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
nn0red.1	⊢ (𝜑 → 𝐴 ∈ ℕ0)
nn0addcld.2	⊢ (𝜑 → 𝐵 ∈ ℕ0)

Assertion

Ref	Expression
nn0addcld	⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℕ0)

Proof of Theorem nn0addcld

Step	Hyp	Ref	Expression
1		nn0red.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ0)
2		nn0addcld.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℕ0)
3		nn0addcl 12438	. 2 ⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → (𝐴 + 𝐵) ∈ ℕ0)
4	1, 2, 3	syl2anc 585	1 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℕ0)

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7358   + caddc 11031  ℕ₀cn0 12403

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-10 2147  ax-11 2163  ax-12 2183  ax-ext 2707  ax-sep 5240  ax-nul 5250  ax-pow 5309  ax-pr 5376  ax-un 7680  ax-resscn 11085  ax-1cn 11086  ax-icn 11087  ax-addcl 11088  ax-addrcl 11089  ax-mulcl 11090  ax-mulrcl 11091  ax-mulcom 11092  ax-addass 11093  ax-mulass 11094  ax-distr 11095  ax-i2m1 11096  ax-1ne0 11097  ax-1rid 11098  ax-rnegex 11099  ax-rrecex 11100  ax-cnre 11101  ax-pre-lttri 11102  ax-pre-lttrn 11103  ax-pre-ltadd 11104

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2538  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2810  df-nfc 2884  df-ne 2932  df-nel 3036  df-ral 3051  df-rex 3060  df-reu 3350  df-rab 3399  df-v 3441  df-sbc 3740  df-csb 3849  df-dif 3903  df-un 3905  df-in 3907  df-ss 3917  df-pss 3920  df-nul 4285  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-iun 4947  df-br 5098  df-opab 5160  df-mpt 5179  df-tr 5205  df-id 5518  df-eprel 5523  df-po 5531  df-so 5532  df-fr 5576  df-we 5578  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-pred 6258  df-ord 6319  df-on 6320  df-lim 6321  df-suc 6322  df-iota 6447  df-fun 6493  df-fn 6494  df-f 6495  df-f1 6496  df-fo 6497  df-f1o 6498  df-fv 6499  df-ov 7361  df-om 7809  df-2nd 7934  df-frecs 8223  df-wrecs 8254  df-recs 8303  df-rdg 8341  df-er 8635  df-en 8886  df-dom 8887  df-sdom 8888  df-pnf 11170  df-mnf 11171  df-ltxr 11173  df-nn 12148  df-n0 12404

This theorem is referenced by:  expaddz  14031  bccl  14247  splval2  14682  relexpaddg  14978  rtrclreclem3  14985  mertenslem1  15809  bitsmod  16365  bitsinv1lem  16370  sadcaddlem  16386  sadadd2lem  16388  sadadd  16396  sadass  16400  smupp1  16409  smumul  16422  pcpremul  16773  gzabssqcl  16871  mul4sq  16884  4sqlem12  16886  4sqlem14  16888  4sqlem16  16890  cycsubm  19133  sylow1lem1  19529  efgcpbllemb  19686  omndmul2  20064  mhpmulcl  22094  psdmvr  22114  coe1tmmul2fv  22222  coe1pwmulfv  22224  chfacfscmulgsum  22806  chfacfpmmulfsupp  22809  chfacfpmmulgsum  22810  cpmadugsumlemF  22822  itgpowd  26015  mdegmullem  26041  coe1mul3  26062  deg1mul2  26077  ply1domn  26087  ply1divex  26100  plymullem  26179  coeeulem  26187  dgrmul  26234  dvntaylp  26337  taylthlem2  26340  taylthlem2OLD  26341  dmgmaddnn0  26995  mumullem2  27148  lgseisenlem2  27345  2sqlem8  27395  vtxdgfisnn0  29530  crctcshwlkn0lem5  29868  crctcshwlkn0  29875  eucrctshift  30299  fldext2chn  33864  madjusmdetlem4  33966  oddpwdc  34490  iwrdsplit  34523  fiblem  34534  fibp1  34537  signshlen  34726  fsum2dsub  34743  reprsuc  34751  breprexplemc  34768  subfacp1lem6  35358  faclim2  35921  lcmineqlem3  42320  lcmineqlem11  42328  lcmineqlem18  42335  lcmineqlem21  42338  lcmineqlem22  42339  2np3bcnp1  42433  2ap1caineq  42434  sticksstones6  42440  sticksstones7  42441  sticksstones12a  42446  sticksstones14  42449  sticksstones22  42457  aks6d1c6lem3  42461  bcle2d  42468  aks6d1c7lem1  42469  aks6d1c7lem2  42470  frlmfzoccat  42797  3cubeslem3l  42965  3cubeslem3r  42966  mon1psubm  43478  radcnvrat  44592  binomcxplemnn0  44627  binomcxplemfrat  44629  itgsinexp  46236  wallispilem5  46350  wallispi2lem2  46353  stirlinglem5  46359  stirlinglem7  46361  fourierdlem48  46435  elaa2lem  46514  etransclem32  46547  etransclem46  46561  ormkglobd  47156  sqrtpwpw2p  47821  fmtnofac2lem  47851  fmtnofac2  47852  dignn0flhalflem2  48899  itcovalpclem2  48954  itcovalt2lem2lem1  48956  itcovalt2lem2lem2  48957  itcovalt2lem1  48958