This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 addlidd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑆 ) → ( 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 addridd ⊢ ( ( 𝜑 ∧ 𝑀 ∈ 𝑇 ) → ( 𝑀 + 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 biimtrid ⊢ ( ( 𝜑 ∧ 𝑀 ∈ 𝑇 ) → ( 𝑁 ∈ 𝑇 → ( 𝑀 + 𝑁 ) ∈ 𝑇 ) )
40 39 impr ⊢ ( ( 𝜑 ∧ ( 𝑀 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ) ) → ( 𝑀 + 𝑁 ) ∈ 𝑇 )