Step | Hyp | Ref
| Expression |
1 | | recosval 16025 |
. 2
โข (๐ด โ โ โ
(cosโ๐ด) =
(โโ(expโ(i ยท ๐ด)))) |
2 | | recn 11148 |
. . . . 5
โข (๐ด โ โ โ ๐ด โ
โ) |
3 | | efi4p.1 |
. . . . . 6
โข ๐น = (๐ โ โ0 โฆ (((i
ยท ๐ด)โ๐) / (!โ๐))) |
4 | 3 | efi4p 16026 |
. . . . 5
โข (๐ด โ โ โ
(expโ(i ยท ๐ด))
= (((1 โ ((๐ดโ2)
/ 2)) + (i ยท (๐ด
โ ((๐ดโ3) / 6))))
+ ฮฃ๐ โ
(โคโฅโ4)(๐นโ๐))) |
5 | 2, 4 | syl 17 |
. . . 4
โข (๐ด โ โ โ
(expโ(i ยท ๐ด))
= (((1 โ ((๐ดโ2)
/ 2)) + (i ยท (๐ด
โ ((๐ดโ3) / 6))))
+ ฮฃ๐ โ
(โคโฅโ4)(๐นโ๐))) |
6 | 5 | fveq2d 6851 |
. . 3
โข (๐ด โ โ โ
(โโ(expโ(i ยท ๐ด))) = (โโ(((1 โ ((๐ดโ2) / 2)) + (i ยท
(๐ด โ ((๐ดโ3) / 6)))) + ฮฃ๐ โ
(โคโฅโ4)(๐นโ๐)))) |
7 | | 1re 11162 |
. . . . . . 7
โข 1 โ
โ |
8 | | resqcl 14036 |
. . . . . . . 8
โข (๐ด โ โ โ (๐ดโ2) โ
โ) |
9 | 8 | rehalfcld 12407 |
. . . . . . 7
โข (๐ด โ โ โ ((๐ดโ2) / 2) โ
โ) |
10 | | resubcl 11472 |
. . . . . . 7
โข ((1
โ โ โง ((๐ดโ2) / 2) โ โ) โ (1
โ ((๐ดโ2) / 2))
โ โ) |
11 | 7, 9, 10 | sylancr 588 |
. . . . . 6
โข (๐ด โ โ โ (1
โ ((๐ดโ2) / 2))
โ โ) |
12 | 11 | recnd 11190 |
. . . . 5
โข (๐ด โ โ โ (1
โ ((๐ดโ2) / 2))
โ โ) |
13 | | ax-icn 11117 |
. . . . . 6
โข i โ
โ |
14 | | 3nn0 12438 |
. . . . . . . . . 10
โข 3 โ
โ0 |
15 | | reexpcl 13991 |
. . . . . . . . . 10
โข ((๐ด โ โ โง 3 โ
โ0) โ (๐ดโ3) โ โ) |
16 | 14, 15 | mpan2 690 |
. . . . . . . . 9
โข (๐ด โ โ โ (๐ดโ3) โ
โ) |
17 | | 6re 12250 |
. . . . . . . . . 10
โข 6 โ
โ |
18 | | 6pos 12270 |
. . . . . . . . . . 11
โข 0 <
6 |
19 | 17, 18 | gt0ne0ii 11698 |
. . . . . . . . . 10
โข 6 โ
0 |
20 | | redivcl 11881 |
. . . . . . . . . 10
โข (((๐ดโ3) โ โ โง 6
โ โ โง 6 โ 0) โ ((๐ดโ3) / 6) โ
โ) |
21 | 17, 19, 20 | mp3an23 1454 |
. . . . . . . . 9
โข ((๐ดโ3) โ โ โ
((๐ดโ3) / 6) โ
โ) |
22 | 16, 21 | syl 17 |
. . . . . . . 8
โข (๐ด โ โ โ ((๐ดโ3) / 6) โ
โ) |
23 | | resubcl 11472 |
. . . . . . . 8
โข ((๐ด โ โ โง ((๐ดโ3) / 6) โ โ)
โ (๐ด โ ((๐ดโ3) / 6)) โ
โ) |
24 | 22, 23 | mpdan 686 |
. . . . . . 7
โข (๐ด โ โ โ (๐ด โ ((๐ดโ3) / 6)) โ
โ) |
25 | 24 | recnd 11190 |
. . . . . 6
โข (๐ด โ โ โ (๐ด โ ((๐ดโ3) / 6)) โ
โ) |
26 | | mulcl 11142 |
. . . . . 6
โข ((i
โ โ โง (๐ด
โ ((๐ดโ3) / 6))
โ โ) โ (i ยท (๐ด โ ((๐ดโ3) / 6))) โ
โ) |
27 | 13, 25, 26 | sylancr 588 |
. . . . 5
โข (๐ด โ โ โ (i
ยท (๐ด โ ((๐ดโ3) / 6))) โ
โ) |
28 | 12, 27 | addcld 11181 |
. . . 4
โข (๐ด โ โ โ ((1
โ ((๐ดโ2) / 2)) +
(i ยท (๐ด โ
((๐ดโ3) / 6)))) โ
โ) |
29 | | mulcl 11142 |
. . . . . 6
โข ((i
โ โ โง ๐ด
โ โ) โ (i ยท ๐ด) โ โ) |
30 | 13, 2, 29 | sylancr 588 |
. . . . 5
โข (๐ด โ โ โ (i
ยท ๐ด) โ
โ) |
31 | | 4nn0 12439 |
. . . . 5
โข 4 โ
โ0 |
32 | 3 | eftlcl 15996 |
. . . . 5
โข (((i
ยท ๐ด) โ โ
โง 4 โ โ0) โ ฮฃ๐ โ
(โคโฅโ4)(๐นโ๐) โ โ) |
33 | 30, 31, 32 | sylancl 587 |
. . . 4
โข (๐ด โ โ โ
ฮฃ๐ โ
(โคโฅโ4)(๐นโ๐) โ โ) |
34 | 28, 33 | readdd 15106 |
. . 3
โข (๐ด โ โ โ
(โโ(((1 โ ((๐ดโ2) / 2)) + (i ยท (๐ด โ ((๐ดโ3) / 6)))) + ฮฃ๐ โ
(โคโฅโ4)(๐นโ๐))) = ((โโ((1 โ ((๐ดโ2) / 2)) + (i ยท
(๐ด โ ((๐ดโ3) / 6))))) +
(โโฮฃ๐
โ (โคโฅโ4)(๐นโ๐)))) |
35 | 11, 24 | crred 15123 |
. . . 4
โข (๐ด โ โ โ
(โโ((1 โ ((๐ดโ2) / 2)) + (i ยท (๐ด โ ((๐ดโ3) / 6))))) = (1 โ ((๐ดโ2) / 2))) |
36 | 35 | oveq1d 7377 |
. . 3
โข (๐ด โ โ โ
((โโ((1 โ ((๐ดโ2) / 2)) + (i ยท (๐ด โ ((๐ดโ3) / 6))))) +
(โโฮฃ๐
โ (โคโฅโ4)(๐นโ๐))) = ((1 โ ((๐ดโ2) / 2)) + (โโฮฃ๐ โ
(โคโฅโ4)(๐นโ๐)))) |
37 | 6, 34, 36 | 3eqtrd 2781 |
. 2
โข (๐ด โ โ โ
(โโ(expโ(i ยท ๐ด))) = ((1 โ ((๐ดโ2) / 2)) + (โโฮฃ๐ โ
(โคโฅโ4)(๐นโ๐)))) |
38 | 1, 37 | eqtrd 2777 |
1
โข (๐ด โ โ โ
(cosโ๐ด) = ((1 โ
((๐ดโ2) / 2)) +
(โโฮฃ๐
โ (โคโฅโ4)(๐นโ๐)))) |