Step | Hyp | Ref
| Expression |
1 | | replim 15008 |
. . . . . 6
โข (๐ด โ โ โ ๐ด = ((โโ๐ด) + (i ยท
(โโ๐ด)))) |
2 | 1 | fveq2d 6851 |
. . . . 5
โข (๐ด โ โ โ
(expโ๐ด) =
(expโ((โโ๐ด) + (i ยท (โโ๐ด))))) |
3 | | recl 15002 |
. . . . . . 7
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
4 | 3 | recnd 11190 |
. . . . . 6
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
5 | | ax-icn 11117 |
. . . . . . 7
โข i โ
โ |
6 | | imcl 15003 |
. . . . . . . 8
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
7 | 6 | recnd 11190 |
. . . . . . 7
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
8 | | mulcl 11142 |
. . . . . . 7
โข ((i
โ โ โง (โโ๐ด) โ โ) โ (i ยท
(โโ๐ด)) โ
โ) |
9 | 5, 7, 8 | sylancr 588 |
. . . . . 6
โข (๐ด โ โ โ (i
ยท (โโ๐ด))
โ โ) |
10 | | efadd 15983 |
. . . . . 6
โข
(((โโ๐ด)
โ โ โง (i ยท (โโ๐ด)) โ โ) โ
(expโ((โโ๐ด) + (i ยท (โโ๐ด)))) =
((expโ(โโ๐ด)) ยท (expโ(i ยท
(โโ๐ด))))) |
11 | 4, 9, 10 | syl2anc 585 |
. . . . 5
โข (๐ด โ โ โ
(expโ((โโ๐ด) + (i ยท (โโ๐ด)))) =
((expโ(โโ๐ด)) ยท (expโ(i ยท
(โโ๐ด))))) |
12 | 2, 11 | eqtrd 2777 |
. . . 4
โข (๐ด โ โ โ
(expโ๐ด) =
((expโ(โโ๐ด)) ยท (expโ(i ยท
(โโ๐ด))))) |
13 | 12 | fveq2d 6851 |
. . 3
โข (๐ด โ โ โ
(absโ(expโ๐ด)) =
(absโ((expโ(โโ๐ด)) ยท (expโ(i ยท
(โโ๐ด)))))) |
14 | 3 | reefcld 15977 |
. . . . 5
โข (๐ด โ โ โ
(expโ(โโ๐ด)) โ โ) |
15 | 14 | recnd 11190 |
. . . 4
โข (๐ด โ โ โ
(expโ(โโ๐ด)) โ โ) |
16 | | efcl 15972 |
. . . . 5
โข ((i
ยท (โโ๐ด))
โ โ โ (expโ(i ยท (โโ๐ด))) โ โ) |
17 | 9, 16 | syl 17 |
. . . 4
โข (๐ด โ โ โ
(expโ(i ยท (โโ๐ด))) โ โ) |
18 | 15, 17 | absmuld 15346 |
. . 3
โข (๐ด โ โ โ
(absโ((expโ(โโ๐ด)) ยท (expโ(i ยท
(โโ๐ด))))) =
((absโ(expโ(โโ๐ด))) ยท (absโ(expโ(i
ยท (โโ๐ด)))))) |
19 | | absefi 16085 |
. . . . 5
โข
((โโ๐ด)
โ โ โ (absโ(expโ(i ยท (โโ๐ด)))) = 1) |
20 | 6, 19 | syl 17 |
. . . 4
โข (๐ด โ โ โ
(absโ(expโ(i ยท (โโ๐ด)))) = 1) |
21 | 20 | oveq2d 7378 |
. . 3
โข (๐ด โ โ โ
((absโ(expโ(โโ๐ด))) ยท (absโ(expโ(i
ยท (โโ๐ด))))) =
((absโ(expโ(โโ๐ด))) ยท 1)) |
22 | 13, 18, 21 | 3eqtrd 2781 |
. 2
โข (๐ด โ โ โ
(absโ(expโ๐ด)) =
((absโ(expโ(โโ๐ด))) ยท 1)) |
23 | 15 | abscld 15328 |
. . . 4
โข (๐ด โ โ โ
(absโ(expโ(โโ๐ด))) โ โ) |
24 | 23 | recnd 11190 |
. . 3
โข (๐ด โ โ โ
(absโ(expโ(โโ๐ด))) โ โ) |
25 | 24 | mulid1d 11179 |
. 2
โข (๐ด โ โ โ
((absโ(expโ(โโ๐ด))) ยท 1) =
(absโ(expโ(โโ๐ด)))) |
26 | | efgt0 15992 |
. . . . 5
โข
((โโ๐ด)
โ โ โ 0 < (expโ(โโ๐ด))) |
27 | 3, 26 | syl 17 |
. . . 4
โข (๐ด โ โ โ 0 <
(expโ(โโ๐ด))) |
28 | | 0re 11164 |
. . . . 5
โข 0 โ
โ |
29 | | ltle 11250 |
. . . . 5
โข ((0
โ โ โง (expโ(โโ๐ด)) โ โ) โ (0 <
(expโ(โโ๐ด)) โ 0 โค
(expโ(โโ๐ด)))) |
30 | 28, 14, 29 | sylancr 588 |
. . . 4
โข (๐ด โ โ โ (0 <
(expโ(โโ๐ด)) โ 0 โค
(expโ(โโ๐ด)))) |
31 | 27, 30 | mpd 15 |
. . 3
โข (๐ด โ โ โ 0 โค
(expโ(โโ๐ด))) |
32 | 14, 31 | absidd 15314 |
. 2
โข (๐ด โ โ โ
(absโ(expโ(โโ๐ด))) = (expโ(โโ๐ด))) |
33 | 22, 25, 32 | 3eqtrd 2781 |
1
โข (๐ด โ โ โ
(absโ(expโ๐ด)) =
(expโ(โโ๐ด))) |