Step | Hyp | Ref
| Expression |
1 | | ef0 15980 |
. . . . 5
โข
(expโ0) = 1 |
2 | 1 | eqeq2i 2750 |
. . . 4
โข
((expโ-(โโ๐ด)) = (expโ0) โ
(expโ-(โโ๐ด)) = 1) |
3 | | imcl 15003 |
. . . . . 6
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
4 | 3 | renegcld 11589 |
. . . . 5
โข (๐ด โ โ โ
-(โโ๐ด) โ
โ) |
5 | | 0re 11164 |
. . . . 5
โข 0 โ
โ |
6 | | reef11 16008 |
. . . . 5
โข
((-(โโ๐ด)
โ โ โง 0 โ โ) โ ((expโ-(โโ๐ด)) = (expโ0) โ
-(โโ๐ด) =
0)) |
7 | 4, 5, 6 | sylancl 587 |
. . . 4
โข (๐ด โ โ โ
((expโ-(โโ๐ด)) = (expโ0) โ
-(โโ๐ด) =
0)) |
8 | 2, 7 | bitr3id 285 |
. . 3
โข (๐ด โ โ โ
((expโ-(โโ๐ด)) = 1 โ -(โโ๐ด) = 0)) |
9 | 3 | recnd 11190 |
. . . 4
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
10 | 9 | negeq0d 11511 |
. . 3
โข (๐ด โ โ โ
((โโ๐ด) = 0
โ -(โโ๐ด) =
0)) |
11 | 8, 10 | bitr4d 282 |
. 2
โข (๐ด โ โ โ
((expโ-(โโ๐ด)) = 1 โ (โโ๐ด) = 0)) |
12 | | ax-icn 11117 |
. . . . . 6
โข i โ
โ |
13 | | mulcl 11142 |
. . . . . 6
โข ((i
โ โ โง ๐ด
โ โ) โ (i ยท ๐ด) โ โ) |
14 | 12, 13 | mpan 689 |
. . . . 5
โข (๐ด โ โ โ (i
ยท ๐ด) โ
โ) |
15 | | absef 16086 |
. . . . 5
โข ((i
ยท ๐ด) โ โ
โ (absโ(expโ(i ยท ๐ด))) = (expโ(โโ(i ยท
๐ด)))) |
16 | 14, 15 | syl 17 |
. . . 4
โข (๐ด โ โ โ
(absโ(expโ(i ยท ๐ด))) = (expโ(โโ(i ยท
๐ด)))) |
17 | | recl 15002 |
. . . . . . . . . . 11
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
18 | 17 | recnd 11190 |
. . . . . . . . . 10
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
19 | | mulcl 11142 |
. . . . . . . . . . 11
โข ((i
โ โ โง (โโ๐ด) โ โ) โ (i ยท
(โโ๐ด)) โ
โ) |
20 | 12, 9, 19 | sylancr 588 |
. . . . . . . . . 10
โข (๐ด โ โ โ (i
ยท (โโ๐ด))
โ โ) |
21 | | replim 15008 |
. . . . . . . . . 10
โข (๐ด โ โ โ ๐ด = ((โโ๐ด) + (i ยท
(โโ๐ด)))) |
22 | 18, 20, 21 | comraddd 11376 |
. . . . . . . . 9
โข (๐ด โ โ โ ๐ด = ((i ยท
(โโ๐ด)) +
(โโ๐ด))) |
23 | 22 | oveq2d 7378 |
. . . . . . . 8
โข (๐ด โ โ โ (i
ยท ๐ด) = (i ยท
((i ยท (โโ๐ด)) + (โโ๐ด)))) |
24 | | adddi 11147 |
. . . . . . . . . 10
โข ((i
โ โ โง (i ยท (โโ๐ด)) โ โ โง (โโ๐ด) โ โ) โ (i
ยท ((i ยท (โโ๐ด)) + (โโ๐ด))) = ((i ยท (i ยท
(โโ๐ด))) + (i
ยท (โโ๐ด)))) |
25 | 12, 20, 18, 24 | mp3an2i 1467 |
. . . . . . . . 9
โข (๐ด โ โ โ (i
ยท ((i ยท (โโ๐ด)) + (โโ๐ด))) = ((i ยท (i ยท
(โโ๐ด))) + (i
ยท (โโ๐ด)))) |
26 | | ixi 11791 |
. . . . . . . . . . . 12
โข (i
ยท i) = -1 |
27 | 26 | oveq1i 7372 |
. . . . . . . . . . 11
โข ((i
ยท i) ยท (โโ๐ด)) = (-1 ยท (โโ๐ด)) |
28 | | mulass 11146 |
. . . . . . . . . . . 12
โข ((i
โ โ โง i โ โ โง (โโ๐ด) โ โ) โ ((i ยท i)
ยท (โโ๐ด))
= (i ยท (i ยท (โโ๐ด)))) |
29 | 12, 12, 9, 28 | mp3an12i 1466 |
. . . . . . . . . . 11
โข (๐ด โ โ โ ((i
ยท i) ยท (โโ๐ด)) = (i ยท (i ยท
(โโ๐ด)))) |
30 | 9 | mulm1d 11614 |
. . . . . . . . . . 11
โข (๐ด โ โ โ (-1
ยท (โโ๐ด))
= -(โโ๐ด)) |
31 | 27, 29, 30 | 3eqtr3a 2801 |
. . . . . . . . . 10
โข (๐ด โ โ โ (i
ยท (i ยท (โโ๐ด))) = -(โโ๐ด)) |
32 | 31 | oveq1d 7377 |
. . . . . . . . 9
โข (๐ด โ โ โ ((i
ยท (i ยท (โโ๐ด))) + (i ยท (โโ๐ด))) = (-(โโ๐ด) + (i ยท
(โโ๐ด)))) |
33 | 25, 32 | eqtrd 2777 |
. . . . . . . 8
โข (๐ด โ โ โ (i
ยท ((i ยท (โโ๐ด)) + (โโ๐ด))) = (-(โโ๐ด) + (i ยท (โโ๐ด)))) |
34 | 23, 33 | eqtrd 2777 |
. . . . . . 7
โข (๐ด โ โ โ (i
ยท ๐ด) =
(-(โโ๐ด) + (i
ยท (โโ๐ด)))) |
35 | 34 | fveq2d 6851 |
. . . . . 6
โข (๐ด โ โ โ
(โโ(i ยท ๐ด)) = (โโ(-(โโ๐ด) + (i ยท
(โโ๐ด))))) |
36 | 4, 17 | crred 15123 |
. . . . . 6
โข (๐ด โ โ โ
(โโ(-(โโ๐ด) + (i ยท (โโ๐ด)))) = -(โโ๐ด)) |
37 | 35, 36 | eqtrd 2777 |
. . . . 5
โข (๐ด โ โ โ
(โโ(i ยท ๐ด)) = -(โโ๐ด)) |
38 | 37 | fveq2d 6851 |
. . . 4
โข (๐ด โ โ โ
(expโ(โโ(i ยท ๐ด))) = (expโ-(โโ๐ด))) |
39 | 16, 38 | eqtrd 2777 |
. . 3
โข (๐ด โ โ โ
(absโ(expโ(i ยท ๐ด))) = (expโ-(โโ๐ด))) |
40 | 39 | eqeq1d 2739 |
. 2
โข (๐ด โ โ โ
((absโ(expโ(i ยท ๐ด))) = 1 โ
(expโ-(โโ๐ด)) = 1)) |
41 | | reim0b 15011 |
. 2
โข (๐ด โ โ โ (๐ด โ โ โ
(โโ๐ด) =
0)) |
42 | 11, 40, 41 | 3bitr4rd 312 |
1
โข (๐ด โ โ โ (๐ด โ โ โ
(absโ(expโ(i ยท ๐ด))) = 1)) |