| Step | Hyp | Ref
| Expression |
| 1 | | bitsf 16464 |
. 2
⊢
bits:ℤ⟶𝒫 ℕ0 |
| 2 | | simpl 482 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → 𝑥 ∈
ℤ) |
| 3 | 2 | zcnd 12723 |
. . . . . . 7
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → 𝑥 ∈
ℂ) |
| 4 | 3 | adantr 480 |
. . . . . 6
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧
(bits‘𝑥) =
(bits‘𝑦))) →
𝑥 ∈
ℂ) |
| 5 | | simpr 484 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → 𝑦 ∈
ℤ) |
| 6 | 5 | zcnd 12723 |
. . . . . . 7
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → 𝑦 ∈
ℂ) |
| 7 | 6 | adantr 480 |
. . . . . 6
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧
(bits‘𝑥) =
(bits‘𝑦))) →
𝑦 ∈
ℂ) |
| 8 | 4 | negcld 11607 |
. . . . . . 7
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧
(bits‘𝑥) =
(bits‘𝑦))) →
-𝑥 ∈
ℂ) |
| 9 | 7 | negcld 11607 |
. . . . . . 7
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧
(bits‘𝑥) =
(bits‘𝑦))) →
-𝑦 ∈
ℂ) |
| 10 | | 1cnd 11256 |
. . . . . . 7
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧
(bits‘𝑥) =
(bits‘𝑦))) → 1
∈ ℂ) |
| 11 | | simprr 773 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧
(bits‘𝑥) =
(bits‘𝑦))) →
(bits‘𝑥) =
(bits‘𝑦)) |
| 12 | 11 | difeq2d 4126 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧
(bits‘𝑥) =
(bits‘𝑦))) →
(ℕ0 ∖ (bits‘𝑥)) = (ℕ0 ∖
(bits‘𝑦))) |
| 13 | | bitscmp 16475 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℤ →
(ℕ0 ∖ (bits‘𝑥)) = (bits‘(-𝑥 − 1))) |
| 14 | 13 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧
(bits‘𝑥) =
(bits‘𝑦))) →
(ℕ0 ∖ (bits‘𝑥)) = (bits‘(-𝑥 − 1))) |
| 15 | | bitscmp 16475 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℤ →
(ℕ0 ∖ (bits‘𝑦)) = (bits‘(-𝑦 − 1))) |
| 16 | 15 | ad2antlr 727 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧
(bits‘𝑥) =
(bits‘𝑦))) →
(ℕ0 ∖ (bits‘𝑦)) = (bits‘(-𝑦 − 1))) |
| 17 | 12, 14, 16 | 3eqtr3d 2785 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧
(bits‘𝑥) =
(bits‘𝑦))) →
(bits‘(-𝑥 − 1))
= (bits‘(-𝑦 −
1))) |
| 18 | | nnm1nn0 12567 |
. . . . . . . . . . 11
⊢ (-𝑥 ∈ ℕ → (-𝑥 − 1) ∈
ℕ0) |
| 19 | 18 | ad2antrl 728 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧
(bits‘𝑥) =
(bits‘𝑦))) →
(-𝑥 − 1) ∈
ℕ0) |
| 20 | 19 | fvresd 6926 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧
(bits‘𝑥) =
(bits‘𝑦))) →
((bits ↾ ℕ0)‘(-𝑥 − 1)) = (bits‘(-𝑥 − 1))) |
| 21 | | ominf 9294 |
. . . . . . . . . . . . . . . . 17
⊢ ¬
ω ∈ Fin |
| 22 | | nn0ennn 14020 |
. . . . . . . . . . . . . . . . . . 19
⊢
ℕ0 ≈ ℕ |
| 23 | | nnenom 14021 |
. . . . . . . . . . . . . . . . . . 19
⊢ ℕ
≈ ω |
| 24 | 22, 23 | entr2i 9049 |
. . . . . . . . . . . . . . . . . 18
⊢ ω
≈ ℕ0 |
| 25 | | enfii 9226 |
. . . . . . . . . . . . . . . . . 18
⊢
((ℕ0 ∈ Fin ∧ ω ≈
ℕ0) → ω ∈ Fin) |
| 26 | 24, 25 | mpan2 691 |
. . . . . . . . . . . . . . . . 17
⊢
(ℕ0 ∈ Fin → ω ∈
Fin) |
| 27 | 21, 26 | mto 197 |
. . . . . . . . . . . . . . . 16
⊢ ¬
ℕ0 ∈ Fin |
| 28 | | difinf 9349 |
. . . . . . . . . . . . . . . 16
⊢ ((¬
ℕ0 ∈ Fin ∧ (bits‘𝑥) ∈ Fin) → ¬
(ℕ0 ∖ (bits‘𝑥)) ∈ Fin) |
| 29 | 27, 28 | mpan 690 |
. . . . . . . . . . . . . . 15
⊢
((bits‘𝑥)
∈ Fin → ¬ (ℕ0 ∖ (bits‘𝑥)) ∈ Fin) |
| 30 | | bitsfi 16474 |
. . . . . . . . . . . . . . . . 17
⊢ ((-𝑥 − 1) ∈
ℕ0 → (bits‘(-𝑥 − 1)) ∈ Fin) |
| 31 | 19, 30 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧
(bits‘𝑥) =
(bits‘𝑦))) →
(bits‘(-𝑥 − 1))
∈ Fin) |
| 32 | 14, 31 | eqeltrd 2841 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧
(bits‘𝑥) =
(bits‘𝑦))) →
(ℕ0 ∖ (bits‘𝑥)) ∈ Fin) |
| 33 | 29, 32 | nsyl3 138 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧
(bits‘𝑥) =
(bits‘𝑦))) →
¬ (bits‘𝑥) ∈
Fin) |
| 34 | 11, 33 | eqneltrrd 2862 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧
(bits‘𝑥) =
(bits‘𝑦))) →
¬ (bits‘𝑦) ∈
Fin) |
| 35 | | bitsfi 16474 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ0
→ (bits‘𝑦)
∈ Fin) |
| 36 | 34, 35 | nsyl 140 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧
(bits‘𝑥) =
(bits‘𝑦))) →
¬ 𝑦 ∈
ℕ0) |
| 37 | 5 | znegcld 12724 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → -𝑦 ∈
ℤ) |
| 38 | | elznn 12629 |
. . . . . . . . . . . . . . . . 17
⊢ (-𝑦 ∈ ℤ ↔ (-𝑦 ∈ ℝ ∧ (-𝑦 ∈ ℕ ∨ --𝑦 ∈
ℕ0))) |
| 39 | 38 | simprbi 496 |
. . . . . . . . . . . . . . . 16
⊢ (-𝑦 ∈ ℤ → (-𝑦 ∈ ℕ ∨ --𝑦 ∈
ℕ0)) |
| 40 | 37, 39 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (-𝑦 ∈ ℕ ∨ --𝑦 ∈
ℕ0)) |
| 41 | 6 | negnegd 11611 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → --𝑦 = 𝑦) |
| 42 | 41 | eleq1d 2826 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (--𝑦 ∈ ℕ0
↔ 𝑦 ∈
ℕ0)) |
| 43 | 42 | orbi2d 916 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → ((-𝑦 ∈ ℕ ∨ --𝑦 ∈ ℕ0)
↔ (-𝑦 ∈ ℕ
∨ 𝑦 ∈
ℕ0))) |
| 44 | 40, 43 | mpbid 232 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (-𝑦 ∈ ℕ ∨ 𝑦 ∈
ℕ0)) |
| 45 | 44 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧
(bits‘𝑥) =
(bits‘𝑦))) →
(-𝑦 ∈ ℕ ∨
𝑦 ∈
ℕ0)) |
| 46 | 45 | ord 865 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧
(bits‘𝑥) =
(bits‘𝑦))) →
(¬ -𝑦 ∈ ℕ
→ 𝑦 ∈
ℕ0)) |
| 47 | 36, 46 | mt3d 148 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧
(bits‘𝑥) =
(bits‘𝑦))) →
-𝑦 ∈
ℕ) |
| 48 | | nnm1nn0 12567 |
. . . . . . . . . . 11
⊢ (-𝑦 ∈ ℕ → (-𝑦 − 1) ∈
ℕ0) |
| 49 | 47, 48 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧
(bits‘𝑥) =
(bits‘𝑦))) →
(-𝑦 − 1) ∈
ℕ0) |
| 50 | 49 | fvresd 6926 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧
(bits‘𝑥) =
(bits‘𝑦))) →
((bits ↾ ℕ0)‘(-𝑦 − 1)) = (bits‘(-𝑦 − 1))) |
| 51 | 17, 20, 50 | 3eqtr4d 2787 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧
(bits‘𝑥) =
(bits‘𝑦))) →
((bits ↾ ℕ0)‘(-𝑥 − 1)) = ((bits ↾
ℕ0)‘(-𝑦 − 1))) |
| 52 | | bitsf1o 16482 |
. . . . . . . . . . 11
⊢ (bits
↾ ℕ0):ℕ0–1-1-onto→(𝒫 ℕ0 ∩
Fin) |
| 53 | | f1of1 6847 |
. . . . . . . . . . 11
⊢ ((bits
↾ ℕ0):ℕ0–1-1-onto→(𝒫 ℕ0 ∩ Fin)
→ (bits ↾ ℕ0):ℕ0–1-1→(𝒫 ℕ0 ∩
Fin)) |
| 54 | 52, 53 | ax-mp 5 |
. . . . . . . . . 10
⊢ (bits
↾ ℕ0):ℕ0–1-1→(𝒫 ℕ0 ∩
Fin) |
| 55 | | f1fveq 7282 |
. . . . . . . . . 10
⊢ (((bits
↾ ℕ0):ℕ0–1-1→(𝒫 ℕ0 ∩ Fin) ∧
((-𝑥 − 1) ∈
ℕ0 ∧ (-𝑦 − 1) ∈ ℕ0))
→ (((bits ↾ ℕ0)‘(-𝑥 − 1)) = ((bits ↾
ℕ0)‘(-𝑦 − 1)) ↔ (-𝑥 − 1) = (-𝑦 − 1))) |
| 56 | 54, 55 | mpan 690 |
. . . . . . . . 9
⊢ (((-𝑥 − 1) ∈
ℕ0 ∧ (-𝑦 − 1) ∈ ℕ0)
→ (((bits ↾ ℕ0)‘(-𝑥 − 1)) = ((bits ↾
ℕ0)‘(-𝑦 − 1)) ↔ (-𝑥 − 1) = (-𝑦 − 1))) |
| 57 | 19, 49, 56 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧
(bits‘𝑥) =
(bits‘𝑦))) →
(((bits ↾ ℕ0)‘(-𝑥 − 1)) = ((bits ↾
ℕ0)‘(-𝑦 − 1)) ↔ (-𝑥 − 1) = (-𝑦 − 1))) |
| 58 | 51, 57 | mpbid 232 |
. . . . . . 7
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧
(bits‘𝑥) =
(bits‘𝑦))) →
(-𝑥 − 1) = (-𝑦 − 1)) |
| 59 | 8, 9, 10, 58 | subcan2d 11662 |
. . . . . 6
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧
(bits‘𝑥) =
(bits‘𝑦))) →
-𝑥 = -𝑦) |
| 60 | 4, 7, 59 | neg11d 11632 |
. . . . 5
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧
(bits‘𝑥) =
(bits‘𝑦))) →
𝑥 = 𝑦) |
| 61 | 60 | expr 456 |
. . . 4
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ -𝑥 ∈ ℕ) →
((bits‘𝑥) =
(bits‘𝑦) → 𝑥 = 𝑦)) |
| 62 | 3 | negnegd 11611 |
. . . . . . 7
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → --𝑥 = 𝑥) |
| 63 | 62 | eleq1d 2826 |
. . . . . 6
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (--𝑥 ∈ ℕ0
↔ 𝑥 ∈
ℕ0)) |
| 64 | 63 | biimpa 476 |
. . . . 5
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ --𝑥 ∈ ℕ0)
→ 𝑥 ∈
ℕ0) |
| 65 | | simprr 773 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ0
∧ (bits‘𝑥) =
(bits‘𝑦))) →
(bits‘𝑥) =
(bits‘𝑦)) |
| 66 | | fvres 6925 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℕ0
→ ((bits ↾ ℕ0)‘𝑥) = (bits‘𝑥)) |
| 67 | 66 | ad2antrl 728 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ0
∧ (bits‘𝑥) =
(bits‘𝑦))) →
((bits ↾ ℕ0)‘𝑥) = (bits‘𝑥)) |
| 68 | 15 | ad2antlr 727 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ0
∧ (bits‘𝑥) =
(bits‘𝑦))) →
(ℕ0 ∖ (bits‘𝑦)) = (bits‘(-𝑦 − 1))) |
| 69 | | bitsfi 16474 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℕ0
→ (bits‘𝑥)
∈ Fin) |
| 70 | 69 | ad2antrl 728 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ0
∧ (bits‘𝑥) =
(bits‘𝑦))) →
(bits‘𝑥) ∈
Fin) |
| 71 | 65, 70 | eqeltrrd 2842 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ0
∧ (bits‘𝑥) =
(bits‘𝑦))) →
(bits‘𝑦) ∈
Fin) |
| 72 | | difinf 9349 |
. . . . . . . . . . . . . 14
⊢ ((¬
ℕ0 ∈ Fin ∧ (bits‘𝑦) ∈ Fin) → ¬
(ℕ0 ∖ (bits‘𝑦)) ∈ Fin) |
| 73 | 27, 71, 72 | sylancr 587 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ0
∧ (bits‘𝑥) =
(bits‘𝑦))) →
¬ (ℕ0 ∖ (bits‘𝑦)) ∈ Fin) |
| 74 | 68, 73 | eqneltrrd 2862 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ0
∧ (bits‘𝑥) =
(bits‘𝑦))) →
¬ (bits‘(-𝑦
− 1)) ∈ Fin) |
| 75 | | bitsfi 16474 |
. . . . . . . . . . . 12
⊢ ((-𝑦 − 1) ∈
ℕ0 → (bits‘(-𝑦 − 1)) ∈ Fin) |
| 76 | 74, 75 | nsyl 140 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ0
∧ (bits‘𝑥) =
(bits‘𝑦))) →
¬ (-𝑦 − 1) ∈
ℕ0) |
| 77 | 76, 48 | nsyl 140 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ0
∧ (bits‘𝑥) =
(bits‘𝑦))) →
¬ -𝑦 ∈
ℕ) |
| 78 | 44 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ0
∧ (bits‘𝑥) =
(bits‘𝑦))) →
(-𝑦 ∈ ℕ ∨
𝑦 ∈
ℕ0)) |
| 79 | 78 | ord 865 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ0
∧ (bits‘𝑥) =
(bits‘𝑦))) →
(¬ -𝑦 ∈ ℕ
→ 𝑦 ∈
ℕ0)) |
| 80 | 77, 79 | mpd 15 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ0
∧ (bits‘𝑥) =
(bits‘𝑦))) →
𝑦 ∈
ℕ0) |
| 81 | 80 | fvresd 6926 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ0
∧ (bits‘𝑥) =
(bits‘𝑦))) →
((bits ↾ ℕ0)‘𝑦) = (bits‘𝑦)) |
| 82 | 65, 67, 81 | 3eqtr4d 2787 |
. . . . . . 7
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ0
∧ (bits‘𝑥) =
(bits‘𝑦))) →
((bits ↾ ℕ0)‘𝑥) = ((bits ↾
ℕ0)‘𝑦)) |
| 83 | | simprl 771 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ0
∧ (bits‘𝑥) =
(bits‘𝑦))) →
𝑥 ∈
ℕ0) |
| 84 | | f1fveq 7282 |
. . . . . . . . 9
⊢ (((bits
↾ ℕ0):ℕ0–1-1→(𝒫 ℕ0 ∩ Fin) ∧
(𝑥 ∈
ℕ0 ∧ 𝑦
∈ ℕ0)) → (((bits ↾
ℕ0)‘𝑥) = ((bits ↾
ℕ0)‘𝑦) ↔ 𝑥 = 𝑦)) |
| 85 | 54, 84 | mpan 690 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℕ0
∧ 𝑦 ∈
ℕ0) → (((bits ↾ ℕ0)‘𝑥) = ((bits ↾
ℕ0)‘𝑦) ↔ 𝑥 = 𝑦)) |
| 86 | 83, 80, 85 | syl2anc 584 |
. . . . . . 7
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ0
∧ (bits‘𝑥) =
(bits‘𝑦))) →
(((bits ↾ ℕ0)‘𝑥) = ((bits ↾
ℕ0)‘𝑦) ↔ 𝑥 = 𝑦)) |
| 87 | 82, 86 | mpbid 232 |
. . . . . 6
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ0
∧ (bits‘𝑥) =
(bits‘𝑦))) →
𝑥 = 𝑦) |
| 88 | 87 | expr 456 |
. . . . 5
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ 𝑥 ∈ ℕ0)
→ ((bits‘𝑥) =
(bits‘𝑦) → 𝑥 = 𝑦)) |
| 89 | 64, 88 | syldan 591 |
. . . 4
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ --𝑥 ∈ ℕ0)
→ ((bits‘𝑥) =
(bits‘𝑦) → 𝑥 = 𝑦)) |
| 90 | 2 | znegcld 12724 |
. . . . 5
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → -𝑥 ∈
ℤ) |
| 91 | | elznn 12629 |
. . . . . 6
⊢ (-𝑥 ∈ ℤ ↔ (-𝑥 ∈ ℝ ∧ (-𝑥 ∈ ℕ ∨ --𝑥 ∈
ℕ0))) |
| 92 | 91 | simprbi 496 |
. . . . 5
⊢ (-𝑥 ∈ ℤ → (-𝑥 ∈ ℕ ∨ --𝑥 ∈
ℕ0)) |
| 93 | 90, 92 | syl 17 |
. . . 4
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (-𝑥 ∈ ℕ ∨ --𝑥 ∈
ℕ0)) |
| 94 | 61, 89, 93 | mpjaodan 961 |
. . 3
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) →
((bits‘𝑥) =
(bits‘𝑦) → 𝑥 = 𝑦)) |
| 95 | 94 | rgen2 3199 |
. 2
⊢
∀𝑥 ∈
ℤ ∀𝑦 ∈
ℤ ((bits‘𝑥) =
(bits‘𝑦) → 𝑥 = 𝑦) |
| 96 | | dff13 7275 |
. 2
⊢
(bits:ℤ–1-1→𝒫 ℕ0 ↔
(bits:ℤ⟶𝒫 ℕ0 ∧ ∀𝑥 ∈ ℤ ∀𝑦 ∈ ℤ
((bits‘𝑥) =
(bits‘𝑦) → 𝑥 = 𝑦))) |
| 97 | 1, 95, 96 | mpbir2an 711 |
1
⊢
bits:ℤ–1-1→𝒫 ℕ0 |