Step | Hyp | Ref
| Expression |
1 | | 0xr 8006 |
. . . . . . . 8
β’ 0 β
β* |
2 | | 1re 7958 |
. . . . . . . 8
β’ 1 β
β |
3 | | elioc2 9938 |
. . . . . . . 8
β’ ((0
β β* β§ 1 β β) β (π΄ β (0(,]1) β (π΄ β β β§ 0 < π΄ β§ π΄ β€ 1))) |
4 | 1, 2, 3 | mp2an 426 |
. . . . . . 7
β’ (π΄ β (0(,]1) β (π΄ β β β§ 0 <
π΄ β§ π΄ β€ 1)) |
5 | 4 | simp1bi 1012 |
. . . . . 6
β’ (π΄ β (0(,]1) β π΄ β
β) |
6 | | 3nn0 9196 |
. . . . . 6
β’ 3 β
β0 |
7 | | reexpcl 10539 |
. . . . . 6
β’ ((π΄ β β β§ 3 β
β0) β (π΄β3) β β) |
8 | 5, 6, 7 | sylancl 413 |
. . . . 5
β’ (π΄ β (0(,]1) β (π΄β3) β
β) |
9 | | 3re 8995 |
. . . . . 6
β’ 3 β
β |
10 | | 3ap0 9017 |
. . . . . 6
β’ 3 #
0 |
11 | | redivclap 8690 |
. . . . . 6
β’ (((π΄β3) β β β§ 3
β β β§ 3 # 0) β ((π΄β3) / 3) β
β) |
12 | 9, 10, 11 | mp3an23 1329 |
. . . . 5
β’ ((π΄β3) β β β
((π΄β3) / 3) β
β) |
13 | 8, 12 | syl 14 |
. . . 4
β’ (π΄ β (0(,]1) β ((π΄β3) / 3) β
β) |
14 | | 3z 9284 |
. . . . . . . . 9
β’ 3 β
β€ |
15 | | expgt0 10555 |
. . . . . . . . 9
β’ ((π΄ β β β§ 3 β
β€ β§ 0 < π΄)
β 0 < (π΄β3)) |
16 | 14, 15 | mp3an2 1325 |
. . . . . . . 8
β’ ((π΄ β β β§ 0 <
π΄) β 0 < (π΄β3)) |
17 | 16 | 3adant3 1017 |
. . . . . . 7
β’ ((π΄ β β β§ 0 <
π΄ β§ π΄ β€ 1) β 0 < (π΄β3)) |
18 | 4, 17 | sylbi 121 |
. . . . . 6
β’ (π΄ β (0(,]1) β 0 <
(π΄β3)) |
19 | | 0lt1 8086 |
. . . . . . . 8
β’ 0 <
1 |
20 | 2, 19 | pm3.2i 272 |
. . . . . . 7
β’ (1 β
β β§ 0 < 1) |
21 | | 3pos 9015 |
. . . . . . . 8
β’ 0 <
3 |
22 | 9, 21 | pm3.2i 272 |
. . . . . . 7
β’ (3 β
β β§ 0 < 3) |
23 | | 1lt3 9092 |
. . . . . . . 8
β’ 1 <
3 |
24 | | ltdiv2 8846 |
. . . . . . . 8
β’ (((1
β β β§ 0 < 1) β§ (3 β β β§ 0 < 3) β§
((π΄β3) β β
β§ 0 < (π΄β3)))
β (1 < 3 β ((π΄β3) / 3) < ((π΄β3) / 1))) |
25 | 23, 24 | mpbii 148 |
. . . . . . 7
β’ (((1
β β β§ 0 < 1) β§ (3 β β β§ 0 < 3) β§
((π΄β3) β β
β§ 0 < (π΄β3)))
β ((π΄β3) / 3)
< ((π΄β3) /
1)) |
26 | 20, 22, 25 | mp3an12 1327 |
. . . . . 6
β’ (((π΄β3) β β β§ 0
< (π΄β3)) β
((π΄β3) / 3) <
((π΄β3) /
1)) |
27 | 8, 18, 26 | syl2anc 411 |
. . . . 5
β’ (π΄ β (0(,]1) β ((π΄β3) / 3) < ((π΄β3) / 1)) |
28 | 8 | recnd 7988 |
. . . . . 6
β’ (π΄ β (0(,]1) β (π΄β3) β
β) |
29 | 28 | div1d 8739 |
. . . . 5
β’ (π΄ β (0(,]1) β ((π΄β3) / 1) = (π΄β3)) |
30 | 27, 29 | breqtrd 4031 |
. . . 4
β’ (π΄ β (0(,]1) β ((π΄β3) / 3) < (π΄β3)) |
31 | | 1nn0 9194 |
. . . . . . 7
β’ 1 β
β0 |
32 | 31 | a1i 9 |
. . . . . 6
β’ (π΄ β (0(,]1) β 1 β
β0) |
33 | | 1le3 9132 |
. . . . . . . 8
β’ 1 β€
3 |
34 | | 1z 9281 |
. . . . . . . . 9
β’ 1 β
β€ |
35 | 34 | eluz1i 9537 |
. . . . . . . 8
β’ (3 β
(β€β₯β1) β (3 β β€ β§ 1 β€
3)) |
36 | 14, 33, 35 | mpbir2an 942 |
. . . . . . 7
β’ 3 β
(β€β₯β1) |
37 | 36 | a1i 9 |
. . . . . 6
β’ (π΄ β (0(,]1) β 3 β
(β€β₯β1)) |
38 | 4 | simp2bi 1013 |
. . . . . . 7
β’ (π΄ β (0(,]1) β 0 <
π΄) |
39 | | 0re 7959 |
. . . . . . . 8
β’ 0 β
β |
40 | | ltle 8047 |
. . . . . . . 8
β’ ((0
β β β§ π΄
β β) β (0 < π΄ β 0 β€ π΄)) |
41 | 39, 5, 40 | sylancr 414 |
. . . . . . 7
β’ (π΄ β (0(,]1) β (0 <
π΄ β 0 β€ π΄)) |
42 | 38, 41 | mpd 13 |
. . . . . 6
β’ (π΄ β (0(,]1) β 0 β€
π΄) |
43 | 4 | simp3bi 1014 |
. . . . . 6
β’ (π΄ β (0(,]1) β π΄ β€ 1) |
44 | 5, 32, 37, 42, 43 | leexp2rd 10686 |
. . . . 5
β’ (π΄ β (0(,]1) β (π΄β3) β€ (π΄β1)) |
45 | 5 | recnd 7988 |
. . . . . 6
β’ (π΄ β (0(,]1) β π΄ β
β) |
46 | 45 | exp1d 10651 |
. . . . 5
β’ (π΄ β (0(,]1) β (π΄β1) = π΄) |
47 | 44, 46 | breqtrd 4031 |
. . . 4
β’ (π΄ β (0(,]1) β (π΄β3) β€ π΄) |
48 | 13, 8, 5, 30, 47 | ltletrd 8382 |
. . 3
β’ (π΄ β (0(,]1) β ((π΄β3) / 3) < π΄) |
49 | 13, 5 | posdifd 8491 |
. . 3
β’ (π΄ β (0(,]1) β (((π΄β3) / 3) < π΄ β 0 < (π΄ β ((π΄β3) / 3)))) |
50 | 48, 49 | mpbid 147 |
. 2
β’ (π΄ β (0(,]1) β 0 <
(π΄ β ((π΄β3) / 3))) |
51 | | sin01bnd 11767 |
. . 3
β’ (π΄ β (0(,]1) β ((π΄ β ((π΄β3) / 3)) < (sinβπ΄) β§ (sinβπ΄) < π΄)) |
52 | 51 | simpld 112 |
. 2
β’ (π΄ β (0(,]1) β (π΄ β ((π΄β3) / 3)) < (sinβπ΄)) |
53 | 5, 13 | resubcld 8340 |
. . 3
β’ (π΄ β (0(,]1) β (π΄ β ((π΄β3) / 3)) β
β) |
54 | 5 | resincld 11733 |
. . 3
β’ (π΄ β (0(,]1) β
(sinβπ΄) β
β) |
55 | | lttr 8033 |
. . 3
β’ ((0
β β β§ (π΄
β ((π΄β3) / 3))
β β β§ (sinβπ΄) β β) β ((0 < (π΄ β ((π΄β3) / 3)) β§ (π΄ β ((π΄β3) / 3)) < (sinβπ΄)) β 0 <
(sinβπ΄))) |
56 | 39, 53, 54, 55 | mp3an2i 1342 |
. 2
β’ (π΄ β (0(,]1) β ((0 <
(π΄ β ((π΄β3) / 3)) β§ (π΄ β ((π΄β3) / 3)) < (sinβπ΄)) β 0 <
(sinβπ΄))) |
57 | 50, 52, 56 | mp2and 433 |
1
β’ (π΄ β (0(,]1) β 0 <
(sinβπ΄)) |