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 MNM+N

Proof

Step Hyp Ref Expression
1 elz2 MxyM=xy
2 elz2 NzwN=zw
3 reeanv xzyM=xywN=zwxyM=xyzwN=zw
4 reeanv ywM=xyN=zwyM=xywN=zw
5 nnaddcl xzx+z
6 5 adantr xzywx+z
7 nnaddcl ywy+w
8 7 adantl xzywy+w
9 nncn xx
10 nncn zz
11 9 10 anim12i xzxz
12 nncn yy
13 nncn ww
14 12 13 anim12i ywyw
15 addsub4 xzywx+z-y+w=xy+z-w
16 11 14 15 syl2an xzywx+z-y+w=xy+z-w
17 16 eqcomd xzywxy+z-w=x+z-y+w
18 rspceov x+zy+wxy+z-w=x+z-y+wuvxy+z-w=uv
19 6 8 17 18 syl3anc xzywuvxy+z-w=uv
20 elz2 xy+z-wuvxy+z-w=uv
21 19 20 sylibr xzywxy+z-w
22 oveq12 M=xyN=zwM+N=xy+z-w
23 22 eleq1d M=xyN=zwM+Nxy+z-w
24 21 23 syl5ibrcom xzywM=xyN=zwM+N
25 24 rexlimdvva xzywM=xyN=zwM+N
26 4 25 syl5bir xzyM=xywN=zwM+N
27 26 rexlimivv xzyM=xywN=zwM+N
28 3 27 sylbir xyM=xyzwN=zwM+N
29 1 2 28 syl2anb MNM+N