Step | Hyp | Ref
| Expression |
1 | | ax-icn 11117 |
. . . . 5
โข i โ
โ |
2 | | mulcl 11142 |
. . . . 5
โข ((i
โ โ โง ๐ด
โ โ) โ (i ยท ๐ด) โ โ) |
3 | 1, 2 | mpan 689 |
. . . 4
โข (๐ด โ โ โ (i
ยท ๐ด) โ
โ) |
4 | | ax-1cn 11116 |
. . . . . 6
โข 1 โ
โ |
5 | | sqcl 14030 |
. . . . . 6
โข (๐ด โ โ โ (๐ดโ2) โ
โ) |
6 | | subcl 11407 |
. . . . . 6
โข ((1
โ โ โง (๐ดโ2) โ โ) โ (1 โ
(๐ดโ2)) โ
โ) |
7 | 4, 5, 6 | sylancr 588 |
. . . . 5
โข (๐ด โ โ โ (1
โ (๐ดโ2)) โ
โ) |
8 | 7 | sqrtcld 15329 |
. . . 4
โข (๐ด โ โ โ
(โโ(1 โ (๐ดโ2))) โ โ) |
9 | 3, 8 | addcomd 11364 |
. . 3
โข (๐ด โ โ โ ((i
ยท ๐ด) +
(โโ(1 โ (๐ดโ2)))) = ((โโ(1 โ
(๐ดโ2))) + (i ยท
๐ด))) |
10 | | mulneg2 11599 |
. . . . . 6
โข ((i
โ โ โง ๐ด
โ โ) โ (i ยท -๐ด) = -(i ยท ๐ด)) |
11 | 1, 10 | mpan 689 |
. . . . 5
โข (๐ด โ โ โ (i
ยท -๐ด) = -(i ยท
๐ด)) |
12 | | sqneg 14028 |
. . . . . . 7
โข (๐ด โ โ โ (-๐ดโ2) = (๐ดโ2)) |
13 | 12 | oveq2d 7378 |
. . . . . 6
โข (๐ด โ โ โ (1
โ (-๐ดโ2)) = (1
โ (๐ดโ2))) |
14 | 13 | fveq2d 6851 |
. . . . 5
โข (๐ด โ โ โ
(โโ(1 โ (-๐ดโ2))) = (โโ(1 โ
(๐ดโ2)))) |
15 | 11, 14 | oveq12d 7380 |
. . . 4
โข (๐ด โ โ โ ((i
ยท -๐ด) +
(โโ(1 โ (-๐ดโ2)))) = (-(i ยท ๐ด) + (โโ(1 โ
(๐ดโ2))))) |
16 | 3 | negcld 11506 |
. . . . 5
โข (๐ด โ โ โ -(i
ยท ๐ด) โ
โ) |
17 | 16, 8 | addcomd 11364 |
. . . 4
โข (๐ด โ โ โ (-(i
ยท ๐ด) +
(โโ(1 โ (๐ดโ2)))) = ((โโ(1 โ
(๐ดโ2))) + -(i ยท
๐ด))) |
18 | 8, 3 | negsubd 11525 |
. . . 4
โข (๐ด โ โ โ
((โโ(1 โ (๐ดโ2))) + -(i ยท ๐ด)) = ((โโ(1 โ (๐ดโ2))) โ (i ยท
๐ด))) |
19 | 15, 17, 18 | 3eqtrd 2781 |
. . 3
โข (๐ด โ โ โ ((i
ยท -๐ด) +
(โโ(1 โ (-๐ดโ2)))) = ((โโ(1 โ
(๐ดโ2))) โ (i
ยท ๐ด))) |
20 | 9, 19 | oveq12d 7380 |
. 2
โข (๐ด โ โ โ (((i
ยท ๐ด) +
(โโ(1 โ (๐ดโ2)))) ยท ((i ยท -๐ด) + (โโ(1 โ
(-๐ดโ2))))) =
(((โโ(1 โ (๐ดโ2))) + (i ยท ๐ด)) ยท ((โโ(1 โ
(๐ดโ2))) โ (i
ยท ๐ด)))) |
21 | 7 | sqsqrtd 15331 |
. . . 4
โข (๐ด โ โ โ
((โโ(1 โ (๐ดโ2)))โ2) = (1 โ (๐ดโ2))) |
22 | | sqmul 14031 |
. . . . . 6
โข ((i
โ โ โง ๐ด
โ โ) โ ((i ยท ๐ด)โ2) = ((iโ2) ยท (๐ดโ2))) |
23 | 1, 22 | mpan 689 |
. . . . 5
โข (๐ด โ โ โ ((i
ยท ๐ด)โ2) =
((iโ2) ยท (๐ดโ2))) |
24 | | i2 14113 |
. . . . . . 7
โข
(iโ2) = -1 |
25 | 24 | oveq1i 7372 |
. . . . . 6
โข
((iโ2) ยท (๐ดโ2)) = (-1 ยท (๐ดโ2)) |
26 | 5 | mulm1d 11614 |
. . . . . 6
โข (๐ด โ โ โ (-1
ยท (๐ดโ2)) =
-(๐ดโ2)) |
27 | 25, 26 | eqtrid 2789 |
. . . . 5
โข (๐ด โ โ โ
((iโ2) ยท (๐ดโ2)) = -(๐ดโ2)) |
28 | 23, 27 | eqtrd 2777 |
. . . 4
โข (๐ด โ โ โ ((i
ยท ๐ด)โ2) =
-(๐ดโ2)) |
29 | 21, 28 | oveq12d 7380 |
. . 3
โข (๐ด โ โ โ
(((โโ(1 โ (๐ดโ2)))โ2) โ ((i ยท
๐ด)โ2)) = ((1 โ
(๐ดโ2)) โ -(๐ดโ2))) |
30 | | subsq 14121 |
. . . 4
โข
(((โโ(1 โ (๐ดโ2))) โ โ โง (i ยท
๐ด) โ โ) โ
(((โโ(1 โ (๐ดโ2)))โ2) โ ((i ยท
๐ด)โ2)) =
(((โโ(1 โ (๐ดโ2))) + (i ยท ๐ด)) ยท ((โโ(1 โ
(๐ดโ2))) โ (i
ยท ๐ด)))) |
31 | 8, 3, 30 | syl2anc 585 |
. . 3
โข (๐ด โ โ โ
(((โโ(1 โ (๐ดโ2)))โ2) โ ((i ยท
๐ด)โ2)) =
(((โโ(1 โ (๐ดโ2))) + (i ยท ๐ด)) ยท ((โโ(1 โ
(๐ดโ2))) โ (i
ยท ๐ด)))) |
32 | 7, 5 | subnegd 11526 |
. . 3
โข (๐ด โ โ โ ((1
โ (๐ดโ2)) โ
-(๐ดโ2)) = ((1 โ
(๐ดโ2)) + (๐ดโ2))) |
33 | 29, 31, 32 | 3eqtr3d 2785 |
. 2
โข (๐ด โ โ โ
(((โโ(1 โ (๐ดโ2))) + (i ยท ๐ด)) ยท ((โโ(1 โ
(๐ดโ2))) โ (i
ยท ๐ด))) = ((1 โ
(๐ดโ2)) + (๐ดโ2))) |
34 | | npcan 11417 |
. . 3
โข ((1
โ โ โง (๐ดโ2) โ โ) โ ((1 โ
(๐ดโ2)) + (๐ดโ2)) = 1) |
35 | 4, 5, 34 | sylancr 588 |
. 2
โข (๐ด โ โ โ ((1
โ (๐ดโ2)) +
(๐ดโ2)) =
1) |
36 | 20, 33, 35 | 3eqtrd 2781 |
1
โข (๐ด โ โ โ (((i
ยท ๐ด) +
(โโ(1 โ (๐ดโ2)))) ยท ((i ยท -๐ด) + (โโ(1 โ
(-๐ดโ2))))) =
1) |