Step | Hyp | Ref
| Expression |
1 | | ef0 16041 |
. . . . 5
โข
(expโ0) = 1 |
2 | 1 | eqeq2i 2739 |
. . . 4
โข
((expโ-(โโ๐ด)) = (expโ0) โ
(expโ-(โโ๐ด)) = 1) |
3 | | imcl 15064 |
. . . . . 6
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
4 | 3 | renegcld 11645 |
. . . . 5
โข (๐ด โ โ โ
-(โโ๐ด) โ
โ) |
5 | | 0re 11220 |
. . . . 5
โข 0 โ
โ |
6 | | reef11 16069 |
. . . . 5
โข
((-(โโ๐ด)
โ โ โง 0 โ โ) โ ((expโ-(โโ๐ด)) = (expโ0) โ
-(โโ๐ด) =
0)) |
7 | 4, 5, 6 | sylancl 585 |
. . . 4
โข (๐ด โ โ โ
((expโ-(โโ๐ด)) = (expโ0) โ
-(โโ๐ด) =
0)) |
8 | 2, 7 | bitr3id 285 |
. . 3
โข (๐ด โ โ โ
((expโ-(โโ๐ด)) = 1 โ -(โโ๐ด) = 0)) |
9 | 3 | recnd 11246 |
. . . 4
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
10 | 9 | negeq0d 11567 |
. . 3
โข (๐ด โ โ โ
((โโ๐ด) = 0
โ -(โโ๐ด) =
0)) |
11 | 8, 10 | bitr4d 282 |
. 2
โข (๐ด โ โ โ
((expโ-(โโ๐ด)) = 1 โ (โโ๐ด) = 0)) |
12 | | ax-icn 11171 |
. . . . . 6
โข i โ
โ |
13 | | mulcl 11196 |
. . . . . 6
โข ((i
โ โ โง ๐ด
โ โ) โ (i ยท ๐ด) โ โ) |
14 | 12, 13 | mpan 687 |
. . . . 5
โข (๐ด โ โ โ (i
ยท ๐ด) โ
โ) |
15 | | absef 16147 |
. . . . 5
โข ((i
ยท ๐ด) โ โ
โ (absโ(expโ(i ยท ๐ด))) = (expโ(โโ(i ยท
๐ด)))) |
16 | 14, 15 | syl 17 |
. . . 4
โข (๐ด โ โ โ
(absโ(expโ(i ยท ๐ด))) = (expโ(โโ(i ยท
๐ด)))) |
17 | | recl 15063 |
. . . . . . . . . . 11
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
18 | 17 | recnd 11246 |
. . . . . . . . . 10
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
19 | | mulcl 11196 |
. . . . . . . . . . 11
โข ((i
โ โ โง (โโ๐ด) โ โ) โ (i ยท
(โโ๐ด)) โ
โ) |
20 | 12, 9, 19 | sylancr 586 |
. . . . . . . . . 10
โข (๐ด โ โ โ (i
ยท (โโ๐ด))
โ โ) |
21 | | replim 15069 |
. . . . . . . . . 10
โข (๐ด โ โ โ ๐ด = ((โโ๐ด) + (i ยท
(โโ๐ด)))) |
22 | 18, 20, 21 | comraddd 11432 |
. . . . . . . . 9
โข (๐ด โ โ โ ๐ด = ((i ยท
(โโ๐ด)) +
(โโ๐ด))) |
23 | 22 | oveq2d 7421 |
. . . . . . . 8
โข (๐ด โ โ โ (i
ยท ๐ด) = (i ยท
((i ยท (โโ๐ด)) + (โโ๐ด)))) |
24 | | adddi 11201 |
. . . . . . . . . 10
โข ((i
โ โ โง (i ยท (โโ๐ด)) โ โ โง (โโ๐ด) โ โ) โ (i
ยท ((i ยท (โโ๐ด)) + (โโ๐ด))) = ((i ยท (i ยท
(โโ๐ด))) + (i
ยท (โโ๐ด)))) |
25 | 12, 20, 18, 24 | mp3an2i 1462 |
. . . . . . . . 9
โข (๐ด โ โ โ (i
ยท ((i ยท (โโ๐ด)) + (โโ๐ด))) = ((i ยท (i ยท
(โโ๐ด))) + (i
ยท (โโ๐ด)))) |
26 | | ixi 11847 |
. . . . . . . . . . . 12
โข (i
ยท i) = -1 |
27 | 26 | oveq1i 7415 |
. . . . . . . . . . 11
โข ((i
ยท i) ยท (โโ๐ด)) = (-1 ยท (โโ๐ด)) |
28 | | mulass 11200 |
. . . . . . . . . . . 12
โข ((i
โ โ โง i โ โ โง (โโ๐ด) โ โ) โ ((i ยท i)
ยท (โโ๐ด))
= (i ยท (i ยท (โโ๐ด)))) |
29 | 12, 12, 9, 28 | mp3an12i 1461 |
. . . . . . . . . . 11
โข (๐ด โ โ โ ((i
ยท i) ยท (โโ๐ด)) = (i ยท (i ยท
(โโ๐ด)))) |
30 | 9 | mulm1d 11670 |
. . . . . . . . . . 11
โข (๐ด โ โ โ (-1
ยท (โโ๐ด))
= -(โโ๐ด)) |
31 | 27, 29, 30 | 3eqtr3a 2790 |
. . . . . . . . . 10
โข (๐ด โ โ โ (i
ยท (i ยท (โโ๐ด))) = -(โโ๐ด)) |
32 | 31 | oveq1d 7420 |
. . . . . . . . 9
โข (๐ด โ โ โ ((i
ยท (i ยท (โโ๐ด))) + (i ยท (โโ๐ด))) = (-(โโ๐ด) + (i ยท
(โโ๐ด)))) |
33 | 25, 32 | eqtrd 2766 |
. . . . . . . 8
โข (๐ด โ โ โ (i
ยท ((i ยท (โโ๐ด)) + (โโ๐ด))) = (-(โโ๐ด) + (i ยท (โโ๐ด)))) |
34 | 23, 33 | eqtrd 2766 |
. . . . . . 7
โข (๐ด โ โ โ (i
ยท ๐ด) =
(-(โโ๐ด) + (i
ยท (โโ๐ด)))) |
35 | 34 | fveq2d 6889 |
. . . . . 6
โข (๐ด โ โ โ
(โโ(i ยท ๐ด)) = (โโ(-(โโ๐ด) + (i ยท
(โโ๐ด))))) |
36 | 4, 17 | crred 15184 |
. . . . . 6
โข (๐ด โ โ โ
(โโ(-(โโ๐ด) + (i ยท (โโ๐ด)))) = -(โโ๐ด)) |
37 | 35, 36 | eqtrd 2766 |
. . . . 5
โข (๐ด โ โ โ
(โโ(i ยท ๐ด)) = -(โโ๐ด)) |
38 | 37 | fveq2d 6889 |
. . . 4
โข (๐ด โ โ โ
(expโ(โโ(i ยท ๐ด))) = (expโ-(โโ๐ด))) |
39 | 16, 38 | eqtrd 2766 |
. . 3
โข (๐ด โ โ โ
(absโ(expโ(i ยท ๐ด))) = (expโ-(โโ๐ด))) |
40 | 39 | eqeq1d 2728 |
. 2
โข (๐ด โ โ โ
((absโ(expโ(i ยท ๐ด))) = 1 โ
(expโ-(โโ๐ด)) = 1)) |
41 | | reim0b 15072 |
. 2
โข (๐ด โ โ โ (๐ด โ โ โ
(โโ๐ด) =
0)) |
42 | 11, 40, 41 | 3bitr4rd 312 |
1
โข (๐ด โ โ โ (๐ด โ โ โ
(absโ(expโ(i ยท ๐ด))) = 1)) |