Step | Hyp | Ref
| Expression |
1 | | recl 15002 |
. . . . . 6
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
2 | 1 | recnd 11190 |
. . . . 5
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
3 | | ax-icn 11117 |
. . . . . 6
โข i โ
โ |
4 | | imcl 15003 |
. . . . . . 7
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
5 | 4 | recnd 11190 |
. . . . . 6
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
6 | | mulcl 11142 |
. . . . . 6
โข ((i
โ โ โง (โโ๐ด) โ โ) โ (i ยท
(โโ๐ด)) โ
โ) |
7 | 3, 5, 6 | sylancr 588 |
. . . . 5
โข (๐ด โ โ โ (i
ยท (โโ๐ด))
โ โ) |
8 | 2, 7 | negsubd 11525 |
. . . 4
โข (๐ด โ โ โ
((โโ๐ด) + -(i
ยท (โโ๐ด))) = ((โโ๐ด) โ (i ยท (โโ๐ด)))) |
9 | | mulneg2 11599 |
. . . . . 6
โข ((i
โ โ โง (โโ๐ด) โ โ) โ (i ยท
-(โโ๐ด)) = -(i
ยท (โโ๐ด))) |
10 | 3, 5, 9 | sylancr 588 |
. . . . 5
โข (๐ด โ โ โ (i
ยท -(โโ๐ด)) = -(i ยท (โโ๐ด))) |
11 | 10 | oveq2d 7378 |
. . . 4
โข (๐ด โ โ โ
((โโ๐ด) + (i
ยท -(โโ๐ด))) = ((โโ๐ด) + -(i ยท (โโ๐ด)))) |
12 | | remim 15009 |
. . . 4
โข (๐ด โ โ โ
(โโ๐ด) =
((โโ๐ด) โ
(i ยท (โโ๐ด)))) |
13 | 8, 11, 12 | 3eqtr4rd 2788 |
. . 3
โข (๐ด โ โ โ
(โโ๐ด) =
((โโ๐ด) + (i
ยท -(โโ๐ด)))) |
14 | | replim 15008 |
. . 3
โข (๐ด โ โ โ ๐ด = ((โโ๐ด) + (i ยท
(โโ๐ด)))) |
15 | 13, 14 | eqeq12d 2753 |
. 2
โข (๐ด โ โ โ
((โโ๐ด) = ๐ด โ ((โโ๐ด) + (i ยท
-(โโ๐ด))) =
((โโ๐ด) + (i
ยท (โโ๐ด))))) |
16 | 5 | negcld 11506 |
. . . 4
โข (๐ด โ โ โ
-(โโ๐ด) โ
โ) |
17 | | mulcl 11142 |
. . . 4
โข ((i
โ โ โง -(โโ๐ด) โ โ) โ (i ยท
-(โโ๐ด)) โ
โ) |
18 | 3, 16, 17 | sylancr 588 |
. . 3
โข (๐ด โ โ โ (i
ยท -(โโ๐ด)) โ โ) |
19 | 2, 18, 7 | addcand 11365 |
. 2
โข (๐ด โ โ โ
(((โโ๐ด) + (i
ยท -(โโ๐ด))) = ((โโ๐ด) + (i ยท (โโ๐ด))) โ (i ยท
-(โโ๐ด)) = (i
ยท (โโ๐ด)))) |
20 | | eqcom 2744 |
. . . 4
โข
(-(โโ๐ด)
= (โโ๐ด) โ
(โโ๐ด) =
-(โโ๐ด)) |
21 | 5 | eqnegd 11883 |
. . . 4
โข (๐ด โ โ โ
((โโ๐ด) =
-(โโ๐ด) โ
(โโ๐ด) =
0)) |
22 | 20, 21 | bitrid 283 |
. . 3
โข (๐ด โ โ โ
(-(โโ๐ด) =
(โโ๐ด) โ
(โโ๐ด) =
0)) |
23 | | ine0 11597 |
. . . . . 6
โข i โ
0 |
24 | 3, 23 | pm3.2i 472 |
. . . . 5
โข (i โ
โ โง i โ 0) |
25 | 24 | a1i 11 |
. . . 4
โข (๐ด โ โ โ (i โ
โ โง i โ 0)) |
26 | | mulcan 11799 |
. . . 4
โข
((-(โโ๐ด)
โ โ โง (โโ๐ด) โ โ โง (i โ โ
โง i โ 0)) โ ((i ยท -(โโ๐ด)) = (i ยท (โโ๐ด)) โ -(โโ๐ด) = (โโ๐ด))) |
27 | 16, 5, 25, 26 | syl3anc 1372 |
. . 3
โข (๐ด โ โ โ ((i
ยท -(โโ๐ด)) = (i ยท (โโ๐ด)) โ -(โโ๐ด) = (โโ๐ด))) |
28 | | reim0b 15011 |
. . 3
โข (๐ด โ โ โ (๐ด โ โ โ
(โโ๐ด) =
0)) |
29 | 22, 27, 28 | 3bitr4d 311 |
. 2
โข (๐ด โ โ โ ((i
ยท -(โโ๐ด)) = (i ยท (โโ๐ด)) โ ๐ด โ โ)) |
30 | 15, 19, 29 | 3bitrrd 306 |
1
โข (๐ด โ โ โ (๐ด โ โ โ
(โโ๐ด) = ๐ด)) |