Step | Hyp | Ref
| Expression |
1 | | ax-icn 11115 |
. . . 4
โข i โ
โ |
2 | | mulcl 11140 |
. . . 4
โข ((i
โ โ โง ๐ด
โ โ) โ (i ยท ๐ด) โ โ) |
3 | 1, 2 | mpan 689 |
. . 3
โข (๐ด โ โ โ (i
ยท ๐ด) โ
โ) |
4 | | efi4p.1 |
. . . 4
โข ๐น = (๐ โ โ0 โฆ (((i
ยท ๐ด)โ๐) / (!โ๐))) |
5 | 4 | ef4p 16000 |
. . 3
โข ((i
ยท ๐ด) โ โ
โ (expโ(i ยท ๐ด)) = ((((1 + (i ยท ๐ด)) + (((i ยท ๐ด)โ2) / 2)) + (((i ยท ๐ด)โ3) / 6)) + ฮฃ๐ โ
(โคโฅโ4)(๐นโ๐))) |
6 | 3, 5 | syl 17 |
. 2
โข (๐ด โ โ โ
(expโ(i ยท ๐ด))
= ((((1 + (i ยท ๐ด)) +
(((i ยท ๐ด)โ2) /
2)) + (((i ยท ๐ด)โ3) / 6)) + ฮฃ๐ โ
(โคโฅโ4)(๐นโ๐))) |
7 | | ax-1cn 11114 |
. . . . . 6
โข 1 โ
โ |
8 | | addcl 11138 |
. . . . . 6
โข ((1
โ โ โง (i ยท ๐ด) โ โ) โ (1 + (i ยท
๐ด)) โ
โ) |
9 | 7, 3, 8 | sylancr 588 |
. . . . 5
โข (๐ด โ โ โ (1 + (i
ยท ๐ด)) โ
โ) |
10 | 3 | sqcld 14055 |
. . . . . 6
โข (๐ด โ โ โ ((i
ยท ๐ด)โ2) โ
โ) |
11 | 10 | halfcld 12403 |
. . . . 5
โข (๐ด โ โ โ (((i
ยท ๐ด)โ2) / 2)
โ โ) |
12 | | 3nn0 12436 |
. . . . . . 7
โข 3 โ
โ0 |
13 | | expcl 13991 |
. . . . . . 7
โข (((i
ยท ๐ด) โ โ
โง 3 โ โ0) โ ((i ยท ๐ด)โ3) โ โ) |
14 | 3, 12, 13 | sylancl 587 |
. . . . . 6
โข (๐ด โ โ โ ((i
ยท ๐ด)โ3) โ
โ) |
15 | | 6cn 12249 |
. . . . . . 7
โข 6 โ
โ |
16 | | 6re 12248 |
. . . . . . . 8
โข 6 โ
โ |
17 | | 6pos 12268 |
. . . . . . . 8
โข 0 <
6 |
18 | 16, 17 | gt0ne0ii 11696 |
. . . . . . 7
โข 6 โ
0 |
19 | | divcl 11824 |
. . . . . . 7
โข ((((i
ยท ๐ด)โ3) โ
โ โง 6 โ โ โง 6 โ 0) โ (((i ยท ๐ด)โ3) / 6) โ
โ) |
20 | 15, 18, 19 | mp3an23 1454 |
. . . . . 6
โข (((i
ยท ๐ด)โ3) โ
โ โ (((i ยท ๐ด)โ3) / 6) โ
โ) |
21 | 14, 20 | syl 17 |
. . . . 5
โข (๐ด โ โ โ (((i
ยท ๐ด)โ3) / 6)
โ โ) |
22 | 9, 11, 21 | addassd 11182 |
. . . 4
โข (๐ด โ โ โ (((1 + (i
ยท ๐ด)) + (((i
ยท ๐ด)โ2) / 2)) +
(((i ยท ๐ด)โ3) /
6)) = ((1 + (i ยท ๐ด))
+ ((((i ยท ๐ด)โ2)
/ 2) + (((i ยท ๐ด)โ3) / 6)))) |
23 | 7 | a1i 11 |
. . . . 5
โข (๐ด โ โ โ 1 โ
โ) |
24 | 23, 3, 11, 21 | add4d 11388 |
. . . 4
โข (๐ด โ โ โ ((1 + (i
ยท ๐ด)) + ((((i
ยท ๐ด)โ2) / 2) +
(((i ยท ๐ด)โ3) /
6))) = ((1 + (((i ยท ๐ด)โ2) / 2)) + ((i ยท ๐ด) + (((i ยท ๐ด)โ3) /
6)))) |
25 | | 2nn0 12435 |
. . . . . . . . . . 11
โข 2 โ
โ0 |
26 | | mulexp 14013 |
. . . . . . . . . . 11
โข ((i
โ โ โง ๐ด
โ โ โง 2 โ โ0) โ ((i ยท ๐ด)โ2) = ((iโ2) ยท
(๐ดโ2))) |
27 | 1, 25, 26 | mp3an13 1453 |
. . . . . . . . . 10
โข (๐ด โ โ โ ((i
ยท ๐ด)โ2) =
((iโ2) ยท (๐ดโ2))) |
28 | | i2 14112 |
. . . . . . . . . . . 12
โข
(iโ2) = -1 |
29 | 28 | oveq1i 7368 |
. . . . . . . . . . 11
โข
((iโ2) ยท (๐ดโ2)) = (-1 ยท (๐ดโ2)) |
30 | 29 | a1i 11 |
. . . . . . . . . 10
โข (๐ด โ โ โ
((iโ2) ยท (๐ดโ2)) = (-1 ยท (๐ดโ2))) |
31 | | sqcl 14029 |
. . . . . . . . . . 11
โข (๐ด โ โ โ (๐ดโ2) โ
โ) |
32 | 31 | mulm1d 11612 |
. . . . . . . . . 10
โข (๐ด โ โ โ (-1
ยท (๐ดโ2)) =
-(๐ดโ2)) |
33 | 27, 30, 32 | 3eqtrd 2777 |
. . . . . . . . 9
โข (๐ด โ โ โ ((i
ยท ๐ด)โ2) =
-(๐ดโ2)) |
34 | 33 | oveq1d 7373 |
. . . . . . . 8
โข (๐ด โ โ โ (((i
ยท ๐ด)โ2) / 2) =
(-(๐ดโ2) /
2)) |
35 | | 2cn 12233 |
. . . . . . . . . 10
โข 2 โ
โ |
36 | | 2ne0 12262 |
. . . . . . . . . 10
โข 2 โ
0 |
37 | | divneg 11852 |
. . . . . . . . . 10
โข (((๐ดโ2) โ โ โง 2
โ โ โง 2 โ 0) โ -((๐ดโ2) / 2) = (-(๐ดโ2) / 2)) |
38 | 35, 36, 37 | mp3an23 1454 |
. . . . . . . . 9
โข ((๐ดโ2) โ โ โ
-((๐ดโ2) / 2) =
(-(๐ดโ2) /
2)) |
39 | 31, 38 | syl 17 |
. . . . . . . 8
โข (๐ด โ โ โ -((๐ดโ2) / 2) = (-(๐ดโ2) / 2)) |
40 | 34, 39 | eqtr4d 2776 |
. . . . . . 7
โข (๐ด โ โ โ (((i
ยท ๐ด)โ2) / 2) =
-((๐ดโ2) /
2)) |
41 | 40 | oveq2d 7374 |
. . . . . 6
โข (๐ด โ โ โ (1 + (((i
ยท ๐ด)โ2) / 2)) =
(1 + -((๐ดโ2) /
2))) |
42 | 31 | halfcld 12403 |
. . . . . . 7
โข (๐ด โ โ โ ((๐ดโ2) / 2) โ
โ) |
43 | | negsub 11454 |
. . . . . . 7
โข ((1
โ โ โง ((๐ดโ2) / 2) โ โ) โ (1 +
-((๐ดโ2) / 2)) = (1
โ ((๐ดโ2) /
2))) |
44 | 7, 42, 43 | sylancr 588 |
. . . . . 6
โข (๐ด โ โ โ (1 +
-((๐ดโ2) / 2)) = (1
โ ((๐ดโ2) /
2))) |
45 | 41, 44 | eqtrd 2773 |
. . . . 5
โข (๐ด โ โ โ (1 + (((i
ยท ๐ด)โ2) / 2)) =
(1 โ ((๐ดโ2) /
2))) |
46 | | mulexp 14013 |
. . . . . . . . . . 11
โข ((i
โ โ โง ๐ด
โ โ โง 3 โ โ0) โ ((i ยท ๐ด)โ3) = ((iโ3) ยท
(๐ดโ3))) |
47 | 1, 12, 46 | mp3an13 1453 |
. . . . . . . . . 10
โข (๐ด โ โ โ ((i
ยท ๐ด)โ3) =
((iโ3) ยท (๐ดโ3))) |
48 | | i3 14113 |
. . . . . . . . . . 11
โข
(iโ3) = -i |
49 | 48 | oveq1i 7368 |
. . . . . . . . . 10
โข
((iโ3) ยท (๐ดโ3)) = (-i ยท (๐ดโ3)) |
50 | 47, 49 | eqtrdi 2789 |
. . . . . . . . 9
โข (๐ด โ โ โ ((i
ยท ๐ด)โ3) = (-i
ยท (๐ดโ3))) |
51 | 50 | oveq1d 7373 |
. . . . . . . 8
โข (๐ด โ โ โ (((i
ยท ๐ด)โ3) / 6) =
((-i ยท (๐ดโ3)) /
6)) |
52 | | expcl 13991 |
. . . . . . . . . 10
โข ((๐ด โ โ โง 3 โ
โ0) โ (๐ดโ3) โ โ) |
53 | 12, 52 | mpan2 690 |
. . . . . . . . 9
โข (๐ด โ โ โ (๐ดโ3) โ
โ) |
54 | | negicn 11407 |
. . . . . . . . . 10
โข -i โ
โ |
55 | 15, 18 | pm3.2i 472 |
. . . . . . . . . 10
โข (6 โ
โ โง 6 โ 0) |
56 | | divass 11836 |
. . . . . . . . . 10
โข ((-i
โ โ โง (๐ดโ3) โ โ โง (6 โ
โ โง 6 โ 0)) โ ((-i ยท (๐ดโ3)) / 6) = (-i ยท ((๐ดโ3) / 6))) |
57 | 54, 55, 56 | mp3an13 1453 |
. . . . . . . . 9
โข ((๐ดโ3) โ โ โ
((-i ยท (๐ดโ3)) /
6) = (-i ยท ((๐ดโ3) / 6))) |
58 | 53, 57 | syl 17 |
. . . . . . . 8
โข (๐ด โ โ โ ((-i
ยท (๐ดโ3)) / 6) =
(-i ยท ((๐ดโ3) /
6))) |
59 | | divcl 11824 |
. . . . . . . . . . 11
โข (((๐ดโ3) โ โ โง 6
โ โ โง 6 โ 0) โ ((๐ดโ3) / 6) โ
โ) |
60 | 15, 18, 59 | mp3an23 1454 |
. . . . . . . . . 10
โข ((๐ดโ3) โ โ โ
((๐ดโ3) / 6) โ
โ) |
61 | 53, 60 | syl 17 |
. . . . . . . . 9
โข (๐ด โ โ โ ((๐ดโ3) / 6) โ
โ) |
62 | | mulneg12 11598 |
. . . . . . . . 9
โข ((i
โ โ โง ((๐ดโ3) / 6) โ โ) โ (-i
ยท ((๐ดโ3) / 6))
= (i ยท -((๐ดโ3)
/ 6))) |
63 | 1, 61, 62 | sylancr 588 |
. . . . . . . 8
โข (๐ด โ โ โ (-i
ยท ((๐ดโ3) / 6))
= (i ยท -((๐ดโ3)
/ 6))) |
64 | 51, 58, 63 | 3eqtrd 2777 |
. . . . . . 7
โข (๐ด โ โ โ (((i
ยท ๐ด)โ3) / 6) =
(i ยท -((๐ดโ3) /
6))) |
65 | 64 | oveq2d 7374 |
. . . . . 6
โข (๐ด โ โ โ ((i
ยท ๐ด) + (((i ยท
๐ด)โ3) / 6)) = ((i
ยท ๐ด) + (i ยท
-((๐ดโ3) /
6)))) |
66 | 61 | negcld 11504 |
. . . . . . 7
โข (๐ด โ โ โ -((๐ดโ3) / 6) โ
โ) |
67 | | adddi 11145 |
. . . . . . . 8
โข ((i
โ โ โง ๐ด
โ โ โง -((๐ดโ3) / 6) โ โ) โ (i
ยท (๐ด + -((๐ดโ3) / 6))) = ((i ยท
๐ด) + (i ยท -((๐ดโ3) /
6)))) |
68 | 1, 67 | mp3an1 1449 |
. . . . . . 7
โข ((๐ด โ โ โง -((๐ดโ3) / 6) โ โ)
โ (i ยท (๐ด +
-((๐ดโ3) / 6))) = ((i
ยท ๐ด) + (i ยท
-((๐ดโ3) /
6)))) |
69 | 66, 68 | mpdan 686 |
. . . . . 6
โข (๐ด โ โ โ (i
ยท (๐ด + -((๐ดโ3) / 6))) = ((i ยท
๐ด) + (i ยท -((๐ดโ3) /
6)))) |
70 | | negsub 11454 |
. . . . . . . 8
โข ((๐ด โ โ โง ((๐ดโ3) / 6) โ โ)
โ (๐ด + -((๐ดโ3) / 6)) = (๐ด โ ((๐ดโ3) / 6))) |
71 | 61, 70 | mpdan 686 |
. . . . . . 7
โข (๐ด โ โ โ (๐ด + -((๐ดโ3) / 6)) = (๐ด โ ((๐ดโ3) / 6))) |
72 | 71 | oveq2d 7374 |
. . . . . 6
โข (๐ด โ โ โ (i
ยท (๐ด + -((๐ดโ3) / 6))) = (i ยท
(๐ด โ ((๐ดโ3) /
6)))) |
73 | 65, 69, 72 | 3eqtr2d 2779 |
. . . . 5
โข (๐ด โ โ โ ((i
ยท ๐ด) + (((i ยท
๐ด)โ3) / 6)) = (i
ยท (๐ด โ ((๐ดโ3) /
6)))) |
74 | 45, 73 | oveq12d 7376 |
. . . 4
โข (๐ด โ โ โ ((1 +
(((i ยท ๐ด)โ2) /
2)) + ((i ยท ๐ด) +
(((i ยท ๐ด)โ3) /
6))) = ((1 โ ((๐ดโ2) / 2)) + (i ยท (๐ด โ ((๐ดโ3) / 6))))) |
75 | 22, 24, 74 | 3eqtrd 2777 |
. . 3
โข (๐ด โ โ โ (((1 + (i
ยท ๐ด)) + (((i
ยท ๐ด)โ2) / 2)) +
(((i ยท ๐ด)โ3) /
6)) = ((1 โ ((๐ดโ2) / 2)) + (i ยท (๐ด โ ((๐ดโ3) / 6))))) |
76 | 75 | oveq1d 7373 |
. 2
โข (๐ด โ โ โ ((((1 +
(i ยท ๐ด)) + (((i
ยท ๐ด)โ2) / 2)) +
(((i ยท ๐ด)โ3) /
6)) + ฮฃ๐ โ
(โคโฅโ4)(๐นโ๐)) = (((1 โ ((๐ดโ2) / 2)) + (i ยท (๐ด โ ((๐ดโ3) / 6)))) + ฮฃ๐ โ
(โคโฅโ4)(๐นโ๐))) |
77 | 6, 76 | eqtrd 2773 |
1
โข (๐ด โ โ โ
(expโ(i ยท ๐ด))
= (((1 โ ((๐ดโ2)
/ 2)) + (i ยท (๐ด
โ ((๐ดโ3) / 6))))
+ ฮฃ๐ โ
(โคโฅโ4)(๐นโ๐))) |