Step | Hyp | Ref
| Expression |
1 | | recl 15057 |
. . . . . 6
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
2 | 1 | recnd 11242 |
. . . . 5
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
3 | | ax-icn 11169 |
. . . . . 6
โข i โ
โ |
4 | | imcl 15058 |
. . . . . . 7
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
5 | 4 | recnd 11242 |
. . . . . 6
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
6 | | mulcl 11194 |
. . . . . 6
โข ((i
โ โ โง (โโ๐ด) โ โ) โ (i ยท
(โโ๐ด)) โ
โ) |
7 | 3, 5, 6 | sylancr 588 |
. . . . 5
โข (๐ด โ โ โ (i
ยท (โโ๐ด))
โ โ) |
8 | 2, 7 | negsubd 11577 |
. . . 4
โข (๐ด โ โ โ
((โโ๐ด) + -(i
ยท (โโ๐ด))) = ((โโ๐ด) โ (i ยท (โโ๐ด)))) |
9 | | mulneg2 11651 |
. . . . . 6
โข ((i
โ โ โง (โโ๐ด) โ โ) โ (i ยท
-(โโ๐ด)) = -(i
ยท (โโ๐ด))) |
10 | 3, 5, 9 | sylancr 588 |
. . . . 5
โข (๐ด โ โ โ (i
ยท -(โโ๐ด)) = -(i ยท (โโ๐ด))) |
11 | 10 | oveq2d 7425 |
. . . 4
โข (๐ด โ โ โ
((โโ๐ด) + (i
ยท -(โโ๐ด))) = ((โโ๐ด) + -(i ยท (โโ๐ด)))) |
12 | | remim 15064 |
. . . 4
โข (๐ด โ โ โ
(โโ๐ด) =
((โโ๐ด) โ
(i ยท (โโ๐ด)))) |
13 | 8, 11, 12 | 3eqtr4rd 2784 |
. . 3
โข (๐ด โ โ โ
(โโ๐ด) =
((โโ๐ด) + (i
ยท -(โโ๐ด)))) |
14 | | replim 15063 |
. . 3
โข (๐ด โ โ โ ๐ด = ((โโ๐ด) + (i ยท
(โโ๐ด)))) |
15 | 13, 14 | eqeq12d 2749 |
. 2
โข (๐ด โ โ โ
((โโ๐ด) = ๐ด โ ((โโ๐ด) + (i ยท
-(โโ๐ด))) =
((โโ๐ด) + (i
ยท (โโ๐ด))))) |
16 | 5 | negcld 11558 |
. . . 4
โข (๐ด โ โ โ
-(โโ๐ด) โ
โ) |
17 | | mulcl 11194 |
. . . 4
โข ((i
โ โ โง -(โโ๐ด) โ โ) โ (i ยท
-(โโ๐ด)) โ
โ) |
18 | 3, 16, 17 | sylancr 588 |
. . 3
โข (๐ด โ โ โ (i
ยท -(โโ๐ด)) โ โ) |
19 | 2, 18, 7 | addcand 11417 |
. 2
โข (๐ด โ โ โ
(((โโ๐ด) + (i
ยท -(โโ๐ด))) = ((โโ๐ด) + (i ยท (โโ๐ด))) โ (i ยท
-(โโ๐ด)) = (i
ยท (โโ๐ด)))) |
20 | | eqcom 2740 |
. . . 4
โข
(-(โโ๐ด)
= (โโ๐ด) โ
(โโ๐ด) =
-(โโ๐ด)) |
21 | 5 | eqnegd 11935 |
. . . 4
โข (๐ด โ โ โ
((โโ๐ด) =
-(โโ๐ด) โ
(โโ๐ด) =
0)) |
22 | 20, 21 | bitrid 283 |
. . 3
โข (๐ด โ โ โ
(-(โโ๐ด) =
(โโ๐ด) โ
(โโ๐ด) =
0)) |
23 | | ine0 11649 |
. . . . . 6
โข i โ
0 |
24 | 3, 23 | pm3.2i 472 |
. . . . 5
โข (i โ
โ โง i โ 0) |
25 | 24 | a1i 11 |
. . . 4
โข (๐ด โ โ โ (i โ
โ โง i โ 0)) |
26 | | mulcan 11851 |
. . . 4
โข
((-(โโ๐ด)
โ โ โง (โโ๐ด) โ โ โง (i โ โ
โง i โ 0)) โ ((i ยท -(โโ๐ด)) = (i ยท (โโ๐ด)) โ -(โโ๐ด) = (โโ๐ด))) |
27 | 16, 5, 25, 26 | syl3anc 1372 |
. . 3
โข (๐ด โ โ โ ((i
ยท -(โโ๐ด)) = (i ยท (โโ๐ด)) โ -(โโ๐ด) = (โโ๐ด))) |
28 | | reim0b 15066 |
. . 3
โข (๐ด โ โ โ (๐ด โ โ โ
(โโ๐ด) =
0)) |
29 | 22, 27, 28 | 3bitr4d 311 |
. 2
โข (๐ด โ โ โ ((i
ยท -(โโ๐ด)) = (i ยท (โโ๐ด)) โ ๐ด โ โ)) |
30 | 15, 19, 29 | 3bitrrd 306 |
1
โข (๐ด โ โ โ (๐ด โ โ โ
(โโ๐ด) = ๐ด)) |