Step | Hyp | Ref
| Expression |
1 | | bitsval2 16310 |
. . . . . . 7
β’ ((π β β€ β§ π β β0)
β (π β
(bitsβπ) β Β¬
2 β₯ (ββ(π
/ (2βπ))))) |
2 | | 2z 12540 |
. . . . . . . . . 10
β’ 2 β
β€ |
3 | 2 | a1i 11 |
. . . . . . . . 9
β’ ((π β β€ β§ π β β0)
β 2 β β€) |
4 | | simpl 484 |
. . . . . . . . . . . 12
β’ ((π β β€ β§ π β β0)
β π β
β€) |
5 | 4 | zred 12612 |
. . . . . . . . . . 11
β’ ((π β β€ β§ π β β0)
β π β
β) |
6 | | 2nn 12231 |
. . . . . . . . . . . . 13
β’ 2 β
β |
7 | 6 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β β€ β§ π β β0)
β 2 β β) |
8 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((π β β€ β§ π β β0)
β π β
β0) |
9 | 7, 8 | nnexpcld 14154 |
. . . . . . . . . . 11
β’ ((π β β€ β§ π β β0)
β (2βπ) β
β) |
10 | 5, 9 | nndivred 12212 |
. . . . . . . . . 10
β’ ((π β β€ β§ π β β0)
β (π / (2βπ)) β
β) |
11 | 10 | flcld 13709 |
. . . . . . . . 9
β’ ((π β β€ β§ π β β0)
β (ββ(π /
(2βπ))) β
β€) |
12 | | dvdsnegb 16161 |
. . . . . . . . 9
β’ ((2
β β€ β§ (ββ(π / (2βπ))) β β€) β (2 β₯
(ββ(π /
(2βπ))) β 2
β₯ -(ββ(π
/ (2βπ))))) |
13 | 3, 11, 12 | syl2anc 585 |
. . . . . . . 8
β’ ((π β β€ β§ π β β0)
β (2 β₯ (ββ(π / (2βπ))) β 2 β₯ -(ββ(π / (2βπ))))) |
14 | 13 | notbid 318 |
. . . . . . 7
β’ ((π β β€ β§ π β β0)
β (Β¬ 2 β₯ (ββ(π / (2βπ))) β Β¬ 2 β₯
-(ββ(π /
(2βπ))))) |
15 | 11 | znegcld 12614 |
. . . . . . . . 9
β’ ((π β β€ β§ π β β0)
β -(ββ(π /
(2βπ))) β
β€) |
16 | | oddm1even 16230 |
. . . . . . . . 9
β’
(-(ββ(π
/ (2βπ))) β
β€ β (Β¬ 2 β₯ -(ββ(π / (2βπ))) β 2 β₯ (-(ββ(π / (2βπ))) β 1))) |
17 | 15, 16 | syl 17 |
. . . . . . . 8
β’ ((π β β€ β§ π β β0)
β (Β¬ 2 β₯ -(ββ(π / (2βπ))) β 2 β₯ (-(ββ(π / (2βπ))) β 1))) |
18 | | flltp1 13711 |
. . . . . . . . . . . . . . . 16
β’ ((π / (2βπ)) β β β (π / (2βπ)) < ((ββ(π / (2βπ))) + 1)) |
19 | 10, 18 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π β β€ β§ π β β0)
β (π / (2βπ)) < ((ββ(π / (2βπ))) + 1)) |
20 | 11 | zred 12612 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β€ β§ π β β0)
β (ββ(π /
(2βπ))) β
β) |
21 | | 1red 11161 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β€ β§ π β β0)
β 1 β β) |
22 | 20, 21 | readdcld 11189 |
. . . . . . . . . . . . . . . 16
β’ ((π β β€ β§ π β β0)
β ((ββ(π /
(2βπ))) + 1) β
β) |
23 | 10, 22 | ltnegd 11738 |
. . . . . . . . . . . . . . 15
β’ ((π β β€ β§ π β β0)
β ((π / (2βπ)) < ((ββ(π / (2βπ))) + 1) β -((ββ(π / (2βπ))) + 1) < -(π / (2βπ)))) |
24 | 19, 23 | mpbid 231 |
. . . . . . . . . . . . . 14
β’ ((π β β€ β§ π β β0)
β -((ββ(π
/ (2βπ))) + 1) <
-(π / (2βπ))) |
25 | 20 | recnd 11188 |
. . . . . . . . . . . . . . 15
β’ ((π β β€ β§ π β β0)
β (ββ(π /
(2βπ))) β
β) |
26 | 21 | recnd 11188 |
. . . . . . . . . . . . . . 15
β’ ((π β β€ β§ π β β0)
β 1 β β) |
27 | 25, 26 | negdi2d 11531 |
. . . . . . . . . . . . . 14
β’ ((π β β€ β§ π β β0)
β -((ββ(π
/ (2βπ))) + 1) =
(-(ββ(π /
(2βπ))) β
1)) |
28 | 5 | recnd 11188 |
. . . . . . . . . . . . . . 15
β’ ((π β β€ β§ π β β0)
β π β
β) |
29 | 9 | nncnd 12174 |
. . . . . . . . . . . . . . 15
β’ ((π β β€ β§ π β β0)
β (2βπ) β
β) |
30 | 9 | nnne0d 12208 |
. . . . . . . . . . . . . . 15
β’ ((π β β€ β§ π β β0)
β (2βπ) β
0) |
31 | 28, 29, 30 | divnegd 11949 |
. . . . . . . . . . . . . 14
β’ ((π β β€ β§ π β β0)
β -(π / (2βπ)) = (-π / (2βπ))) |
32 | 24, 27, 31 | 3brtr3d 5137 |
. . . . . . . . . . . . 13
β’ ((π β β€ β§ π β β0)
β (-(ββ(π
/ (2βπ))) β 1)
< (-π / (2βπ))) |
33 | | 1zzd 12539 |
. . . . . . . . . . . . . . . 16
β’ ((π β β€ β§ π β β0)
β 1 β β€) |
34 | 15, 33 | zsubcld 12617 |
. . . . . . . . . . . . . . 15
β’ ((π β β€ β§ π β β0)
β (-(ββ(π
/ (2βπ))) β 1)
β β€) |
35 | 34 | zred 12612 |
. . . . . . . . . . . . . 14
β’ ((π β β€ β§ π β β0)
β (-(ββ(π
/ (2βπ))) β 1)
β β) |
36 | 5 | renegcld 11587 |
. . . . . . . . . . . . . 14
β’ ((π β β€ β§ π β β0)
β -π β
β) |
37 | 9 | nnrpd 12960 |
. . . . . . . . . . . . . 14
β’ ((π β β€ β§ π β β0)
β (2βπ) β
β+) |
38 | 35, 36, 37 | ltmuldivd 13009 |
. . . . . . . . . . . . 13
β’ ((π β β€ β§ π β β0)
β (((-(ββ(π / (2βπ))) β 1) Β· (2βπ)) < -π β (-(ββ(π / (2βπ))) β 1) < (-π / (2βπ)))) |
39 | 32, 38 | mpbird 257 |
. . . . . . . . . . . 12
β’ ((π β β€ β§ π β β0)
β ((-(ββ(π
/ (2βπ))) β 1)
Β· (2βπ)) <
-π) |
40 | 9 | nnzd 12531 |
. . . . . . . . . . . . . 14
β’ ((π β β€ β§ π β β0)
β (2βπ) β
β€) |
41 | 34, 40 | zmulcld 12618 |
. . . . . . . . . . . . 13
β’ ((π β β€ β§ π β β0)
β ((-(ββ(π
/ (2βπ))) β 1)
Β· (2βπ)) β
β€) |
42 | 4 | znegcld 12614 |
. . . . . . . . . . . . 13
β’ ((π β β€ β§ π β β0)
β -π β
β€) |
43 | | zltlem1 12561 |
. . . . . . . . . . . . 13
β’
((((-(ββ(π / (2βπ))) β 1) Β· (2βπ)) β β€ β§ -π β β€) β
(((-(ββ(π /
(2βπ))) β 1)
Β· (2βπ)) <
-π β
((-(ββ(π /
(2βπ))) β 1)
Β· (2βπ)) β€
(-π β
1))) |
44 | 41, 42, 43 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((π β β€ β§ π β β0)
β (((-(ββ(π / (2βπ))) β 1) Β· (2βπ)) < -π β ((-(ββ(π / (2βπ))) β 1) Β· (2βπ)) β€ (-π β 1))) |
45 | 39, 44 | mpbid 231 |
. . . . . . . . . . 11
β’ ((π β β€ β§ π β β0)
β ((-(ββ(π
/ (2βπ))) β 1)
Β· (2βπ)) β€
(-π β
1)) |
46 | 36, 21 | resubcld 11588 |
. . . . . . . . . . . 12
β’ ((π β β€ β§ π β β0)
β (-π β 1)
β β) |
47 | 35, 46, 37 | lemuldivd 13011 |
. . . . . . . . . . 11
β’ ((π β β€ β§ π β β0)
β (((-(ββ(π / (2βπ))) β 1) Β· (2βπ)) β€ (-π β 1) β (-(ββ(π / (2βπ))) β 1) β€ ((-π β 1) / (2βπ)))) |
48 | 45, 47 | mpbid 231 |
. . . . . . . . . 10
β’ ((π β β€ β§ π β β0)
β (-(ββ(π
/ (2βπ))) β 1)
β€ ((-π β 1) /
(2βπ))) |
49 | | flle 13710 |
. . . . . . . . . . . . . . . . 17
β’ ((π / (2βπ)) β β β
(ββ(π /
(2βπ))) β€ (π / (2βπ))) |
50 | 10, 49 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((π β β€ β§ π β β0)
β (ββ(π /
(2βπ))) β€ (π / (2βπ))) |
51 | 20, 10 | lenegd 11739 |
. . . . . . . . . . . . . . . 16
β’ ((π β β€ β§ π β β0)
β ((ββ(π /
(2βπ))) β€ (π / (2βπ)) β -(π / (2βπ)) β€ -(ββ(π / (2βπ))))) |
52 | 50, 51 | mpbid 231 |
. . . . . . . . . . . . . . 15
β’ ((π β β€ β§ π β β0)
β -(π / (2βπ)) β€ -(ββ(π / (2βπ)))) |
53 | 31, 52 | eqbrtrrd 5130 |
. . . . . . . . . . . . . 14
β’ ((π β β€ β§ π β β0)
β (-π / (2βπ)) β€ -(ββ(π / (2βπ)))) |
54 | 20 | renegcld 11587 |
. . . . . . . . . . . . . . 15
β’ ((π β β€ β§ π β β0)
β -(ββ(π /
(2βπ))) β
β) |
55 | 36, 54, 37 | ledivmuld 13015 |
. . . . . . . . . . . . . 14
β’ ((π β β€ β§ π β β0)
β ((-π / (2βπ)) β€ -(ββ(π / (2βπ))) β -π β€ ((2βπ) Β· -(ββ(π / (2βπ)))))) |
56 | 53, 55 | mpbid 231 |
. . . . . . . . . . . . 13
β’ ((π β β€ β§ π β β0)
β -π β€
((2βπ) Β·
-(ββ(π /
(2βπ))))) |
57 | 40, 15 | zmulcld 12618 |
. . . . . . . . . . . . . 14
β’ ((π β β€ β§ π β β0)
β ((2βπ) Β·
-(ββ(π /
(2βπ)))) β
β€) |
58 | | zlem1lt 12560 |
. . . . . . . . . . . . . 14
β’ ((-π β β€ β§
((2βπ) Β·
-(ββ(π /
(2βπ)))) β
β€) β (-π β€
((2βπ) Β·
-(ββ(π /
(2βπ)))) β
(-π β 1) <
((2βπ) Β·
-(ββ(π /
(2βπ)))))) |
59 | 42, 57, 58 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((π β β€ β§ π β β0)
β (-π β€
((2βπ) Β·
-(ββ(π /
(2βπ)))) β
(-π β 1) <
((2βπ) Β·
-(ββ(π /
(2βπ)))))) |
60 | 56, 59 | mpbid 231 |
. . . . . . . . . . . 12
β’ ((π β β€ β§ π β β0)
β (-π β 1) <
((2βπ) Β·
-(ββ(π /
(2βπ))))) |
61 | 46, 54, 37 | ltdivmuld 13013 |
. . . . . . . . . . . 12
β’ ((π β β€ β§ π β β0)
β (((-π β 1) /
(2βπ)) <
-(ββ(π /
(2βπ))) β (-π β 1) < ((2βπ) Β·
-(ββ(π /
(2βπ)))))) |
62 | 60, 61 | mpbird 257 |
. . . . . . . . . . 11
β’ ((π β β€ β§ π β β0)
β ((-π β 1) /
(2βπ)) <
-(ββ(π /
(2βπ)))) |
63 | 25 | negcld 11504 |
. . . . . . . . . . . 12
β’ ((π β β€ β§ π β β0)
β -(ββ(π /
(2βπ))) β
β) |
64 | 63, 26 | npcand 11521 |
. . . . . . . . . . 11
β’ ((π β β€ β§ π β β0)
β ((-(ββ(π
/ (2βπ))) β 1) +
1) = -(ββ(π /
(2βπ)))) |
65 | 62, 64 | breqtrrd 5134 |
. . . . . . . . . 10
β’ ((π β β€ β§ π β β0)
β ((-π β 1) /
(2βπ)) <
((-(ββ(π /
(2βπ))) β 1) +
1)) |
66 | 46, 9 | nndivred 12212 |
. . . . . . . . . . 11
β’ ((π β β€ β§ π β β0)
β ((-π β 1) /
(2βπ)) β
β) |
67 | | flbi 13727 |
. . . . . . . . . . 11
β’
((((-π β 1) /
(2βπ)) β β
β§ (-(ββ(π /
(2βπ))) β 1)
β β€) β ((ββ((-π β 1) / (2βπ))) = (-(ββ(π / (2βπ))) β 1) β
((-(ββ(π /
(2βπ))) β 1)
β€ ((-π β 1) /
(2βπ)) β§ ((-π β 1) / (2βπ)) < ((-(ββ(π / (2βπ))) β 1) + 1)))) |
68 | 66, 34, 67 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π β β€ β§ π β β0)
β ((ββ((-π
β 1) / (2βπ))) =
(-(ββ(π /
(2βπ))) β 1)
β ((-(ββ(π
/ (2βπ))) β 1)
β€ ((-π β 1) /
(2βπ)) β§ ((-π β 1) / (2βπ)) < ((-(ββ(π / (2βπ))) β 1) + 1)))) |
69 | 48, 65, 68 | mpbir2and 712 |
. . . . . . . . 9
β’ ((π β β€ β§ π β β0)
β (ββ((-π
β 1) / (2βπ))) =
(-(ββ(π /
(2βπ))) β
1)) |
70 | 69 | breq2d 5118 |
. . . . . . . 8
β’ ((π β β€ β§ π β β0)
β (2 β₯ (ββ((-π β 1) / (2βπ))) β 2 β₯ (-(ββ(π / (2βπ))) β 1))) |
71 | 17, 70 | bitr4d 282 |
. . . . . . 7
β’ ((π β β€ β§ π β β0)
β (Β¬ 2 β₯ -(ββ(π / (2βπ))) β 2 β₯ (ββ((-π β 1) / (2βπ))))) |
72 | 1, 14, 71 | 3bitrd 305 |
. . . . . 6
β’ ((π β β€ β§ π β β0)
β (π β
(bitsβπ) β 2
β₯ (ββ((-π
β 1) / (2βπ))))) |
73 | 72 | notbid 318 |
. . . . 5
β’ ((π β β€ β§ π β β0)
β (Β¬ π β
(bitsβπ) β Β¬
2 β₯ (ββ((-π β 1) / (2βπ))))) |
74 | 73 | pm5.32da 580 |
. . . 4
β’ (π β β€ β ((π β β0
β§ Β¬ π β
(bitsβπ)) β
(π β
β0 β§ Β¬ 2 β₯ (ββ((-π β 1) / (2βπ)))))) |
75 | | znegcl 12543 |
. . . . . 6
β’ (π β β€ β -π β
β€) |
76 | | 1zzd 12539 |
. . . . . 6
β’ (π β β€ β 1 β
β€) |
77 | 75, 76 | zsubcld 12617 |
. . . . 5
β’ (π β β€ β (-π β 1) β
β€) |
78 | 77 | biantrurd 534 |
. . . 4
β’ (π β β€ β ((π β β0
β§ Β¬ 2 β₯ (ββ((-π β 1) / (2βπ)))) β ((-π β 1) β β€ β§ (π β β0
β§ Β¬ 2 β₯ (ββ((-π β 1) / (2βπ))))))) |
79 | 74, 78 | bitrd 279 |
. . 3
β’ (π β β€ β ((π β β0
β§ Β¬ π β
(bitsβπ)) β
((-π β 1) β
β€ β§ (π β
β0 β§ Β¬ 2 β₯ (ββ((-π β 1) / (2βπ))))))) |
80 | | eldif 3921 |
. . 3
β’ (π β (β0
β (bitsβπ))
β (π β
β0 β§ Β¬ π β (bitsβπ))) |
81 | | bitsval 16309 |
. . . 4
β’ (π β (bitsβ(-π β 1)) β ((-π β 1) β β€ β§
π β
β0 β§ Β¬ 2 β₯ (ββ((-π β 1) / (2βπ))))) |
82 | | 3anass 1096 |
. . . 4
β’ (((-π β 1) β β€ β§
π β
β0 β§ Β¬ 2 β₯ (ββ((-π β 1) / (2βπ)))) β ((-π β 1) β β€ β§ (π β β0
β§ Β¬ 2 β₯ (ββ((-π β 1) / (2βπ)))))) |
83 | 81, 82 | bitri 275 |
. . 3
β’ (π β (bitsβ(-π β 1)) β ((-π β 1) β β€ β§
(π β
β0 β§ Β¬ 2 β₯ (ββ((-π β 1) / (2βπ)))))) |
84 | 79, 80, 83 | 3bitr4g 314 |
. 2
β’ (π β β€ β (π β (β0
β (bitsβπ))
β π β
(bitsβ(-π β
1)))) |
85 | 84 | eqrdv 2731 |
1
β’ (π β β€ β
(β0 β (bitsβπ)) = (bitsβ(-π β 1))) |