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