Step | Hyp | Ref
| Expression |
1 | | cbits 16304 |
. 2
class
bits |
2 | | vn |
. . 3
setvar π |
3 | | cz 12504 |
. . 3
class
β€ |
4 | | c2 12213 |
. . . . . 6
class
2 |
5 | 2 | cv 1541 |
. . . . . . . 8
class π |
6 | | vm |
. . . . . . . . . 10
setvar π |
7 | 6 | cv 1541 |
. . . . . . . . 9
class π |
8 | | cexp 13973 |
. . . . . . . . 9
class
β |
9 | 4, 7, 8 | co 7358 |
. . . . . . . 8
class
(2βπ) |
10 | | cdiv 11817 |
. . . . . . . 8
class
/ |
11 | 5, 9, 10 | co 7358 |
. . . . . . 7
class (π / (2βπ)) |
12 | | cfl 13701 |
. . . . . . 7
class
β |
13 | 11, 12 | cfv 6497 |
. . . . . 6
class
(ββ(π /
(2βπ))) |
14 | | cdvds 16141 |
. . . . . 6
class
β₯ |
15 | 4, 13, 14 | wbr 5106 |
. . . . 5
wff 2 β₯
(ββ(π /
(2βπ))) |
16 | 15 | wn 3 |
. . . 4
wff Β¬ 2
β₯ (ββ(π /
(2βπ))) |
17 | | cn0 12418 |
. . . 4
class
β0 |
18 | 16, 6, 17 | crab 3406 |
. . 3
class {π β β0
β£ Β¬ 2 β₯ (ββ(π / (2βπ)))} |
19 | 2, 3, 18 | cmpt 5189 |
. 2
class (π β β€ β¦ {π β β0
β£ Β¬ 2 β₯ (ββ(π / (2βπ)))}) |
20 | 1, 19 | wceq 1542 |
1
wff bits =
(π β β€ β¦
{π β
β0 β£ Β¬ 2 β₯ (ββ(π / (2βπ)))}) |