Theorem nn0addcld 12671

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  (class class class)co 7420   + caddc 11203  ℕ₀cn0 12606

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-resscn 11257  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-addrcl 11261  ax-mulcl 11262  ax-mulrcl 11263  ax-mulcom 11264  ax-addass 11265  ax-mulass 11266  ax-distr 11267  ax-i2m1 11268  ax-1ne0 11269  ax-1rid 11270  ax-rnegex 11271  ax-rrecex 11272  ax-cnre 11273  ax-pre-lttri 11274  ax-pre-lttrn 11275  ax-pre-ltadd 11276

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-ov 7423  df-om 7878  df-2nd 8002  df-frecs 8299  df-wrecs 8330  df-recs 8379  df-rdg 8418  df-er 8717  df-en 8974  df-dom 8975  df-sdom 8976  df-pnf 11345  df-mnf 11346  df-ltxr 11348  df-nn 12336  df-n0 12607

This theorem is used by:  expaddz  14249  bccl  14466  splval2  14906  relexpaddg  15206  rtrclreclem3  15213  mertenslem1  16053  bitsmod  16606  bitsinv1lem  16611  sadcaddlem  16627  sadadd2lem  16629  sadadd  16637  sadass  16641  smupp1  16650  smumul  16663  pcpremul  17021  gzabssqcl  17119  mul4sq  17132  4sqlem12  17134  4sqlem14  17136  4sqlem16  17138  cycsubm  19417  sylow1lem1  19812  efgcpbllemb  19969  omndmul2  20347  mhpmulcl  22470  psdmvr  22490  coe1tmmul2fv  22597  coe1pwmulfv  22599  chfacfscmulgsum  23178  chfacfpmmulfsupp  23181  chfacfpmmulgsum  23182  cpmadugsumlemF  23194  itgpowd  26370  mdegmullem  26396  coe1mul3  26417  deg1mul2  26432  ply1domn  26442  ply1divex  26455  plymullem  26535  coeeulem  26543  dgrmul  26589  dvntaylp  26698  taylthlem2  26701  dmgmaddnn0  27354  mumullem2  27507  lgseisenlem2  27703  2sqlem8  27753  vtxdgfisnn0  30056  crctcshwlkn0lem5  30403  crctcshwlkn0  30410  eucrctshift  30844  fldext2chn  34360  madjusmdetlem4  34462  oddpwdc  34986  iwrdsplit  35019  fiblem  35030  fibp1  35033  signshlen  35219  fsum2dsub  35236  reprsuc  35244  breprexplemc  35261  subfacp1lem6  35950  faclim2  36513  lcmineqlem3  43082  lcmineqlem11  43090  lcmineqlem18  43097  lcmineqlem21  43100  lcmineqlem22  43101  2np3bcnp1  43195  2ap1caineq  43196  sticksstones6  43202  sticksstones7  43203  sticksstones12a  43208  sticksstones14  43211  sticksstones22  43219  aks6d1c6lem3  43223  bcle2d  43230  aks6d1c7lem1  43231  aks6d1c7lem2  43232  frlmfzoccat  43573  3cubeslem3l  43697  3cubeslem3r  43698  mon1psubm  44201  radcnvrat  45298  binomcxplemnn0  45333  binomcxplemfrat  45335  itgsinexp  46965  wallispilem5  47079  wallispi2lem2  47082  stirlinglem5  47088  stirlinglem7  47090  fourierdlem48  47164  elaa2lem  47243  etransclem32  47276  etransclem46  47290  ormkglobd  47887  sqrtpwpw2p  48623  fmtnofac2lem  48653  fmtnofac2  48654  dignn0flhalflem2  49728  itcovalpclem2  49783  itcovalt2lem2lem1  49785  itcovalt2lem2lem2  49786  itcovalt2lem1  49787