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	$⊢ φ \to S \subseteq ℂ$
	un0addcl.2	$⊢ T = S \cup \{0\}$
	un0addcl.3	$⊢ (φ \land (M \in S \land N \in S)) \to M + N \in S$
Assertion	un0addcl	$⊢ (φ \land (M \in T \land N \in T)) \to M + N \in T$

Proof

Step	Hyp	Ref	Expression
1		un0addcl.1	$⊢ φ \to S \subseteq ℂ$
2		un0addcl.2	$⊢ T = S \cup \{0\}$
3		un0addcl.3	$⊢ (φ \land (M \in S \land N \in S)) \to M + N \in S$
4	2	eleq2i	$⊢ N \in T \leftrightarrow N \in (S \cup \{0\})$
5		elun	$⊢ N \in (S \cup \{0\}) \leftrightarrow (N \in S \lor N \in \{0\})$
6	4 5	bitri	$⊢ N \in T \leftrightarrow (N \in S \lor N \in \{0\})$
7	2	eleq2i	$⊢ M \in T \leftrightarrow M \in (S \cup \{0\})$
8		elun	$⊢ M \in (S \cup \{0\}) \leftrightarrow (M \in S \lor M \in \{0\})$
9	7 8	bitri	$⊢ M \in T \leftrightarrow (M \in S \lor M \in \{0\})$
10		ssun1	$⊢ S \subseteq S \cup \{0\}$
11	10 2	sseqtrri	$⊢ S \subseteq T$
12	11 3	sselid	$⊢ (φ \land (M \in S \land N \in S)) \to M + N \in T$
13	12	expr	$⊢ (φ \land M \in S) \to (N \in S \to M + N \in T)$
14	1	sselda	$⊢ (φ \land N \in S) \to N \in ℂ$
15	14	addlidd	$⊢ (φ \land N \in S) \to 0 + N = N$
16	11	a1i	$⊢ φ \to S \subseteq T$
17	16	sselda	$⊢ (φ \land N \in S) \to N \in T$
18	15 17	eqeltrd	$⊢ (φ \land N \in S) \to 0 + N \in T$
19		elsni	$⊢ M \in \{0\} \to M = 0$
20	19	oveq1d	$⊢ M \in \{0\} \to M + N = 0 + N$
21	20	eleq1d	$⊢ M \in \{0\} \to (M + N \in T \leftrightarrow 0 + N \in T)$
22	18 21	syl5ibrcom	$⊢ (φ \land N \in S) \to (M \in \{0\} \to M + N \in T)$
23	22	impancom	$⊢ (φ \land M \in \{0\}) \to (N \in S \to M + N \in T)$
24	13 23	jaodan	$⊢ (φ \land (M \in S \lor M \in \{0\})) \to (N \in S \to M + N \in T)$
25	9 24	sylan2b	$⊢ (φ \land M \in T) \to (N \in S \to M + N \in T)$
26		0cnd	$⊢ φ \to 0 \in ℂ$
27	26	snssd	$⊢ φ \to \{0\} \subseteq ℂ$
28	1 27	unssd	$⊢ φ \to S \cup \{0\} \subseteq ℂ$
29	2 28	eqsstrid	$⊢ φ \to T \subseteq ℂ$
30	29	sselda	$⊢ (φ \land M \in T) \to M \in ℂ$
31	30	addridd	$⊢ (φ \land M \in T) \to M + 0 = M$
32		simpr	$⊢ (φ \land M \in T) \to M \in T$
33	31 32	eqeltrd	$⊢ (φ \land M \in T) \to M + 0 \in T$
34		elsni	$⊢ N \in \{0\} \to N = 0$
35	34	oveq2d	$⊢ N \in \{0\} \to M + N = M + 0$
36	35	eleq1d	$⊢ N \in \{0\} \to (M + N \in T \leftrightarrow M + 0 \in T)$
37	33 36	syl5ibrcom	$⊢ (φ \land M \in T) \to (N \in \{0\} \to M + N \in T)$
38	25 37	jaod	$⊢ (φ \land M \in T) \to ((N \in S \lor N \in \{0\}) \to M + N \in T)$
39	6 38	biimtrid	$⊢ (φ \land M \in T) \to (N \in T \to M + N \in T)$
40	39	impr	$⊢ (φ \land (M \in T \land N \in T)) \to M + N \in T$

Metamath Proof Explorer

Theorem un0addcl

Proof