Step | Hyp | Ref
| Expression |
1 | | ax-icn 11117 |
. . . 4
โข i โ
โ |
2 | | mulcl 11142 |
. . . 4
โข ((i
โ โ โง ๐ด
โ โ) โ (i ยท ๐ด) โ โ) |
3 | 1, 2 | mpan 689 |
. . 3
โข (๐ด โ โ โ (i
ยท ๐ด) โ
โ) |
4 | | ax-1cn 11116 |
. . . . 5
โข 1 โ
โ |
5 | | sqcl 14030 |
. . . . 5
โข (๐ด โ โ โ (๐ดโ2) โ
โ) |
6 | | subcl 11407 |
. . . . 5
โข ((1
โ โ โง (๐ดโ2) โ โ) โ (1 โ
(๐ดโ2)) โ
โ) |
7 | 4, 5, 6 | sylancr 588 |
. . . 4
โข (๐ด โ โ โ (1
โ (๐ดโ2)) โ
โ) |
8 | 7 | sqrtcld 15329 |
. . 3
โข (๐ด โ โ โ
(โโ(1 โ (๐ดโ2))) โ โ) |
9 | 3, 8 | subnegd 11526 |
. 2
โข (๐ด โ โ โ ((i
ยท ๐ด) โ
-(โโ(1 โ (๐ดโ2)))) = ((i ยท ๐ด) + (โโ(1 โ (๐ดโ2))))) |
10 | 8 | negcld 11506 |
. . 3
โข (๐ด โ โ โ
-(โโ(1 โ (๐ดโ2))) โ โ) |
11 | | 0ne1 12231 |
. . . . . 6
โข 0 โ
1 |
12 | | 0cnd 11155 |
. . . . . . 7
โข (๐ด โ โ โ 0 โ
โ) |
13 | | 1cnd 11157 |
. . . . . . 7
โข (๐ด โ โ โ 1 โ
โ) |
14 | | subcan2 11433 |
. . . . . . . 8
โข ((0
โ โ โง 1 โ โ โง (๐ดโ2) โ โ) โ ((0 โ
(๐ดโ2)) = (1 โ
(๐ดโ2)) โ 0 =
1)) |
15 | 14 | necon3bid 2989 |
. . . . . . 7
โข ((0
โ โ โง 1 โ โ โง (๐ดโ2) โ โ) โ ((0 โ
(๐ดโ2)) โ (1 โ
(๐ดโ2)) โ 0 โ
1)) |
16 | 12, 13, 5, 15 | syl3anc 1372 |
. . . . . 6
โข (๐ด โ โ โ ((0
โ (๐ดโ2)) โ (1
โ (๐ดโ2)) โ
0 โ 1)) |
17 | 11, 16 | mpbiri 258 |
. . . . 5
โข (๐ด โ โ โ (0
โ (๐ดโ2)) โ (1
โ (๐ดโ2))) |
18 | | sqmul 14031 |
. . . . . . . 8
โข ((i
โ โ โง ๐ด
โ โ) โ ((i ยท ๐ด)โ2) = ((iโ2) ยท (๐ดโ2))) |
19 | 1, 18 | mpan 689 |
. . . . . . 7
โข (๐ด โ โ โ ((i
ยท ๐ด)โ2) =
((iโ2) ยท (๐ดโ2))) |
20 | | i2 14113 |
. . . . . . . . 9
โข
(iโ2) = -1 |
21 | 20 | oveq1i 7372 |
. . . . . . . 8
โข
((iโ2) ยท (๐ดโ2)) = (-1 ยท (๐ดโ2)) |
22 | 5 | mulm1d 11614 |
. . . . . . . 8
โข (๐ด โ โ โ (-1
ยท (๐ดโ2)) =
-(๐ดโ2)) |
23 | 21, 22 | eqtrid 2789 |
. . . . . . 7
โข (๐ด โ โ โ
((iโ2) ยท (๐ดโ2)) = -(๐ดโ2)) |
24 | 19, 23 | eqtrd 2777 |
. . . . . 6
โข (๐ด โ โ โ ((i
ยท ๐ด)โ2) =
-(๐ดโ2)) |
25 | | df-neg 11395 |
. . . . . 6
โข -(๐ดโ2) = (0 โ (๐ดโ2)) |
26 | 24, 25 | eqtrdi 2793 |
. . . . 5
โข (๐ด โ โ โ ((i
ยท ๐ด)โ2) = (0
โ (๐ดโ2))) |
27 | | sqneg 14028 |
. . . . . . 7
โข
((โโ(1 โ (๐ดโ2))) โ โ โ
(-(โโ(1 โ (๐ดโ2)))โ2) = ((โโ(1
โ (๐ดโ2)))โ2)) |
28 | 8, 27 | syl 17 |
. . . . . 6
โข (๐ด โ โ โ
(-(โโ(1 โ (๐ดโ2)))โ2) = ((โโ(1
โ (๐ดโ2)))โ2)) |
29 | 7 | sqsqrtd 15331 |
. . . . . 6
โข (๐ด โ โ โ
((โโ(1 โ (๐ดโ2)))โ2) = (1 โ (๐ดโ2))) |
30 | 28, 29 | eqtrd 2777 |
. . . . 5
โข (๐ด โ โ โ
(-(โโ(1 โ (๐ดโ2)))โ2) = (1 โ (๐ดโ2))) |
31 | 17, 26, 30 | 3netr4d 3022 |
. . . 4
โข (๐ด โ โ โ ((i
ยท ๐ด)โ2) โ
(-(โโ(1 โ (๐ดโ2)))โ2)) |
32 | | oveq1 7369 |
. . . . 5
โข ((i
ยท ๐ด) =
-(โโ(1 โ (๐ดโ2))) โ ((i ยท ๐ด)โ2) = (-(โโ(1
โ (๐ดโ2)))โ2)) |
33 | 32 | necon3i 2977 |
. . . 4
โข (((i
ยท ๐ด)โ2) โ
(-(โโ(1 โ (๐ดโ2)))โ2) โ (i ยท ๐ด) โ -(โโ(1
โ (๐ดโ2)))) |
34 | 31, 33 | syl 17 |
. . 3
โข (๐ด โ โ โ (i
ยท ๐ด) โ
-(โโ(1 โ (๐ดโ2)))) |
35 | 3, 10, 34 | subne0d 11528 |
. 2
โข (๐ด โ โ โ ((i
ยท ๐ด) โ
-(โโ(1 โ (๐ดโ2)))) โ 0) |
36 | 9, 35 | eqnetrrd 3013 |
1
โข (๐ด โ โ โ ((i
ยท ๐ด) +
(โโ(1 โ (๐ดโ2)))) โ 0) |