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 
|- ( ph -> S C_ CC )
un0addcl.2 
|- T = ( S u. { 0 } )
un0addcl.3 
|- ( ( ph /\ ( M e. S /\ N e. S ) ) -> ( M + N ) e. S )
Assertion un0addcl 
|- ( ( ph /\ ( M e. T /\ N e. T ) ) -> ( M + N ) e. T )

Proof

Step Hyp Ref Expression
1 un0addcl.1 
 |-  ( ph -> S C_ CC )
2 un0addcl.2 
 |-  T = ( S u. { 0 } )
3 un0addcl.3 
 |-  ( ( ph /\ ( M e. S /\ N e. S ) ) -> ( M + N ) e. S )
4 2 eleq2i 
 |-  ( N e. T <-> N e. ( S u. { 0 } ) )
5 elun 
 |-  ( N e. ( S u. { 0 } ) <-> ( N e. S \/ N e. { 0 } ) )
6 4 5 bitri 
 |-  ( N e. T <-> ( N e. S \/ N e. { 0 } ) )
7 2 eleq2i 
 |-  ( M e. T <-> M e. ( S u. { 0 } ) )
8 elun 
 |-  ( M e. ( S u. { 0 } ) <-> ( M e. S \/ M e. { 0 } ) )
9 7 8 bitri 
 |-  ( M e. T <-> ( M e. S \/ M e. { 0 } ) )
10 ssun1 
 |-  S C_ ( S u. { 0 } )
11 10 2 sseqtrri 
 |-  S C_ T
12 11 3 sselid 
 |-  ( ( ph /\ ( M e. S /\ N e. S ) ) -> ( M + N ) e. T )
13 12 expr 
 |-  ( ( ph /\ M e. S ) -> ( N e. S -> ( M + N ) e. T ) )
14 1 sselda 
 |-  ( ( ph /\ N e. S ) -> N e. CC )
15 14 addid2d 
 |-  ( ( ph /\ N e. S ) -> ( 0 + N ) = N )
16 11 a1i 
 |-  ( ph -> S C_ T )
17 16 sselda 
 |-  ( ( ph /\ N e. S ) -> N e. T )
18 15 17 eqeltrd 
 |-  ( ( ph /\ N e. S ) -> ( 0 + N ) e. T )
19 elsni 
 |-  ( M e. { 0 } -> M = 0 )
20 19 oveq1d 
 |-  ( M e. { 0 } -> ( M + N ) = ( 0 + N ) )
21 20 eleq1d 
 |-  ( M e. { 0 } -> ( ( M + N ) e. T <-> ( 0 + N ) e. T ) )
22 18 21 syl5ibrcom 
 |-  ( ( ph /\ N e. S ) -> ( M e. { 0 } -> ( M + N ) e. T ) )
23 22 impancom 
 |-  ( ( ph /\ M e. { 0 } ) -> ( N e. S -> ( M + N ) e. T ) )
24 13 23 jaodan 
 |-  ( ( ph /\ ( M e. S \/ M e. { 0 } ) ) -> ( N e. S -> ( M + N ) e. T ) )
25 9 24 sylan2b 
 |-  ( ( ph /\ M e. T ) -> ( N e. S -> ( M + N ) e. T ) )
26 0cnd 
 |-  ( ph -> 0 e. CC )
27 26 snssd 
 |-  ( ph -> { 0 } C_ CC )
28 1 27 unssd 
 |-  ( ph -> ( S u. { 0 } ) C_ CC )
29 2 28 eqsstrid 
 |-  ( ph -> T C_ CC )
30 29 sselda 
 |-  ( ( ph /\ M e. T ) -> M e. CC )
31 30 addid1d 
 |-  ( ( ph /\ M e. T ) -> ( M + 0 ) = M )
32 simpr 
 |-  ( ( ph /\ M e. T ) -> M e. T )
33 31 32 eqeltrd 
 |-  ( ( ph /\ M e. T ) -> ( M + 0 ) e. T )
34 elsni 
 |-  ( N e. { 0 } -> N = 0 )
35 34 oveq2d 
 |-  ( N e. { 0 } -> ( M + N ) = ( M + 0 ) )
36 35 eleq1d 
 |-  ( N e. { 0 } -> ( ( M + N ) e. T <-> ( M + 0 ) e. T ) )
37 33 36 syl5ibrcom 
 |-  ( ( ph /\ M e. T ) -> ( N e. { 0 } -> ( M + N ) e. T ) )
38 25 37 jaod 
 |-  ( ( ph /\ M e. T ) -> ( ( N e. S \/ N e. { 0 } ) -> ( M + N ) e. T ) )
39 6 38 syl5bi 
 |-  ( ( ph /\ M e. T ) -> ( N e. T -> ( M + N ) e. T ) )
40 39 impr 
 |-  ( ( ph /\ ( M e. T /\ N e. T ) ) -> ( M + N ) e. T )