Step | Hyp | Ref
| Expression |
1 | | 0xr 11209 |
. . . . . . . . . 10
โข 0 โ
โ* |
2 | | 1re 11162 |
. . . . . . . . . 10
โข 1 โ
โ |
3 | | elioc2 13334 |
. . . . . . . . . 10
โข ((0
โ โ* โง 1 โ โ) โ (๐ด โ (0(,]1) โ (๐ด โ โ โง 0 < ๐ด โง ๐ด โค 1))) |
4 | 1, 2, 3 | mp2an 691 |
. . . . . . . . 9
โข (๐ด โ (0(,]1) โ (๐ด โ โ โง 0 <
๐ด โง ๐ด โค 1)) |
5 | 4 | simp1bi 1146 |
. . . . . . . 8
โข (๐ด โ (0(,]1) โ ๐ด โ
โ) |
6 | 5 | resqcld 14037 |
. . . . . . 7
โข (๐ด โ (0(,]1) โ (๐ดโ2) โ
โ) |
7 | 6 | recnd 11190 |
. . . . . 6
โข (๐ด โ (0(,]1) โ (๐ดโ2) โ
โ) |
8 | | 2cn 12235 |
. . . . . . 7
โข 2 โ
โ |
9 | | 3cn 12241 |
. . . . . . . 8
โข 3 โ
โ |
10 | | 3ne0 12266 |
. . . . . . . 8
โข 3 โ
0 |
11 | 9, 10 | pm3.2i 472 |
. . . . . . 7
โข (3 โ
โ โง 3 โ 0) |
12 | | div12 11842 |
. . . . . . 7
โข ((2
โ โ โง (๐ดโ2) โ โ โง (3 โ
โ โง 3 โ 0)) โ (2 ยท ((๐ดโ2) / 3)) = ((๐ดโ2) ยท (2 / 3))) |
13 | 8, 11, 12 | mp3an13 1453 |
. . . . . 6
โข ((๐ดโ2) โ โ โ
(2 ยท ((๐ดโ2) /
3)) = ((๐ดโ2) ยท
(2 / 3))) |
14 | 7, 13 | syl 17 |
. . . . 5
โข (๐ด โ (0(,]1) โ (2
ยท ((๐ดโ2) / 3))
= ((๐ดโ2) ยท (2 /
3))) |
15 | | 2z 12542 |
. . . . . . . . . 10
โข 2 โ
โค |
16 | | expgt0 14008 |
. . . . . . . . . 10
โข ((๐ด โ โ โง 2 โ
โค โง 0 < ๐ด)
โ 0 < (๐ดโ2)) |
17 | 15, 16 | mp3an2 1450 |
. . . . . . . . 9
โข ((๐ด โ โ โง 0 <
๐ด) โ 0 < (๐ดโ2)) |
18 | 17 | 3adant3 1133 |
. . . . . . . 8
โข ((๐ด โ โ โง 0 <
๐ด โง ๐ด โค 1) โ 0 < (๐ดโ2)) |
19 | 4, 18 | sylbi 216 |
. . . . . . 7
โข (๐ด โ (0(,]1) โ 0 <
(๐ดโ2)) |
20 | | 2lt3 12332 |
. . . . . . . . . 10
โข 2 <
3 |
21 | | 2re 12234 |
. . . . . . . . . . 11
โข 2 โ
โ |
22 | | 3re 12240 |
. . . . . . . . . . 11
โข 3 โ
โ |
23 | | 3pos 12265 |
. . . . . . . . . . 11
โข 0 <
3 |
24 | 21, 22, 22, 23 | ltdiv1ii 12091 |
. . . . . . . . . 10
โข (2 < 3
โ (2 / 3) < (3 / 3)) |
25 | 20, 24 | mpbi 229 |
. . . . . . . . 9
โข (2 / 3)
< (3 / 3) |
26 | 9, 10 | dividi 11895 |
. . . . . . . . 9
โข (3 / 3) =
1 |
27 | 25, 26 | breqtri 5135 |
. . . . . . . 8
โข (2 / 3)
< 1 |
28 | 21, 22, 10 | redivcli 11929 |
. . . . . . . . 9
โข (2 / 3)
โ โ |
29 | | ltmul2 12013 |
. . . . . . . . 9
โข (((2 / 3)
โ โ โง 1 โ โ โง ((๐ดโ2) โ โ โง 0 < (๐ดโ2))) โ ((2 / 3) <
1 โ ((๐ดโ2)
ยท (2 / 3)) < ((๐ดโ2) ยท 1))) |
30 | 28, 2, 29 | mp3an12 1452 |
. . . . . . . 8
โข (((๐ดโ2) โ โ โง 0
< (๐ดโ2)) โ ((2
/ 3) < 1 โ ((๐ดโ2) ยท (2 / 3)) < ((๐ดโ2) ยท
1))) |
31 | 27, 30 | mpbii 232 |
. . . . . . 7
โข (((๐ดโ2) โ โ โง 0
< (๐ดโ2)) โ
((๐ดโ2) ยท (2 /
3)) < ((๐ดโ2)
ยท 1)) |
32 | 6, 19, 31 | syl2anc 585 |
. . . . . 6
โข (๐ด โ (0(,]1) โ ((๐ดโ2) ยท (2 / 3)) <
((๐ดโ2) ยท
1)) |
33 | 7 | mulid1d 11179 |
. . . . . 6
โข (๐ด โ (0(,]1) โ ((๐ดโ2) ยท 1) = (๐ดโ2)) |
34 | 32, 33 | breqtrd 5136 |
. . . . 5
โข (๐ด โ (0(,]1) โ ((๐ดโ2) ยท (2 / 3)) <
(๐ดโ2)) |
35 | 14, 34 | eqbrtrd 5132 |
. . . 4
โข (๐ด โ (0(,]1) โ (2
ยท ((๐ดโ2) / 3))
< (๐ดโ2)) |
36 | | 0re 11164 |
. . . . . . . . 9
โข 0 โ
โ |
37 | | ltle 11250 |
. . . . . . . . 9
โข ((0
โ โ โง ๐ด
โ โ) โ (0 < ๐ด โ 0 โค ๐ด)) |
38 | 36, 37 | mpan 689 |
. . . . . . . 8
โข (๐ด โ โ โ (0 <
๐ด โ 0 โค ๐ด)) |
39 | 38 | imdistani 570 |
. . . . . . 7
โข ((๐ด โ โ โง 0 <
๐ด) โ (๐ด โ โ โง 0 โค
๐ด)) |
40 | | le2sq2 14047 |
. . . . . . . 8
โข (((๐ด โ โ โง 0 โค
๐ด) โง (1 โ โ
โง ๐ด โค 1)) โ
(๐ดโ2) โค
(1โ2)) |
41 | 2, 40 | mpanr1 702 |
. . . . . . 7
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ด โค 1) โ (๐ดโ2) โค (1โ2)) |
42 | 39, 41 | stoic3 1779 |
. . . . . 6
โข ((๐ด โ โ โง 0 <
๐ด โง ๐ด โค 1) โ (๐ดโ2) โค (1โ2)) |
43 | 4, 42 | sylbi 216 |
. . . . 5
โข (๐ด โ (0(,]1) โ (๐ดโ2) โค
(1โ2)) |
44 | | sq1 14106 |
. . . . 5
โข
(1โ2) = 1 |
45 | 43, 44 | breqtrdi 5151 |
. . . 4
โข (๐ด โ (0(,]1) โ (๐ดโ2) โค
1) |
46 | | redivcl 11881 |
. . . . . . . 8
โข (((๐ดโ2) โ โ โง 3
โ โ โง 3 โ 0) โ ((๐ดโ2) / 3) โ
โ) |
47 | 22, 10, 46 | mp3an23 1454 |
. . . . . . 7
โข ((๐ดโ2) โ โ โ
((๐ดโ2) / 3) โ
โ) |
48 | 6, 47 | syl 17 |
. . . . . 6
โข (๐ด โ (0(,]1) โ ((๐ดโ2) / 3) โ
โ) |
49 | | remulcl 11143 |
. . . . . 6
โข ((2
โ โ โง ((๐ดโ2) / 3) โ โ) โ (2
ยท ((๐ดโ2) / 3))
โ โ) |
50 | 21, 48, 49 | sylancr 588 |
. . . . 5
โข (๐ด โ (0(,]1) โ (2
ยท ((๐ดโ2) / 3))
โ โ) |
51 | | ltletr 11254 |
. . . . . 6
โข (((2
ยท ((๐ดโ2) / 3))
โ โ โง (๐ดโ2) โ โ โง 1 โ
โ) โ (((2 ยท ((๐ดโ2) / 3)) < (๐ดโ2) โง (๐ดโ2) โค 1) โ (2 ยท ((๐ดโ2) / 3)) <
1)) |
52 | 2, 51 | mp3an3 1451 |
. . . . 5
โข (((2
ยท ((๐ดโ2) / 3))
โ โ โง (๐ดโ2) โ โ) โ (((2
ยท ((๐ดโ2) / 3))
< (๐ดโ2) โง
(๐ดโ2) โค 1) โ
(2 ยท ((๐ดโ2) /
3)) < 1)) |
53 | 50, 6, 52 | syl2anc 585 |
. . . 4
โข (๐ด โ (0(,]1) โ (((2
ยท ((๐ดโ2) / 3))
< (๐ดโ2) โง
(๐ดโ2) โค 1) โ
(2 ยท ((๐ดโ2) /
3)) < 1)) |
54 | 35, 45, 53 | mp2and 698 |
. . 3
โข (๐ด โ (0(,]1) โ (2
ยท ((๐ดโ2) / 3))
< 1) |
55 | | posdif 11655 |
. . . 4
โข (((2
ยท ((๐ดโ2) / 3))
โ โ โง 1 โ โ) โ ((2 ยท ((๐ดโ2) / 3)) < 1 โ 0 < (1
โ (2 ยท ((๐ดโ2) / 3))))) |
56 | 50, 2, 55 | sylancl 587 |
. . 3
โข (๐ด โ (0(,]1) โ ((2
ยท ((๐ดโ2) / 3))
< 1 โ 0 < (1 โ (2 ยท ((๐ดโ2) / 3))))) |
57 | 54, 56 | mpbid 231 |
. 2
โข (๐ด โ (0(,]1) โ 0 < (1
โ (2 ยท ((๐ดโ2) / 3)))) |
58 | | cos01bnd 16075 |
. . 3
โข (๐ด โ (0(,]1) โ ((1
โ (2 ยท ((๐ดโ2) / 3))) < (cosโ๐ด) โง (cosโ๐ด) < (1 โ ((๐ดโ2) /
3)))) |
59 | 58 | simpld 496 |
. 2
โข (๐ด โ (0(,]1) โ (1
โ (2 ยท ((๐ดโ2) / 3))) < (cosโ๐ด)) |
60 | | resubcl 11472 |
. . . 4
โข ((1
โ โ โง (2 ยท ((๐ดโ2) / 3)) โ โ) โ (1
โ (2 ยท ((๐ดโ2) / 3))) โ
โ) |
61 | 2, 50, 60 | sylancr 588 |
. . 3
โข (๐ด โ (0(,]1) โ (1
โ (2 ยท ((๐ดโ2) / 3))) โ
โ) |
62 | 5 | recoscld 16033 |
. . 3
โข (๐ด โ (0(,]1) โ
(cosโ๐ด) โ
โ) |
63 | | lttr 11238 |
. . 3
โข ((0
โ โ โง (1 โ (2 ยท ((๐ดโ2) / 3))) โ โ โง
(cosโ๐ด) โ
โ) โ ((0 < (1 โ (2 ยท ((๐ดโ2) / 3))) โง (1 โ (2 ยท
((๐ดโ2) / 3))) <
(cosโ๐ด)) โ 0
< (cosโ๐ด))) |
64 | 36, 61, 62, 63 | mp3an2i 1467 |
. 2
โข (๐ด โ (0(,]1) โ ((0 <
(1 โ (2 ยท ((๐ดโ2) / 3))) โง (1 โ (2 ยท
((๐ดโ2) / 3))) <
(cosโ๐ด)) โ 0
< (cosโ๐ด))) |
65 | 57, 59, 64 | mp2and 698 |
1
โข (๐ด โ (0(,]1) โ 0 <
(cosโ๐ด)) |