Step | Hyp | Ref
| Expression |
1 | | cjcl 14915 |
. . 3
โข (๐ต โ โ โ
(โโ๐ต) โ
โ) |
2 | | remul 14939 |
. . 3
โข ((๐ด โ โ โง
(โโ๐ต) โ
โ) โ (โโ(๐ด ยท (โโ๐ต))) = (((โโ๐ด) ยท
(โโ(โโ๐ต))) โ ((โโ๐ด) ยท
(โโ(โโ๐ต))))) |
3 | 1, 2 | sylan2 593 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ(๐ด ยท
(โโ๐ต))) =
(((โโ๐ด) ยท
(โโ(โโ๐ต))) โ ((โโ๐ด) ยท
(โโ(โโ๐ต))))) |
4 | | recj 14934 |
. . . . 5
โข (๐ต โ โ โ
(โโ(โโ๐ต)) = (โโ๐ต)) |
5 | 4 | adantl 482 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ(โโ๐ต)) = (โโ๐ต)) |
6 | 5 | oveq2d 7353 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ
((โโ๐ด) ยท
(โโ(โโ๐ต))) = ((โโ๐ด) ยท (โโ๐ต))) |
7 | | imcj 14942 |
. . . . . 6
โข (๐ต โ โ โ
(โโ(โโ๐ต)) = -(โโ๐ต)) |
8 | 7 | adantl 482 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ(โโ๐ต)) = -(โโ๐ต)) |
9 | 8 | oveq2d 7353 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ
((โโ๐ด) ยท
(โโ(โโ๐ต))) = ((โโ๐ด) ยท -(โโ๐ต))) |
10 | | imcl 14921 |
. . . . . 6
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
11 | 10 | recnd 11104 |
. . . . 5
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
12 | | imcl 14921 |
. . . . . 6
โข (๐ต โ โ โ
(โโ๐ต) โ
โ) |
13 | 12 | recnd 11104 |
. . . . 5
โข (๐ต โ โ โ
(โโ๐ต) โ
โ) |
14 | | mulneg2 11513 |
. . . . 5
โข
(((โโ๐ด)
โ โ โง (โโ๐ต) โ โ) โ
((โโ๐ด) ยท
-(โโ๐ต)) =
-((โโ๐ด)
ยท (โโ๐ต))) |
15 | 11, 13, 14 | syl2an 596 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ
((โโ๐ด) ยท
-(โโ๐ต)) =
-((โโ๐ด)
ยท (โโ๐ต))) |
16 | 9, 15 | eqtrd 2776 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ
((โโ๐ด) ยท
(โโ(โโ๐ต))) = -((โโ๐ด) ยท (โโ๐ต))) |
17 | 6, 16 | oveq12d 7355 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ) โ
(((โโ๐ด) ยท
(โโ(โโ๐ต))) โ ((โโ๐ด) ยท
(โโ(โโ๐ต)))) = (((โโ๐ด) ยท (โโ๐ต)) โ -((โโ๐ด) ยท (โโ๐ต)))) |
18 | | recl 14920 |
. . . . 5
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
19 | 18 | recnd 11104 |
. . . 4
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
20 | | recl 14920 |
. . . . 5
โข (๐ต โ โ โ
(โโ๐ต) โ
โ) |
21 | 20 | recnd 11104 |
. . . 4
โข (๐ต โ โ โ
(โโ๐ต) โ
โ) |
22 | | mulcl 11056 |
. . . 4
โข
(((โโ๐ด)
โ โ โง (โโ๐ต) โ โ) โ
((โโ๐ด) ยท
(โโ๐ต)) โ
โ) |
23 | 19, 21, 22 | syl2an 596 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ
((โโ๐ด) ยท
(โโ๐ต)) โ
โ) |
24 | | mulcl 11056 |
. . . 4
โข
(((โโ๐ด)
โ โ โง (โโ๐ต) โ โ) โ
((โโ๐ด) ยท
(โโ๐ต)) โ
โ) |
25 | 11, 13, 24 | syl2an 596 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ
((โโ๐ด) ยท
(โโ๐ต)) โ
โ) |
26 | 23, 25 | subnegd 11440 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ) โ
(((โโ๐ด) ยท
(โโ๐ต)) โ
-((โโ๐ด)
ยท (โโ๐ต))) = (((โโ๐ด) ยท (โโ๐ต)) + ((โโ๐ด) ยท (โโ๐ต)))) |
27 | 3, 17, 26 | 3eqtrd 2780 |
1
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ(๐ด ยท
(โโ๐ต))) =
(((โโ๐ด) ยท
(โโ๐ต)) +
((โโ๐ด) ยท
(โโ๐ต)))) |