This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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