# Metamath Proof Explorer

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

Ref Expression
Assertion zaddcl ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to {M}+{N}\in ℤ$

### Proof

Step Hyp Ref Expression
1 elz2 ${⊢}{M}\in ℤ↔\exists {x}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℕ\phantom{\rule{.4em}{0ex}}{M}={x}-{y}$
2 elz2 ${⊢}{N}\in ℤ↔\exists {z}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {w}\in ℕ\phantom{\rule{.4em}{0ex}}{N}={z}-{w}$
3 reeanv ${⊢}\exists {x}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {z}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\exists {y}\in ℕ\phantom{\rule{.4em}{0ex}}{M}={x}-{y}\wedge \exists {w}\in ℕ\phantom{\rule{.4em}{0ex}}{N}={z}-{w}\right)↔\left(\exists {x}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℕ\phantom{\rule{.4em}{0ex}}{M}={x}-{y}\wedge \exists {z}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {w}\in ℕ\phantom{\rule{.4em}{0ex}}{N}={z}-{w}\right)$
4 reeanv ${⊢}\exists {y}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {w}\in ℕ\phantom{\rule{.4em}{0ex}}\left({M}={x}-{y}\wedge {N}={z}-{w}\right)↔\left(\exists {y}\in ℕ\phantom{\rule{.4em}{0ex}}{M}={x}-{y}\wedge \exists {w}\in ℕ\phantom{\rule{.4em}{0ex}}{N}={z}-{w}\right)$
5 nnaddcl ${⊢}\left({x}\in ℕ\wedge {z}\in ℕ\right)\to {x}+{z}\in ℕ$
6 5 adantr ${⊢}\left(\left({x}\in ℕ\wedge {z}\in ℕ\right)\wedge \left({y}\in ℕ\wedge {w}\in ℕ\right)\right)\to {x}+{z}\in ℕ$
7 nnaddcl ${⊢}\left({y}\in ℕ\wedge {w}\in ℕ\right)\to {y}+{w}\in ℕ$
8 7 adantl ${⊢}\left(\left({x}\in ℕ\wedge {z}\in ℕ\right)\wedge \left({y}\in ℕ\wedge {w}\in ℕ\right)\right)\to {y}+{w}\in ℕ$
9 nncn ${⊢}{x}\in ℕ\to {x}\in ℂ$
10 nncn ${⊢}{z}\in ℕ\to {z}\in ℂ$
11 9 10 anim12i ${⊢}\left({x}\in ℕ\wedge {z}\in ℕ\right)\to \left({x}\in ℂ\wedge {z}\in ℂ\right)$
12 nncn ${⊢}{y}\in ℕ\to {y}\in ℂ$
13 nncn ${⊢}{w}\in ℕ\to {w}\in ℂ$
14 12 13 anim12i ${⊢}\left({y}\in ℕ\wedge {w}\in ℕ\right)\to \left({y}\in ℂ\wedge {w}\in ℂ\right)$
15 addsub4 ${⊢}\left(\left({x}\in ℂ\wedge {z}\in ℂ\right)\wedge \left({y}\in ℂ\wedge {w}\in ℂ\right)\right)\to {x}+{z}-\left({y}+{w}\right)=\left({x}-{y}\right)+{z}-{w}$
16 11 14 15 syl2an ${⊢}\left(\left({x}\in ℕ\wedge {z}\in ℕ\right)\wedge \left({y}\in ℕ\wedge {w}\in ℕ\right)\right)\to {x}+{z}-\left({y}+{w}\right)=\left({x}-{y}\right)+{z}-{w}$
17 16 eqcomd ${⊢}\left(\left({x}\in ℕ\wedge {z}\in ℕ\right)\wedge \left({y}\in ℕ\wedge {w}\in ℕ\right)\right)\to \left({x}-{y}\right)+{z}-{w}={x}+{z}-\left({y}+{w}\right)$
18 rspceov ${⊢}\left({x}+{z}\in ℕ\wedge {y}+{w}\in ℕ\wedge \left({x}-{y}\right)+{z}-{w}={x}+{z}-\left({y}+{w}\right)\right)\to \exists {u}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {v}\in ℕ\phantom{\rule{.4em}{0ex}}\left({x}-{y}\right)+{z}-{w}={u}-{v}$
19 6 8 17 18 syl3anc ${⊢}\left(\left({x}\in ℕ\wedge {z}\in ℕ\right)\wedge \left({y}\in ℕ\wedge {w}\in ℕ\right)\right)\to \exists {u}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {v}\in ℕ\phantom{\rule{.4em}{0ex}}\left({x}-{y}\right)+{z}-{w}={u}-{v}$
20 elz2 ${⊢}\left({x}-{y}\right)+{z}-{w}\in ℤ↔\exists {u}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {v}\in ℕ\phantom{\rule{.4em}{0ex}}\left({x}-{y}\right)+{z}-{w}={u}-{v}$
21 19 20 sylibr ${⊢}\left(\left({x}\in ℕ\wedge {z}\in ℕ\right)\wedge \left({y}\in ℕ\wedge {w}\in ℕ\right)\right)\to \left({x}-{y}\right)+{z}-{w}\in ℤ$
22 oveq12 ${⊢}\left({M}={x}-{y}\wedge {N}={z}-{w}\right)\to {M}+{N}=\left({x}-{y}\right)+{z}-{w}$
23 22 eleq1d ${⊢}\left({M}={x}-{y}\wedge {N}={z}-{w}\right)\to \left({M}+{N}\in ℤ↔\left({x}-{y}\right)+{z}-{w}\in ℤ\right)$
24 21 23 syl5ibrcom ${⊢}\left(\left({x}\in ℕ\wedge {z}\in ℕ\right)\wedge \left({y}\in ℕ\wedge {w}\in ℕ\right)\right)\to \left(\left({M}={x}-{y}\wedge {N}={z}-{w}\right)\to {M}+{N}\in ℤ\right)$
25 24 rexlimdvva ${⊢}\left({x}\in ℕ\wedge {z}\in ℕ\right)\to \left(\exists {y}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {w}\in ℕ\phantom{\rule{.4em}{0ex}}\left({M}={x}-{y}\wedge {N}={z}-{w}\right)\to {M}+{N}\in ℤ\right)$
26 4 25 syl5bir ${⊢}\left({x}\in ℕ\wedge {z}\in ℕ\right)\to \left(\left(\exists {y}\in ℕ\phantom{\rule{.4em}{0ex}}{M}={x}-{y}\wedge \exists {w}\in ℕ\phantom{\rule{.4em}{0ex}}{N}={z}-{w}\right)\to {M}+{N}\in ℤ\right)$
27 26 rexlimivv ${⊢}\exists {x}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {z}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\exists {y}\in ℕ\phantom{\rule{.4em}{0ex}}{M}={x}-{y}\wedge \exists {w}\in ℕ\phantom{\rule{.4em}{0ex}}{N}={z}-{w}\right)\to {M}+{N}\in ℤ$
28 3 27 sylbir ${⊢}\left(\exists {x}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℕ\phantom{\rule{.4em}{0ex}}{M}={x}-{y}\wedge \exists {z}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {w}\in ℕ\phantom{\rule{.4em}{0ex}}{N}={z}-{w}\right)\to {M}+{N}\in ℤ$
29 1 2 28 syl2anb ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to {M}+{N}\in ℤ$