elz2

Description: Membership in the set of integers. Commonly used in constructions of the integers as equivalence classes under subtraction of the positive integers. (Contributed by Mario Carneiro, 16-May-2014)

		Ref	Expression
	Assertion	elz2	$⊢ N \in ℤ \leftrightarrow \exists x \in ℕ \exists y \in ℕ N = x - y$

Proof

Step	Hyp	Ref	Expression
1		elznn0	$⊢ N \in ℤ \leftrightarrow (N \in ℝ \land (N \in ℕ_{0} \lor - N \in ℕ_{0}))$
2		nn0p1nn	$⊢ N \in ℕ_{0} \to N + 1 \in ℕ$
3	2	adantl	$⊢ (N \in ℝ \land N \in ℕ_{0}) \to N + 1 \in ℕ$
4		1nn	$⊢ 1 \in ℕ$
5	4	a1i	$⊢ (N \in ℝ \land N \in ℕ_{0}) \to 1 \in ℕ$
6		recn	$⊢ N \in ℝ \to N \in ℂ$
7	6	adantr	$⊢ (N \in ℝ \land N \in ℕ_{0}) \to N \in ℂ$
8		ax-1cn	$⊢ 1 \in ℂ$
9		pncan	$⊢ (N \in ℂ \land 1 \in ℂ) \to N + 1 - 1 = N$
10	7 8 9	sylancl	$⊢ (N \in ℝ \land N \in ℕ_{0}) \to N + 1 - 1 = N$
11	10	eqcomd	$⊢ (N \in ℝ \land N \in ℕ_{0}) \to N = N + 1 - 1$
12		rspceov	$⊢ (N + 1 \in ℕ \land 1 \in ℕ \land N = N + 1 - 1) \to \exists x \in ℕ \exists y \in ℕ N = x - y$
13	3 5 11 12	syl3anc	$⊢ (N \in ℝ \land N \in ℕ_{0}) \to \exists x \in ℕ \exists y \in ℕ N = x - y$
14	4	a1i	$⊢ (N \in ℝ \land - N \in ℕ_{0}) \to 1 \in ℕ$
15	6	adantr	$⊢ (N \in ℝ \land - N \in ℕ_{0}) \to N \in ℂ$
16		negsub	$⊢ (1 \in ℂ \land N \in ℂ) \to 1 + -N = 1 - N$
17	8 15 16	sylancr	$⊢ (N \in ℝ \land - N \in ℕ_{0}) \to 1 + -N = 1 - N$
18		simpr	$⊢ (N \in ℝ \land - N \in ℕ_{0}) \to - N \in ℕ_{0}$
19		nnnn0addcl	$⊢ (1 \in ℕ \land - N \in ℕ_{0}) \to 1 + -N \in ℕ$
20	4 18 19	sylancr	$⊢ (N \in ℝ \land - N \in ℕ_{0}) \to 1 + -N \in ℕ$
21	17 20	eqeltrrd	$⊢ (N \in ℝ \land - N \in ℕ_{0}) \to 1 - N \in ℕ$
22		nncan	$⊢ (1 \in ℂ \land N \in ℂ) \to 1 - (1 - N) = N$
23	8 15 22	sylancr	$⊢ (N \in ℝ \land - N \in ℕ_{0}) \to 1 - (1 - N) = N$
24	23	eqcomd	$⊢ (N \in ℝ \land - N \in ℕ_{0}) \to N = 1 - (1 - N)$
25		rspceov	$⊢ (1 \in ℕ \land 1 - N \in ℕ \land N = 1 - (1 - N)) \to \exists x \in ℕ \exists y \in ℕ N = x - y$
26	14 21 24 25	syl3anc	$⊢ (N \in ℝ \land - N \in ℕ_{0}) \to \exists x \in ℕ \exists y \in ℕ N = x - y$
27	13 26	jaodan	$⊢ (N \in ℝ \land (N \in ℕ_{0} \lor - N \in ℕ_{0})) \to \exists x \in ℕ \exists y \in ℕ N = x - y$
28		nnre	$⊢ x \in ℕ \to x \in ℝ$
29		nnre	$⊢ y \in ℕ \to y \in ℝ$
30		resubcl	$⊢ (x \in ℝ \land y \in ℝ) \to x - y \in ℝ$
31	28 29 30	syl2an	$⊢ (x \in ℕ \land y \in ℕ) \to x - y \in ℝ$
32		letric	$⊢ (y \in ℝ \land x \in ℝ) \to (y \leq x \lor x \leq y)$
33	29 28 32	syl2anr	$⊢ (x \in ℕ \land y \in ℕ) \to (y \leq x \lor x \leq y)$
34		nnnn0	$⊢ y \in ℕ \to y \in ℕ_{0}$
35		nnnn0	$⊢ x \in ℕ \to x \in ℕ_{0}$
36		nn0sub	$⊢ (y \in ℕ_{0} \land x \in ℕ_{0}) \to (y \leq x \leftrightarrow x - y \in ℕ_{0})$
37	34 35 36	syl2anr	$⊢ (x \in ℕ \land y \in ℕ) \to (y \leq x \leftrightarrow x - y \in ℕ_{0})$
38		nn0sub	$⊢ (x \in ℕ_{0} \land y \in ℕ_{0}) \to (x \leq y \leftrightarrow y - x \in ℕ_{0})$
39	35 34 38	syl2an	$⊢ (x \in ℕ \land y \in ℕ) \to (x \leq y \leftrightarrow y - x \in ℕ_{0})$
40		nncn	$⊢ x \in ℕ \to x \in ℂ$
41		nncn	$⊢ y \in ℕ \to y \in ℂ$
42		negsubdi2	$⊢ (x \in ℂ \land y \in ℂ) \to - (x - y) = y - x$
43	40 41 42	syl2an	$⊢ (x \in ℕ \land y \in ℕ) \to - (x - y) = y - x$
44	43	eleq1d	$⊢ (x \in ℕ \land y \in ℕ) \to (- (x - y) \in ℕ_{0} \leftrightarrow y - x \in ℕ_{0})$
45	39 44	bitr4d	$⊢ (x \in ℕ \land y \in ℕ) \to (x \leq y \leftrightarrow - (x - y) \in ℕ_{0})$
46	37 45	orbi12d	$⊢ (x \in ℕ \land y \in ℕ) \to ((y \leq x \lor x \leq y) \leftrightarrow (x - y \in ℕ_{0} \lor - (x - y) \in ℕ_{0}))$
47	33 46	mpbid	$⊢ (x \in ℕ \land y \in ℕ) \to (x - y \in ℕ_{0} \lor - (x - y) \in ℕ_{0})$
48	31 47	jca	$⊢ (x \in ℕ \land y \in ℕ) \to (x - y \in ℝ \land (x - y \in ℕ_{0} \lor - (x - y) \in ℕ_{0}))$
49		eleq1	$⊢ N = x - y \to (N \in ℝ \leftrightarrow x - y \in ℝ)$
50		eleq1	$⊢ N = x - y \to (N \in ℕ_{0} \leftrightarrow x - y \in ℕ_{0})$
51		negeq	$⊢ N = x - y \to - N = - (x - y)$
52	51	eleq1d	$⊢ N = x - y \to (- N \in ℕ_{0} \leftrightarrow - (x - y) \in ℕ_{0})$
53	50 52	orbi12d	$⊢ N = x - y \to ((N \in ℕ_{0} \lor - N \in ℕ_{0}) \leftrightarrow (x - y \in ℕ_{0} \lor - (x - y) \in ℕ_{0}))$
54	49 53	anbi12d	$⊢ N = x - y \to ((N \in ℝ \land (N \in ℕ_{0} \lor - N \in ℕ_{0})) \leftrightarrow (x - y \in ℝ \land (x - y \in ℕ_{0} \lor - (x - y) \in ℕ_{0})))$
55	48 54	syl5ibrcom	$⊢ (x \in ℕ \land y \in ℕ) \to (N = x - y \to (N \in ℝ \land (N \in ℕ_{0} \lor - N \in ℕ_{0})))$
56	55	rexlimivv	$⊢ \exists x \in ℕ \exists y \in ℕ N = x - y \to (N \in ℝ \land (N \in ℕ_{0} \lor - N \in ℕ_{0}))$
57	27 56	impbii	$⊢ (N \in ℝ \land (N \in ℕ_{0} \lor - N \in ℕ_{0})) \leftrightarrow \exists x \in ℕ \exists y \in ℕ N = x - y$
58	1 57	bitri	$⊢ N \in ℤ \leftrightarrow \exists x \in ℕ \exists y \in ℕ N = x - y$

Metamath Proof Explorer

Theorem elz2

Proof