Step | Hyp | Ref
| Expression |
1 | | bitsval 16311 |
. . . 4
β’ (π β (bitsβπ) β (π β β€ β§ π β β0 β§ Β¬ 2
β₯ (ββ(π /
(2βπ))))) |
2 | | simp32 1211 |
. . . . . . 7
β’ (((π β β€ β§ π β β0)
β§ π β
(0..^(2βπ)) β§
(π β β€ β§
π β
β0 β§ Β¬ 2 β₯ (ββ(π / (2βπ))))) β π β β0) |
3 | | nn0uz 12812 |
. . . . . . 7
β’
β0 = (β€β₯β0) |
4 | 2, 3 | eleqtrdi 2848 |
. . . . . 6
β’ (((π β β€ β§ π β β0)
β§ π β
(0..^(2βπ)) β§
(π β β€ β§
π β
β0 β§ Β¬ 2 β₯ (ββ(π / (2βπ))))) β π β
(β€β₯β0)) |
5 | | simp1r 1199 |
. . . . . . 7
β’ (((π β β€ β§ π β β0)
β§ π β
(0..^(2βπ)) β§
(π β β€ β§
π β
β0 β§ Β¬ 2 β₯ (ββ(π / (2βπ))))) β π β
β0) |
6 | 5 | nn0zd 12532 |
. . . . . 6
β’ (((π β β€ β§ π β β0)
β§ π β
(0..^(2βπ)) β§
(π β β€ β§
π β
β0 β§ Β¬ 2 β₯ (ββ(π / (2βπ))))) β π β β€) |
7 | | 2re 12234 |
. . . . . . . . . 10
β’ 2 β
β |
8 | 7 | a1i 11 |
. . . . . . . . 9
β’ (((π β β€ β§ π β β0)
β§ π β
(0..^(2βπ)) β§
(π β β€ β§
π β
β0 β§ Β¬ 2 β₯ (ββ(π / (2βπ))))) β 2 β
β) |
9 | 8, 2 | reexpcld 14075 |
. . . . . . . 8
β’ (((π β β€ β§ π β β0)
β§ π β
(0..^(2βπ)) β§
(π β β€ β§
π β
β0 β§ Β¬ 2 β₯ (ββ(π / (2βπ))))) β (2βπ) β β) |
10 | | simp1l 1198 |
. . . . . . . . 9
β’ (((π β β€ β§ π β β0)
β§ π β
(0..^(2βπ)) β§
(π β β€ β§
π β
β0 β§ Β¬ 2 β₯ (ββ(π / (2βπ))))) β π β β€) |
11 | 10 | zred 12614 |
. . . . . . . 8
β’ (((π β β€ β§ π β β0)
β§ π β
(0..^(2βπ)) β§
(π β β€ β§
π β
β0 β§ Β¬ 2 β₯ (ββ(π / (2βπ))))) β π β β) |
12 | 8, 5 | reexpcld 14075 |
. . . . . . . 8
β’ (((π β β€ β§ π β β0)
β§ π β
(0..^(2βπ)) β§
(π β β€ β§
π β
β0 β§ Β¬ 2 β₯ (ββ(π / (2βπ))))) β (2βπ) β β) |
13 | 9 | recnd 11190 |
. . . . . . . . . 10
β’ (((π β β€ β§ π β β0)
β§ π β
(0..^(2βπ)) β§
(π β β€ β§
π β
β0 β§ Β¬ 2 β₯ (ββ(π / (2βπ))))) β (2βπ) β β) |
14 | 13 | mulid2d 11180 |
. . . . . . . . 9
β’ (((π β β€ β§ π β β0)
β§ π β
(0..^(2βπ)) β§
(π β β€ β§
π β
β0 β§ Β¬ 2 β₯ (ββ(π / (2βπ))))) β (1 Β· (2βπ)) = (2βπ)) |
15 | | simp33 1212 |
. . . . . . . . . . 11
β’ (((π β β€ β§ π β β0)
β§ π β
(0..^(2βπ)) β§
(π β β€ β§
π β
β0 β§ Β¬ 2 β₯ (ββ(π / (2βπ))))) β Β¬ 2 β₯
(ββ(π /
(2βπ)))) |
16 | | 2rp 12927 |
. . . . . . . . . . . . . . . 16
β’ 2 β
β+ |
17 | 16 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (((π β β€ β§ π β β0)
β§ π β
(0..^(2βπ)) β§
(π β β€ β§
π β
β0 β§ Β¬ 2 β₯ (ββ(π / (2βπ))))) β 2 β
β+) |
18 | 2 | nn0zd 12532 |
. . . . . . . . . . . . . . 15
β’ (((π β β€ β§ π β β0)
β§ π β
(0..^(2βπ)) β§
(π β β€ β§
π β
β0 β§ Β¬ 2 β₯ (ββ(π / (2βπ))))) β π β β€) |
19 | 17, 18 | rpexpcld 14157 |
. . . . . . . . . . . . . 14
β’ (((π β β€ β§ π β β0)
β§ π β
(0..^(2βπ)) β§
(π β β€ β§
π β
β0 β§ Β¬ 2 β₯ (ββ(π / (2βπ))))) β (2βπ) β
β+) |
20 | 11, 19 | rerpdivcld 12995 |
. . . . . . . . . . . . 13
β’ (((π β β€ β§ π β β0)
β§ π β
(0..^(2βπ)) β§
(π β β€ β§
π β
β0 β§ Β¬ 2 β₯ (ββ(π / (2βπ))))) β (π / (2βπ)) β β) |
21 | | 1red 11163 |
. . . . . . . . . . . . 13
β’ (((π β β€ β§ π β β0)
β§ π β
(0..^(2βπ)) β§
(π β β€ β§
π β
β0 β§ Β¬ 2 β₯ (ββ(π / (2βπ))))) β 1 β
β) |
22 | 20, 21 | ltnled 11309 |
. . . . . . . . . . . 12
β’ (((π β β€ β§ π β β0)
β§ π β
(0..^(2βπ)) β§
(π β β€ β§
π β
β0 β§ Β¬ 2 β₯ (ββ(π / (2βπ))))) β ((π / (2βπ)) < 1 β Β¬ 1 β€ (π / (2βπ)))) |
23 | | 0p1e1 12282 |
. . . . . . . . . . . . . 14
β’ (0 + 1) =
1 |
24 | 23 | breq2i 5118 |
. . . . . . . . . . . . 13
β’ ((π / (2βπ)) < (0 + 1) β (π / (2βπ)) < 1) |
25 | | elfzole1 13587 |
. . . . . . . . . . . . . . . 16
β’ (π β (0..^(2βπ)) β 0 β€ π) |
26 | 25 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . 15
β’ (((π β β€ β§ π β β0)
β§ π β
(0..^(2βπ)) β§
(π β β€ β§
π β
β0 β§ Β¬ 2 β₯ (ββ(π / (2βπ))))) β 0 β€ π) |
27 | 11, 19, 26 | divge0d 13004 |
. . . . . . . . . . . . . 14
β’ (((π β β€ β§ π β β0)
β§ π β
(0..^(2βπ)) β§
(π β β€ β§
π β
β0 β§ Β¬ 2 β₯ (ββ(π / (2βπ))))) β 0 β€ (π / (2βπ))) |
28 | | 0z 12517 |
. . . . . . . . . . . . . . . 16
β’ 0 β
β€ |
29 | | flbi 13728 |
. . . . . . . . . . . . . . . 16
β’ (((π / (2βπ)) β β β§ 0 β β€)
β ((ββ(π /
(2βπ))) = 0 β (0
β€ (π / (2βπ)) β§ (π / (2βπ)) < (0 + 1)))) |
30 | 20, 28, 29 | sylancl 587 |
. . . . . . . . . . . . . . 15
β’ (((π β β€ β§ π β β0)
β§ π β
(0..^(2βπ)) β§
(π β β€ β§
π β
β0 β§ Β¬ 2 β₯ (ββ(π / (2βπ))))) β ((ββ(π / (2βπ))) = 0 β (0 β€ (π / (2βπ)) β§ (π / (2βπ)) < (0 + 1)))) |
31 | | z0even 16256 |
. . . . . . . . . . . . . . . 16
β’ 2 β₯
0 |
32 | | id 22 |
. . . . . . . . . . . . . . . 16
β’
((ββ(π /
(2βπ))) = 0 β
(ββ(π /
(2βπ))) =
0) |
33 | 31, 32 | breqtrrid 5148 |
. . . . . . . . . . . . . . 15
β’
((ββ(π /
(2βπ))) = 0 β 2
β₯ (ββ(π /
(2βπ)))) |
34 | 30, 33 | syl6bir 254 |
. . . . . . . . . . . . . 14
β’ (((π β β€ β§ π β β0)
β§ π β
(0..^(2βπ)) β§
(π β β€ β§
π β
β0 β§ Β¬ 2 β₯ (ββ(π / (2βπ))))) β ((0 β€ (π / (2βπ)) β§ (π / (2βπ)) < (0 + 1)) β 2 β₯
(ββ(π /
(2βπ))))) |
35 | 27, 34 | mpand 694 |
. . . . . . . . . . . . 13
β’ (((π β β€ β§ π β β0)
β§ π β
(0..^(2βπ)) β§
(π β β€ β§
π β
β0 β§ Β¬ 2 β₯ (ββ(π / (2βπ))))) β ((π / (2βπ)) < (0 + 1) β 2 β₯
(ββ(π /
(2βπ))))) |
36 | 24, 35 | biimtrrid 242 |
. . . . . . . . . . . 12
β’ (((π β β€ β§ π β β0)
β§ π β
(0..^(2βπ)) β§
(π β β€ β§
π β
β0 β§ Β¬ 2 β₯ (ββ(π / (2βπ))))) β ((π / (2βπ)) < 1 β 2 β₯
(ββ(π /
(2βπ))))) |
37 | 22, 36 | sylbird 260 |
. . . . . . . . . . 11
β’ (((π β β€ β§ π β β0)
β§ π β
(0..^(2βπ)) β§
(π β β€ β§
π β
β0 β§ Β¬ 2 β₯ (ββ(π / (2βπ))))) β (Β¬ 1 β€ (π / (2βπ)) β 2 β₯ (ββ(π / (2βπ))))) |
38 | 15, 37 | mt3d 148 |
. . . . . . . . . 10
β’ (((π β β€ β§ π β β0)
β§ π β
(0..^(2βπ)) β§
(π β β€ β§
π β
β0 β§ Β¬ 2 β₯ (ββ(π / (2βπ))))) β 1 β€ (π / (2βπ))) |
39 | 21, 11, 19 | lemuldivd 13013 |
. . . . . . . . . 10
β’ (((π β β€ β§ π β β0)
β§ π β
(0..^(2βπ)) β§
(π β β€ β§
π β
β0 β§ Β¬ 2 β₯ (ββ(π / (2βπ))))) β ((1 Β· (2βπ)) β€ π β 1 β€ (π / (2βπ)))) |
40 | 38, 39 | mpbird 257 |
. . . . . . . . 9
β’ (((π β β€ β§ π β β0)
β§ π β
(0..^(2βπ)) β§
(π β β€ β§
π β
β0 β§ Β¬ 2 β₯ (ββ(π / (2βπ))))) β (1 Β· (2βπ)) β€ π) |
41 | 14, 40 | eqbrtrrd 5134 |
. . . . . . . 8
β’ (((π β β€ β§ π β β0)
β§ π β
(0..^(2βπ)) β§
(π β β€ β§
π β
β0 β§ Β¬ 2 β₯ (ββ(π / (2βπ))))) β (2βπ) β€ π) |
42 | | elfzolt2 13588 |
. . . . . . . . 9
β’ (π β (0..^(2βπ)) β π < (2βπ)) |
43 | 42 | 3ad2ant2 1135 |
. . . . . . . 8
β’ (((π β β€ β§ π β β0)
β§ π β
(0..^(2βπ)) β§
(π β β€ β§
π β
β0 β§ Β¬ 2 β₯ (ββ(π / (2βπ))))) β π < (2βπ)) |
44 | 9, 11, 12, 41, 43 | lelttrd 11320 |
. . . . . . 7
β’ (((π β β€ β§ π β β0)
β§ π β
(0..^(2βπ)) β§
(π β β€ β§
π β
β0 β§ Β¬ 2 β₯ (ββ(π / (2βπ))))) β (2βπ) < (2βπ)) |
45 | | 1lt2 12331 |
. . . . . . . . 9
β’ 1 <
2 |
46 | 45 | a1i 11 |
. . . . . . . 8
β’ (((π β β€ β§ π β β0)
β§ π β
(0..^(2βπ)) β§
(π β β€ β§
π β
β0 β§ Β¬ 2 β₯ (ββ(π / (2βπ))))) β 1 < 2) |
47 | 8, 18, 6, 46 | ltexp2d 14161 |
. . . . . . 7
β’ (((π β β€ β§ π β β0)
β§ π β
(0..^(2βπ)) β§
(π β β€ β§
π β
β0 β§ Β¬ 2 β₯ (ββ(π / (2βπ))))) β (π < π β (2βπ) < (2βπ))) |
48 | 44, 47 | mpbird 257 |
. . . . . 6
β’ (((π β β€ β§ π β β0)
β§ π β
(0..^(2βπ)) β§
(π β β€ β§
π β
β0 β§ Β¬ 2 β₯ (ββ(π / (2βπ))))) β π < π) |
49 | | elfzo2 13582 |
. . . . . 6
β’ (π β (0..^π) β (π β (β€β₯β0)
β§ π β β€
β§ π < π)) |
50 | 4, 6, 48, 49 | syl3anbrc 1344 |
. . . . 5
β’ (((π β β€ β§ π β β0)
β§ π β
(0..^(2βπ)) β§
(π β β€ β§
π β
β0 β§ Β¬ 2 β₯ (ββ(π / (2βπ))))) β π β (0..^π)) |
51 | 50 | 3expia 1122 |
. . . 4
β’ (((π β β€ β§ π β β0)
β§ π β
(0..^(2βπ))) β
((π β β€ β§
π β
β0 β§ Β¬ 2 β₯ (ββ(π / (2βπ)))) β π β (0..^π))) |
52 | 1, 51 | biimtrid 241 |
. . 3
β’ (((π β β€ β§ π β β0)
β§ π β
(0..^(2βπ))) β
(π β (bitsβπ) β π β (0..^π))) |
53 | 52 | ssrdv 3955 |
. 2
β’ (((π β β€ β§ π β β0)
β§ π β
(0..^(2βπ))) β
(bitsβπ) β
(0..^π)) |
54 | | simpr 486 |
. . . . . . . 8
β’ ((((π β β€ β§ π β β0)
β§ (bitsβπ)
β (0..^π)) β§
-π β β) β
-π β
β) |
55 | 54 | nnred 12175 |
. . . . . . 7
β’ ((((π β β€ β§ π β β0)
β§ (bitsβπ)
β (0..^π)) β§
-π β β) β
-π β
β) |
56 | | simpllr 775 |
. . . . . . . 8
β’ ((((π β β€ β§ π β β0)
β§ (bitsβπ)
β (0..^π)) β§
-π β β) β
π β
β0) |
57 | 56 | nn0red 12481 |
. . . . . . 7
β’ ((((π β β€ β§ π β β0)
β§ (bitsβπ)
β (0..^π)) β§
-π β β) β
π β
β) |
58 | | max2 13113 |
. . . . . . 7
β’ ((-π β β β§ π β β) β π β€ if(-π β€ π, π, -π)) |
59 | 55, 57, 58 | syl2anc 585 |
. . . . . 6
β’ ((((π β β€ β§ π β β0)
β§ (bitsβπ)
β (0..^π)) β§
-π β β) β
π β€ if(-π β€ π, π, -π)) |
60 | | simplr 768 |
. . . . . . . . 9
β’ ((((π β β€ β§ π β β0)
β§ (bitsβπ)
β (0..^π)) β§
-π β β) β
(bitsβπ) β
(0..^π)) |
61 | | n2dvdsm1 16258 |
. . . . . . . . . . 11
β’ Β¬ 2
β₯ -1 |
62 | | simplll 774 |
. . . . . . . . . . . . . . . 16
β’ ((((π β β€ β§ π β β0)
β§ (bitsβπ)
β (0..^π)) β§
-π β β) β
π β
β€) |
63 | 62 | zred 12614 |
. . . . . . . . . . . . . . 15
β’ ((((π β β€ β§ π β β0)
β§ (bitsβπ)
β (0..^π)) β§
-π β β) β
π β
β) |
64 | | 2nn 12233 |
. . . . . . . . . . . . . . . . 17
β’ 2 β
β |
65 | 64 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ ((((π β β€ β§ π β β0)
β§ (bitsβπ)
β (0..^π)) β§
-π β β) β 2
β β) |
66 | 54 | nnnn0d 12480 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β β€ β§ π β β0)
β§ (bitsβπ)
β (0..^π)) β§
-π β β) β
-π β
β0) |
67 | 56, 66 | ifcld 4537 |
. . . . . . . . . . . . . . . 16
β’ ((((π β β€ β§ π β β0)
β§ (bitsβπ)
β (0..^π)) β§
-π β β) β
if(-π β€ π, π, -π) β
β0) |
68 | 65, 67 | nnexpcld 14155 |
. . . . . . . . . . . . . . 15
β’ ((((π β β€ β§ π β β0)
β§ (bitsβπ)
β (0..^π)) β§
-π β β) β
(2βif(-π β€ π, π, -π)) β β) |
69 | 63, 68 | nndivred 12214 |
. . . . . . . . . . . . . 14
β’ ((((π β β€ β§ π β β0)
β§ (bitsβπ)
β (0..^π)) β§
-π β β) β
(π / (2βif(-π β€ π, π, -π))) β β) |
70 | | 1red 11163 |
. . . . . . . . . . . . . 14
β’ ((((π β β€ β§ π β β0)
β§ (bitsβπ)
β (0..^π)) β§
-π β β) β 1
β β) |
71 | 62 | zcnd 12615 |
. . . . . . . . . . . . . . . 16
β’ ((((π β β€ β§ π β β0)
β§ (bitsβπ)
β (0..^π)) β§
-π β β) β
π β
β) |
72 | 68 | nncnd 12176 |
. . . . . . . . . . . . . . . 16
β’ ((((π β β€ β§ π β β0)
β§ (bitsβπ)
β (0..^π)) β§
-π β β) β
(2βif(-π β€ π, π, -π)) β β) |
73 | | 2cnd 12238 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β β€ β§ π β β0)
β§ (bitsβπ)
β (0..^π)) β§
-π β β) β 2
β β) |
74 | | 2ne0 12264 |
. . . . . . . . . . . . . . . . . 18
β’ 2 β
0 |
75 | 74 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β β€ β§ π β β0)
β§ (bitsβπ)
β (0..^π)) β§
-π β β) β 2
β 0) |
76 | 67 | nn0zd 12532 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β β€ β§ π β β0)
β§ (bitsβπ)
β (0..^π)) β§
-π β β) β
if(-π β€ π, π, -π) β β€) |
77 | 73, 75, 76 | expne0d 14064 |
. . . . . . . . . . . . . . . 16
β’ ((((π β β€ β§ π β β0)
β§ (bitsβπ)
β (0..^π)) β§
-π β β) β
(2βif(-π β€ π, π, -π)) β 0) |
78 | 71, 72, 77 | divnegd 11951 |
. . . . . . . . . . . . . . 15
β’ ((((π β β€ β§ π β β0)
β§ (bitsβπ)
β (0..^π)) β§
-π β β) β
-(π / (2βif(-π β€ π, π, -π))) = (-π / (2βif(-π β€ π, π, -π)))) |
79 | 67 | nn0red 12481 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β β€ β§ π β β0)
β§ (bitsβπ)
β (0..^π)) β§
-π β β) β
if(-π β€ π, π, -π) β β) |
80 | 68 | nnred 12175 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β β€ β§ π β β0)
β§ (bitsβπ)
β (0..^π)) β§
-π β β) β
(2βif(-π β€ π, π, -π)) β β) |
81 | | max1 13111 |
. . . . . . . . . . . . . . . . . . 19
β’ ((-π β β β§ π β β) β -π β€ if(-π β€ π, π, -π)) |
82 | 55, 57, 81 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β β€ β§ π β β0)
β§ (bitsβπ)
β (0..^π)) β§
-π β β) β
-π β€ if(-π β€ π, π, -π)) |
83 | | 2z 12542 |
. . . . . . . . . . . . . . . . . . . . 21
β’ 2 β
β€ |
84 | | uzid 12785 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (2 β
β€ β 2 β (β€β₯β2)) |
85 | 83, 84 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
β’ 2 β
(β€β₯β2) |
86 | | bernneq3 14141 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((2
β (β€β₯β2) β§ if(-π β€ π, π, -π) β β0) β
if(-π β€ π, π, -π) < (2βif(-π β€ π, π, -π))) |
87 | 85, 67, 86 | sylancr 588 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β β€ β§ π β β0)
β§ (bitsβπ)
β (0..^π)) β§
-π β β) β
if(-π β€ π, π, -π) < (2βif(-π β€ π, π, -π))) |
88 | 79, 80, 87 | ltled 11310 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β β€ β§ π β β0)
β§ (bitsβπ)
β (0..^π)) β§
-π β β) β
if(-π β€ π, π, -π) β€ (2βif(-π β€ π, π, -π))) |
89 | 55, 79, 80, 82, 88 | letrd 11319 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β β€ β§ π β β0)
β§ (bitsβπ)
β (0..^π)) β§
-π β β) β
-π β€ (2βif(-π β€ π, π, -π))) |
90 | 72 | mulid1d 11179 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β β€ β§ π β β0)
β§ (bitsβπ)
β (0..^π)) β§
-π β β) β
((2βif(-π β€ π, π, -π)) Β· 1) = (2βif(-π β€ π, π, -π))) |
91 | 89, 90 | breqtrrd 5138 |
. . . . . . . . . . . . . . . 16
β’ ((((π β β€ β§ π β β0)
β§ (bitsβπ)
β (0..^π)) β§
-π β β) β
-π β€ ((2βif(-π β€ π, π, -π)) Β· 1)) |
92 | 68 | nnrpd 12962 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β β€ β§ π β β0)
β§ (bitsβπ)
β (0..^π)) β§
-π β β) β
(2βif(-π β€ π, π, -π)) β
β+) |
93 | 55, 70, 92 | ledivmuld 13017 |
. . . . . . . . . . . . . . . 16
β’ ((((π β β€ β§ π β β0)
β§ (bitsβπ)
β (0..^π)) β§
-π β β) β
((-π / (2βif(-π β€ π, π, -π))) β€ 1 β -π β€ ((2βif(-π β€ π, π, -π)) Β· 1))) |
94 | 91, 93 | mpbird 257 |
. . . . . . . . . . . . . . 15
β’ ((((π β β€ β§ π β β0)
β§ (bitsβπ)
β (0..^π)) β§
-π β β) β
(-π / (2βif(-π β€ π, π, -π))) β€ 1) |
95 | 78, 94 | eqbrtrd 5132 |
. . . . . . . . . . . . . 14
β’ ((((π β β€ β§ π β β0)
β§ (bitsβπ)
β (0..^π)) β§
-π β β) β
-(π / (2βif(-π β€ π, π, -π))) β€ 1) |
96 | 69, 70, 95 | lenegcon1d 11744 |
. . . . . . . . . . . . 13
β’ ((((π β β€ β§ π β β0)
β§ (bitsβπ)
β (0..^π)) β§
-π β β) β
-1 β€ (π /
(2βif(-π β€ π, π, -π)))) |
97 | 54 | nngt0d 12209 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β β€ β§ π β β0)
β§ (bitsβπ)
β (0..^π)) β§
-π β β) β 0
< -π) |
98 | 68 | nngt0d 12209 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β β€ β§ π β β0)
β§ (bitsβπ)
β (0..^π)) β§
-π β β) β 0
< (2βif(-π β€
π, π, -π))) |
99 | 55, 80, 97, 98 | divgt0d 12097 |
. . . . . . . . . . . . . . . 16
β’ ((((π β β€ β§ π β β0)
β§ (bitsβπ)
β (0..^π)) β§
-π β β) β 0
< (-π /
(2βif(-π β€ π, π, -π)))) |
100 | 99, 78 | breqtrrd 5138 |
. . . . . . . . . . . . . . 15
β’ ((((π β β€ β§ π β β0)
β§ (bitsβπ)
β (0..^π)) β§
-π β β) β 0
< -(π /
(2βif(-π β€ π, π, -π)))) |
101 | 69 | lt0neg1d 11731 |
. . . . . . . . . . . . . . 15
β’ ((((π β β€ β§ π β β0)
β§ (bitsβπ)
β (0..^π)) β§
-π β β) β
((π / (2βif(-π β€ π, π, -π))) < 0 β 0 < -(π / (2βif(-π β€ π, π, -π))))) |
102 | 100, 101 | mpbird 257 |
. . . . . . . . . . . . . 14
β’ ((((π β β€ β§ π β β0)
β§ (bitsβπ)
β (0..^π)) β§
-π β β) β
(π / (2βif(-π β€ π, π, -π))) < 0) |
103 | | ax-1cn 11116 |
. . . . . . . . . . . . . . 15
β’ 1 β
β |
104 | | neg1cn 12274 |
. . . . . . . . . . . . . . 15
β’ -1 β
β |
105 | | 1pneg1e0 12279 |
. . . . . . . . . . . . . . 15
β’ (1 + -1)
= 0 |
106 | 103, 104,
105 | addcomli 11354 |
. . . . . . . . . . . . . 14
β’ (-1 + 1)
= 0 |
107 | 102, 106 | breqtrrdi 5152 |
. . . . . . . . . . . . 13
β’ ((((π β β€ β§ π β β0)
β§ (bitsβπ)
β (0..^π)) β§
-π β β) β
(π / (2βif(-π β€ π, π, -π))) < (-1 + 1)) |
108 | | neg1z 12546 |
. . . . . . . . . . . . . 14
β’ -1 β
β€ |
109 | | flbi 13728 |
. . . . . . . . . . . . . 14
β’ (((π / (2βif(-π β€ π, π, -π))) β β β§ -1 β β€)
β ((ββ(π /
(2βif(-π β€ π, π, -π)))) = -1 β (-1 β€ (π / (2βif(-π β€ π, π, -π))) β§ (π / (2βif(-π β€ π, π, -π))) < (-1 + 1)))) |
110 | 69, 108, 109 | sylancl 587 |
. . . . . . . . . . . . 13
β’ ((((π β β€ β§ π β β0)
β§ (bitsβπ)
β (0..^π)) β§
-π β β) β
((ββ(π /
(2βif(-π β€ π, π, -π)))) = -1 β (-1 β€ (π / (2βif(-π β€ π, π, -π))) β§ (π / (2βif(-π β€ π, π, -π))) < (-1 + 1)))) |
111 | 96, 107, 110 | mpbir2and 712 |
. . . . . . . . . . . 12
β’ ((((π β β€ β§ π β β0)
β§ (bitsβπ)
β (0..^π)) β§
-π β β) β
(ββ(π /
(2βif(-π β€ π, π, -π)))) = -1) |
112 | 111 | breq2d 5122 |
. . . . . . . . . . 11
β’ ((((π β β€ β§ π β β0)
β§ (bitsβπ)
β (0..^π)) β§
-π β β) β
(2 β₯ (ββ(π / (2βif(-π β€ π, π, -π)))) β 2 β₯ -1)) |
113 | 61, 112 | mtbiri 327 |
. . . . . . . . . 10
β’ ((((π β β€ β§ π β β0)
β§ (bitsβπ)
β (0..^π)) β§
-π β β) β
Β¬ 2 β₯ (ββ(π / (2βif(-π β€ π, π, -π))))) |
114 | | bitsval2 16312 |
. . . . . . . . . . 11
β’ ((π β β€ β§ if(-π β€ π, π, -π) β β0) β
(if(-π β€ π, π, -π) β (bitsβπ) β Β¬ 2 β₯
(ββ(π /
(2βif(-π β€ π, π, -π)))))) |
115 | 62, 67, 114 | syl2anc 585 |
. . . . . . . . . 10
β’ ((((π β β€ β§ π β β0)
β§ (bitsβπ)
β (0..^π)) β§
-π β β) β
(if(-π β€ π, π, -π) β (bitsβπ) β Β¬ 2 β₯
(ββ(π /
(2βif(-π β€ π, π, -π)))))) |
116 | 113, 115 | mpbird 257 |
. . . . . . . . 9
β’ ((((π β β€ β§ π β β0)
β§ (bitsβπ)
β (0..^π)) β§
-π β β) β
if(-π β€ π, π, -π) β (bitsβπ)) |
117 | 60, 116 | sseldd 3950 |
. . . . . . . 8
β’ ((((π β β€ β§ π β β0)
β§ (bitsβπ)
β (0..^π)) β§
-π β β) β
if(-π β€ π, π, -π) β (0..^π)) |
118 | | elfzolt2 13588 |
. . . . . . . 8
β’
(if(-π β€ π, π, -π) β (0..^π) β if(-π β€ π, π, -π) < π) |
119 | 117, 118 | syl 17 |
. . . . . . 7
β’ ((((π β β€ β§ π β β0)
β§ (bitsβπ)
β (0..^π)) β§
-π β β) β
if(-π β€ π, π, -π) < π) |
120 | 79, 57 | ltnled 11309 |
. . . . . . 7
β’ ((((π β β€ β§ π β β0)
β§ (bitsβπ)
β (0..^π)) β§
-π β β) β
(if(-π β€ π, π, -π) < π β Β¬ π β€ if(-π β€ π, π, -π))) |
121 | 119, 120 | mpbid 231 |
. . . . . 6
β’ ((((π β β€ β§ π β β0)
β§ (bitsβπ)
β (0..^π)) β§
-π β β) β
Β¬ π β€ if(-π β€ π, π, -π)) |
122 | 59, 121 | pm2.65da 816 |
. . . . 5
β’ (((π β β€ β§ π β β0)
β§ (bitsβπ)
β (0..^π)) β
Β¬ -π β
β) |
123 | 122 | intnand 490 |
. . . 4
β’ (((π β β€ β§ π β β0)
β§ (bitsβπ)
β (0..^π)) β
Β¬ (π β β
β§ -π β
β)) |
124 | | simpll 766 |
. . . . . 6
β’ (((π β β€ β§ π β β0)
β§ (bitsβπ)
β (0..^π)) β
π β
β€) |
125 | | elznn0nn 12520 |
. . . . . 6
β’ (π β β€ β (π β β0 β¨
(π β β β§
-π β
β))) |
126 | 124, 125 | sylib 217 |
. . . . 5
β’ (((π β β€ β§ π β β0)
β§ (bitsβπ)
β (0..^π)) β
(π β
β0 β¨ (π
β β β§ -π
β β))) |
127 | 126 | ord 863 |
. . . 4
β’ (((π β β€ β§ π β β0)
β§ (bitsβπ)
β (0..^π)) β
(Β¬ π β
β0 β (π β β β§ -π β β))) |
128 | 123, 127 | mt3d 148 |
. . 3
β’ (((π β β€ β§ π β β0)
β§ (bitsβπ)
β (0..^π)) β
π β
β0) |
129 | | simplr 768 |
. . 3
β’ (((π β β€ β§ π β β0)
β§ (bitsβπ)
β (0..^π)) β
π β
β0) |
130 | | simpr 486 |
. . 3
β’ (((π β β€ β§ π β β0)
β§ (bitsβπ)
β (0..^π)) β
(bitsβπ) β
(0..^π)) |
131 | | eqid 2737 |
. . 3
β’
inf({π β
β0 β£ π < (2βπ)}, β, < ) = inf({π β β0 β£ π < (2βπ)}, β, < ) |
132 | 128, 129,
130, 131 | bitsfzolem 16321 |
. 2
β’ (((π β β€ β§ π β β0)
β§ (bitsβπ)
β (0..^π)) β
π β (0..^(2βπ))) |
133 | 53, 132 | impbida 800 |
1
β’ ((π β β€ β§ π β β0)
β (π β
(0..^(2βπ)) β
(bitsβπ) β
(0..^π))) |