nn0addcld - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > nn0addcld		Structured version Visualization version GIF version

Theorem nn0addcld 12572

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

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

**Assertion**
Ref	Expression
nn0addcld	⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℕ₀)

**Proof of Theorem nn0addcld**
Step	Hyp	Ref	Expression
1		nn0red.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ₀)
2		nn0addcld.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℕ₀)
3		nn0addcl 12543	. 2 ⊢ ((𝐴 ∈ ℕ₀ ∧ 𝐵 ∈ ℕ₀) → (𝐴 + 𝐵) ∈ ℕ₀)
4	1, 2, 3	syl2anc 582	1 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℕ₀)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∈ wcel 2098 (class class class)co 7424 + caddc 11147 ℕ₀cn0 12508

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2698 ax-sep 5301 ax-nul 5308 ax-pow 5367 ax-pr 5431 ax-un 7744 ax-resscn 11201 ax-1cn 11202 ax-icn 11203 ax-addcl 11204 ax-addrcl 11205 ax-mulcl 11206 ax-mulrcl 11207 ax-mulcom 11208 ax-addass 11209 ax-mulass 11210 ax-distr 11211 ax-i2m1 11212 ax-1ne0 11213 ax-1rid 11214 ax-rnegex 11215 ax-rrecex 11216 ax-cnre 11217 ax-pre-lttri 11218 ax-pre-lttrn 11219 ax-pre-ltadd 11220

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2529 df-eu 2558 df-clab 2705 df-cleq 2719 df-clel 2805 df-nfc 2880 df-ne 2937 df-nel 3043 df-ral 3058 df-rex 3067 df-reu 3373 df-rab 3429 df-v 3473 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3966 df-nul 4325 df-if 4531 df-pw 4606 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4911 df-iun 5000 df-br 5151 df-opab 5213 df-mpt 5234 df-tr 5268 df-id 5578 df-eprel 5584 df-po 5592 df-so 5593 df-fr 5635 df-we 5637 df-xp 5686 df-rel 5687 df-cnv 5688 df-co 5689 df-dm 5690 df-rn 5691 df-res 5692 df-ima 5693 df-pred 6308 df-ord 6375 df-on 6376 df-lim 6377 df-suc 6378 df-iota 6503 df-fun 6553 df-fn 6554 df-f 6555 df-f1 6556 df-fo 6557 df-f1o 6558 df-fv 6559 df-ov 7427 df-om 7875 df-2nd 7998 df-frecs 8291 df-wrecs 8322 df-recs 8396 df-rdg 8435 df-er 8729 df-en 8969 df-dom 8970 df-sdom 8971 df-pnf 11286 df-mnf 11287 df-ltxr 11289 df-nn 12249 df-n0 12509

This theorem is referenced by: expaddz 14109 bccl 14319 splval2 14745 relexpaddg 15038 rtrclreclem3 15045 mertenslem1 15868 bitsmod 16416 bitsinv1lem 16421 sadcaddlem 16437 sadadd2lem 16439 sadadd 16447 sadass 16451 smupp1 16460 smumul 16473 pcpremul 16817 gzabssqcl 16915 mul4sq 16928 4sqlem12 16930 4sqlem14 16932 4sqlem16 16934 cycsubm 19162 sylow1lem1 19558 efgcpbllemb 19715 mhpmulcl 22078 coe1tmmul2fv 22202 coe1pwmulfv 22204 chfacfscmulgsum 22780 chfacfpmmulfsupp 22783 chfacfpmmulgsum 22784 cpmadugsumlemF 22796 itgpowd 26003 mdegmullem 26032 coe1mul3 26053 deg1mul2 26068 ply1domn 26077 ply1divex 26090 plymullem 26168 coeeulem 26176 dgrmul 26223 dvntaylp 26324 taylthlem2 26327 taylthlem2OLD 26328 dmgmaddnn0 26977 mumullem2 27130 lgseisenlem2 27327 2sqlem8 27377 vtxdgfisnn0 29307 crctcshwlkn0lem5 29643 crctcshwlkn0 29650 eucrctshift 30071 omndmul2 32810 madjusmdetlem4 33436 oddpwdc 33979 iwrdsplit 34012 fiblem 34023 fibp1 34026 signshlen 34227 fsum2dsub 34244 reprsuc 34252 breprexplemc 34269 subfacp1lem6 34800 faclim2 35347 lcmineqlem3 41506 lcmineqlem11 41514 lcmineqlem18 41521 lcmineqlem21 41524 lcmineqlem22 41525 2np3bcnp1 41620 2ap1caineq 41621 sticksstones6 41627 sticksstones7 41628 sticksstones12a 41633 sticksstones14 41636 sticksstones22 41644 aks6d1c6lem3 41648 bcle2d 41655 aks6d1c7lem1 41656 aks6d1c7lem2 41657 frlmfzoccat 41748 3cubeslem3l 42109 3cubeslem3r 42110 mon1psubm 42630 radcnvrat 43754 binomcxplemnn0 43789 binomcxplemfrat 43791 itgsinexp 45345 wallispilem5 45459 wallispi2lem2 45462 stirlinglem5 45468 stirlinglem7 45470 fourierdlem48 45544 elaa2lem 45623 etransclem32 45656 etransclem46 45670 sqrtpwpw2p 46880 fmtnofac2lem 46910 fmtnofac2 46911 dignn0flhalflem2 47740 itcovalpclem2 47795 itcovalt2lem2lem1 47797 itcovalt2lem2lem2 47798 itcovalt2lem1 47799

W3C validator

	
		OSZAR »