Step | Hyp | Ref
| Expression |
1 | | 1re 11162 |
. . . . . . 7
โข 1 โ
โ |
2 | | 0xr 11209 |
. . . . . . . . . . 11
โข 0 โ
โ* |
3 | | elioc2 13334 |
. . . . . . . . . . 11
โข ((0
โ โ* โง 1 โ โ) โ (๐ด โ (0(,]1) โ (๐ด โ โ โง 0 < ๐ด โง ๐ด โค 1))) |
4 | 2, 1, 3 | mp2an 691 |
. . . . . . . . . 10
โข (๐ด โ (0(,]1) โ (๐ด โ โ โง 0 <
๐ด โง ๐ด โค 1)) |
5 | 4 | simp1bi 1146 |
. . . . . . . . 9
โข (๐ด โ (0(,]1) โ ๐ด โ
โ) |
6 | 5 | resqcld 14037 |
. . . . . . . 8
โข (๐ด โ (0(,]1) โ (๐ดโ2) โ
โ) |
7 | 6 | rehalfcld 12407 |
. . . . . . 7
โข (๐ด โ (0(,]1) โ ((๐ดโ2) / 2) โ
โ) |
8 | | resubcl 11472 |
. . . . . . 7
โข ((1
โ โ โง ((๐ดโ2) / 2) โ โ) โ (1
โ ((๐ดโ2) / 2))
โ โ) |
9 | 1, 7, 8 | sylancr 588 |
. . . . . 6
โข (๐ด โ (0(,]1) โ (1
โ ((๐ดโ2) / 2))
โ โ) |
10 | 9 | recnd 11190 |
. . . . 5
โข (๐ด โ (0(,]1) โ (1
โ ((๐ดโ2) / 2))
โ โ) |
11 | | ax-icn 11117 |
. . . . . . . . 9
โข i โ
โ |
12 | 5 | recnd 11190 |
. . . . . . . . 9
โข (๐ด โ (0(,]1) โ ๐ด โ
โ) |
13 | | mulcl 11142 |
. . . . . . . . 9
โข ((i
โ โ โง ๐ด
โ โ) โ (i ยท ๐ด) โ โ) |
14 | 11, 12, 13 | sylancr 588 |
. . . . . . . 8
โข (๐ด โ (0(,]1) โ (i
ยท ๐ด) โ
โ) |
15 | | 4nn0 12439 |
. . . . . . . 8
โข 4 โ
โ0 |
16 | | eqid 2737 |
. . . . . . . . 9
โข (๐ โ โ0
โฆ (((i ยท ๐ด)โ๐) / (!โ๐))) = (๐ โ โ0 โฆ (((i
ยท ๐ด)โ๐) / (!โ๐))) |
17 | 16 | eftlcl 15996 |
. . . . . . . 8
โข (((i
ยท ๐ด) โ โ
โง 4 โ โ0) โ ฮฃ๐ โ
(โคโฅโ4)((๐ โ โ0 โฆ (((i
ยท ๐ด)โ๐) / (!โ๐)))โ๐) โ โ) |
18 | 14, 15, 17 | sylancl 587 |
. . . . . . 7
โข (๐ด โ (0(,]1) โ
ฮฃ๐ โ
(โคโฅโ4)((๐ โ โ0 โฆ (((i
ยท ๐ด)โ๐) / (!โ๐)))โ๐) โ โ) |
19 | 18 | recld 15086 |
. . . . . 6
โข (๐ด โ (0(,]1) โ
(โโฮฃ๐
โ (โคโฅโ4)((๐ โ โ0 โฆ (((i
ยท ๐ด)โ๐) / (!โ๐)))โ๐)) โ โ) |
20 | 19 | recnd 11190 |
. . . . 5
โข (๐ด โ (0(,]1) โ
(โโฮฃ๐
โ (โคโฅโ4)((๐ โ โ0 โฆ (((i
ยท ๐ด)โ๐) / (!โ๐)))โ๐)) โ โ) |
21 | 16 | recos4p 16028 |
. . . . . 6
โข (๐ด โ โ โ
(cosโ๐ด) = ((1 โ
((๐ดโ2) / 2)) +
(โโฮฃ๐
โ (โคโฅโ4)((๐ โ โ0 โฆ (((i
ยท ๐ด)โ๐) / (!โ๐)))โ๐)))) |
22 | 5, 21 | syl 17 |
. . . . 5
โข (๐ด โ (0(,]1) โ
(cosโ๐ด) = ((1 โ
((๐ดโ2) / 2)) +
(โโฮฃ๐
โ (โคโฅโ4)((๐ โ โ0 โฆ (((i
ยท ๐ด)โ๐) / (!โ๐)))โ๐)))) |
23 | 10, 20, 22 | mvrladdd 11575 |
. . . 4
โข (๐ด โ (0(,]1) โ
((cosโ๐ด) โ (1
โ ((๐ดโ2) / 2)))
= (โโฮฃ๐
โ (โคโฅโ4)((๐ โ โ0 โฆ (((i
ยท ๐ด)โ๐) / (!โ๐)))โ๐))) |
24 | 23 | fveq2d 6851 |
. . 3
โข (๐ด โ (0(,]1) โ
(absโ((cosโ๐ด)
โ (1 โ ((๐ดโ2) / 2)))) =
(absโ(โโฮฃ๐ โ
(โคโฅโ4)((๐ โ โ0 โฆ (((i
ยท ๐ด)โ๐) / (!โ๐)))โ๐)))) |
25 | 20 | abscld 15328 |
. . . 4
โข (๐ด โ (0(,]1) โ
(absโ(โโฮฃ๐ โ
(โคโฅโ4)((๐ โ โ0 โฆ (((i
ยท ๐ด)โ๐) / (!โ๐)))โ๐))) โ โ) |
26 | 18 | abscld 15328 |
. . . 4
โข (๐ด โ (0(,]1) โ
(absโฮฃ๐ โ
(โคโฅโ4)((๐ โ โ0 โฆ (((i
ยท ๐ด)โ๐) / (!โ๐)))โ๐)) โ โ) |
27 | | 6nn 12249 |
. . . . 5
โข 6 โ
โ |
28 | | nndivre 12201 |
. . . . 5
โข (((๐ดโ2) โ โ โง 6
โ โ) โ ((๐ดโ2) / 6) โ
โ) |
29 | 6, 27, 28 | sylancl 587 |
. . . 4
โข (๐ด โ (0(,]1) โ ((๐ดโ2) / 6) โ
โ) |
30 | | absrele 15200 |
. . . . 5
โข
(ฮฃ๐ โ
(โคโฅโ4)((๐ โ โ0 โฆ (((i
ยท ๐ด)โ๐) / (!โ๐)))โ๐) โ โ โ
(absโ(โโฮฃ๐ โ
(โคโฅโ4)((๐ โ โ0 โฆ (((i
ยท ๐ด)โ๐) / (!โ๐)))โ๐))) โค (absโฮฃ๐ โ
(โคโฅโ4)((๐ โ โ0 โฆ (((i
ยท ๐ด)โ๐) / (!โ๐)))โ๐))) |
31 | 18, 30 | syl 17 |
. . . 4
โข (๐ด โ (0(,]1) โ
(absโ(โโฮฃ๐ โ
(โคโฅโ4)((๐ โ โ0 โฆ (((i
ยท ๐ด)โ๐) / (!โ๐)))โ๐))) โค (absโฮฃ๐ โ
(โคโฅโ4)((๐ โ โ0 โฆ (((i
ยท ๐ด)โ๐) / (!โ๐)))โ๐))) |
32 | | reexpcl 13991 |
. . . . . . 7
โข ((๐ด โ โ โง 4 โ
โ0) โ (๐ดโ4) โ โ) |
33 | 5, 15, 32 | sylancl 587 |
. . . . . 6
โข (๐ด โ (0(,]1) โ (๐ดโ4) โ
โ) |
34 | | nndivre 12201 |
. . . . . 6
โข (((๐ดโ4) โ โ โง 6
โ โ) โ ((๐ดโ4) / 6) โ
โ) |
35 | 33, 27, 34 | sylancl 587 |
. . . . 5
โข (๐ด โ (0(,]1) โ ((๐ดโ4) / 6) โ
โ) |
36 | 16 | ef01bndlem 16073 |
. . . . 5
โข (๐ด โ (0(,]1) โ
(absโฮฃ๐ โ
(โคโฅโ4)((๐ โ โ0 โฆ (((i
ยท ๐ด)โ๐) / (!โ๐)))โ๐)) < ((๐ดโ4) / 6)) |
37 | | 2nn0 12437 |
. . . . . . . 8
โข 2 โ
โ0 |
38 | 37 | a1i 11 |
. . . . . . 7
โข (๐ด โ (0(,]1) โ 2 โ
โ0) |
39 | | 4z 12544 |
. . . . . . . . 9
โข 4 โ
โค |
40 | | 2re 12234 |
. . . . . . . . . 10
โข 2 โ
โ |
41 | | 4re 12244 |
. . . . . . . . . 10
โข 4 โ
โ |
42 | | 2lt4 12335 |
. . . . . . . . . 10
โข 2 <
4 |
43 | 40, 41, 42 | ltleii 11285 |
. . . . . . . . 9
โข 2 โค
4 |
44 | | 2z 12542 |
. . . . . . . . . 10
โข 2 โ
โค |
45 | 44 | eluz1i 12778 |
. . . . . . . . 9
โข (4 โ
(โคโฅโ2) โ (4 โ โค โง 2 โค
4)) |
46 | 39, 43, 45 | mpbir2an 710 |
. . . . . . . 8
โข 4 โ
(โคโฅโ2) |
47 | 46 | a1i 11 |
. . . . . . 7
โข (๐ด โ (0(,]1) โ 4 โ
(โคโฅโ2)) |
48 | 4 | simp2bi 1147 |
. . . . . . . 8
โข (๐ด โ (0(,]1) โ 0 <
๐ด) |
49 | | 0re 11164 |
. . . . . . . . 9
โข 0 โ
โ |
50 | | ltle 11250 |
. . . . . . . . 9
โข ((0
โ โ โง ๐ด
โ โ) โ (0 < ๐ด โ 0 โค ๐ด)) |
51 | 49, 5, 50 | sylancr 588 |
. . . . . . . 8
โข (๐ด โ (0(,]1) โ (0 <
๐ด โ 0 โค ๐ด)) |
52 | 48, 51 | mpd 15 |
. . . . . . 7
โข (๐ด โ (0(,]1) โ 0 โค
๐ด) |
53 | 4 | simp3bi 1148 |
. . . . . . 7
โข (๐ด โ (0(,]1) โ ๐ด โค 1) |
54 | 5, 38, 47, 52, 53 | leexp2rd 14165 |
. . . . . 6
โข (๐ด โ (0(,]1) โ (๐ดโ4) โค (๐ดโ2)) |
55 | | 6re 12250 |
. . . . . . . 8
โข 6 โ
โ |
56 | 55 | a1i 11 |
. . . . . . 7
โข (๐ด โ (0(,]1) โ 6 โ
โ) |
57 | | 6pos 12270 |
. . . . . . . 8
โข 0 <
6 |
58 | 57 | a1i 11 |
. . . . . . 7
โข (๐ด โ (0(,]1) โ 0 <
6) |
59 | | lediv1 12027 |
. . . . . . 7
โข (((๐ดโ4) โ โ โง
(๐ดโ2) โ โ
โง (6 โ โ โง 0 < 6)) โ ((๐ดโ4) โค (๐ดโ2) โ ((๐ดโ4) / 6) โค ((๐ดโ2) / 6))) |
60 | 33, 6, 56, 58, 59 | syl112anc 1375 |
. . . . . 6
โข (๐ด โ (0(,]1) โ ((๐ดโ4) โค (๐ดโ2) โ ((๐ดโ4) / 6) โค ((๐ดโ2) / 6))) |
61 | 54, 60 | mpbid 231 |
. . . . 5
โข (๐ด โ (0(,]1) โ ((๐ดโ4) / 6) โค ((๐ดโ2) / 6)) |
62 | 26, 35, 29, 36, 61 | ltletrd 11322 |
. . . 4
โข (๐ด โ (0(,]1) โ
(absโฮฃ๐ โ
(โคโฅโ4)((๐ โ โ0 โฆ (((i
ยท ๐ด)โ๐) / (!โ๐)))โ๐)) < ((๐ดโ2) / 6)) |
63 | 25, 26, 29, 31, 62 | lelttrd 11320 |
. . 3
โข (๐ด โ (0(,]1) โ
(absโ(โโฮฃ๐ โ
(โคโฅโ4)((๐ โ โ0 โฆ (((i
ยท ๐ด)โ๐) / (!โ๐)))โ๐))) < ((๐ดโ2) / 6)) |
64 | 24, 63 | eqbrtrd 5132 |
. 2
โข (๐ด โ (0(,]1) โ
(absโ((cosโ๐ด)
โ (1 โ ((๐ดโ2) / 2)))) < ((๐ดโ2) / 6)) |
65 | 5 | recoscld 16033 |
. . . 4
โข (๐ด โ (0(,]1) โ
(cosโ๐ด) โ
โ) |
66 | 65, 9, 29 | absdifltd 15325 |
. . 3
โข (๐ด โ (0(,]1) โ
((absโ((cosโ๐ด)
โ (1 โ ((๐ดโ2) / 2)))) < ((๐ดโ2) / 6) โ (((1 โ ((๐ดโ2) / 2)) โ ((๐ดโ2) / 6)) <
(cosโ๐ด) โง
(cosโ๐ด) < ((1
โ ((๐ดโ2) / 2)) +
((๐ดโ2) /
6))))) |
67 | | 1cnd 11157 |
. . . . . . 7
โข (๐ด โ (0(,]1) โ 1 โ
โ) |
68 | 7 | recnd 11190 |
. . . . . . 7
โข (๐ด โ (0(,]1) โ ((๐ดโ2) / 2) โ
โ) |
69 | 29 | recnd 11190 |
. . . . . . 7
โข (๐ด โ (0(,]1) โ ((๐ดโ2) / 6) โ
โ) |
70 | 67, 68, 69 | subsub4d 11550 |
. . . . . 6
โข (๐ด โ (0(,]1) โ ((1
โ ((๐ดโ2) / 2))
โ ((๐ดโ2) / 6)) =
(1 โ (((๐ดโ2) /
2) + ((๐ดโ2) /
6)))) |
71 | | halfpm6th 12381 |
. . . . . . . . . . 11
โข (((1 / 2)
โ (1 / 6)) = (1 / 3) โง ((1 / 2) + (1 / 6)) = (2 /
3)) |
72 | 71 | simpri 487 |
. . . . . . . . . 10
โข ((1 / 2)
+ (1 / 6)) = (2 / 3) |
73 | 72 | oveq2i 7373 |
. . . . . . . . 9
โข ((๐ดโ2) ยท ((1 / 2) + (1
/ 6))) = ((๐ดโ2)
ยท (2 / 3)) |
74 | 6 | recnd 11190 |
. . . . . . . . . 10
โข (๐ด โ (0(,]1) โ (๐ดโ2) โ
โ) |
75 | | 2cn 12235 |
. . . . . . . . . . . 12
โข 2 โ
โ |
76 | | 2ne0 12264 |
. . . . . . . . . . . 12
โข 2 โ
0 |
77 | 75, 76 | reccli 11892 |
. . . . . . . . . . 11
โข (1 / 2)
โ โ |
78 | | 6cn 12251 |
. . . . . . . . . . . 12
โข 6 โ
โ |
79 | 27 | nnne0i 12200 |
. . . . . . . . . . . 12
โข 6 โ
0 |
80 | 78, 79 | reccli 11892 |
. . . . . . . . . . 11
โข (1 / 6)
โ โ |
81 | | adddi 11147 |
. . . . . . . . . . 11
โข (((๐ดโ2) โ โ โง (1
/ 2) โ โ โง (1 / 6) โ โ) โ ((๐ดโ2) ยท ((1 / 2) + (1 / 6))) =
(((๐ดโ2) ยท (1 /
2)) + ((๐ดโ2) ยท
(1 / 6)))) |
82 | 77, 80, 81 | mp3an23 1454 |
. . . . . . . . . 10
โข ((๐ดโ2) โ โ โ
((๐ดโ2) ยท ((1 /
2) + (1 / 6))) = (((๐ดโ2) ยท (1 / 2)) + ((๐ดโ2) ยท (1 /
6)))) |
83 | 74, 82 | syl 17 |
. . . . . . . . 9
โข (๐ด โ (0(,]1) โ ((๐ดโ2) ยท ((1 / 2) + (1
/ 6))) = (((๐ดโ2)
ยท (1 / 2)) + ((๐ดโ2) ยท (1 /
6)))) |
84 | 73, 83 | eqtr3id 2791 |
. . . . . . . 8
โข (๐ด โ (0(,]1) โ ((๐ดโ2) ยท (2 / 3)) =
(((๐ดโ2) ยท (1 /
2)) + ((๐ดโ2) ยท
(1 / 6)))) |
85 | | 3cn 12241 |
. . . . . . . . . . 11
โข 3 โ
โ |
86 | | 3ne0 12266 |
. . . . . . . . . . 11
โข 3 โ
0 |
87 | 85, 86 | pm3.2i 472 |
. . . . . . . . . 10
โข (3 โ
โ โง 3 โ 0) |
88 | | div12 11842 |
. . . . . . . . . 10
โข ((2
โ โ โง (๐ดโ2) โ โ โง (3 โ
โ โง 3 โ 0)) โ (2 ยท ((๐ดโ2) / 3)) = ((๐ดโ2) ยท (2 / 3))) |
89 | 75, 87, 88 | mp3an13 1453 |
. . . . . . . . 9
โข ((๐ดโ2) โ โ โ
(2 ยท ((๐ดโ2) /
3)) = ((๐ดโ2) ยท
(2 / 3))) |
90 | 74, 89 | syl 17 |
. . . . . . . 8
โข (๐ด โ (0(,]1) โ (2
ยท ((๐ดโ2) / 3))
= ((๐ดโ2) ยท (2 /
3))) |
91 | | divrec 11836 |
. . . . . . . . . . 11
โข (((๐ดโ2) โ โ โง 2
โ โ โง 2 โ 0) โ ((๐ดโ2) / 2) = ((๐ดโ2) ยท (1 / 2))) |
92 | 75, 76, 91 | mp3an23 1454 |
. . . . . . . . . 10
โข ((๐ดโ2) โ โ โ
((๐ดโ2) / 2) = ((๐ดโ2) ยท (1 /
2))) |
93 | 74, 92 | syl 17 |
. . . . . . . . 9
โข (๐ด โ (0(,]1) โ ((๐ดโ2) / 2) = ((๐ดโ2) ยท (1 /
2))) |
94 | | divrec 11836 |
. . . . . . . . . . 11
โข (((๐ดโ2) โ โ โง 6
โ โ โง 6 โ 0) โ ((๐ดโ2) / 6) = ((๐ดโ2) ยท (1 / 6))) |
95 | 78, 79, 94 | mp3an23 1454 |
. . . . . . . . . 10
โข ((๐ดโ2) โ โ โ
((๐ดโ2) / 6) = ((๐ดโ2) ยท (1 /
6))) |
96 | 74, 95 | syl 17 |
. . . . . . . . 9
โข (๐ด โ (0(,]1) โ ((๐ดโ2) / 6) = ((๐ดโ2) ยท (1 /
6))) |
97 | 93, 96 | oveq12d 7380 |
. . . . . . . 8
โข (๐ด โ (0(,]1) โ (((๐ดโ2) / 2) + ((๐ดโ2) / 6)) = (((๐ดโ2) ยท (1 / 2)) +
((๐ดโ2) ยท (1 /
6)))) |
98 | 84, 90, 97 | 3eqtr4rd 2788 |
. . . . . . 7
โข (๐ด โ (0(,]1) โ (((๐ดโ2) / 2) + ((๐ดโ2) / 6)) = (2 ยท
((๐ดโ2) /
3))) |
99 | 98 | oveq2d 7378 |
. . . . . 6
โข (๐ด โ (0(,]1) โ (1
โ (((๐ดโ2) / 2) +
((๐ดโ2) / 6))) = (1
โ (2 ยท ((๐ดโ2) / 3)))) |
100 | 70, 99 | eqtrd 2777 |
. . . . 5
โข (๐ด โ (0(,]1) โ ((1
โ ((๐ดโ2) / 2))
โ ((๐ดโ2) / 6)) =
(1 โ (2 ยท ((๐ดโ2) / 3)))) |
101 | 100 | breq1d 5120 |
. . . 4
โข (๐ด โ (0(,]1) โ (((1
โ ((๐ดโ2) / 2))
โ ((๐ดโ2) / 6))
< (cosโ๐ด) โ
(1 โ (2 ยท ((๐ดโ2) / 3))) < (cosโ๐ด))) |
102 | 67, 68, 69 | subsubd 11547 |
. . . . . 6
โข (๐ด โ (0(,]1) โ (1
โ (((๐ดโ2) / 2)
โ ((๐ดโ2) / 6)))
= ((1 โ ((๐ดโ2) /
2)) + ((๐ดโ2) /
6))) |
103 | 71 | simpli 485 |
. . . . . . . . . 10
โข ((1 / 2)
โ (1 / 6)) = (1 / 3) |
104 | 103 | oveq2i 7373 |
. . . . . . . . 9
โข ((๐ดโ2) ยท ((1 / 2)
โ (1 / 6))) = ((๐ดโ2) ยท (1 / 3)) |
105 | | subdi 11595 |
. . . . . . . . . . 11
โข (((๐ดโ2) โ โ โง (1
/ 2) โ โ โง (1 / 6) โ โ) โ ((๐ดโ2) ยท ((1 / 2) โ (1 / 6)))
= (((๐ดโ2) ยท (1
/ 2)) โ ((๐ดโ2)
ยท (1 / 6)))) |
106 | 77, 80, 105 | mp3an23 1454 |
. . . . . . . . . 10
โข ((๐ดโ2) โ โ โ
((๐ดโ2) ยท ((1 /
2) โ (1 / 6))) = (((๐ดโ2) ยท (1 / 2)) โ ((๐ดโ2) ยท (1 /
6)))) |
107 | 74, 106 | syl 17 |
. . . . . . . . 9
โข (๐ด โ (0(,]1) โ ((๐ดโ2) ยท ((1 / 2)
โ (1 / 6))) = (((๐ดโ2) ยท (1 / 2)) โ ((๐ดโ2) ยท (1 /
6)))) |
108 | 104, 107 | eqtr3id 2791 |
. . . . . . . 8
โข (๐ด โ (0(,]1) โ ((๐ดโ2) ยท (1 / 3)) =
(((๐ดโ2) ยท (1 /
2)) โ ((๐ดโ2)
ยท (1 / 6)))) |
109 | | divrec 11836 |
. . . . . . . . . 10
โข (((๐ดโ2) โ โ โง 3
โ โ โง 3 โ 0) โ ((๐ดโ2) / 3) = ((๐ดโ2) ยท (1 / 3))) |
110 | 85, 86, 109 | mp3an23 1454 |
. . . . . . . . 9
โข ((๐ดโ2) โ โ โ
((๐ดโ2) / 3) = ((๐ดโ2) ยท (1 /
3))) |
111 | 74, 110 | syl 17 |
. . . . . . . 8
โข (๐ด โ (0(,]1) โ ((๐ดโ2) / 3) = ((๐ดโ2) ยท (1 /
3))) |
112 | 93, 96 | oveq12d 7380 |
. . . . . . . 8
โข (๐ด โ (0(,]1) โ (((๐ดโ2) / 2) โ ((๐ดโ2) / 6)) = (((๐ดโ2) ยท (1 / 2))
โ ((๐ดโ2)
ยท (1 / 6)))) |
113 | 108, 111,
112 | 3eqtr4rd 2788 |
. . . . . . 7
โข (๐ด โ (0(,]1) โ (((๐ดโ2) / 2) โ ((๐ดโ2) / 6)) = ((๐ดโ2) / 3)) |
114 | 113 | oveq2d 7378 |
. . . . . 6
โข (๐ด โ (0(,]1) โ (1
โ (((๐ดโ2) / 2)
โ ((๐ดโ2) / 6)))
= (1 โ ((๐ดโ2) /
3))) |
115 | 102, 114 | eqtr3d 2779 |
. . . . 5
โข (๐ด โ (0(,]1) โ ((1
โ ((๐ดโ2) / 2)) +
((๐ดโ2) / 6)) = (1
โ ((๐ดโ2) /
3))) |
116 | 115 | breq2d 5122 |
. . . 4
โข (๐ด โ (0(,]1) โ
((cosโ๐ด) < ((1
โ ((๐ดโ2) / 2)) +
((๐ดโ2) / 6)) โ
(cosโ๐ด) < (1
โ ((๐ดโ2) /
3)))) |
117 | 101, 116 | anbi12d 632 |
. . 3
โข (๐ด โ (0(,]1) โ ((((1
โ ((๐ดโ2) / 2))
โ ((๐ดโ2) / 6))
< (cosโ๐ด) โง
(cosโ๐ด) < ((1
โ ((๐ดโ2) / 2)) +
((๐ดโ2) / 6))) โ
((1 โ (2 ยท ((๐ดโ2) / 3))) < (cosโ๐ด) โง (cosโ๐ด) < (1 โ ((๐ดโ2) /
3))))) |
118 | 66, 117 | bitrd 279 |
. 2
โข (๐ด โ (0(,]1) โ
((absโ((cosโ๐ด)
โ (1 โ ((๐ดโ2) / 2)))) < ((๐ดโ2) / 6) โ ((1 โ (2 ยท
((๐ดโ2) / 3))) <
(cosโ๐ด) โง
(cosโ๐ด) < (1
โ ((๐ดโ2) /
3))))) |
119 | 64, 118 | mpbid 231 |
1
โข (๐ด โ (0(,]1) โ ((1
โ (2 ยท ((๐ดโ2) / 3))) < (cosโ๐ด) โง (cosโ๐ด) < (1 โ ((๐ดโ2) /
3)))) |