Step | Hyp | Ref
| Expression |
1 | | replim 15008 |
. . . . . . . . 9
โข (๐ด โ โ โ ๐ด = ((โโ๐ด) + (i ยท
(โโ๐ด)))) |
2 | 1 | oveq2d 7378 |
. . . . . . . 8
โข (๐ด โ โ โ (i
ยท ๐ด) = (i ยท
((โโ๐ด) + (i
ยท (โโ๐ด))))) |
3 | | ax-icn 11117 |
. . . . . . . . . 10
โข i โ
โ |
4 | | recl 15002 |
. . . . . . . . . . 11
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
5 | 4 | recnd 11190 |
. . . . . . . . . 10
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
6 | | imcl 15003 |
. . . . . . . . . . . 12
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
7 | 6 | recnd 11190 |
. . . . . . . . . . 11
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
8 | | mulcl 11142 |
. . . . . . . . . . 11
โข ((i
โ โ โง (โโ๐ด) โ โ) โ (i ยท
(โโ๐ด)) โ
โ) |
9 | 3, 7, 8 | sylancr 588 |
. . . . . . . . . 10
โข (๐ด โ โ โ (i
ยท (โโ๐ด))
โ โ) |
10 | | adddi 11147 |
. . . . . . . . . 10
โข ((i
โ โ โง (โโ๐ด) โ โ โง (i ยท
(โโ๐ด)) โ
โ) โ (i ยท ((โโ๐ด) + (i ยท (โโ๐ด)))) = ((i ยท
(โโ๐ด)) + (i
ยท (i ยท (โโ๐ด))))) |
11 | 3, 5, 9, 10 | mp3an2i 1467 |
. . . . . . . . 9
โข (๐ด โ โ โ (i
ยท ((โโ๐ด)
+ (i ยท (โโ๐ด)))) = ((i ยท (โโ๐ด)) + (i ยท (i ยท
(โโ๐ด))))) |
12 | | ixi 11791 |
. . . . . . . . . . . 12
โข (i
ยท i) = -1 |
13 | 12 | oveq1i 7372 |
. . . . . . . . . . 11
โข ((i
ยท i) ยท (โโ๐ด)) = (-1 ยท (โโ๐ด)) |
14 | | mulass 11146 |
. . . . . . . . . . . 12
โข ((i
โ โ โง i โ โ โง (โโ๐ด) โ โ) โ ((i ยท i)
ยท (โโ๐ด))
= (i ยท (i ยท (โโ๐ด)))) |
15 | 3, 3, 7, 14 | mp3an12i 1466 |
. . . . . . . . . . 11
โข (๐ด โ โ โ ((i
ยท i) ยท (โโ๐ด)) = (i ยท (i ยท
(โโ๐ด)))) |
16 | 7 | mulm1d 11614 |
. . . . . . . . . . 11
โข (๐ด โ โ โ (-1
ยท (โโ๐ด))
= -(โโ๐ด)) |
17 | 13, 15, 16 | 3eqtr3a 2801 |
. . . . . . . . . 10
โข (๐ด โ โ โ (i
ยท (i ยท (โโ๐ด))) = -(โโ๐ด)) |
18 | 17 | oveq2d 7378 |
. . . . . . . . 9
โข (๐ด โ โ โ ((i
ยท (โโ๐ด))
+ (i ยท (i ยท (โโ๐ด)))) = ((i ยท (โโ๐ด)) + -(โโ๐ด))) |
19 | 11, 18 | eqtrd 2777 |
. . . . . . . 8
โข (๐ด โ โ โ (i
ยท ((โโ๐ด)
+ (i ยท (โโ๐ด)))) = ((i ยท (โโ๐ด)) + -(โโ๐ด))) |
20 | 2, 19 | eqtrd 2777 |
. . . . . . 7
โข (๐ด โ โ โ (i
ยท ๐ด) = ((i ยท
(โโ๐ด)) +
-(โโ๐ด))) |
21 | 20 | fveq2d 6851 |
. . . . . 6
โข (๐ด โ โ โ
(expโ(i ยท ๐ด))
= (expโ((i ยท (โโ๐ด)) + -(โโ๐ด)))) |
22 | | mulcl 11142 |
. . . . . . . 8
โข ((i
โ โ โง (โโ๐ด) โ โ) โ (i ยท
(โโ๐ด)) โ
โ) |
23 | 3, 5, 22 | sylancr 588 |
. . . . . . 7
โข (๐ด โ โ โ (i
ยท (โโ๐ด))
โ โ) |
24 | 6 | renegcld 11589 |
. . . . . . . 8
โข (๐ด โ โ โ
-(โโ๐ด) โ
โ) |
25 | 24 | recnd 11190 |
. . . . . . 7
โข (๐ด โ โ โ
-(โโ๐ด) โ
โ) |
26 | | efadd 15983 |
. . . . . . 7
โข (((i
ยท (โโ๐ด))
โ โ โง -(โโ๐ด) โ โ) โ (expโ((i
ยท (โโ๐ด))
+ -(โโ๐ด))) =
((expโ(i ยท (โโ๐ด))) ยท
(expโ-(โโ๐ด)))) |
27 | 23, 25, 26 | syl2anc 585 |
. . . . . 6
โข (๐ด โ โ โ
(expโ((i ยท (โโ๐ด)) + -(โโ๐ด))) = ((expโ(i ยท
(โโ๐ด))) ยท
(expโ-(โโ๐ด)))) |
28 | 21, 27 | eqtrd 2777 |
. . . . 5
โข (๐ด โ โ โ
(expโ(i ยท ๐ด))
= ((expโ(i ยท (โโ๐ด))) ยท
(expโ-(โโ๐ด)))) |
29 | 28 | eqeq1d 2739 |
. . . 4
โข (๐ด โ โ โ
((expโ(i ยท ๐ด))
= 1 โ ((expโ(i ยท (โโ๐ด))) ยท
(expโ-(โโ๐ด))) = 1)) |
30 | | efcl 15972 |
. . . . . . . . 9
โข ((i
ยท (โโ๐ด))
โ โ โ (expโ(i ยท (โโ๐ด))) โ โ) |
31 | 23, 30 | syl 17 |
. . . . . . . 8
โข (๐ด โ โ โ
(expโ(i ยท (โโ๐ด))) โ โ) |
32 | | efcl 15972 |
. . . . . . . . 9
โข
(-(โโ๐ด)
โ โ โ (expโ-(โโ๐ด)) โ โ) |
33 | 25, 32 | syl 17 |
. . . . . . . 8
โข (๐ด โ โ โ
(expโ-(โโ๐ด)) โ โ) |
34 | 31, 33 | absmuld 15346 |
. . . . . . 7
โข (๐ด โ โ โ
(absโ((expโ(i ยท (โโ๐ด))) ยท
(expโ-(โโ๐ด)))) = ((absโ(expโ(i ยท
(โโ๐ด))))
ยท (absโ(expโ-(โโ๐ด))))) |
35 | | absefi 16085 |
. . . . . . . . 9
โข
((โโ๐ด)
โ โ โ (absโ(expโ(i ยท (โโ๐ด)))) = 1) |
36 | 4, 35 | syl 17 |
. . . . . . . 8
โข (๐ด โ โ โ
(absโ(expโ(i ยท (โโ๐ด)))) = 1) |
37 | 24 | reefcld 15977 |
. . . . . . . . 9
โข (๐ด โ โ โ
(expโ-(โโ๐ด)) โ โ) |
38 | | efgt0 15992 |
. . . . . . . . . . 11
โข
(-(โโ๐ด)
โ โ โ 0 < (expโ-(โโ๐ด))) |
39 | 24, 38 | syl 17 |
. . . . . . . . . 10
โข (๐ด โ โ โ 0 <
(expโ-(โโ๐ด))) |
40 | | 0re 11164 |
. . . . . . . . . . 11
โข 0 โ
โ |
41 | | ltle 11250 |
. . . . . . . . . . 11
โข ((0
โ โ โง (expโ-(โโ๐ด)) โ โ) โ (0 <
(expโ-(โโ๐ด)) โ 0 โค
(expโ-(โโ๐ด)))) |
42 | 40, 41 | mpan 689 |
. . . . . . . . . 10
โข
((expโ-(โโ๐ด)) โ โ โ (0 <
(expโ-(โโ๐ด)) โ 0 โค
(expโ-(โโ๐ด)))) |
43 | 37, 39, 42 | sylc 65 |
. . . . . . . . 9
โข (๐ด โ โ โ 0 โค
(expโ-(โโ๐ด))) |
44 | 37, 43 | absidd 15314 |
. . . . . . . 8
โข (๐ด โ โ โ
(absโ(expโ-(โโ๐ด))) = (expโ-(โโ๐ด))) |
45 | 36, 44 | oveq12d 7380 |
. . . . . . 7
โข (๐ด โ โ โ
((absโ(expโ(i ยท (โโ๐ด)))) ยท
(absโ(expโ-(โโ๐ด)))) = (1 ยท
(expโ-(โโ๐ด)))) |
46 | 33 | mulid2d 11180 |
. . . . . . 7
โข (๐ด โ โ โ (1
ยท (expโ-(โโ๐ด))) = (expโ-(โโ๐ด))) |
47 | 34, 45, 46 | 3eqtrrd 2782 |
. . . . . 6
โข (๐ด โ โ โ
(expโ-(โโ๐ด)) = (absโ((expโ(i ยท
(โโ๐ด))) ยท
(expโ-(โโ๐ด))))) |
48 | | fveq2 6847 |
. . . . . 6
โข
(((expโ(i ยท (โโ๐ด))) ยท
(expโ-(โโ๐ด))) = 1 โ (absโ((expโ(i
ยท (โโ๐ด)))
ยท (expโ-(โโ๐ด)))) = (absโ1)) |
49 | 47, 48 | sylan9eq 2797 |
. . . . 5
โข ((๐ด โ โ โง
((expโ(i ยท (โโ๐ด))) ยท
(expโ-(โโ๐ด))) = 1) โ
(expโ-(โโ๐ด)) = (absโ1)) |
50 | 49 | ex 414 |
. . . 4
โข (๐ด โ โ โ
(((expโ(i ยท (โโ๐ด))) ยท
(expโ-(โโ๐ด))) = 1 โ
(expโ-(โโ๐ด)) = (absโ1))) |
51 | 29, 50 | sylbid 239 |
. . 3
โข (๐ด โ โ โ
((expโ(i ยท ๐ด))
= 1 โ (expโ-(โโ๐ด)) = (absโ1))) |
52 | 7 | negeq0d 11511 |
. . . 4
โข (๐ด โ โ โ
((โโ๐ด) = 0
โ -(โโ๐ด) =
0)) |
53 | | reim0b 15011 |
. . . 4
โข (๐ด โ โ โ (๐ด โ โ โ
(โโ๐ด) =
0)) |
54 | | ef0 15980 |
. . . . . . 7
โข
(expโ0) = 1 |
55 | | abs1 15189 |
. . . . . . 7
โข
(absโ1) = 1 |
56 | 54, 55 | eqtr4i 2768 |
. . . . . 6
โข
(expโ0) = (absโ1) |
57 | 56 | eqeq2i 2750 |
. . . . 5
โข
((expโ-(โโ๐ด)) = (expโ0) โ
(expโ-(โโ๐ด)) = (absโ1)) |
58 | | reef11 16008 |
. . . . . 6
โข
((-(โโ๐ด)
โ โ โง 0 โ โ) โ ((expโ-(โโ๐ด)) = (expโ0) โ
-(โโ๐ด) =
0)) |
59 | 24, 40, 58 | sylancl 587 |
. . . . 5
โข (๐ด โ โ โ
((expโ-(โโ๐ด)) = (expโ0) โ
-(โโ๐ด) =
0)) |
60 | 57, 59 | bitr3id 285 |
. . . 4
โข (๐ด โ โ โ
((expโ-(โโ๐ด)) = (absโ1) โ
-(โโ๐ด) =
0)) |
61 | 52, 53, 60 | 3bitr4rd 312 |
. . 3
โข (๐ด โ โ โ
((expโ-(โโ๐ด)) = (absโ1) โ ๐ด โ โ)) |
62 | 51, 61 | sylibd 238 |
. 2
โข (๐ด โ โ โ
((expโ(i ยท ๐ด))
= 1 โ ๐ด โ
โ)) |
63 | 62 | imp 408 |
1
โข ((๐ด โ โ โง
(expโ(i ยท ๐ด))
= 1) โ ๐ด โ
โ) |