Step | Hyp | Ref
| Expression |
1 | | ef0 11680 |
. . . . 5
โข
(expโ0) = 1 |
2 | 1 | eqeq2i 2188 |
. . . 4
โข
((expโ-(โโ๐ด)) = (expโ0) โ
(expโ-(โโ๐ด)) = 1) |
3 | | imcl 10863 |
. . . . . 6
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
4 | 3 | renegcld 8337 |
. . . . 5
โข (๐ด โ โ โ
-(โโ๐ด) โ
โ) |
5 | | 0re 7957 |
. . . . 5
โข 0 โ
โ |
6 | | reef11 11707 |
. . . . 5
โข
((-(โโ๐ด)
โ โ โง 0 โ โ) โ ((expโ-(โโ๐ด)) = (expโ0) โ
-(โโ๐ด) =
0)) |
7 | 4, 5, 6 | sylancl 413 |
. . . 4
โข (๐ด โ โ โ
((expโ-(โโ๐ด)) = (expโ0) โ
-(โโ๐ด) =
0)) |
8 | 2, 7 | bitr3id 194 |
. . 3
โข (๐ด โ โ โ
((expโ-(โโ๐ด)) = 1 โ -(โโ๐ด) = 0)) |
9 | 3 | recnd 7986 |
. . . 4
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
10 | 9 | negeq0d 8260 |
. . 3
โข (๐ด โ โ โ
((โโ๐ด) = 0
โ -(โโ๐ด) =
0)) |
11 | 8, 10 | bitr4d 191 |
. 2
โข (๐ด โ โ โ
((expโ-(โโ๐ด)) = 1 โ (โโ๐ด) = 0)) |
12 | | ax-icn 7906 |
. . . . . 6
โข i โ
โ |
13 | | mulcl 7938 |
. . . . . 6
โข ((i
โ โ โง ๐ด
โ โ) โ (i ยท ๐ด) โ โ) |
14 | 12, 13 | mpan 424 |
. . . . 5
โข (๐ด โ โ โ (i
ยท ๐ด) โ
โ) |
15 | | absef 11777 |
. . . . 5
โข ((i
ยท ๐ด) โ โ
โ (absโ(expโ(i ยท ๐ด))) = (expโ(โโ(i ยท
๐ด)))) |
16 | 14, 15 | syl 14 |
. . . 4
โข (๐ด โ โ โ
(absโ(expโ(i ยท ๐ด))) = (expโ(โโ(i ยท
๐ด)))) |
17 | | replim 10868 |
. . . . . . . . . 10
โข (๐ด โ โ โ ๐ด = ((โโ๐ด) + (i ยท
(โโ๐ด)))) |
18 | | recl 10862 |
. . . . . . . . . . . 12
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
19 | 18 | recnd 7986 |
. . . . . . . . . . 11
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
20 | | mulcl 7938 |
. . . . . . . . . . . 12
โข ((i
โ โ โง (โโ๐ด) โ โ) โ (i ยท
(โโ๐ด)) โ
โ) |
21 | 12, 9, 20 | sylancr 414 |
. . . . . . . . . . 11
โข (๐ด โ โ โ (i
ยท (โโ๐ด))
โ โ) |
22 | 19, 21 | addcomd 8108 |
. . . . . . . . . 10
โข (๐ด โ โ โ
((โโ๐ด) + (i
ยท (โโ๐ด))) = ((i ยท (โโ๐ด)) + (โโ๐ด))) |
23 | 17, 22 | eqtrd 2210 |
. . . . . . . . 9
โข (๐ด โ โ โ ๐ด = ((i ยท
(โโ๐ด)) +
(โโ๐ด))) |
24 | 23 | oveq2d 5891 |
. . . . . . . 8
โข (๐ด โ โ โ (i
ยท ๐ด) = (i ยท
((i ยท (โโ๐ด)) + (โโ๐ด)))) |
25 | | adddi 7943 |
. . . . . . . . . . 11
โข ((i
โ โ โง (i ยท (โโ๐ด)) โ โ โง (โโ๐ด) โ โ) โ (i
ยท ((i ยท (โโ๐ด)) + (โโ๐ด))) = ((i ยท (i ยท
(โโ๐ด))) + (i
ยท (โโ๐ด)))) |
26 | 12, 25 | mp3an1 1324 |
. . . . . . . . . 10
โข (((i
ยท (โโ๐ด))
โ โ โง (โโ๐ด) โ โ) โ (i ยท ((i
ยท (โโ๐ด))
+ (โโ๐ด))) = ((i
ยท (i ยท (โโ๐ด))) + (i ยท (โโ๐ด)))) |
27 | 21, 19, 26 | syl2anc 411 |
. . . . . . . . 9
โข (๐ด โ โ โ (i
ยท ((i ยท (โโ๐ด)) + (โโ๐ด))) = ((i ยท (i ยท
(โโ๐ด))) + (i
ยท (โโ๐ด)))) |
28 | | ixi 8540 |
. . . . . . . . . . . 12
โข (i
ยท i) = -1 |
29 | 28 | oveq1i 5885 |
. . . . . . . . . . 11
โข ((i
ยท i) ยท (โโ๐ด)) = (-1 ยท (โโ๐ด)) |
30 | | mulass 7942 |
. . . . . . . . . . . . 13
โข ((i
โ โ โง i โ โ โง (โโ๐ด) โ โ) โ ((i ยท i)
ยท (โโ๐ด))
= (i ยท (i ยท (โโ๐ด)))) |
31 | 12, 12, 30 | mp3an12 1327 |
. . . . . . . . . . . 12
โข
((โโ๐ด)
โ โ โ ((i ยท i) ยท (โโ๐ด)) = (i ยท (i ยท
(โโ๐ด)))) |
32 | 9, 31 | syl 14 |
. . . . . . . . . . 11
โข (๐ด โ โ โ ((i
ยท i) ยท (โโ๐ด)) = (i ยท (i ยท
(โโ๐ด)))) |
33 | 9 | mulm1d 8367 |
. . . . . . . . . . 11
โข (๐ด โ โ โ (-1
ยท (โโ๐ด))
= -(โโ๐ด)) |
34 | 29, 32, 33 | 3eqtr3a 2234 |
. . . . . . . . . 10
โข (๐ด โ โ โ (i
ยท (i ยท (โโ๐ด))) = -(โโ๐ด)) |
35 | 34 | oveq1d 5890 |
. . . . . . . . 9
โข (๐ด โ โ โ ((i
ยท (i ยท (โโ๐ด))) + (i ยท (โโ๐ด))) = (-(โโ๐ด) + (i ยท
(โโ๐ด)))) |
36 | 27, 35 | eqtrd 2210 |
. . . . . . . 8
โข (๐ด โ โ โ (i
ยท ((i ยท (โโ๐ด)) + (โโ๐ด))) = (-(โโ๐ด) + (i ยท (โโ๐ด)))) |
37 | 24, 36 | eqtrd 2210 |
. . . . . . 7
โข (๐ด โ โ โ (i
ยท ๐ด) =
(-(โโ๐ด) + (i
ยท (โโ๐ด)))) |
38 | 37 | fveq2d 5520 |
. . . . . 6
โข (๐ด โ โ โ
(โโ(i ยท ๐ด)) = (โโ(-(โโ๐ด) + (i ยท
(โโ๐ด))))) |
39 | 4, 18 | crred 10985 |
. . . . . 6
โข (๐ด โ โ โ
(โโ(-(โโ๐ด) + (i ยท (โโ๐ด)))) = -(โโ๐ด)) |
40 | 38, 39 | eqtrd 2210 |
. . . . 5
โข (๐ด โ โ โ
(โโ(i ยท ๐ด)) = -(โโ๐ด)) |
41 | 40 | fveq2d 5520 |
. . . 4
โข (๐ด โ โ โ
(expโ(โโ(i ยท ๐ด))) = (expโ-(โโ๐ด))) |
42 | 16, 41 | eqtrd 2210 |
. . 3
โข (๐ด โ โ โ
(absโ(expโ(i ยท ๐ด))) = (expโ-(โโ๐ด))) |
43 | 42 | eqeq1d 2186 |
. 2
โข (๐ด โ โ โ
((absโ(expโ(i ยท ๐ด))) = 1 โ
(expโ-(โโ๐ด)) = 1)) |
44 | | reim0b 10871 |
. 2
โข (๐ด โ โ โ (๐ด โ โ โ
(โโ๐ด) =
0)) |
45 | 11, 43, 44 | 3bitr4rd 221 |
1
โข (๐ด โ โ โ (๐ด โ โ โ
(absโ(expโ(i ยท ๐ด))) = 1)) |