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

Metamath Proof Explorer

Theorem zaddcl

Description: Closure of addition of integers. (Contributed by NM, 9-May-2004) (Proof shortened by Mario Carneiro, 16-May-2014)

Ref Expression
Assertion zaddcl 
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M + N ) e. ZZ )

Proof

Step Hyp Ref Expression
1 elz2 
 |-  ( M e. ZZ <-> E. x e. NN E. y e. NN M = ( x - y ) )
2 elz2 
 |-  ( N e. ZZ <-> E. z e. NN E. w e. NN N = ( z - w ) )
3 reeanv 
 |-  ( E. x e. NN E. z e. NN ( E. y e. NN M = ( x - y ) /\ E. w e. NN N = ( z - w ) ) <-> ( E. x e. NN E. y e. NN M = ( x - y ) /\ E. z e. NN E. w e. NN N = ( z - w ) ) )
4 reeanv 
 |-  ( E. y e. NN E. w e. NN ( M = ( x - y ) /\ N = ( z - w ) ) <-> ( E. y e. NN M = ( x - y ) /\ E. w e. NN N = ( z - w ) ) )
5 nnaddcl 
 |-  ( ( x e. NN /\ z e. NN ) -> ( x + z ) e. NN )
6 5 adantr 
 |-  ( ( ( x e. NN /\ z e. NN ) /\ ( y e. NN /\ w e. NN ) ) -> ( x + z ) e. NN )
7 nnaddcl 
 |-  ( ( y e. NN /\ w e. NN ) -> ( y + w ) e. NN )
8 7 adantl 
 |-  ( ( ( x e. NN /\ z e. NN ) /\ ( y e. NN /\ w e. NN ) ) -> ( y + w ) e. NN )
9 nncn 
 |-  ( x e. NN -> x e. CC )
10 nncn 
 |-  ( z e. NN -> z e. CC )
11 9 10 anim12i 
 |-  ( ( x e. NN /\ z e. NN ) -> ( x e. CC /\ z e. CC ) )
12 nncn 
 |-  ( y e. NN -> y e. CC )
13 nncn 
 |-  ( w e. NN -> w e. CC )
14 12 13 anim12i 
 |-  ( ( y e. NN /\ w e. NN ) -> ( y e. CC /\ w e. CC ) )
15 addsub4 
 |-  ( ( ( x e. CC /\ z e. CC ) /\ ( y e. CC /\ w e. CC ) ) -> ( ( x + z ) - ( y + w ) ) = ( ( x - y ) + ( z - w ) ) )
16 11 14 15 syl2an 
 |-  ( ( ( x e. NN /\ z e. NN ) /\ ( y e. NN /\ w e. NN ) ) -> ( ( x + z ) - ( y + w ) ) = ( ( x - y ) + ( z - w ) ) )
17 16 eqcomd 
 |-  ( ( ( x e. NN /\ z e. NN ) /\ ( y e. NN /\ w e. NN ) ) -> ( ( x - y ) + ( z - w ) ) = ( ( x + z ) - ( y + w ) ) )
18 rspceov 
 |-  ( ( ( x + z ) e. NN /\ ( y + w ) e. NN /\ ( ( x - y ) + ( z - w ) ) = ( ( x + z ) - ( y + w ) ) ) -> E. u e. NN E. v e. NN ( ( x - y ) + ( z - w ) ) = ( u - v ) )
19 6 8 17 18 syl3anc 
 |-  ( ( ( x e. NN /\ z e. NN ) /\ ( y e. NN /\ w e. NN ) ) -> E. u e. NN E. v e. NN ( ( x - y ) + ( z - w ) ) = ( u - v ) )
20 elz2 
 |-  ( ( ( x - y ) + ( z - w ) ) e. ZZ <-> E. u e. NN E. v e. NN ( ( x - y ) + ( z - w ) ) = ( u - v ) )
21 19 20 sylibr 
 |-  ( ( ( x e. NN /\ z e. NN ) /\ ( y e. NN /\ w e. NN ) ) -> ( ( x - y ) + ( z - w ) ) e. ZZ )
22 oveq12 
 |-  ( ( M = ( x - y ) /\ N = ( z - w ) ) -> ( M + N ) = ( ( x - y ) + ( z - w ) ) )
23 22 eleq1d 
 |-  ( ( M = ( x - y ) /\ N = ( z - w ) ) -> ( ( M + N ) e. ZZ <-> ( ( x - y ) + ( z - w ) ) e. ZZ ) )
24 21 23 syl5ibrcom 
 |-  ( ( ( x e. NN /\ z e. NN ) /\ ( y e. NN /\ w e. NN ) ) -> ( ( M = ( x - y ) /\ N = ( z - w ) ) -> ( M + N ) e. ZZ ) )
25 24 rexlimdvva 
 |-  ( ( x e. NN /\ z e. NN ) -> ( E. y e. NN E. w e. NN ( M = ( x - y ) /\ N = ( z - w ) ) -> ( M + N ) e. ZZ ) )
26 4 25 biimtrrid 
 |-  ( ( x e. NN /\ z e. NN ) -> ( ( E. y e. NN M = ( x - y ) /\ E. w e. NN N = ( z - w ) ) -> ( M + N ) e. ZZ ) )
27 26 rexlimivv 
 |-  ( E. x e. NN E. z e. NN ( E. y e. NN M = ( x - y ) /\ E. w e. NN N = ( z - w ) ) -> ( M + N ) e. ZZ )
28 3 27 sylbir 
 |-  ( ( E. x e. NN E. y e. NN M = ( x - y ) /\ E. z e. NN E. w e. NN N = ( z - w ) ) -> ( M + N ) e. ZZ )
29 1 2 28 syl2anb 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M + N ) e. ZZ )