Theorem nn0addcld 12497

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 12467	. 2 ⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → (𝐴 + 𝐵) ∈ ℕ0)
4	1, 2, 3	syl2anc 585	1 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℕ0)

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7362   + caddc 11036  ℕ₀cn0 12432

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 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pow 5304  ax-pr 5372  ax-un 7684  ax-resscn 11090  ax-1cn 11091  ax-icn 11092  ax-addcl 11093  ax-addrcl 11094  ax-mulcl 11095  ax-mulrcl 11096  ax-mulcom 11097  ax-addass 11098  ax-mulass 11099  ax-distr 11100  ax-i2m1 11101  ax-1ne0 11102  ax-1rid 11103  ax-rnegex 11104  ax-rrecex 11105  ax-cnre 11106  ax-pre-lttri 11107  ax-pre-lttrn 11108  ax-pre-ltadd 11109

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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5521  df-eprel 5526  df-po 5534  df-so 5535  df-fr 5579  df-we 5581  df-xp 5632  df-rel 5633  df-cnv 5634  df-co 5635  df-dm 5636  df-rn 5637  df-res 5638  df-ima 5639  df-pred 6261  df-ord 6322  df-on 6323  df-lim 6324  df-suc 6325  df-iota 6450  df-fun 6496  df-fn 6497  df-f 6498  df-f1 6499  df-fo 6500  df-f1o 6501  df-fv 6502  df-ov 7365  df-om 7813  df-2nd 7938  df-frecs 8226  df-wrecs 8257  df-recs 8306  df-rdg 8344  df-er 8638  df-en 8889  df-dom 8890  df-sdom 8891  df-pnf 11176  df-mnf 11177  df-ltxr 11179  df-nn 12170  df-n0 12433

This theorem is referenced by:  expaddz  14063  bccl  14279  splval2  14714  relexpaddg  15010  rtrclreclem3  15017  mertenslem1  15844  bitsmod  16400  bitsinv1lem  16405  sadcaddlem  16421  sadadd2lem  16423  sadadd  16431  sadass  16435  smupp1  16444  smumul  16457  pcpremul  16809  gzabssqcl  16907  mul4sq  16920  4sqlem12  16922  4sqlem14  16924  4sqlem16  16926  cycsubm  19172  sylow1lem1  19568  efgcpbllemb  19725  omndmul2  20103  mhpmulcl  22129  psdmvr  22149  coe1tmmul2fv  22257  coe1pwmulfv  22259  chfacfscmulgsum  22839  chfacfpmmulfsupp  22842  chfacfpmmulgsum  22843  cpmadugsumlemF  22855  itgpowd  26031  mdegmullem  26057  coe1mul3  26078  deg1mul2  26093  ply1domn  26103  ply1divex  26116  plymullem  26195  coeeulem  26203  dgrmul  26249  dvntaylp  26352  taylthlem2  26355  taylthlem2OLD  26356  dmgmaddnn0  27008  mumullem2  27161  lgseisenlem2  27357  2sqlem8  27407  vtxdgfisnn0  29563  crctcshwlkn0lem5  29901  crctcshwlkn0  29908  eucrctshift  30332  fldext2chn  33892  madjusmdetlem4  33994  oddpwdc  34518  iwrdsplit  34551  fiblem  34562  fibp1  34565  signshlen  34754  fsum2dsub  34771  reprsuc  34779  breprexplemc  34796  subfacp1lem6  35387  faclim2  35950  lcmineqlem3  42490  lcmineqlem11  42498  lcmineqlem18  42505  lcmineqlem21  42508  lcmineqlem22  42509  2np3bcnp1  42603  2ap1caineq  42604  sticksstones6  42610  sticksstones7  42611  sticksstones12a  42616  sticksstones14  42619  sticksstones22  42627  aks6d1c6lem3  42631  bcle2d  42638  aks6d1c7lem1  42639  aks6d1c7lem2  42640  frlmfzoccat  42970  3cubeslem3l  43138  3cubeslem3r  43139  mon1psubm  43651  radcnvrat  44765  binomcxplemnn0  44800  binomcxplemfrat  44802  itgsinexp  46407  wallispilem5  46521  wallispi2lem2  46524  stirlinglem5  46530  stirlinglem7  46532  fourierdlem48  46606  elaa2lem  46685  etransclem32  46718  etransclem46  46732  ormkglobd  47327  sqrtpwpw2p  48019  fmtnofac2lem  48049  fmtnofac2  48050  dignn0flhalflem2  49110  itcovalpclem2  49165  itcovalt2lem2lem1  49167  itcovalt2lem2lem2  49168  itcovalt2lem1  49169