Step | Hyp | Ref
| Expression |
1 | | oveq2 7413 |
. . 3
β’
((2βπ) =
if(π β
(bitsβπ),
(2βπ), 0) β
((π mod (2βπ)) + (2βπ)) = ((π mod (2βπ)) + if(π β (bitsβπ), (2βπ), 0))) |
2 | 1 | eqeq2d 2743 |
. 2
β’
((2βπ) =
if(π β
(bitsβπ),
(2βπ), 0) β
((π mod (2β(π + 1))) = ((π mod (2βπ)) + (2βπ)) β (π mod (2β(π + 1))) = ((π mod (2βπ)) + if(π β (bitsβπ), (2βπ), 0)))) |
3 | | oveq2 7413 |
. . 3
β’ (0 =
if(π β
(bitsβπ),
(2βπ), 0) β
((π mod (2βπ)) + 0) = ((π mod (2βπ)) + if(π β (bitsβπ), (2βπ), 0))) |
4 | 3 | eqeq2d 2743 |
. 2
β’ (0 =
if(π β
(bitsβπ),
(2βπ), 0) β
((π mod (2β(π + 1))) = ((π mod (2βπ)) + 0) β (π mod (2β(π + 1))) = ((π mod (2βπ)) + if(π β (bitsβπ), (2βπ), 0)))) |
5 | | simpl 483 |
. . . . . . 7
β’ ((π β β€ β§ π β β0)
β π β
β€) |
6 | | 2nn 12281 |
. . . . . . . . 9
β’ 2 β
β |
7 | 6 | a1i 11 |
. . . . . . . 8
β’ ((π β β€ β§ π β β0)
β 2 β β) |
8 | | simpr 485 |
. . . . . . . 8
β’ ((π β β€ β§ π β β0)
β π β
β0) |
9 | 7, 8 | nnexpcld 14204 |
. . . . . . 7
β’ ((π β β€ β§ π β β0)
β (2βπ) β
β) |
10 | 5, 9 | zmodcld 13853 |
. . . . . 6
β’ ((π β β€ β§ π β β0)
β (π mod (2βπ)) β
β0) |
11 | 10 | nn0cnd 12530 |
. . . . 5
β’ ((π β β€ β§ π β β0)
β (π mod (2βπ)) β
β) |
12 | 11 | adantr 481 |
. . . 4
β’ (((π β β€ β§ π β β0)
β§ π β
(bitsβπ)) β
(π mod (2βπ)) β
β) |
13 | | 1nn0 12484 |
. . . . . . . . . 10
β’ 1 β
β0 |
14 | 13 | a1i 11 |
. . . . . . . . 9
β’ ((π β β€ β§ π β β0)
β 1 β β0) |
15 | 8, 14 | nn0addcld 12532 |
. . . . . . . 8
β’ ((π β β€ β§ π β β0)
β (π + 1) β
β0) |
16 | 7, 15 | nnexpcld 14204 |
. . . . . . 7
β’ ((π β β€ β§ π β β0)
β (2β(π + 1))
β β) |
17 | 5, 16 | zmodcld 13853 |
. . . . . 6
β’ ((π β β€ β§ π β β0)
β (π mod
(2β(π + 1))) β
β0) |
18 | 17 | nn0cnd 12530 |
. . . . 5
β’ ((π β β€ β§ π β β0)
β (π mod
(2β(π + 1))) β
β) |
19 | 18 | adantr 481 |
. . . 4
β’ (((π β β€ β§ π β β0)
β§ π β
(bitsβπ)) β
(π mod (2β(π + 1))) β
β) |
20 | 12, 19 | pncan3d 11570 |
. . 3
β’ (((π β β€ β§ π β β0)
β§ π β
(bitsβπ)) β
((π mod (2βπ)) + ((π mod (2β(π + 1))) β (π mod (2βπ)))) = (π mod (2β(π + 1)))) |
21 | 18, 11 | subcld 11567 |
. . . . . 6
β’ ((π β β€ β§ π β β0)
β ((π mod
(2β(π + 1))) β
(π mod (2βπ))) β
β) |
22 | 21 | adantr 481 |
. . . . 5
β’ (((π β β€ β§ π β β0)
β§ π β
(bitsβπ)) β
((π mod (2β(π + 1))) β (π mod (2βπ))) β β) |
23 | 6 | a1i 11 |
. . . . . . 7
β’ (((π β β€ β§ π β β0)
β§ π β
(bitsβπ)) β 2
β β) |
24 | | simplr 767 |
. . . . . . 7
β’ (((π β β€ β§ π β β0)
β§ π β
(bitsβπ)) β
π β
β0) |
25 | 23, 24 | nnexpcld 14204 |
. . . . . 6
β’ (((π β β€ β§ π β β0)
β§ π β
(bitsβπ)) β
(2βπ) β
β) |
26 | 25 | nncnd 12224 |
. . . . 5
β’ (((π β β€ β§ π β β0)
β§ π β
(bitsβπ)) β
(2βπ) β
β) |
27 | | 2cnd 12286 |
. . . . . . 7
β’ ((π β β€ β§ π β β0)
β 2 β β) |
28 | | 2ne0 12312 |
. . . . . . . 8
β’ 2 β
0 |
29 | 28 | a1i 11 |
. . . . . . 7
β’ ((π β β€ β§ π β β0)
β 2 β 0) |
30 | 8 | nn0zd 12580 |
. . . . . . 7
β’ ((π β β€ β§ π β β0)
β π β
β€) |
31 | 27, 29, 30 | expne0d 14113 |
. . . . . 6
β’ ((π β β€ β§ π β β0)
β (2βπ) β
0) |
32 | 31 | adantr 481 |
. . . . 5
β’ (((π β β€ β§ π β β0)
β§ π β
(bitsβπ)) β
(2βπ) β
0) |
33 | | z0even 16306 |
. . . . . . . . . 10
β’ 2 β₯
0 |
34 | | id 22 |
. . . . . . . . . 10
β’ ((((π mod (2β(π + 1))) β (π mod (2βπ))) / (2βπ)) = 0 β (((π mod (2β(π + 1))) β (π mod (2βπ))) / (2βπ)) = 0) |
35 | 33, 34 | breqtrrid 5185 |
. . . . . . . . 9
β’ ((((π mod (2β(π + 1))) β (π mod (2βπ))) / (2βπ)) = 0 β 2 β₯ (((π mod (2β(π + 1))) β (π mod (2βπ))) / (2βπ))) |
36 | | bitsval2 16362 |
. . . . . . . . . . 11
β’ ((π β β€ β§ π β β0)
β (π β
(bitsβπ) β Β¬
2 β₯ (ββ(π
/ (2βπ))))) |
37 | 5 | zred 12662 |
. . . . . . . . . . . . . . 15
β’ ((π β β€ β§ π β β0)
β π β
β) |
38 | 9 | nnrpd 13010 |
. . . . . . . . . . . . . . 15
β’ ((π β β€ β§ π β β0)
β (2βπ) β
β+) |
39 | | moddiffl 13843 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§
(2βπ) β
β+) β ((π β (π mod (2βπ))) / (2βπ)) = (ββ(π / (2βπ)))) |
40 | 37, 38, 39 | syl2anc 584 |
. . . . . . . . . . . . . 14
β’ ((π β β€ β§ π β β0)
β ((π β (π mod (2βπ))) / (2βπ)) = (ββ(π / (2βπ)))) |
41 | 40 | breq2d 5159 |
. . . . . . . . . . . . 13
β’ ((π β β€ β§ π β β0)
β (2 β₯ ((π
β (π mod
(2βπ))) /
(2βπ)) β 2
β₯ (ββ(π /
(2βπ))))) |
42 | | 2z 12590 |
. . . . . . . . . . . . . . 15
β’ 2 β
β€ |
43 | 42 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((π β β€ β§ π β β0)
β 2 β β€) |
44 | | moddifz 13844 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§
(2βπ) β
β+) β ((π β (π mod (2βπ))) / (2βπ)) β β€) |
45 | 37, 38, 44 | syl2anc 584 |
. . . . . . . . . . . . . 14
β’ ((π β β€ β§ π β β0)
β ((π β (π mod (2βπ))) / (2βπ)) β β€) |
46 | 5 | zcnd 12663 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β€ β§ π β β0)
β π β
β) |
47 | 46, 11, 18 | nnncan1d 11601 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β€ β§ π β β0)
β ((π β (π mod (2βπ))) β (π β (π mod (2β(π + 1))))) = ((π mod (2β(π + 1))) β (π mod (2βπ)))) |
48 | 47 | oveq1d 7420 |
. . . . . . . . . . . . . . . 16
β’ ((π β β€ β§ π β β0)
β (((π β (π mod (2βπ))) β (π β (π mod (2β(π + 1))))) / (2βπ)) = (((π mod (2β(π + 1))) β (π mod (2βπ))) / (2βπ))) |
49 | 46, 11 | subcld 11567 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β€ β§ π β β0)
β (π β (π mod (2βπ))) β β) |
50 | 46, 18 | subcld 11567 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β€ β§ π β β0)
β (π β (π mod (2β(π + 1)))) β β) |
51 | 9 | nncnd 12224 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β€ β§ π β β0)
β (2βπ) β
β) |
52 | 49, 50, 51, 31 | divsubdird 12025 |
. . . . . . . . . . . . . . . 16
β’ ((π β β€ β§ π β β0)
β (((π β (π mod (2βπ))) β (π β (π mod (2β(π + 1))))) / (2βπ)) = (((π β (π mod (2βπ))) / (2βπ)) β ((π β (π mod (2β(π + 1)))) / (2βπ)))) |
53 | 48, 52 | eqtr3d 2774 |
. . . . . . . . . . . . . . 15
β’ ((π β β€ β§ π β β0)
β (((π mod
(2β(π + 1))) β
(π mod (2βπ))) / (2βπ)) = (((π β (π mod (2βπ))) / (2βπ)) β ((π β (π mod (2β(π + 1)))) / (2βπ)))) |
54 | 27, 50 | mulcomd 11231 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β€ β§ π β β0)
β (2 Β· (π
β (π mod
(2β(π + 1))))) =
((π β (π mod (2β(π + 1)))) Β· 2)) |
55 | 27, 51 | mulcomd 11231 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β€ β§ π β β0)
β (2 Β· (2βπ)) = ((2βπ) Β· 2)) |
56 | 27, 8 | expp1d 14108 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β€ β§ π β β0)
β (2β(π + 1)) =
((2βπ) Β·
2)) |
57 | 55, 56 | eqtr4d 2775 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β€ β§ π β β0)
β (2 Β· (2βπ)) = (2β(π + 1))) |
58 | 54, 57 | oveq12d 7423 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β€ β§ π β β0)
β ((2 Β· (π
β (π mod
(2β(π + 1))))) / (2
Β· (2βπ))) =
(((π β (π mod (2β(π + 1)))) Β· 2) / (2β(π + 1)))) |
59 | 50, 51, 27, 31, 29 | divcan5d 12012 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β€ β§ π β β0)
β ((2 Β· (π
β (π mod
(2β(π + 1))))) / (2
Β· (2βπ))) =
((π β (π mod (2β(π + 1)))) / (2βπ))) |
60 | 16 | nncnd 12224 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β€ β§ π β β0)
β (2β(π + 1))
β β) |
61 | 30 | peano2zd 12665 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β€ β§ π β β0)
β (π + 1) β
β€) |
62 | 27, 29, 61 | expne0d 14113 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β€ β§ π β β0)
β (2β(π + 1))
β 0) |
63 | 50, 27, 60, 62 | div23d 12023 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β€ β§ π β β0)
β (((π β (π mod (2β(π + 1)))) Β· 2) / (2β(π + 1))) = (((π β (π mod (2β(π + 1)))) / (2β(π + 1))) Β· 2)) |
64 | 58, 59, 63 | 3eqtr3d 2780 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β€ β§ π β β0)
β ((π β (π mod (2β(π + 1)))) / (2βπ)) = (((π β (π mod (2β(π + 1)))) / (2β(π + 1))) Β· 2)) |
65 | 16 | nnrpd 13010 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β€ β§ π β β0)
β (2β(π + 1))
β β+) |
66 | | moddifz 13844 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β β§
(2β(π + 1)) β
β+) β ((π β (π mod (2β(π + 1)))) / (2β(π + 1))) β β€) |
67 | 37, 65, 66 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β€ β§ π β β0)
β ((π β (π mod (2β(π + 1)))) / (2β(π + 1))) β β€) |
68 | 67, 43 | zmulcld 12668 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β€ β§ π β β0)
β (((π β (π mod (2β(π + 1)))) / (2β(π + 1))) Β· 2) β
β€) |
69 | 64, 68 | eqeltrd 2833 |
. . . . . . . . . . . . . . . 16
β’ ((π β β€ β§ π β β0)
β ((π β (π mod (2β(π + 1)))) / (2βπ)) β β€) |
70 | 45, 69 | zsubcld 12667 |
. . . . . . . . . . . . . . 15
β’ ((π β β€ β§ π β β0)
β (((π β (π mod (2βπ))) / (2βπ)) β ((π β (π mod (2β(π + 1)))) / (2βπ))) β β€) |
71 | 53, 70 | eqeltrd 2833 |
. . . . . . . . . . . . . 14
β’ ((π β β€ β§ π β β0)
β (((π mod
(2β(π + 1))) β
(π mod (2βπ))) / (2βπ)) β β€) |
72 | | dvdsmul2 16218 |
. . . . . . . . . . . . . . . 16
β’ ((((π β (π mod (2β(π + 1)))) / (2β(π + 1))) β β€ β§ 2 β
β€) β 2 β₯ (((π β (π mod (2β(π + 1)))) / (2β(π + 1))) Β· 2)) |
73 | 67, 43, 72 | syl2anc 584 |
. . . . . . . . . . . . . . 15
β’ ((π β β€ β§ π β β0)
β 2 β₯ (((π
β (π mod
(2β(π + 1)))) /
(2β(π + 1))) Β·
2)) |
74 | 46, 18, 11 | nnncan2d 11602 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β€ β§ π β β0)
β ((π β (π mod (2βπ))) β ((π mod (2β(π + 1))) β (π mod (2βπ)))) = (π β (π mod (2β(π + 1))))) |
75 | 74 | oveq1d 7420 |
. . . . . . . . . . . . . . . 16
β’ ((π β β€ β§ π β β0)
β (((π β (π mod (2βπ))) β ((π mod (2β(π + 1))) β (π mod (2βπ)))) / (2βπ)) = ((π β (π mod (2β(π + 1)))) / (2βπ))) |
76 | 49, 21, 51, 31 | divsubdird 12025 |
. . . . . . . . . . . . . . . 16
β’ ((π β β€ β§ π β β0)
β (((π β (π mod (2βπ))) β ((π mod (2β(π + 1))) β (π mod (2βπ)))) / (2βπ)) = (((π β (π mod (2βπ))) / (2βπ)) β (((π mod (2β(π + 1))) β (π mod (2βπ))) / (2βπ)))) |
77 | 75, 76, 64 | 3eqtr3d 2780 |
. . . . . . . . . . . . . . 15
β’ ((π β β€ β§ π β β0)
β (((π β (π mod (2βπ))) / (2βπ)) β (((π mod (2β(π + 1))) β (π mod (2βπ))) / (2βπ))) = (((π β (π mod (2β(π + 1)))) / (2β(π + 1))) Β· 2)) |
78 | 73, 77 | breqtrrd 5175 |
. . . . . . . . . . . . . 14
β’ ((π β β€ β§ π β β0)
β 2 β₯ (((π
β (π mod
(2βπ))) /
(2βπ)) β
(((π mod (2β(π + 1))) β (π mod (2βπ))) / (2βπ)))) |
79 | | dvdssub2 16240 |
. . . . . . . . . . . . . 14
β’ (((2
β β€ β§ ((π
β (π mod
(2βπ))) /
(2βπ)) β β€
β§ (((π mod
(2β(π + 1))) β
(π mod (2βπ))) / (2βπ)) β β€) β§ 2 β₯ (((π β (π mod (2βπ))) / (2βπ)) β (((π mod (2β(π + 1))) β (π mod (2βπ))) / (2βπ)))) β (2 β₯ ((π β (π mod (2βπ))) / (2βπ)) β 2 β₯ (((π mod (2β(π + 1))) β (π mod (2βπ))) / (2βπ)))) |
80 | 43, 45, 71, 78, 79 | syl31anc 1373 |
. . . . . . . . . . . . 13
β’ ((π β β€ β§ π β β0)
β (2 β₯ ((π
β (π mod
(2βπ))) /
(2βπ)) β 2
β₯ (((π mod
(2β(π + 1))) β
(π mod (2βπ))) / (2βπ)))) |
81 | 41, 80 | bitr3d 280 |
. . . . . . . . . . . 12
β’ ((π β β€ β§ π β β0)
β (2 β₯ (ββ(π / (2βπ))) β 2 β₯ (((π mod (2β(π + 1))) β (π mod (2βπ))) / (2βπ)))) |
82 | 81 | notbid 317 |
. . . . . . . . . . 11
β’ ((π β β€ β§ π β β0)
β (Β¬ 2 β₯ (ββ(π / (2βπ))) β Β¬ 2 β₯ (((π mod (2β(π + 1))) β (π mod (2βπ))) / (2βπ)))) |
83 | 36, 82 | bitrd 278 |
. . . . . . . . . 10
β’ ((π β β€ β§ π β β0)
β (π β
(bitsβπ) β Β¬
2 β₯ (((π mod
(2β(π + 1))) β
(π mod (2βπ))) / (2βπ)))) |
84 | 83 | con2bid 354 |
. . . . . . . . 9
β’ ((π β β€ β§ π β β0)
β (2 β₯ (((π mod
(2β(π + 1))) β
(π mod (2βπ))) / (2βπ)) β Β¬ π β (bitsβπ))) |
85 | 35, 84 | imbitrid 243 |
. . . . . . . 8
β’ ((π β β€ β§ π β β0)
β ((((π mod
(2β(π + 1))) β
(π mod (2βπ))) / (2βπ)) = 0 β Β¬ π β (bitsβπ))) |
86 | 85 | con2d 134 |
. . . . . . 7
β’ ((π β β€ β§ π β β0)
β (π β
(bitsβπ) β Β¬
(((π mod (2β(π + 1))) β (π mod (2βπ))) / (2βπ)) = 0)) |
87 | | df-neg 11443 |
. . . . . . . . . . . . . . 15
β’ -1 = (0
β 1) |
88 | 51 | mulm1d 11662 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β€ β§ π β β0)
β (-1 Β· (2βπ)) = -(2βπ)) |
89 | 9 | nnred 12223 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β€ β§ π β β0)
β (2βπ) β
β) |
90 | 89 | renegcld 11637 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β€ β§ π β β0)
β -(2βπ) β
β) |
91 | 37, 38 | modcld 13836 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β€ β§ π β β0)
β (π mod (2βπ)) β
β) |
92 | 91 | renegcld 11637 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β€ β§ π β β0)
β -(π mod
(2βπ)) β
β) |
93 | 37, 65 | modcld 13836 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β€ β§ π β β0)
β (π mod
(2β(π + 1))) β
β) |
94 | 93, 91 | resubcld 11638 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β€ β§ π β β0)
β ((π mod
(2β(π + 1))) β
(π mod (2βπ))) β
β) |
95 | | modlt 13841 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β β§
(2βπ) β
β+) β (π mod (2βπ)) < (2βπ)) |
96 | 37, 38, 95 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β€ β§ π β β0)
β (π mod (2βπ)) < (2βπ)) |
97 | 91, 89 | ltnegd 11788 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β€ β§ π β β0)
β ((π mod
(2βπ)) <
(2βπ) β
-(2βπ) < -(π mod (2βπ)))) |
98 | 96, 97 | mpbid 231 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β€ β§ π β β0)
β -(2βπ) <
-(π mod (2βπ))) |
99 | | df-neg 11443 |
. . . . . . . . . . . . . . . . . . 19
β’ -(π mod (2βπ)) = (0 β (π mod (2βπ))) |
100 | | 0red 11213 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β€ β§ π β β0)
β 0 β β) |
101 | | modge0 13840 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β β β§
(2β(π + 1)) β
β+) β 0 β€ (π mod (2β(π + 1)))) |
102 | 37, 65, 101 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β€ β§ π β β0)
β 0 β€ (π mod
(2β(π +
1)))) |
103 | 100, 93, 91, 102 | lesub1dd 11826 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β€ β§ π β β0)
β (0 β (π mod
(2βπ))) β€ ((π mod (2β(π + 1))) β (π mod (2βπ)))) |
104 | 99, 103 | eqbrtrid 5182 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β€ β§ π β β0)
β -(π mod
(2βπ)) β€ ((π mod (2β(π + 1))) β (π mod (2βπ)))) |
105 | 90, 92, 94, 98, 104 | ltletrd 11370 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β€ β§ π β β0)
β -(2βπ) <
((π mod (2β(π + 1))) β (π mod (2βπ)))) |
106 | 88, 105 | eqbrtrd 5169 |
. . . . . . . . . . . . . . . 16
β’ ((π β β€ β§ π β β0)
β (-1 Β· (2βπ)) < ((π mod (2β(π + 1))) β (π mod (2βπ)))) |
107 | | 1red 11211 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β€ β§ π β β0)
β 1 β β) |
108 | 107 | renegcld 11637 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β€ β§ π β β0)
β -1 β β) |
109 | 108, 94, 38 | ltmuldivd 13059 |
. . . . . . . . . . . . . . . 16
β’ ((π β β€ β§ π β β0)
β ((-1 Β· (2βπ)) < ((π mod (2β(π + 1))) β (π mod (2βπ))) β -1 < (((π mod (2β(π + 1))) β (π mod (2βπ))) / (2βπ)))) |
110 | 106, 109 | mpbid 231 |
. . . . . . . . . . . . . . 15
β’ ((π β β€ β§ π β β0)
β -1 < (((π mod
(2β(π + 1))) β
(π mod (2βπ))) / (2βπ))) |
111 | 87, 110 | eqbrtrrid 5183 |
. . . . . . . . . . . . . 14
β’ ((π β β€ β§ π β β0)
β (0 β 1) < (((π mod (2β(π + 1))) β (π mod (2βπ))) / (2βπ))) |
112 | | 0zd 12566 |
. . . . . . . . . . . . . . 15
β’ ((π β β€ β§ π β β0)
β 0 β β€) |
113 | | zlem1lt 12610 |
. . . . . . . . . . . . . . 15
β’ ((0
β β€ β§ (((π
mod (2β(π + 1)))
β (π mod
(2βπ))) /
(2βπ)) β β€)
β (0 β€ (((π mod
(2β(π + 1))) β
(π mod (2βπ))) / (2βπ)) β (0 β 1) < (((π mod (2β(π + 1))) β (π mod (2βπ))) / (2βπ)))) |
114 | 112, 71, 113 | syl2anc 584 |
. . . . . . . . . . . . . 14
β’ ((π β β€ β§ π β β0)
β (0 β€ (((π mod
(2β(π + 1))) β
(π mod (2βπ))) / (2βπ)) β (0 β 1) < (((π mod (2β(π + 1))) β (π mod (2βπ))) / (2βπ)))) |
115 | 111, 114 | mpbird 256 |
. . . . . . . . . . . . 13
β’ ((π β β€ β§ π β β0)
β 0 β€ (((π mod
(2β(π + 1))) β
(π mod (2βπ))) / (2βπ))) |
116 | | elnn0z 12567 |
. . . . . . . . . . . . 13
β’ ((((π mod (2β(π + 1))) β (π mod (2βπ))) / (2βπ)) β β0 β
((((π mod (2β(π + 1))) β (π mod (2βπ))) / (2βπ)) β β€ β§ 0 β€ (((π mod (2β(π + 1))) β (π mod (2βπ))) / (2βπ)))) |
117 | 71, 115, 116 | sylanbrc 583 |
. . . . . . . . . . . 12
β’ ((π β β€ β§ π β β0)
β (((π mod
(2β(π + 1))) β
(π mod (2βπ))) / (2βπ)) β
β0) |
118 | | nn0uz 12860 |
. . . . . . . . . . . 12
β’
β0 = (β€β₯β0) |
119 | 117, 118 | eleqtrdi 2843 |
. . . . . . . . . . 11
β’ ((π β β€ β§ π β β0)
β (((π mod
(2β(π + 1))) β
(π mod (2βπ))) / (2βπ)) β
(β€β₯β0)) |
120 | 16 | nnred 12223 |
. . . . . . . . . . . . . 14
β’ ((π β β€ β§ π β β0)
β (2β(π + 1))
β β) |
121 | | modge0 13840 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§
(2βπ) β
β+) β 0 β€ (π mod (2βπ))) |
122 | 37, 38, 121 | syl2anc 584 |
. . . . . . . . . . . . . . 15
β’ ((π β β€ β§ π β β0)
β 0 β€ (π mod
(2βπ))) |
123 | 93, 91 | subge02d 11802 |
. . . . . . . . . . . . . . 15
β’ ((π β β€ β§ π β β0)
β (0 β€ (π mod
(2βπ)) β ((π mod (2β(π + 1))) β (π mod (2βπ))) β€ (π mod (2β(π + 1))))) |
124 | 122, 123 | mpbid 231 |
. . . . . . . . . . . . . 14
β’ ((π β β€ β§ π β β0)
β ((π mod
(2β(π + 1))) β
(π mod (2βπ))) β€ (π mod (2β(π + 1)))) |
125 | | modlt 13841 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§
(2β(π + 1)) β
β+) β (π mod (2β(π + 1))) < (2β(π + 1))) |
126 | 37, 65, 125 | syl2anc 584 |
. . . . . . . . . . . . . 14
β’ ((π β β€ β§ π β β0)
β (π mod
(2β(π + 1))) <
(2β(π +
1))) |
127 | 94, 93, 120, 124, 126 | lelttrd 11368 |
. . . . . . . . . . . . 13
β’ ((π β β€ β§ π β β0)
β ((π mod
(2β(π + 1))) β
(π mod (2βπ))) < (2β(π + 1))) |
128 | 127, 56 | breqtrd 5173 |
. . . . . . . . . . . 12
β’ ((π β β€ β§ π β β0)
β ((π mod
(2β(π + 1))) β
(π mod (2βπ))) < ((2βπ) Β· 2)) |
129 | 7 | nnred 12223 |
. . . . . . . . . . . . 13
β’ ((π β β€ β§ π β β0)
β 2 β β) |
130 | 94, 129, 38 | ltdivmuld 13063 |
. . . . . . . . . . . 12
β’ ((π β β€ β§ π β β0)
β ((((π mod
(2β(π + 1))) β
(π mod (2βπ))) / (2βπ)) < 2 β ((π mod (2β(π + 1))) β (π mod (2βπ))) < ((2βπ) Β· 2))) |
131 | 128, 130 | mpbird 256 |
. . . . . . . . . . 11
β’ ((π β β€ β§ π β β0)
β (((π mod
(2β(π + 1))) β
(π mod (2βπ))) / (2βπ)) < 2) |
132 | | elfzo2 13631 |
. . . . . . . . . . 11
β’ ((((π mod (2β(π + 1))) β (π mod (2βπ))) / (2βπ)) β (0..^2) β ((((π mod (2β(π + 1))) β (π mod (2βπ))) / (2βπ)) β (β€β₯β0)
β§ 2 β β€ β§ (((π mod (2β(π + 1))) β (π mod (2βπ))) / (2βπ)) < 2)) |
133 | 119, 43, 131, 132 | syl3anbrc 1343 |
. . . . . . . . . 10
β’ ((π β β€ β§ π β β0)
β (((π mod
(2β(π + 1))) β
(π mod (2βπ))) / (2βπ)) β (0..^2)) |
134 | | fzo0to2pr 13713 |
. . . . . . . . . 10
β’ (0..^2) =
{0, 1} |
135 | 133, 134 | eleqtrdi 2843 |
. . . . . . . . 9
β’ ((π β β€ β§ π β β0)
β (((π mod
(2β(π + 1))) β
(π mod (2βπ))) / (2βπ)) β {0, 1}) |
136 | | elpri 4649 |
. . . . . . . . 9
β’ ((((π mod (2β(π + 1))) β (π mod (2βπ))) / (2βπ)) β {0, 1} β ((((π mod (2β(π + 1))) β (π mod (2βπ))) / (2βπ)) = 0 β¨ (((π mod (2β(π + 1))) β (π mod (2βπ))) / (2βπ)) = 1)) |
137 | 135, 136 | syl 17 |
. . . . . . . 8
β’ ((π β β€ β§ π β β0)
β ((((π mod
(2β(π + 1))) β
(π mod (2βπ))) / (2βπ)) = 0 β¨ (((π mod (2β(π + 1))) β (π mod (2βπ))) / (2βπ)) = 1)) |
138 | 137 | ord 862 |
. . . . . . 7
β’ ((π β β€ β§ π β β0)
β (Β¬ (((π mod
(2β(π + 1))) β
(π mod (2βπ))) / (2βπ)) = 0 β (((π mod (2β(π + 1))) β (π mod (2βπ))) / (2βπ)) = 1)) |
139 | 86, 138 | syld 47 |
. . . . . 6
β’ ((π β β€ β§ π β β0)
β (π β
(bitsβπ) β
(((π mod (2β(π + 1))) β (π mod (2βπ))) / (2βπ)) = 1)) |
140 | 139 | imp 407 |
. . . . 5
β’ (((π β β€ β§ π β β0)
β§ π β
(bitsβπ)) β
(((π mod (2β(π + 1))) β (π mod (2βπ))) / (2βπ)) = 1) |
141 | 22, 26, 32, 140 | diveq1d 11994 |
. . . 4
β’ (((π β β€ β§ π β β0)
β§ π β
(bitsβπ)) β
((π mod (2β(π + 1))) β (π mod (2βπ))) = (2βπ)) |
142 | 141 | oveq2d 7421 |
. . 3
β’ (((π β β€ β§ π β β0)
β§ π β
(bitsβπ)) β
((π mod (2βπ)) + ((π mod (2β(π + 1))) β (π mod (2βπ)))) = ((π mod (2βπ)) + (2βπ))) |
143 | 20, 142 | eqtr3d 2774 |
. 2
β’ (((π β β€ β§ π β β0)
β§ π β
(bitsβπ)) β
(π mod (2β(π + 1))) = ((π mod (2βπ)) + (2βπ))) |
144 | 18 | adantr 481 |
. . . 4
β’ (((π β β€ β§ π β β0)
β§ Β¬ π β
(bitsβπ)) β
(π mod (2β(π + 1))) β
β) |
145 | 11 | adantr 481 |
. . . 4
β’ (((π β β€ β§ π β β0)
β§ Β¬ π β
(bitsβπ)) β
(π mod (2βπ)) β
β) |
146 | 21 | adantr 481 |
. . . . 5
β’ (((π β β€ β§ π β β0)
β§ Β¬ π β
(bitsβπ)) β
((π mod (2β(π + 1))) β (π mod (2βπ))) β β) |
147 | 51 | adantr 481 |
. . . . 5
β’ (((π β β€ β§ π β β0)
β§ Β¬ π β
(bitsβπ)) β
(2βπ) β
β) |
148 | 31 | adantr 481 |
. . . . 5
β’ (((π β β€ β§ π β β0)
β§ Β¬ π β
(bitsβπ)) β
(2βπ) β
0) |
149 | | n2dvds1 16307 |
. . . . . . . . . 10
β’ Β¬ 2
β₯ 1 |
150 | | breq2 5151 |
. . . . . . . . . 10
β’ ((((π mod (2β(π + 1))) β (π mod (2βπ))) / (2βπ)) = 1 β (2 β₯ (((π mod (2β(π + 1))) β (π mod (2βπ))) / (2βπ)) β 2 β₯ 1)) |
151 | 149, 150 | mtbiri 326 |
. . . . . . . . 9
β’ ((((π mod (2β(π + 1))) β (π mod (2βπ))) / (2βπ)) = 1 β Β¬ 2 β₯ (((π mod (2β(π + 1))) β (π mod (2βπ))) / (2βπ))) |
152 | 138, 151 | syl6 35 |
. . . . . . . 8
β’ ((π β β€ β§ π β β0)
β (Β¬ (((π mod
(2β(π + 1))) β
(π mod (2βπ))) / (2βπ)) = 0 β Β¬ 2 β₯ (((π mod (2β(π + 1))) β (π mod (2βπ))) / (2βπ)))) |
153 | 152, 83 | sylibrd 258 |
. . . . . . 7
β’ ((π β β€ β§ π β β0)
β (Β¬ (((π mod
(2β(π + 1))) β
(π mod (2βπ))) / (2βπ)) = 0 β π β (bitsβπ))) |
154 | 153 | con1d 145 |
. . . . . 6
β’ ((π β β€ β§ π β β0)
β (Β¬ π β
(bitsβπ) β
(((π mod (2β(π + 1))) β (π mod (2βπ))) / (2βπ)) = 0)) |
155 | 154 | imp 407 |
. . . . 5
β’ (((π β β€ β§ π β β0)
β§ Β¬ π β
(bitsβπ)) β
(((π mod (2β(π + 1))) β (π mod (2βπ))) / (2βπ)) = 0) |
156 | 146, 147,
148, 155 | diveq0d 11993 |
. . . 4
β’ (((π β β€ β§ π β β0)
β§ Β¬ π β
(bitsβπ)) β
((π mod (2β(π + 1))) β (π mod (2βπ))) = 0) |
157 | 144, 145,
156 | subeq0d 11575 |
. . 3
β’ (((π β β€ β§ π β β0)
β§ Β¬ π β
(bitsβπ)) β
(π mod (2β(π + 1))) = (π mod (2βπ))) |
158 | 145 | addridd 11410 |
. . 3
β’ (((π β β€ β§ π β β0)
β§ Β¬ π β
(bitsβπ)) β
((π mod (2βπ)) + 0) = (π mod (2βπ))) |
159 | 157, 158 | eqtr4d 2775 |
. 2
β’ (((π β β€ β§ π β β0)
β§ Β¬ π β
(bitsβπ)) β
(π mod (2β(π + 1))) = ((π mod (2βπ)) + 0)) |
160 | 2, 4, 143, 159 | ifbothda 4565 |
1
β’ ((π β β€ β§ π β β0)
β (π mod
(2β(π + 1))) = ((π mod (2βπ)) + if(π β (bitsβπ), (2βπ), 0))) |