Step | Hyp | Ref
| Expression |
1 | | replim 15095 |
. . . . . . . . 9
โข (๐ด โ โ โ ๐ด = ((โโ๐ด) + (i ยท
(โโ๐ด)))) |
2 | 1 | oveq2d 7432 |
. . . . . . . 8
โข (๐ด โ โ โ (i
ยท ๐ด) = (i ยท
((โโ๐ด) + (i
ยท (โโ๐ด))))) |
3 | | ax-icn 11197 |
. . . . . . . . . 10
โข i โ
โ |
4 | | recl 15089 |
. . . . . . . . . . 11
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
5 | 4 | recnd 11272 |
. . . . . . . . . 10
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
6 | | imcl 15090 |
. . . . . . . . . . . 12
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
7 | 6 | recnd 11272 |
. . . . . . . . . . 11
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
8 | | mulcl 11222 |
. . . . . . . . . . 11
โข ((i
โ โ โง (โโ๐ด) โ โ) โ (i ยท
(โโ๐ด)) โ
โ) |
9 | 3, 7, 8 | sylancr 585 |
. . . . . . . . . 10
โข (๐ด โ โ โ (i
ยท (โโ๐ด))
โ โ) |
10 | | adddi 11227 |
. . . . . . . . . 10
โข ((i
โ โ โง (โโ๐ด) โ โ โง (i ยท
(โโ๐ด)) โ
โ) โ (i ยท ((โโ๐ด) + (i ยท (โโ๐ด)))) = ((i ยท
(โโ๐ด)) + (i
ยท (i ยท (โโ๐ด))))) |
11 | 3, 5, 9, 10 | mp3an2i 1462 |
. . . . . . . . 9
โข (๐ด โ โ โ (i
ยท ((โโ๐ด)
+ (i ยท (โโ๐ด)))) = ((i ยท (โโ๐ด)) + (i ยท (i ยท
(โโ๐ด))))) |
12 | | ixi 11873 |
. . . . . . . . . . . 12
โข (i
ยท i) = -1 |
13 | 12 | oveq1i 7426 |
. . . . . . . . . . 11
โข ((i
ยท i) ยท (โโ๐ด)) = (-1 ยท (โโ๐ด)) |
14 | | mulass 11226 |
. . . . . . . . . . . 12
โข ((i
โ โ โง i โ โ โง (โโ๐ด) โ โ) โ ((i ยท i)
ยท (โโ๐ด))
= (i ยท (i ยท (โโ๐ด)))) |
15 | 3, 3, 7, 14 | mp3an12i 1461 |
. . . . . . . . . . 11
โข (๐ด โ โ โ ((i
ยท i) ยท (โโ๐ด)) = (i ยท (i ยท
(โโ๐ด)))) |
16 | 7 | mulm1d 11696 |
. . . . . . . . . . 11
โข (๐ด โ โ โ (-1
ยท (โโ๐ด))
= -(โโ๐ด)) |
17 | 13, 15, 16 | 3eqtr3a 2789 |
. . . . . . . . . 10
โข (๐ด โ โ โ (i
ยท (i ยท (โโ๐ด))) = -(โโ๐ด)) |
18 | 17 | oveq2d 7432 |
. . . . . . . . 9
โข (๐ด โ โ โ ((i
ยท (โโ๐ด))
+ (i ยท (i ยท (โโ๐ด)))) = ((i ยท (โโ๐ด)) + -(โโ๐ด))) |
19 | 11, 18 | eqtrd 2765 |
. . . . . . . 8
โข (๐ด โ โ โ (i
ยท ((โโ๐ด)
+ (i ยท (โโ๐ด)))) = ((i ยท (โโ๐ด)) + -(โโ๐ด))) |
20 | 2, 19 | eqtrd 2765 |
. . . . . . 7
โข (๐ด โ โ โ (i
ยท ๐ด) = ((i ยท
(โโ๐ด)) +
-(โโ๐ด))) |
21 | 20 | fveq2d 6896 |
. . . . . 6
โข (๐ด โ โ โ
(expโ(i ยท ๐ด))
= (expโ((i ยท (โโ๐ด)) + -(โโ๐ด)))) |
22 | | mulcl 11222 |
. . . . . . . 8
โข ((i
โ โ โง (โโ๐ด) โ โ) โ (i ยท
(โโ๐ด)) โ
โ) |
23 | 3, 5, 22 | sylancr 585 |
. . . . . . 7
โข (๐ด โ โ โ (i
ยท (โโ๐ด))
โ โ) |
24 | 6 | renegcld 11671 |
. . . . . . . 8
โข (๐ด โ โ โ
-(โโ๐ด) โ
โ) |
25 | 24 | recnd 11272 |
. . . . . . 7
โข (๐ด โ โ โ
-(โโ๐ด) โ
โ) |
26 | | efadd 16070 |
. . . . . . 7
โข (((i
ยท (โโ๐ด))
โ โ โง -(โโ๐ด) โ โ) โ (expโ((i
ยท (โโ๐ด))
+ -(โโ๐ด))) =
((expโ(i ยท (โโ๐ด))) ยท
(expโ-(โโ๐ด)))) |
27 | 23, 25, 26 | syl2anc 582 |
. . . . . 6
โข (๐ด โ โ โ
(expโ((i ยท (โโ๐ด)) + -(โโ๐ด))) = ((expโ(i ยท
(โโ๐ด))) ยท
(expโ-(โโ๐ด)))) |
28 | 21, 27 | eqtrd 2765 |
. . . . 5
โข (๐ด โ โ โ
(expโ(i ยท ๐ด))
= ((expโ(i ยท (โโ๐ด))) ยท
(expโ-(โโ๐ด)))) |
29 | 28 | eqeq1d 2727 |
. . . 4
โข (๐ด โ โ โ
((expโ(i ยท ๐ด))
= 1 โ ((expโ(i ยท (โโ๐ด))) ยท
(expโ-(โโ๐ด))) = 1)) |
30 | | efcl 16058 |
. . . . . . . . 9
โข ((i
ยท (โโ๐ด))
โ โ โ (expโ(i ยท (โโ๐ด))) โ โ) |
31 | 23, 30 | syl 17 |
. . . . . . . 8
โข (๐ด โ โ โ
(expโ(i ยท (โโ๐ด))) โ โ) |
32 | | efcl 16058 |
. . . . . . . . 9
โข
(-(โโ๐ด)
โ โ โ (expโ-(โโ๐ด)) โ โ) |
33 | 25, 32 | syl 17 |
. . . . . . . 8
โข (๐ด โ โ โ
(expโ-(โโ๐ด)) โ โ) |
34 | 31, 33 | absmuld 15433 |
. . . . . . 7
โข (๐ด โ โ โ
(absโ((expโ(i ยท (โโ๐ด))) ยท
(expโ-(โโ๐ด)))) = ((absโ(expโ(i ยท
(โโ๐ด))))
ยท (absโ(expโ-(โโ๐ด))))) |
35 | | absefi 16172 |
. . . . . . . . 9
โข
((โโ๐ด)
โ โ โ (absโ(expโ(i ยท (โโ๐ด)))) = 1) |
36 | 4, 35 | syl 17 |
. . . . . . . 8
โข (๐ด โ โ โ
(absโ(expโ(i ยท (โโ๐ด)))) = 1) |
37 | 24 | reefcld 16064 |
. . . . . . . . 9
โข (๐ด โ โ โ
(expโ-(โโ๐ด)) โ โ) |
38 | | efgt0 16079 |
. . . . . . . . . . 11
โข
(-(โโ๐ด)
โ โ โ 0 < (expโ-(โโ๐ด))) |
39 | 24, 38 | syl 17 |
. . . . . . . . . 10
โข (๐ด โ โ โ 0 <
(expโ-(โโ๐ด))) |
40 | | 0re 11246 |
. . . . . . . . . . 11
โข 0 โ
โ |
41 | | ltle 11332 |
. . . . . . . . . . 11
โข ((0
โ โ โง (expโ-(โโ๐ด)) โ โ) โ (0 <
(expโ-(โโ๐ด)) โ 0 โค
(expโ-(โโ๐ด)))) |
42 | 40, 41 | mpan 688 |
. . . . . . . . . 10
โข
((expโ-(โโ๐ด)) โ โ โ (0 <
(expโ-(โโ๐ด)) โ 0 โค
(expโ-(โโ๐ด)))) |
43 | 37, 39, 42 | sylc 65 |
. . . . . . . . 9
โข (๐ด โ โ โ 0 โค
(expโ-(โโ๐ด))) |
44 | 37, 43 | absidd 15401 |
. . . . . . . 8
โข (๐ด โ โ โ
(absโ(expโ-(โโ๐ด))) = (expโ-(โโ๐ด))) |
45 | 36, 44 | oveq12d 7434 |
. . . . . . 7
โข (๐ด โ โ โ
((absโ(expโ(i ยท (โโ๐ด)))) ยท
(absโ(expโ-(โโ๐ด)))) = (1 ยท
(expโ-(โโ๐ด)))) |
46 | 33 | mullidd 11262 |
. . . . . . 7
โข (๐ด โ โ โ (1
ยท (expโ-(โโ๐ด))) = (expโ-(โโ๐ด))) |
47 | 34, 45, 46 | 3eqtrrd 2770 |
. . . . . 6
โข (๐ด โ โ โ
(expโ-(โโ๐ด)) = (absโ((expโ(i ยท
(โโ๐ด))) ยท
(expโ-(โโ๐ด))))) |
48 | | fveq2 6892 |
. . . . . 6
โข
(((expโ(i ยท (โโ๐ด))) ยท
(expโ-(โโ๐ด))) = 1 โ (absโ((expโ(i
ยท (โโ๐ด)))
ยท (expโ-(โโ๐ด)))) = (absโ1)) |
49 | 47, 48 | sylan9eq 2785 |
. . . . 5
โข ((๐ด โ โ โง
((expโ(i ยท (โโ๐ด))) ยท
(expโ-(โโ๐ด))) = 1) โ
(expโ-(โโ๐ด)) = (absโ1)) |
50 | 49 | ex 411 |
. . . 4
โข (๐ด โ โ โ
(((expโ(i ยท (โโ๐ด))) ยท
(expโ-(โโ๐ด))) = 1 โ
(expโ-(โโ๐ด)) = (absโ1))) |
51 | 29, 50 | sylbid 239 |
. . 3
โข (๐ด โ โ โ
((expโ(i ยท ๐ด))
= 1 โ (expโ-(โโ๐ด)) = (absโ1))) |
52 | 7 | negeq0d 11593 |
. . . 4
โข (๐ด โ โ โ
((โโ๐ด) = 0
โ -(โโ๐ด) =
0)) |
53 | | reim0b 15098 |
. . . 4
โข (๐ด โ โ โ (๐ด โ โ โ
(โโ๐ด) =
0)) |
54 | | ef0 16067 |
. . . . . . 7
โข
(expโ0) = 1 |
55 | | abs1 15276 |
. . . . . . 7
โข
(absโ1) = 1 |
56 | 54, 55 | eqtr4i 2756 |
. . . . . 6
โข
(expโ0) = (absโ1) |
57 | 56 | eqeq2i 2738 |
. . . . 5
โข
((expโ-(โโ๐ด)) = (expโ0) โ
(expโ-(โโ๐ด)) = (absโ1)) |
58 | | reef11 16095 |
. . . . . 6
โข
((-(โโ๐ด)
โ โ โง 0 โ โ) โ ((expโ-(โโ๐ด)) = (expโ0) โ
-(โโ๐ด) =
0)) |
59 | 24, 40, 58 | sylancl 584 |
. . . . 5
โข (๐ด โ โ โ
((expโ-(โโ๐ด)) = (expโ0) โ
-(โโ๐ด) =
0)) |
60 | 57, 59 | bitr3id 284 |
. . . 4
โข (๐ด โ โ โ
((expโ-(โโ๐ด)) = (absโ1) โ
-(โโ๐ด) =
0)) |
61 | 52, 53, 60 | 3bitr4rd 311 |
. . 3
โข (๐ด โ โ โ
((expโ-(โโ๐ด)) = (absโ1) โ ๐ด โ โ)) |
62 | 51, 61 | sylibd 238 |
. 2
โข (๐ด โ โ โ
((expโ(i ยท ๐ด))
= 1 โ ๐ด โ
โ)) |
63 | 62 | imp 405 |
1
โข ((๐ด โ โ โง
(expโ(i ยท ๐ด))
= 1) โ ๐ด โ
โ) |