Step | Hyp | Ref
| Expression |
1 | | cbits 16385 |
. 2
class
bits |
2 | | vn |
. . 3
setvar π |
3 | | cz 12580 |
. . 3
class
β€ |
4 | | c2 12289 |
. . . . . 6
class
2 |
5 | 2 | cv 1533 |
. . . . . . . 8
class π |
6 | | vm |
. . . . . . . . . 10
setvar π |
7 | 6 | cv 1533 |
. . . . . . . . 9
class π |
8 | | cexp 14050 |
. . . . . . . . 9
class
β |
9 | 4, 7, 8 | co 7414 |
. . . . . . . 8
class
(2βπ) |
10 | | cdiv 11893 |
. . . . . . . 8
class
/ |
11 | 5, 9, 10 | co 7414 |
. . . . . . 7
class (π / (2βπ)) |
12 | | cfl 13779 |
. . . . . . 7
class
β |
13 | 11, 12 | cfv 6542 |
. . . . . 6
class
(ββ(π /
(2βπ))) |
14 | | cdvds 16222 |
. . . . . 6
class
β₯ |
15 | 4, 13, 14 | wbr 5142 |
. . . . 5
wff 2 β₯
(ββ(π /
(2βπ))) |
16 | 15 | wn 3 |
. . . 4
wff Β¬ 2
β₯ (ββ(π /
(2βπ))) |
17 | | cn0 12494 |
. . . 4
class
β0 |
18 | 16, 6, 17 | crab 3427 |
. . 3
class {π β β0
β£ Β¬ 2 β₯ (ββ(π / (2βπ)))} |
19 | 2, 3, 18 | cmpt 5225 |
. 2
class (π β β€ β¦ {π β β0
β£ Β¬ 2 β₯ (ββ(π / (2βπ)))}) |
20 | 1, 19 | wceq 1534 |
1
wff bits =
(π β β€ β¦
{π β
β0 β£ Β¬ 2 β₯ (ββ(π / (2βπ)))}) |