Step | Hyp | Ref
| Expression |
1 | | 2nn 12286 |
. . . . . . . . . . . 12
β’ 2 β
β |
2 | 1 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β β€ β§ π β β0)
β 2 β β) |
3 | 2 | nncnd 12229 |
. . . . . . . . . 10
β’ ((π β β€ β§ π β β0)
β 2 β β) |
4 | | simpr 484 |
. . . . . . . . . 10
β’ ((π β β€ β§ π β β0)
β π β
β0) |
5 | 3, 4 | expp1d 14115 |
. . . . . . . . 9
β’ ((π β β€ β§ π β β0)
β (2β(π + 1)) =
((2βπ) Β·
2)) |
6 | 2, 4 | nnexpcld 14211 |
. . . . . . . . . . 11
β’ ((π β β€ β§ π β β0)
β (2βπ) β
β) |
7 | 6 | nncnd 12229 |
. . . . . . . . . 10
β’ ((π β β€ β§ π β β0)
β (2βπ) β
β) |
8 | 7, 3 | mulcomd 11236 |
. . . . . . . . 9
β’ ((π β β€ β§ π β β0)
β ((2βπ) Β·
2) = (2 Β· (2βπ))) |
9 | 5, 8 | eqtrd 2766 |
. . . . . . . 8
β’ ((π β β€ β§ π β β0)
β (2β(π + 1)) =
(2 Β· (2βπ))) |
10 | 9 | oveq2d 7420 |
. . . . . . 7
β’ ((π β β€ β§ π β β0)
β (π / (2β(π + 1))) = (π / (2 Β· (2βπ)))) |
11 | | simpl 482 |
. . . . . . . . 9
β’ ((π β β€ β§ π β β0)
β π β
β€) |
12 | 11 | zcnd 12668 |
. . . . . . . 8
β’ ((π β β€ β§ π β β0)
β π β
β) |
13 | 2 | nnne0d 12263 |
. . . . . . . 8
β’ ((π β β€ β§ π β β0)
β 2 β 0) |
14 | 6 | nnne0d 12263 |
. . . . . . . 8
β’ ((π β β€ β§ π β β0)
β (2βπ) β
0) |
15 | 12, 3, 7, 13, 14 | divdiv1d 12022 |
. . . . . . 7
β’ ((π β β€ β§ π β β0)
β ((π / 2) /
(2βπ)) = (π / (2 Β· (2βπ)))) |
16 | 10, 15 | eqtr4d 2769 |
. . . . . 6
β’ ((π β β€ β§ π β β0)
β (π / (2β(π + 1))) = ((π / 2) / (2βπ))) |
17 | 16 | fveq2d 6888 |
. . . . 5
β’ ((π β β€ β§ π β β0)
β (ββ(π /
(2β(π + 1)))) =
(ββ((π / 2) /
(2βπ)))) |
18 | 11 | zred 12667 |
. . . . . . 7
β’ ((π β β€ β§ π β β0)
β π β
β) |
19 | 18 | rehalfcld 12460 |
. . . . . 6
β’ ((π β β€ β§ π β β0)
β (π / 2) β
β) |
20 | | fldiv 13828 |
. . . . . 6
β’ (((π / 2) β β β§
(2βπ) β β)
β (ββ((ββ(π / 2)) / (2βπ))) = (ββ((π / 2) / (2βπ)))) |
21 | 19, 6, 20 | syl2anc 583 |
. . . . 5
β’ ((π β β€ β§ π β β0)
β (ββ((ββ(π / 2)) / (2βπ))) = (ββ((π / 2) / (2βπ)))) |
22 | 17, 21 | eqtr4d 2769 |
. . . 4
β’ ((π β β€ β§ π β β0)
β (ββ(π /
(2β(π + 1)))) =
(ββ((ββ(π / 2)) / (2βπ)))) |
23 | 22 | breq2d 5153 |
. . 3
β’ ((π β β€ β§ π β β0)
β (2 β₯ (ββ(π / (2β(π + 1)))) β 2 β₯
(ββ((ββ(π / 2)) / (2βπ))))) |
24 | 23 | notbid 318 |
. 2
β’ ((π β β€ β§ π β β0)
β (Β¬ 2 β₯ (ββ(π / (2β(π + 1)))) β Β¬ 2 β₯
(ββ((ββ(π / 2)) / (2βπ))))) |
25 | | peano2nn0 12513 |
. . 3
β’ (π β β0
β (π + 1) β
β0) |
26 | | bitsval2 16371 |
. . 3
β’ ((π β β€ β§ (π + 1) β
β0) β ((π + 1) β (bitsβπ) β Β¬ 2 β₯
(ββ(π /
(2β(π +
1)))))) |
27 | 25, 26 | sylan2 592 |
. 2
β’ ((π β β€ β§ π β β0)
β ((π + 1) β
(bitsβπ) β Β¬
2 β₯ (ββ(π
/ (2β(π +
1)))))) |
28 | 19 | flcld 13766 |
. . 3
β’ ((π β β€ β§ π β β0)
β (ββ(π /
2)) β β€) |
29 | | bitsval2 16371 |
. . 3
β’
(((ββ(π
/ 2)) β β€ β§ π β β0) β (π β
(bitsβ(ββ(π / 2))) β Β¬ 2 β₯
(ββ((ββ(π / 2)) / (2βπ))))) |
30 | 28, 29 | sylancom 587 |
. 2
β’ ((π β β€ β§ π β β0)
β (π β
(bitsβ(ββ(π / 2))) β Β¬ 2 β₯
(ββ((ββ(π / 2)) / (2βπ))))) |
31 | 24, 27, 30 | 3bitr4d 311 |
1
β’ ((π β β€ β§ π β β0)
β ((π + 1) β
(bitsβπ) β π β
(bitsβ(ββ(π / 2))))) |