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 \in ℤ \land N \in ℤ) \to M + N \in ℤ$

Proof

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

Metamath Proof Explorer

Theorem zaddcl

Proof