Step | Hyp | Ref
| Expression |
1 | | bitsf 16312 |
. 2
β’
bits:β€βΆπ« β0 |
2 | | simpl 484 |
. . . . . . . 8
β’ ((π₯ β β€ β§ π¦ β β€) β π₯ β
β€) |
3 | 2 | zcnd 12613 |
. . . . . . 7
β’ ((π₯ β β€ β§ π¦ β β€) β π₯ β
β) |
4 | 3 | adantr 482 |
. . . . . 6
β’ (((π₯ β β€ β§ π¦ β β€) β§ (-π₯ β β β§
(bitsβπ₯) =
(bitsβπ¦))) β
π₯ β
β) |
5 | | simpr 486 |
. . . . . . . 8
β’ ((π₯ β β€ β§ π¦ β β€) β π¦ β
β€) |
6 | 5 | zcnd 12613 |
. . . . . . 7
β’ ((π₯ β β€ β§ π¦ β β€) β π¦ β
β) |
7 | 6 | adantr 482 |
. . . . . 6
β’ (((π₯ β β€ β§ π¦ β β€) β§ (-π₯ β β β§
(bitsβπ₯) =
(bitsβπ¦))) β
π¦ β
β) |
8 | 4 | negcld 11504 |
. . . . . . 7
β’ (((π₯ β β€ β§ π¦ β β€) β§ (-π₯ β β β§
(bitsβπ₯) =
(bitsβπ¦))) β
-π₯ β
β) |
9 | 7 | negcld 11504 |
. . . . . . 7
β’ (((π₯ β β€ β§ π¦ β β€) β§ (-π₯ β β β§
(bitsβπ₯) =
(bitsβπ¦))) β
-π¦ β
β) |
10 | | 1cnd 11155 |
. . . . . . 7
β’ (((π₯ β β€ β§ π¦ β β€) β§ (-π₯ β β β§
(bitsβπ₯) =
(bitsβπ¦))) β 1
β β) |
11 | | simprr 772 |
. . . . . . . . . . 11
β’ (((π₯ β β€ β§ π¦ β β€) β§ (-π₯ β β β§
(bitsβπ₯) =
(bitsβπ¦))) β
(bitsβπ₯) =
(bitsβπ¦)) |
12 | 11 | difeq2d 4083 |
. . . . . . . . . 10
β’ (((π₯ β β€ β§ π¦ β β€) β§ (-π₯ β β β§
(bitsβπ₯) =
(bitsβπ¦))) β
(β0 β (bitsβπ₯)) = (β0 β
(bitsβπ¦))) |
13 | | bitscmp 16323 |
. . . . . . . . . . 11
β’ (π₯ β β€ β
(β0 β (bitsβπ₯)) = (bitsβ(-π₯ β 1))) |
14 | 13 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π₯ β β€ β§ π¦ β β€) β§ (-π₯ β β β§
(bitsβπ₯) =
(bitsβπ¦))) β
(β0 β (bitsβπ₯)) = (bitsβ(-π₯ β 1))) |
15 | | bitscmp 16323 |
. . . . . . . . . . 11
β’ (π¦ β β€ β
(β0 β (bitsβπ¦)) = (bitsβ(-π¦ β 1))) |
16 | 15 | ad2antlr 726 |
. . . . . . . . . 10
β’ (((π₯ β β€ β§ π¦ β β€) β§ (-π₯ β β β§
(bitsβπ₯) =
(bitsβπ¦))) β
(β0 β (bitsβπ¦)) = (bitsβ(-π¦ β 1))) |
17 | 12, 14, 16 | 3eqtr3d 2781 |
. . . . . . . . 9
β’ (((π₯ β β€ β§ π¦ β β€) β§ (-π₯ β β β§
(bitsβπ₯) =
(bitsβπ¦))) β
(bitsβ(-π₯ β 1))
= (bitsβ(-π¦ β
1))) |
18 | | nnm1nn0 12459 |
. . . . . . . . . . 11
β’ (-π₯ β β β (-π₯ β 1) β
β0) |
19 | 18 | ad2antrl 727 |
. . . . . . . . . 10
β’ (((π₯ β β€ β§ π¦ β β€) β§ (-π₯ β β β§
(bitsβπ₯) =
(bitsβπ¦))) β
(-π₯ β 1) β
β0) |
20 | 19 | fvresd 6863 |
. . . . . . . . 9
β’ (((π₯ β β€ β§ π¦ β β€) β§ (-π₯ β β β§
(bitsβπ₯) =
(bitsβπ¦))) β
((bits βΎ β0)β(-π₯ β 1)) = (bitsβ(-π₯ β 1))) |
21 | | ominf 9205 |
. . . . . . . . . . . . . . . . 17
β’ Β¬
Ο β Fin |
22 | | nn0ennn 13890 |
. . . . . . . . . . . . . . . . . . 19
β’
β0 β β |
23 | | nnenom 13891 |
. . . . . . . . . . . . . . . . . . 19
β’ β
β Ο |
24 | 22, 23 | entr2i 8952 |
. . . . . . . . . . . . . . . . . 18
β’ Ο
β β0 |
25 | | enfii 9136 |
. . . . . . . . . . . . . . . . . 18
β’
((β0 β Fin β§ Ο β
β0) β Ο β Fin) |
26 | 24, 25 | mpan2 690 |
. . . . . . . . . . . . . . . . 17
β’
(β0 β Fin β Ο β
Fin) |
27 | 21, 26 | mto 196 |
. . . . . . . . . . . . . . . 16
β’ Β¬
β0 β Fin |
28 | | difinf 9263 |
. . . . . . . . . . . . . . . 16
β’ ((Β¬
β0 β Fin β§ (bitsβπ₯) β Fin) β Β¬
(β0 β (bitsβπ₯)) β Fin) |
29 | 27, 28 | mpan 689 |
. . . . . . . . . . . . . . 15
β’
((bitsβπ₯)
β Fin β Β¬ (β0 β (bitsβπ₯)) β Fin) |
30 | | bitsfi 16322 |
. . . . . . . . . . . . . . . . 17
β’ ((-π₯ β 1) β
β0 β (bitsβ(-π₯ β 1)) β Fin) |
31 | 19, 30 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (((π₯ β β€ β§ π¦ β β€) β§ (-π₯ β β β§
(bitsβπ₯) =
(bitsβπ¦))) β
(bitsβ(-π₯ β 1))
β Fin) |
32 | 14, 31 | eqeltrd 2834 |
. . . . . . . . . . . . . . 15
β’ (((π₯ β β€ β§ π¦ β β€) β§ (-π₯ β β β§
(bitsβπ₯) =
(bitsβπ¦))) β
(β0 β (bitsβπ₯)) β Fin) |
33 | 29, 32 | nsyl3 138 |
. . . . . . . . . . . . . 14
β’ (((π₯ β β€ β§ π¦ β β€) β§ (-π₯ β β β§
(bitsβπ₯) =
(bitsβπ¦))) β
Β¬ (bitsβπ₯) β
Fin) |
34 | 11, 33 | eqneltrrd 2855 |
. . . . . . . . . . . . 13
β’ (((π₯ β β€ β§ π¦ β β€) β§ (-π₯ β β β§
(bitsβπ₯) =
(bitsβπ¦))) β
Β¬ (bitsβπ¦) β
Fin) |
35 | | bitsfi 16322 |
. . . . . . . . . . . . 13
β’ (π¦ β β0
β (bitsβπ¦)
β Fin) |
36 | 34, 35 | nsyl 140 |
. . . . . . . . . . . 12
β’ (((π₯ β β€ β§ π¦ β β€) β§ (-π₯ β β β§
(bitsβπ₯) =
(bitsβπ¦))) β
Β¬ π¦ β
β0) |
37 | 5 | znegcld 12614 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β β€ β§ π¦ β β€) β -π¦ β
β€) |
38 | | elznn 12520 |
. . . . . . . . . . . . . . . . 17
β’ (-π¦ β β€ β (-π¦ β β β§ (-π¦ β β β¨ --π¦ β
β0))) |
39 | 38 | simprbi 498 |
. . . . . . . . . . . . . . . 16
β’ (-π¦ β β€ β (-π¦ β β β¨ --π¦ β
β0)) |
40 | 37, 39 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β β€ β§ π¦ β β€) β (-π¦ β β β¨ --π¦ β
β0)) |
41 | 6 | negnegd 11508 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ β β€ β§ π¦ β β€) β --π¦ = π¦) |
42 | 41 | eleq1d 2819 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β β€ β§ π¦ β β€) β (--π¦ β β0
β π¦ β
β0)) |
43 | 42 | orbi2d 915 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β β€ β§ π¦ β β€) β ((-π¦ β β β¨ --π¦ β β0)
β (-π¦ β β
β¨ π¦ β
β0))) |
44 | 40, 43 | mpbid 231 |
. . . . . . . . . . . . . 14
β’ ((π₯ β β€ β§ π¦ β β€) β (-π¦ β β β¨ π¦ β
β0)) |
45 | 44 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π₯ β β€ β§ π¦ β β€) β§ (-π₯ β β β§
(bitsβπ₯) =
(bitsβπ¦))) β
(-π¦ β β β¨
π¦ β
β0)) |
46 | 45 | ord 863 |
. . . . . . . . . . . 12
β’ (((π₯ β β€ β§ π¦ β β€) β§ (-π₯ β β β§
(bitsβπ₯) =
(bitsβπ¦))) β
(Β¬ -π¦ β β
β π¦ β
β0)) |
47 | 36, 46 | mt3d 148 |
. . . . . . . . . . 11
β’ (((π₯ β β€ β§ π¦ β β€) β§ (-π₯ β β β§
(bitsβπ₯) =
(bitsβπ¦))) β
-π¦ β
β) |
48 | | nnm1nn0 12459 |
. . . . . . . . . . 11
β’ (-π¦ β β β (-π¦ β 1) β
β0) |
49 | 47, 48 | syl 17 |
. . . . . . . . . 10
β’ (((π₯ β β€ β§ π¦ β β€) β§ (-π₯ β β β§
(bitsβπ₯) =
(bitsβπ¦))) β
(-π¦ β 1) β
β0) |
50 | 49 | fvresd 6863 |
. . . . . . . . 9
β’ (((π₯ β β€ β§ π¦ β β€) β§ (-π₯ β β β§
(bitsβπ₯) =
(bitsβπ¦))) β
((bits βΎ β0)β(-π¦ β 1)) = (bitsβ(-π¦ β 1))) |
51 | 17, 20, 50 | 3eqtr4d 2783 |
. . . . . . . 8
β’ (((π₯ β β€ β§ π¦ β β€) β§ (-π₯ β β β§
(bitsβπ₯) =
(bitsβπ¦))) β
((bits βΎ β0)β(-π₯ β 1)) = ((bits βΎ
β0)β(-π¦ β 1))) |
52 | | bitsf1o 16330 |
. . . . . . . . . . 11
β’ (bits
βΎ β0):β0β1-1-ontoβ(π« β0 β©
Fin) |
53 | | f1of1 6784 |
. . . . . . . . . . 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 7210 |
. . . . . . . . . 10
β’ (((bits
βΎ β0):β0β1-1β(π« β0 β© Fin) β§
((-π₯ β 1) β
β0 β§ (-π¦ β 1) β β0))
β (((bits βΎ β0)β(-π₯ β 1)) = ((bits βΎ
β0)β(-π¦ β 1)) β (-π₯ β 1) = (-π¦ β 1))) |
56 | 54, 55 | mpan 689 |
. . . . . . . . 9
β’ (((-π₯ β 1) β
β0 β§ (-π¦ β 1) β β0)
β (((bits βΎ β0)β(-π₯ β 1)) = ((bits βΎ
β0)β(-π¦ β 1)) β (-π₯ β 1) = (-π¦ β 1))) |
57 | 19, 49, 56 | syl2anc 585 |
. . . . . . . 8
β’ (((π₯ β β€ β§ π¦ β β€) β§ (-π₯ β β β§
(bitsβπ₯) =
(bitsβπ¦))) β
(((bits βΎ β0)β(-π₯ β 1)) = ((bits βΎ
β0)β(-π¦ β 1)) β (-π₯ β 1) = (-π¦ β 1))) |
58 | 51, 57 | mpbid 231 |
. . . . . . 7
β’ (((π₯ β β€ β§ π¦ β β€) β§ (-π₯ β β β§
(bitsβπ₯) =
(bitsβπ¦))) β
(-π₯ β 1) = (-π¦ β 1)) |
59 | 8, 9, 10, 58 | subcan2d 11559 |
. . . . . 6
β’ (((π₯ β β€ β§ π¦ β β€) β§ (-π₯ β β β§
(bitsβπ₯) =
(bitsβπ¦))) β
-π₯ = -π¦) |
60 | 4, 7, 59 | neg11d 11529 |
. . . . 5
β’ (((π₯ β β€ β§ π¦ β β€) β§ (-π₯ β β β§
(bitsβπ₯) =
(bitsβπ¦))) β
π₯ = π¦) |
61 | 60 | expr 458 |
. . . 4
β’ (((π₯ β β€ β§ π¦ β β€) β§ -π₯ β β) β
((bitsβπ₯) =
(bitsβπ¦) β π₯ = π¦)) |
62 | 3 | negnegd 11508 |
. . . . . . 7
β’ ((π₯ β β€ β§ π¦ β β€) β --π₯ = π₯) |
63 | 62 | eleq1d 2819 |
. . . . . 6
β’ ((π₯ β β€ β§ π¦ β β€) β (--π₯ β β0
β π₯ β
β0)) |
64 | 63 | biimpa 478 |
. . . . 5
β’ (((π₯ β β€ β§ π¦ β β€) β§ --π₯ β β0)
β π₯ β
β0) |
65 | | simprr 772 |
. . . . . . . 8
β’ (((π₯ β β€ β§ π¦ β β€) β§ (π₯ β β0
β§ (bitsβπ₯) =
(bitsβπ¦))) β
(bitsβπ₯) =
(bitsβπ¦)) |
66 | | fvres 6862 |
. . . . . . . . 9
β’ (π₯ β β0
β ((bits βΎ β0)βπ₯) = (bitsβπ₯)) |
67 | 66 | ad2antrl 727 |
. . . . . . . 8
β’ (((π₯ β β€ β§ π¦ β β€) β§ (π₯ β β0
β§ (bitsβπ₯) =
(bitsβπ¦))) β
((bits βΎ β0)βπ₯) = (bitsβπ₯)) |
68 | 15 | ad2antlr 726 |
. . . . . . . . . . . . 13
β’ (((π₯ β β€ β§ π¦ β β€) β§ (π₯ β β0
β§ (bitsβπ₯) =
(bitsβπ¦))) β
(β0 β (bitsβπ¦)) = (bitsβ(-π¦ β 1))) |
69 | | bitsfi 16322 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β β0
β (bitsβπ₯)
β Fin) |
70 | 69 | ad2antrl 727 |
. . . . . . . . . . . . . . 15
β’ (((π₯ β β€ β§ π¦ β β€) β§ (π₯ β β0
β§ (bitsβπ₯) =
(bitsβπ¦))) β
(bitsβπ₯) β
Fin) |
71 | 65, 70 | eqeltrrd 2835 |
. . . . . . . . . . . . . 14
β’ (((π₯ β β€ β§ π¦ β β€) β§ (π₯ β β0
β§ (bitsβπ₯) =
(bitsβπ¦))) β
(bitsβπ¦) β
Fin) |
72 | | difinf 9263 |
. . . . . . . . . . . . . 14
β’ ((Β¬
β0 β Fin β§ (bitsβπ¦) β Fin) β Β¬
(β0 β (bitsβπ¦)) β Fin) |
73 | 27, 71, 72 | sylancr 588 |
. . . . . . . . . . . . 13
β’ (((π₯ β β€ β§ π¦ β β€) β§ (π₯ β β0
β§ (bitsβπ₯) =
(bitsβπ¦))) β
Β¬ (β0 β (bitsβπ¦)) β Fin) |
74 | 68, 73 | eqneltrrd 2855 |
. . . . . . . . . . . 12
β’ (((π₯ β β€ β§ π¦ β β€) β§ (π₯ β β0
β§ (bitsβπ₯) =
(bitsβπ¦))) β
Β¬ (bitsβ(-π¦
β 1)) β Fin) |
75 | | bitsfi 16322 |
. . . . . . . . . . . 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 482 |
. . . . . . . . . . 11
β’ (((π₯ β β€ β§ π¦ β β€) β§ (π₯ β β0
β§ (bitsβπ₯) =
(bitsβπ¦))) β
(-π¦ β β β¨
π¦ β
β0)) |
79 | 78 | ord 863 |
. . . . . . . . . 10
β’ (((π₯ β β€ β§ π¦ β β€) β§ (π₯ β β0
β§ (bitsβπ₯) =
(bitsβπ¦))) β
(Β¬ -π¦ β β
β π¦ β
β0)) |
80 | 77, 79 | mpd 15 |
. . . . . . . . 9
β’ (((π₯ β β€ β§ π¦ β β€) β§ (π₯ β β0
β§ (bitsβπ₯) =
(bitsβπ¦))) β
π¦ β
β0) |
81 | 80 | fvresd 6863 |
. . . . . . . 8
β’ (((π₯ β β€ β§ π¦ β β€) β§ (π₯ β β0
β§ (bitsβπ₯) =
(bitsβπ¦))) β
((bits βΎ β0)βπ¦) = (bitsβπ¦)) |
82 | 65, 67, 81 | 3eqtr4d 2783 |
. . . . . . 7
β’ (((π₯ β β€ β§ π¦ β β€) β§ (π₯ β β0
β§ (bitsβπ₯) =
(bitsβπ¦))) β
((bits βΎ β0)βπ₯) = ((bits βΎ
β0)βπ¦)) |
83 | | simprl 770 |
. . . . . . . 8
β’ (((π₯ β β€ β§ π¦ β β€) β§ (π₯ β β0
β§ (bitsβπ₯) =
(bitsβπ¦))) β
π₯ β
β0) |
84 | | f1fveq 7210 |
. . . . . . . . 9
β’ (((bits
βΎ β0):β0β1-1β(π« β0 β© Fin) β§
(π₯ β
β0 β§ π¦
β β0)) β (((bits βΎ
β0)βπ₯) = ((bits βΎ
β0)βπ¦) β π₯ = π¦)) |
85 | 54, 84 | mpan 689 |
. . . . . . . 8
β’ ((π₯ β β0
β§ π¦ β
β0) β (((bits βΎ β0)βπ₯) = ((bits βΎ
β0)βπ¦) β π₯ = π¦)) |
86 | 83, 80, 85 | syl2anc 585 |
. . . . . . 7
β’ (((π₯ β β€ β§ π¦ β β€) β§ (π₯ β β0
β§ (bitsβπ₯) =
(bitsβπ¦))) β
(((bits βΎ β0)βπ₯) = ((bits βΎ
β0)βπ¦) β π₯ = π¦)) |
87 | 82, 86 | mpbid 231 |
. . . . . 6
β’ (((π₯ β β€ β§ π¦ β β€) β§ (π₯ β β0
β§ (bitsβπ₯) =
(bitsβπ¦))) β
π₯ = π¦) |
88 | 87 | expr 458 |
. . . . 5
β’ (((π₯ β β€ β§ π¦ β β€) β§ π₯ β β0)
β ((bitsβπ₯) =
(bitsβπ¦) β π₯ = π¦)) |
89 | 64, 88 | syldan 592 |
. . . 4
β’ (((π₯ β β€ β§ π¦ β β€) β§ --π₯ β β0)
β ((bitsβπ₯) =
(bitsβπ¦) β π₯ = π¦)) |
90 | 2 | znegcld 12614 |
. . . . 5
β’ ((π₯ β β€ β§ π¦ β β€) β -π₯ β
β€) |
91 | | elznn 12520 |
. . . . . 6
β’ (-π₯ β β€ β (-π₯ β β β§ (-π₯ β β β¨ --π₯ β
β0))) |
92 | 91 | simprbi 498 |
. . . . 5
β’ (-π₯ β β€ β (-π₯ β β β¨ --π₯ β
β0)) |
93 | 90, 92 | syl 17 |
. . . 4
β’ ((π₯ β β€ β§ π¦ β β€) β (-π₯ β β β¨ --π₯ β
β0)) |
94 | 61, 89, 93 | mpjaodan 958 |
. . 3
β’ ((π₯ β β€ β§ π¦ β β€) β
((bitsβπ₯) =
(bitsβπ¦) β π₯ = π¦)) |
95 | 94 | rgen2 3191 |
. 2
β’
βπ₯ β
β€ βπ¦ β
β€ ((bitsβπ₯) =
(bitsβπ¦) β π₯ = π¦) |
96 | | dff13 7203 |
. 2
β’
(bits:β€β1-1βπ« β0 β
(bits:β€βΆπ« β0 β§ βπ₯ β β€ βπ¦ β β€
((bitsβπ₯) =
(bitsβπ¦) β π₯ = π¦))) |
97 | 1, 95, 96 | mpbir2an 710 |
1
β’
bits:β€β1-1βπ« β0 |