Theorem 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	⊢ ( 𝑁 ∈ ℤ ↔ ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ 𝑁 = ( 𝑥 − 𝑦 ) )

Proof

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