Step | Hyp | Ref
| Expression |
1 | | cbits 16359 |
. 2
class
bits |
2 | | vn |
. . 3
setvar π |
3 | | cz 12557 |
. . 3
class
β€ |
4 | | c2 12266 |
. . . . . 6
class
2 |
5 | 2 | cv 1540 |
. . . . . . . 8
class π |
6 | | vm |
. . . . . . . . . 10
setvar π |
7 | 6 | cv 1540 |
. . . . . . . . 9
class π |
8 | | cexp 14026 |
. . . . . . . . 9
class
β |
9 | 4, 7, 8 | co 7408 |
. . . . . . . 8
class
(2βπ) |
10 | | cdiv 11870 |
. . . . . . . 8
class
/ |
11 | 5, 9, 10 | co 7408 |
. . . . . . 7
class (π / (2βπ)) |
12 | | cfl 13754 |
. . . . . . 7
class
β |
13 | 11, 12 | cfv 6543 |
. . . . . 6
class
(ββ(π /
(2βπ))) |
14 | | cdvds 16196 |
. . . . . 6
class
β₯ |
15 | 4, 13, 14 | wbr 5148 |
. . . . 5
wff 2 β₯
(ββ(π /
(2βπ))) |
16 | 15 | wn 3 |
. . . 4
wff Β¬ 2
β₯ (ββ(π /
(2βπ))) |
17 | | cn0 12471 |
. . . 4
class
β0 |
18 | 16, 6, 17 | crab 3432 |
. . 3
class {π β β0
β£ Β¬ 2 β₯ (ββ(π / (2βπ)))} |
19 | 2, 3, 18 | cmpt 5231 |
. 2
class (π β β€ β¦ {π β β0
β£ Β¬ 2 β₯ (ββ(π / (2βπ)))}) |
20 | 1, 19 | wceq 1541 |
1
wff bits =
(π β β€ β¦
{π β
β0 β£ Β¬ 2 β₯ (ββ(π / (2βπ)))}) |