Step | Hyp | Ref
| Expression |
1 | | bitsf 15522 |
. 2
⊢
bits:ℤ⟶𝒫 ℕ0 |
2 | | simpl 476 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → 𝑥 ∈
ℤ) |
3 | 2 | zcnd 11811 |
. . . . . . 7
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → 𝑥 ∈
ℂ) |
4 | 3 | adantr 474 |
. . . . . 6
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧
(bits‘𝑥) =
(bits‘𝑦))) →
𝑥 ∈
ℂ) |
5 | | simpr 479 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → 𝑦 ∈
ℤ) |
6 | 5 | zcnd 11811 |
. . . . . . 7
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → 𝑦 ∈
ℂ) |
7 | 6 | adantr 474 |
. . . . . 6
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧
(bits‘𝑥) =
(bits‘𝑦))) →
𝑦 ∈
ℂ) |
8 | 4 | negcld 10700 |
. . . . . . 7
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧
(bits‘𝑥) =
(bits‘𝑦))) →
-𝑥 ∈
ℂ) |
9 | 7 | negcld 10700 |
. . . . . . 7
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧
(bits‘𝑥) =
(bits‘𝑦))) →
-𝑦 ∈
ℂ) |
10 | | 1cnd 10351 |
. . . . . . 7
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧
(bits‘𝑥) =
(bits‘𝑦))) → 1
∈ ℂ) |
11 | | simprr 791 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧
(bits‘𝑥) =
(bits‘𝑦))) →
(bits‘𝑥) =
(bits‘𝑦)) |
12 | 11 | difeq2d 3955 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧
(bits‘𝑥) =
(bits‘𝑦))) →
(ℕ0 ∖ (bits‘𝑥)) = (ℕ0 ∖
(bits‘𝑦))) |
13 | | bitscmp 15533 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℤ →
(ℕ0 ∖ (bits‘𝑥)) = (bits‘(-𝑥 − 1))) |
14 | 13 | ad2antrr 719 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧
(bits‘𝑥) =
(bits‘𝑦))) →
(ℕ0 ∖ (bits‘𝑥)) = (bits‘(-𝑥 − 1))) |
15 | | bitscmp 15533 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℤ →
(ℕ0 ∖ (bits‘𝑦)) = (bits‘(-𝑦 − 1))) |
16 | 15 | ad2antlr 720 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧
(bits‘𝑥) =
(bits‘𝑦))) →
(ℕ0 ∖ (bits‘𝑦)) = (bits‘(-𝑦 − 1))) |
17 | 12, 14, 16 | 3eqtr3d 2869 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧
(bits‘𝑥) =
(bits‘𝑦))) →
(bits‘(-𝑥 − 1))
= (bits‘(-𝑦 −
1))) |
18 | | nnm1nn0 11661 |
. . . . . . . . . . 11
⊢ (-𝑥 ∈ ℕ → (-𝑥 − 1) ∈
ℕ0) |
19 | 18 | ad2antrl 721 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧
(bits‘𝑥) =
(bits‘𝑦))) →
(-𝑥 − 1) ∈
ℕ0) |
20 | | fvres 6452 |
. . . . . . . . . 10
⊢ ((-𝑥 − 1) ∈
ℕ0 → ((bits ↾ ℕ0)‘(-𝑥 − 1)) =
(bits‘(-𝑥 −
1))) |
21 | 19, 20 | syl 17 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧
(bits‘𝑥) =
(bits‘𝑦))) →
((bits ↾ ℕ0)‘(-𝑥 − 1)) = (bits‘(-𝑥 − 1))) |
22 | | ominf 8441 |
. . . . . . . . . . . . . . . . 17
⊢ ¬
ω ∈ Fin |
23 | | nn0ennn 13073 |
. . . . . . . . . . . . . . . . . . 19
⊢
ℕ0 ≈ ℕ |
24 | | nnenom 13074 |
. . . . . . . . . . . . . . . . . . 19
⊢ ℕ
≈ ω |
25 | 23, 24 | entr2i 8277 |
. . . . . . . . . . . . . . . . . 18
⊢ ω
≈ ℕ0 |
26 | | enfii 8446 |
. . . . . . . . . . . . . . . . . 18
⊢
((ℕ0 ∈ Fin ∧ ω ≈
ℕ0) → ω ∈ Fin) |
27 | 25, 26 | mpan2 684 |
. . . . . . . . . . . . . . . . 17
⊢
(ℕ0 ∈ Fin → ω ∈
Fin) |
28 | 22, 27 | mto 189 |
. . . . . . . . . . . . . . . 16
⊢ ¬
ℕ0 ∈ Fin |
29 | | difinf 8499 |
. . . . . . . . . . . . . . . 16
⊢ ((¬
ℕ0 ∈ Fin ∧ (bits‘𝑥) ∈ Fin) → ¬
(ℕ0 ∖ (bits‘𝑥)) ∈ Fin) |
30 | 28, 29 | mpan 683 |
. . . . . . . . . . . . . . 15
⊢
((bits‘𝑥)
∈ Fin → ¬ (ℕ0 ∖ (bits‘𝑥)) ∈ Fin) |
31 | | bitsfi 15532 |
. . . . . . . . . . . . . . . . 17
⊢ ((-𝑥 − 1) ∈
ℕ0 → (bits‘(-𝑥 − 1)) ∈ Fin) |
32 | 19, 31 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧
(bits‘𝑥) =
(bits‘𝑦))) →
(bits‘(-𝑥 − 1))
∈ Fin) |
33 | 14, 32 | eqeltrd 2906 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧
(bits‘𝑥) =
(bits‘𝑦))) →
(ℕ0 ∖ (bits‘𝑥)) ∈ Fin) |
34 | 30, 33 | nsyl3 136 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧
(bits‘𝑥) =
(bits‘𝑦))) →
¬ (bits‘𝑥) ∈
Fin) |
35 | 11, 34 | eqneltrrd 2926 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧
(bits‘𝑥) =
(bits‘𝑦))) →
¬ (bits‘𝑦) ∈
Fin) |
36 | | bitsfi 15532 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ0
→ (bits‘𝑦)
∈ Fin) |
37 | 35, 36 | nsyl 138 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧
(bits‘𝑥) =
(bits‘𝑦))) →
¬ 𝑦 ∈
ℕ0) |
38 | 5 | znegcld 11812 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → -𝑦 ∈
ℤ) |
39 | | elznn 11720 |
. . . . . . . . . . . . . . . . 17
⊢ (-𝑦 ∈ ℤ ↔ (-𝑦 ∈ ℝ ∧ (-𝑦 ∈ ℕ ∨ --𝑦 ∈
ℕ0))) |
40 | 39 | simprbi 492 |
. . . . . . . . . . . . . . . 16
⊢ (-𝑦 ∈ ℤ → (-𝑦 ∈ ℕ ∨ --𝑦 ∈
ℕ0)) |
41 | 38, 40 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (-𝑦 ∈ ℕ ∨ --𝑦 ∈
ℕ0)) |
42 | 6 | negnegd 10704 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → --𝑦 = 𝑦) |
43 | 42 | eleq1d 2891 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (--𝑦 ∈ ℕ0
↔ 𝑦 ∈
ℕ0)) |
44 | 43 | orbi2d 946 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → ((-𝑦 ∈ ℕ ∨ --𝑦 ∈ ℕ0)
↔ (-𝑦 ∈ ℕ
∨ 𝑦 ∈
ℕ0))) |
45 | 41, 44 | mpbid 224 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (-𝑦 ∈ ℕ ∨ 𝑦 ∈
ℕ0)) |
46 | 45 | adantr 474 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧
(bits‘𝑥) =
(bits‘𝑦))) →
(-𝑦 ∈ ℕ ∨
𝑦 ∈
ℕ0)) |
47 | 46 | ord 897 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧
(bits‘𝑥) =
(bits‘𝑦))) →
(¬ -𝑦 ∈ ℕ
→ 𝑦 ∈
ℕ0)) |
48 | 37, 47 | mt3d 143 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧
(bits‘𝑥) =
(bits‘𝑦))) →
-𝑦 ∈
ℕ) |
49 | | nnm1nn0 11661 |
. . . . . . . . . . 11
⊢ (-𝑦 ∈ ℕ → (-𝑦 − 1) ∈
ℕ0) |
50 | 48, 49 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧
(bits‘𝑥) =
(bits‘𝑦))) →
(-𝑦 − 1) ∈
ℕ0) |
51 | | fvres 6452 |
. . . . . . . . . 10
⊢ ((-𝑦 − 1) ∈
ℕ0 → ((bits ↾ ℕ0)‘(-𝑦 − 1)) =
(bits‘(-𝑦 −
1))) |
52 | 50, 51 | syl 17 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧
(bits‘𝑥) =
(bits‘𝑦))) →
((bits ↾ ℕ0)‘(-𝑦 − 1)) = (bits‘(-𝑦 − 1))) |
53 | 17, 21, 52 | 3eqtr4d 2871 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧
(bits‘𝑥) =
(bits‘𝑦))) →
((bits ↾ ℕ0)‘(-𝑥 − 1)) = ((bits ↾
ℕ0)‘(-𝑦 − 1))) |
54 | | bitsf1o 15540 |
. . . . . . . . . . 11
⊢ (bits
↾ ℕ0):ℕ0–1-1-onto→(𝒫 ℕ0 ∩
Fin) |
55 | | f1of1 6377 |
. . . . . . . . . . 11
⊢ ((bits
↾ ℕ0):ℕ0–1-1-onto→(𝒫 ℕ0 ∩ Fin)
→ (bits ↾ ℕ0):ℕ0–1-1→(𝒫 ℕ0 ∩
Fin)) |
56 | 54, 55 | ax-mp 5 |
. . . . . . . . . 10
⊢ (bits
↾ ℕ0):ℕ0–1-1→(𝒫 ℕ0 ∩
Fin) |
57 | | f1fveq 6774 |
. . . . . . . . . 10
⊢ (((bits
↾ ℕ0):ℕ0–1-1→(𝒫 ℕ0 ∩ Fin) ∧
((-𝑥 − 1) ∈
ℕ0 ∧ (-𝑦 − 1) ∈ ℕ0))
→ (((bits ↾ ℕ0)‘(-𝑥 − 1)) = ((bits ↾
ℕ0)‘(-𝑦 − 1)) ↔ (-𝑥 − 1) = (-𝑦 − 1))) |
58 | 56, 57 | mpan 683 |
. . . . . . . . 9
⊢ (((-𝑥 − 1) ∈
ℕ0 ∧ (-𝑦 − 1) ∈ ℕ0)
→ (((bits ↾ ℕ0)‘(-𝑥 − 1)) = ((bits ↾
ℕ0)‘(-𝑦 − 1)) ↔ (-𝑥 − 1) = (-𝑦 − 1))) |
59 | 19, 50, 58 | syl2anc 581 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧
(bits‘𝑥) =
(bits‘𝑦))) →
(((bits ↾ ℕ0)‘(-𝑥 − 1)) = ((bits ↾
ℕ0)‘(-𝑦 − 1)) ↔ (-𝑥 − 1) = (-𝑦 − 1))) |
60 | 53, 59 | mpbid 224 |
. . . . . . 7
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧
(bits‘𝑥) =
(bits‘𝑦))) →
(-𝑥 − 1) = (-𝑦 − 1)) |
61 | 8, 9, 10, 60 | subcan2d 10755 |
. . . . . 6
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧
(bits‘𝑥) =
(bits‘𝑦))) →
-𝑥 = -𝑦) |
62 | 4, 7, 61 | neg11d 10725 |
. . . . 5
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧
(bits‘𝑥) =
(bits‘𝑦))) →
𝑥 = 𝑦) |
63 | 62 | expr 450 |
. . . 4
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ -𝑥 ∈ ℕ) →
((bits‘𝑥) =
(bits‘𝑦) → 𝑥 = 𝑦)) |
64 | 3 | negnegd 10704 |
. . . . . . 7
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → --𝑥 = 𝑥) |
65 | 64 | eleq1d 2891 |
. . . . . 6
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (--𝑥 ∈ ℕ0
↔ 𝑥 ∈
ℕ0)) |
66 | 65 | biimpa 470 |
. . . . 5
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ --𝑥 ∈ ℕ0)
→ 𝑥 ∈
ℕ0) |
67 | | simprr 791 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ0
∧ (bits‘𝑥) =
(bits‘𝑦))) →
(bits‘𝑥) =
(bits‘𝑦)) |
68 | | fvres 6452 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℕ0
→ ((bits ↾ ℕ0)‘𝑥) = (bits‘𝑥)) |
69 | 68 | ad2antrl 721 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ0
∧ (bits‘𝑥) =
(bits‘𝑦))) →
((bits ↾ ℕ0)‘𝑥) = (bits‘𝑥)) |
70 | 15 | ad2antlr 720 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ0
∧ (bits‘𝑥) =
(bits‘𝑦))) →
(ℕ0 ∖ (bits‘𝑦)) = (bits‘(-𝑦 − 1))) |
71 | | bitsfi 15532 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℕ0
→ (bits‘𝑥)
∈ Fin) |
72 | 71 | ad2antrl 721 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ0
∧ (bits‘𝑥) =
(bits‘𝑦))) →
(bits‘𝑥) ∈
Fin) |
73 | 67, 72 | eqeltrrd 2907 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ0
∧ (bits‘𝑥) =
(bits‘𝑦))) →
(bits‘𝑦) ∈
Fin) |
74 | | difinf 8499 |
. . . . . . . . . . . . . 14
⊢ ((¬
ℕ0 ∈ Fin ∧ (bits‘𝑦) ∈ Fin) → ¬
(ℕ0 ∖ (bits‘𝑦)) ∈ Fin) |
75 | 28, 73, 74 | sylancr 583 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ0
∧ (bits‘𝑥) =
(bits‘𝑦))) →
¬ (ℕ0 ∖ (bits‘𝑦)) ∈ Fin) |
76 | 70, 75 | eqneltrrd 2926 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ0
∧ (bits‘𝑥) =
(bits‘𝑦))) →
¬ (bits‘(-𝑦
− 1)) ∈ Fin) |
77 | | bitsfi 15532 |
. . . . . . . . . . . 12
⊢ ((-𝑦 − 1) ∈
ℕ0 → (bits‘(-𝑦 − 1)) ∈ Fin) |
78 | 76, 77 | nsyl 138 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ0
∧ (bits‘𝑥) =
(bits‘𝑦))) →
¬ (-𝑦 − 1) ∈
ℕ0) |
79 | 78, 49 | nsyl 138 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ0
∧ (bits‘𝑥) =
(bits‘𝑦))) →
¬ -𝑦 ∈
ℕ) |
80 | 45 | adantr 474 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ0
∧ (bits‘𝑥) =
(bits‘𝑦))) →
(-𝑦 ∈ ℕ ∨
𝑦 ∈
ℕ0)) |
81 | 80 | ord 897 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ0
∧ (bits‘𝑥) =
(bits‘𝑦))) →
(¬ -𝑦 ∈ ℕ
→ 𝑦 ∈
ℕ0)) |
82 | 79, 81 | mpd 15 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ0
∧ (bits‘𝑥) =
(bits‘𝑦))) →
𝑦 ∈
ℕ0) |
83 | | fvres 6452 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ0
→ ((bits ↾ ℕ0)‘𝑦) = (bits‘𝑦)) |
84 | 82, 83 | syl 17 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ0
∧ (bits‘𝑥) =
(bits‘𝑦))) →
((bits ↾ ℕ0)‘𝑦) = (bits‘𝑦)) |
85 | 67, 69, 84 | 3eqtr4d 2871 |
. . . . . . 7
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ0
∧ (bits‘𝑥) =
(bits‘𝑦))) →
((bits ↾ ℕ0)‘𝑥) = ((bits ↾
ℕ0)‘𝑦)) |
86 | | simprl 789 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ0
∧ (bits‘𝑥) =
(bits‘𝑦))) →
𝑥 ∈
ℕ0) |
87 | | f1fveq 6774 |
. . . . . . . . 9
⊢ (((bits
↾ ℕ0):ℕ0–1-1→(𝒫 ℕ0 ∩ Fin) ∧
(𝑥 ∈
ℕ0 ∧ 𝑦
∈ ℕ0)) → (((bits ↾
ℕ0)‘𝑥) = ((bits ↾
ℕ0)‘𝑦) ↔ 𝑥 = 𝑦)) |
88 | 56, 87 | mpan 683 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℕ0
∧ 𝑦 ∈
ℕ0) → (((bits ↾ ℕ0)‘𝑥) = ((bits ↾
ℕ0)‘𝑦) ↔ 𝑥 = 𝑦)) |
89 | 86, 82, 88 | syl2anc 581 |
. . . . . . 7
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ0
∧ (bits‘𝑥) =
(bits‘𝑦))) →
(((bits ↾ ℕ0)‘𝑥) = ((bits ↾
ℕ0)‘𝑦) ↔ 𝑥 = 𝑦)) |
90 | 85, 89 | mpbid 224 |
. . . . . 6
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ0
∧ (bits‘𝑥) =
(bits‘𝑦))) →
𝑥 = 𝑦) |
91 | 90 | expr 450 |
. . . . 5
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ 𝑥 ∈ ℕ0)
→ ((bits‘𝑥) =
(bits‘𝑦) → 𝑥 = 𝑦)) |
92 | 66, 91 | syldan 587 |
. . . 4
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ --𝑥 ∈ ℕ0)
→ ((bits‘𝑥) =
(bits‘𝑦) → 𝑥 = 𝑦)) |
93 | 2 | znegcld 11812 |
. . . . 5
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → -𝑥 ∈
ℤ) |
94 | | elznn 11720 |
. . . . . 6
⊢ (-𝑥 ∈ ℤ ↔ (-𝑥 ∈ ℝ ∧ (-𝑥 ∈ ℕ ∨ --𝑥 ∈
ℕ0))) |
95 | 94 | simprbi 492 |
. . . . 5
⊢ (-𝑥 ∈ ℤ → (-𝑥 ∈ ℕ ∨ --𝑥 ∈
ℕ0)) |
96 | 93, 95 | syl 17 |
. . . 4
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (-𝑥 ∈ ℕ ∨ --𝑥 ∈
ℕ0)) |
97 | 63, 92, 96 | mpjaodan 988 |
. . 3
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) →
((bits‘𝑥) =
(bits‘𝑦) → 𝑥 = 𝑦)) |
98 | 97 | rgen2a 3186 |
. 2
⊢
∀𝑥 ∈
ℤ ∀𝑦 ∈
ℤ ((bits‘𝑥) =
(bits‘𝑦) → 𝑥 = 𝑦) |
99 | | dff13 6767 |
. 2
⊢
(bits:ℤ–1-1→𝒫 ℕ0 ↔
(bits:ℤ⟶𝒫 ℕ0 ∧ ∀𝑥 ∈ ℤ ∀𝑦 ∈ ℤ
((bits‘𝑥) =
(bits‘𝑦) → 𝑥 = 𝑦))) |
100 | 1, 98, 99 | mpbir2an 704 |
1
⊢
bits:ℤ–1-1→𝒫 ℕ0 |