Step | Hyp | Ref
| Expression |
1 | | 2z 12540 |
. . . . . 6
β’ 2 β
β€ |
2 | 1 | a1i 11 |
. . . . 5
β’ (π β β€ β 2 β
β€) |
3 | | id 22 |
. . . . 5
β’ (π β β€ β π β
β€) |
4 | 2, 3 | zmulcld 12618 |
. . . 4
β’ (π β β€ β (2
Β· π) β
β€) |
5 | 4 | peano2zd 12615 |
. . 3
β’ (π β β€ β ((2
Β· π) + 1) β
β€) |
6 | | bitsp1 16316 |
. . 3
β’ ((((2
Β· π) + 1) β
β€ β§ π β
β0) β ((π + 1) β (bitsβ((2 Β· π) + 1)) β π β (bitsβ(ββ(((2
Β· π) + 1) /
2))))) |
7 | 5, 6 | sylan 581 |
. 2
β’ ((π β β€ β§ π β β0)
β ((π + 1) β
(bitsβ((2 Β· π)
+ 1)) β π β
(bitsβ(ββ(((2 Β· π) + 1) / 2))))) |
8 | | 2re 12232 |
. . . . . . . . . . . 12
β’ 2 β
β |
9 | 8 | a1i 11 |
. . . . . . . . . . 11
β’ (π β β€ β 2 β
β) |
10 | | zre 12508 |
. . . . . . . . . . 11
β’ (π β β€ β π β
β) |
11 | 9, 10 | remulcld 11190 |
. . . . . . . . . 10
β’ (π β β€ β (2
Β· π) β
β) |
12 | 11 | recnd 11188 |
. . . . . . . . 9
β’ (π β β€ β (2
Β· π) β
β) |
13 | | 1cnd 11155 |
. . . . . . . . 9
β’ (π β β€ β 1 β
β) |
14 | | 2cnd 12236 |
. . . . . . . . 9
β’ (π β β€ β 2 β
β) |
15 | | 2ne0 12262 |
. . . . . . . . . 10
β’ 2 β
0 |
16 | 15 | a1i 11 |
. . . . . . . . 9
β’ (π β β€ β 2 β
0) |
17 | 12, 13, 14, 16 | divdird 11974 |
. . . . . . . 8
β’ (π β β€ β (((2
Β· π) + 1) / 2) =
(((2 Β· π) / 2) + (1
/ 2))) |
18 | | zcn 12509 |
. . . . . . . . . 10
β’ (π β β€ β π β
β) |
19 | 18, 14, 16 | divcan3d 11941 |
. . . . . . . . 9
β’ (π β β€ β ((2
Β· π) / 2) = π) |
20 | 19 | oveq1d 7373 |
. . . . . . . 8
β’ (π β β€ β (((2
Β· π) / 2) + (1 / 2))
= (π + (1 /
2))) |
21 | 17, 20 | eqtrd 2773 |
. . . . . . 7
β’ (π β β€ β (((2
Β· π) + 1) / 2) =
(π + (1 /
2))) |
22 | 21 | fveq2d 6847 |
. . . . . 6
β’ (π β β€ β
(ββ(((2 Β· π) + 1) / 2)) = (ββ(π + (1 / 2)))) |
23 | | halfge0 12375 |
. . . . . . . 8
β’ 0 β€ (1
/ 2) |
24 | | halflt1 12376 |
. . . . . . . 8
β’ (1 / 2)
< 1 |
25 | 23, 24 | pm3.2i 472 |
. . . . . . 7
β’ (0 β€
(1 / 2) β§ (1 / 2) < 1) |
26 | | halfre 12372 |
. . . . . . . 8
β’ (1 / 2)
β β |
27 | | flbi2 13728 |
. . . . . . . 8
β’ ((π β β€ β§ (1 / 2)
β β) β ((ββ(π + (1 / 2))) = π β (0 β€ (1 / 2) β§ (1 / 2) <
1))) |
28 | 26, 27 | mpan2 690 |
. . . . . . 7
β’ (π β β€ β
((ββ(π + (1 /
2))) = π β (0 β€ (1
/ 2) β§ (1 / 2) < 1))) |
29 | 25, 28 | mpbiri 258 |
. . . . . 6
β’ (π β β€ β
(ββ(π + (1 /
2))) = π) |
30 | 22, 29 | eqtrd 2773 |
. . . . 5
β’ (π β β€ β
(ββ(((2 Β· π) + 1) / 2)) = π) |
31 | 30 | adantr 482 |
. . . 4
β’ ((π β β€ β§ π β β0)
β (ββ(((2 Β· π) + 1) / 2)) = π) |
32 | 31 | fveq2d 6847 |
. . 3
β’ ((π β β€ β§ π β β0)
β (bitsβ(ββ(((2 Β· π) + 1) / 2))) = (bitsβπ)) |
33 | 32 | eleq2d 2820 |
. 2
β’ ((π β β€ β§ π β β0)
β (π β
(bitsβ(ββ(((2 Β· π) + 1) / 2))) β π β (bitsβπ))) |
34 | 7, 33 | bitrd 279 |
1
β’ ((π β β€ β§ π β β0)
β ((π + 1) β
(bitsβ((2 Β· π)
+ 1)) β π β
(bitsβπ))) |