Theorem nn0addcld 12449

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

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7349   + caddc 11012  ℕ₀cn0 12384

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-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671  ax-resscn 11066  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-addrcl 11070  ax-mulcl 11071  ax-mulrcl 11072  ax-mulcom 11073  ax-addass 11074  ax-mulass 11075  ax-distr 11076  ax-i2m1 11077  ax-1ne0 11078  ax-1rid 11079  ax-rnegex 11080  ax-rrecex 11081  ax-cnre 11082  ax-pre-lttri 11083  ax-pre-lttrn 11084  ax-pre-ltadd 11085

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-iun 4943  df-br 5093  df-opab 5155  df-mpt 5174  df-tr 5200  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-pred 6249  df-ord 6310  df-on 6311  df-lim 6312  df-suc 6313  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-ov 7352  df-om 7800  df-2nd 7925  df-frecs 8214  df-wrecs 8245  df-recs 8294  df-rdg 8332  df-er 8625  df-en 8873  df-dom 8874  df-sdom 8875  df-pnf 11151  df-mnf 11152  df-ltxr 11154  df-nn 12129  df-n0 12385

This theorem is referenced by:  expaddz  14013  bccl  14229  splval2  14663  relexpaddg  14960  rtrclreclem3  14967  mertenslem1  15791  bitsmod  16347  bitsinv1lem  16352  sadcaddlem  16368  sadadd2lem  16370  sadadd  16378  sadass  16382  smupp1  16391  smumul  16404  pcpremul  16755  gzabssqcl  16853  mul4sq  16866  4sqlem12  16868  4sqlem14  16870  4sqlem16  16872  cycsubm  19081  sylow1lem1  19477  efgcpbllemb  19634  omndmul2  20012  mhpmulcl  22034  psdmvr  22054  coe1tmmul2fv  22162  coe1pwmulfv  22164  chfacfscmulgsum  22745  chfacfpmmulfsupp  22748  chfacfpmmulgsum  22749  cpmadugsumlemF  22761  itgpowd  25955  mdegmullem  25981  coe1mul3  26002  deg1mul2  26017  ply1domn  26027  ply1divex  26040  plymullem  26119  coeeulem  26127  dgrmul  26174  dvntaylp  26277  taylthlem2  26280  taylthlem2OLD  26281  dmgmaddnn0  26935  mumullem2  27088  lgseisenlem2  27285  2sqlem8  27335  vtxdgfisnn0  29425  crctcshwlkn0lem5  29763  crctcshwlkn0  29770  eucrctshift  30191  fldext2chn  33711  madjusmdetlem4  33813  oddpwdc  34338  iwrdsplit  34371  fiblem  34382  fibp1  34385  signshlen  34574  fsum2dsub  34591  reprsuc  34599  breprexplemc  34616  subfacp1lem6  35178  faclim2  35741  lcmineqlem3  42024  lcmineqlem11  42032  lcmineqlem18  42039  lcmineqlem21  42042  lcmineqlem22  42043  2np3bcnp1  42137  2ap1caineq  42138  sticksstones6  42144  sticksstones7  42145  sticksstones12a  42150  sticksstones14  42153  sticksstones22  42161  aks6d1c6lem3  42165  bcle2d  42172  aks6d1c7lem1  42173  aks6d1c7lem2  42174  frlmfzoccat  42498  3cubeslem3l  42679  3cubeslem3r  42680  mon1psubm  43192  radcnvrat  44307  binomcxplemnn0  44342  binomcxplemfrat  44344  itgsinexp  45956  wallispilem5  46070  wallispi2lem2  46073  stirlinglem5  46079  stirlinglem7  46081  fourierdlem48  46155  elaa2lem  46234  etransclem32  46267  etransclem46  46281  ormkglobd  46876  sqrtpwpw2p  47542  fmtnofac2lem  47572  fmtnofac2  47573  dignn0flhalflem2  48621  itcovalpclem2  48676  itcovalt2lem2lem1  48678  itcovalt2lem2lem2  48679  itcovalt2lem1  48680