Theorem un0addcl

Description: If S is closed under addition, then so is S u. { 0 } . (Contributed by Mario Carneiro, 17-Jul-2014)

	Ref	Expression
Hypotheses	un0addcl.1	⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
	un0addcl.2	⊢ 𝑇 = ( 𝑆 ∪ { 0 } )
	un0addcl.3	⊢ ( ( 𝜑 ∧ ( 𝑀 ∈ 𝑆 ∧ 𝑁 ∈ 𝑆 ) ) → ( 𝑀 + 𝑁 ) ∈ 𝑆 )
Assertion	un0addcl	⊢ ( ( 𝜑 ∧ ( 𝑀 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ) ) → ( 𝑀 + 𝑁 ) ∈ 𝑇 )

Proof

Step	Hyp	Ref	Expression
1		un0addcl.1	⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
2		un0addcl.2	⊢ 𝑇 = ( 𝑆 ∪ { 0 } )
3		un0addcl.3	⊢ ( ( 𝜑 ∧ ( 𝑀 ∈ 𝑆 ∧ 𝑁 ∈ 𝑆 ) ) → ( 𝑀 + 𝑁 ) ∈ 𝑆 )
4	2	eleq2i	⊢ ( 𝑁 ∈ 𝑇 ↔ 𝑁 ∈ ( 𝑆 ∪ { 0 } ) )
5		elun	⊢ ( 𝑁 ∈ ( 𝑆 ∪ { 0 } ) ↔ ( 𝑁 ∈ 𝑆 ∨ 𝑁 ∈ { 0 } ) )
6	4 5	bitri	⊢ ( 𝑁 ∈ 𝑇 ↔ ( 𝑁 ∈ 𝑆 ∨ 𝑁 ∈ { 0 } ) )
7	2	eleq2i	⊢ ( 𝑀 ∈ 𝑇 ↔ 𝑀 ∈ ( 𝑆 ∪ { 0 } ) )
8		elun	⊢ ( 𝑀 ∈ ( 𝑆 ∪ { 0 } ) ↔ ( 𝑀 ∈ 𝑆 ∨ 𝑀 ∈ { 0 } ) )
9	7 8	bitri	⊢ ( 𝑀 ∈ 𝑇 ↔ ( 𝑀 ∈ 𝑆 ∨ 𝑀 ∈ { 0 } ) )
10		ssun1	⊢ 𝑆 ⊆ ( 𝑆 ∪ { 0 } )
11	10 2	sseqtrri	⊢ 𝑆 ⊆ 𝑇
12	11 3	sselid	⊢ ( ( 𝜑 ∧ ( 𝑀 ∈ 𝑆 ∧ 𝑁 ∈ 𝑆 ) ) → ( 𝑀 + 𝑁 ) ∈ 𝑇 )
13	12	expr	⊢ ( ( 𝜑 ∧ 𝑀 ∈ 𝑆 ) → ( 𝑁 ∈ 𝑆 → ( 𝑀 + 𝑁 ) ∈ 𝑇 ) )
14	1	sselda	⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑆 ) → 𝑁 ∈ ℂ )
15	14	addid2d	⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑆 ) → ( 0 + 𝑁 ) = 𝑁 )
16	11	a1i	⊢ ( 𝜑 → 𝑆 ⊆ 𝑇 )
17	16	sselda	⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑆 ) → 𝑁 ∈ 𝑇 )
18	15 17	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑆 ) → ( 0 + 𝑁 ) ∈ 𝑇 )
19		elsni	⊢ ( 𝑀 ∈ { 0 } → 𝑀 = 0 )
20	19	oveq1d	⊢ ( 𝑀 ∈ { 0 } → ( 𝑀 + 𝑁 ) = ( 0 + 𝑁 ) )
21	20	eleq1d	⊢ ( 𝑀 ∈ { 0 } → ( ( 𝑀 + 𝑁 ) ∈ 𝑇 ↔ ( 0 + 𝑁 ) ∈ 𝑇 ) )
22	18 21	syl5ibrcom	⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑆 ) → ( 𝑀 ∈ { 0 } → ( 𝑀 + 𝑁 ) ∈ 𝑇 ) )
23	22	impancom	⊢ ( ( 𝜑 ∧ 𝑀 ∈ { 0 } ) → ( 𝑁 ∈ 𝑆 → ( 𝑀 + 𝑁 ) ∈ 𝑇 ) )
24	13 23	jaodan	⊢ ( ( 𝜑 ∧ ( 𝑀 ∈ 𝑆 ∨ 𝑀 ∈ { 0 } ) ) → ( 𝑁 ∈ 𝑆 → ( 𝑀 + 𝑁 ) ∈ 𝑇 ) )
25	9 24	sylan2b	⊢ ( ( 𝜑 ∧ 𝑀 ∈ 𝑇 ) → ( 𝑁 ∈ 𝑆 → ( 𝑀 + 𝑁 ) ∈ 𝑇 ) )
26		0cnd	⊢ ( 𝜑 → 0 ∈ ℂ )
27	26	snssd	⊢ ( 𝜑 → { 0 } ⊆ ℂ )
28	1 27	unssd	⊢ ( 𝜑 → ( 𝑆 ∪ { 0 } ) ⊆ ℂ )
29	2 28	eqsstrid	⊢ ( 𝜑 → 𝑇 ⊆ ℂ )
30	29	sselda	⊢ ( ( 𝜑 ∧ 𝑀 ∈ 𝑇 ) → 𝑀 ∈ ℂ )
31	30	addid1d	⊢ ( ( 𝜑 ∧ 𝑀 ∈ 𝑇 ) → ( 𝑀 + 0 ) = 𝑀 )
32		simpr	⊢ ( ( 𝜑 ∧ 𝑀 ∈ 𝑇 ) → 𝑀 ∈ 𝑇 )
33	31 32	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑀 ∈ 𝑇 ) → ( 𝑀 + 0 ) ∈ 𝑇 )
34		elsni	⊢ ( 𝑁 ∈ { 0 } → 𝑁 = 0 )
35	34	oveq2d	⊢ ( 𝑁 ∈ { 0 } → ( 𝑀 + 𝑁 ) = ( 𝑀 + 0 ) )
36	35	eleq1d	⊢ ( 𝑁 ∈ { 0 } → ( ( 𝑀 + 𝑁 ) ∈ 𝑇 ↔ ( 𝑀 + 0 ) ∈ 𝑇 ) )
37	33 36	syl5ibrcom	⊢ ( ( 𝜑 ∧ 𝑀 ∈ 𝑇 ) → ( 𝑁 ∈ { 0 } → ( 𝑀 + 𝑁 ) ∈ 𝑇 ) )
38	25 37	jaod	⊢ ( ( 𝜑 ∧ 𝑀 ∈ 𝑇 ) → ( ( 𝑁 ∈ 𝑆 ∨ 𝑁 ∈ { 0 } ) → ( 𝑀 + 𝑁 ) ∈ 𝑇 ) )
39	6 38	syl5bi	⊢ ( ( 𝜑 ∧ 𝑀 ∈ 𝑇 ) → ( 𝑁 ∈ 𝑇 → ( 𝑀 + 𝑁 ) ∈ 𝑇 ) )
40	39	impr	⊢ ( ( 𝜑 ∧ ( 𝑀 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ) ) → ( 𝑀 + 𝑁 ) ∈ 𝑇 )