Step | Hyp | Ref
| Expression |
1 | | 3re 12238 |
. . . . . . 7
β’ 3 β
β |
2 | | 3pos 12263 |
. . . . . . 7
β’ 0 <
3 |
3 | 1, 2 | elrpii 12923 |
. . . . . 6
β’ 3 β
β+ |
4 | | rpdivcl 12945 |
. . . . . 6
β’ ((π β β+
β§ 3 β β+) β (π / 3) β
β+) |
5 | 3, 4 | mpan2 690 |
. . . . 5
β’ (π β β+
β (π / 3) β
β+) |
6 | | 2re 12232 |
. . . . . 6
β’ 2 β
β |
7 | | 1lt2 12329 |
. . . . . 6
β’ 1 <
2 |
8 | | expnlbnd 14142 |
. . . . . 6
β’ (((π / 3) β β+
β§ 2 β β β§ 1 < 2) β βπ β β (1 / (2βπ)) < (π / 3)) |
9 | 6, 7, 8 | mp3an23 1454 |
. . . . 5
β’ ((π / 3) β β+
β βπ β
β (1 / (2βπ))
< (π /
3)) |
10 | 5, 9 | syl 17 |
. . . 4
β’ (π β β+
β βπ β
β (1 / (2βπ))
< (π /
3)) |
11 | | 2nn 12231 |
. . . . . . . . . . 11
β’ 2 β
β |
12 | | nnnn0 12425 |
. . . . . . . . . . 11
β’ (π β β β π β
β0) |
13 | | nnexpcl 13986 |
. . . . . . . . . . 11
β’ ((2
β β β§ π
β β0) β (2βπ) β β) |
14 | 11, 12, 13 | sylancr 588 |
. . . . . . . . . 10
β’ (π β β β
(2βπ) β
β) |
15 | 14 | nnrpd 12960 |
. . . . . . . . 9
β’ (π β β β
(2βπ) β
β+) |
16 | | rpcn 12930 |
. . . . . . . . . 10
β’
((2βπ) β
β+ β (2βπ) β β) |
17 | | rpne0 12936 |
. . . . . . . . . 10
β’
((2βπ) β
β+ β (2βπ) β 0) |
18 | | 3cn 12239 |
. . . . . . . . . . 11
β’ 3 β
β |
19 | | divrec 11834 |
. . . . . . . . . . 11
β’ ((3
β β β§ (2βπ) β β β§ (2βπ) β 0) β (3 /
(2βπ)) = (3 Β·
(1 / (2βπ)))) |
20 | 18, 19 | mp3an1 1449 |
. . . . . . . . . 10
β’
(((2βπ) β
β β§ (2βπ)
β 0) β (3 / (2βπ)) = (3 Β· (1 / (2βπ)))) |
21 | 16, 17, 20 | syl2anc 585 |
. . . . . . . . 9
β’
((2βπ) β
β+ β (3 / (2βπ)) = (3 Β· (1 / (2βπ)))) |
22 | 15, 21 | syl 17 |
. . . . . . . 8
β’ (π β β β (3 /
(2βπ)) = (3 Β·
(1 / (2βπ)))) |
23 | 22 | adantl 483 |
. . . . . . 7
β’ ((π β β+
β§ π β β)
β (3 / (2βπ)) =
(3 Β· (1 / (2βπ)))) |
24 | 23 | breq1d 5116 |
. . . . . 6
β’ ((π β β+
β§ π β β)
β ((3 / (2βπ))
< π β (3 Β·
(1 / (2βπ))) <
π)) |
25 | 14 | nnrecred 12209 |
. . . . . . 7
β’ (π β β β (1 /
(2βπ)) β
β) |
26 | | rpre 12928 |
. . . . . . 7
β’ (π β β+
β π β
β) |
27 | 1, 2 | pm3.2i 472 |
. . . . . . . 8
β’ (3 β
β β§ 0 < 3) |
28 | | ltmuldiv2 12034 |
. . . . . . . 8
β’ (((1 /
(2βπ)) β β
β§ π β β
β§ (3 β β β§ 0 < 3)) β ((3 Β· (1 / (2βπ))) < π β (1 / (2βπ)) < (π / 3))) |
29 | 27, 28 | mp3an3 1451 |
. . . . . . 7
β’ (((1 /
(2βπ)) β β
β§ π β β)
β ((3 Β· (1 / (2βπ))) < π β (1 / (2βπ)) < (π / 3))) |
30 | 25, 26, 29 | syl2anr 598 |
. . . . . 6
β’ ((π β β+
β§ π β β)
β ((3 Β· (1 / (2βπ))) < π β (1 / (2βπ)) < (π / 3))) |
31 | 24, 30 | bitrd 279 |
. . . . 5
β’ ((π β β+
β§ π β β)
β ((3 / (2βπ))
< π β (1 /
(2βπ)) < (π / 3))) |
32 | 31 | rexbidva 3170 |
. . . 4
β’ (π β β+
β (βπ β
β (3 / (2βπ))
< π β βπ β β (1 /
(2βπ)) < (π / 3))) |
33 | 10, 32 | mpbird 257 |
. . 3
β’ (π β β+
β βπ β
β (3 / (2βπ))
< π) |
34 | | fveq2 6843 |
. . . . . . . . 9
β’ (π = π β (πβπ) = (πβπ)) |
35 | | oveq2 7366 |
. . . . . . . . . 10
β’ (π = π β (2βπ) = (2βπ)) |
36 | 35 | oveq2d 7374 |
. . . . . . . . 9
β’ (π = π β (3 / (2βπ)) = (3 / (2βπ))) |
37 | 34, 36 | opeq12d 4839 |
. . . . . . . 8
β’ (π = π β β¨(πβπ), (3 / (2βπ))β© = β¨(πβπ), (3 / (2βπ))β©) |
38 | | heibor.12 |
. . . . . . . 8
β’ π = (π β β β¦ β¨(πβπ), (3 / (2βπ))β©) |
39 | | opex 5422 |
. . . . . . . 8
β’
β¨(πβπ), (3 / (2βπ))β© β
V |
40 | 37, 38, 39 | fvmpt 6949 |
. . . . . . 7
β’ (π β β β (πβπ) = β¨(πβπ), (3 / (2βπ))β©) |
41 | 40 | fveq2d 6847 |
. . . . . 6
β’ (π β β β
(2nd β(πβπ)) = (2nd ββ¨(πβπ), (3 / (2βπ))β©)) |
42 | | fvex 6856 |
. . . . . . 7
β’ (πβπ) β V |
43 | | ovex 7391 |
. . . . . . 7
β’ (3 /
(2βπ)) β
V |
44 | 42, 43 | op2nd 7931 |
. . . . . 6
β’
(2nd ββ¨(πβπ), (3 / (2βπ))β©) = (3 / (2βπ)) |
45 | 41, 44 | eqtrdi 2789 |
. . . . 5
β’ (π β β β
(2nd β(πβπ)) = (3 / (2βπ))) |
46 | 45 | breq1d 5116 |
. . . 4
β’ (π β β β
((2nd β(πβπ)) < π β (3 / (2βπ)) < π)) |
47 | 46 | rexbiia 3092 |
. . 3
β’
(βπ β
β (2nd β(πβπ)) < π β βπ β β (3 / (2βπ)) < π) |
48 | 33, 47 | sylibr 233 |
. 2
β’ (π β β+
β βπ β
β (2nd β(πβπ)) < π) |
49 | 48 | rgen 3063 |
1
β’
βπ β
β+ βπ β β (2nd β(πβπ)) < π |