Step | Hyp | Ref
| Expression |
1 | | cjsub 15043 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ(๐ด โ
๐ต)) =
((โโ๐ด) โ
(โโ๐ต))) |
2 | 1 | oveq2d 7377 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด โ ๐ต) ยท (โโ(๐ด โ ๐ต))) = ((๐ด โ ๐ต) ยท ((โโ๐ด) โ (โโ๐ต)))) |
3 | | cjcl 14999 |
. . . . 5
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
4 | | cjcl 14999 |
. . . . 5
โข (๐ต โ โ โ
(โโ๐ต) โ
โ) |
5 | 3, 4 | anim12i 614 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ
((โโ๐ด) โ
โ โง (โโ๐ต) โ โ)) |
6 | | mulsub 11606 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง
((โโ๐ด) โ
โ โง (โโ๐ต) โ โ)) โ ((๐ด โ ๐ต) ยท ((โโ๐ด) โ (โโ๐ต))) = (((๐ด ยท (โโ๐ด)) + ((โโ๐ต) ยท ๐ต)) โ ((๐ด ยท (โโ๐ต)) + ((โโ๐ด) ยท ๐ต)))) |
7 | 5, 6 | mpdan 686 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด โ ๐ต) ยท ((โโ๐ด) โ (โโ๐ต))) = (((๐ด ยท (โโ๐ด)) + ((โโ๐ต) ยท ๐ต)) โ ((๐ด ยท (โโ๐ต)) + ((โโ๐ด) ยท ๐ต)))) |
8 | 2, 7 | eqtrd 2773 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด โ ๐ต) ยท (โโ(๐ด โ ๐ต))) = (((๐ด ยท (โโ๐ด)) + ((โโ๐ต) ยท ๐ต)) โ ((๐ด ยท (โโ๐ต)) + ((โโ๐ด) ยท ๐ต)))) |
9 | | subcl 11408 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด โ ๐ต) โ โ) |
10 | | absvalsq 15174 |
. . 3
โข ((๐ด โ ๐ต) โ โ โ ((absโ(๐ด โ ๐ต))โ2) = ((๐ด โ ๐ต) ยท (โโ(๐ด โ ๐ต)))) |
11 | 9, 10 | syl 17 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ) โ
((absโ(๐ด โ
๐ต))โ2) = ((๐ด โ ๐ต) ยท (โโ(๐ด โ ๐ต)))) |
12 | | absvalsq 15174 |
. . . 4
โข (๐ด โ โ โ
((absโ๐ด)โ2) =
(๐ด ยท
(โโ๐ด))) |
13 | | absvalsq 15174 |
. . . . 5
โข (๐ต โ โ โ
((absโ๐ต)โ2) =
(๐ต ยท
(โโ๐ต))) |
14 | | mulcom 11145 |
. . . . . 6
โข ((๐ต โ โ โง
(โโ๐ต) โ
โ) โ (๐ต ยท
(โโ๐ต)) =
((โโ๐ต)
ยท ๐ต)) |
15 | 4, 14 | mpdan 686 |
. . . . 5
โข (๐ต โ โ โ (๐ต ยท (โโ๐ต)) = ((โโ๐ต) ยท ๐ต)) |
16 | 13, 15 | eqtrd 2773 |
. . . 4
โข (๐ต โ โ โ
((absโ๐ต)โ2) =
((โโ๐ต)
ยท ๐ต)) |
17 | 12, 16 | oveqan12d 7380 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ
(((absโ๐ด)โ2) +
((absโ๐ต)โ2)) =
((๐ด ยท
(โโ๐ด)) +
((โโ๐ต)
ยท ๐ต))) |
18 | | mulcl 11143 |
. . . . . 6
โข ((๐ด โ โ โง
(โโ๐ต) โ
โ) โ (๐ด ยท
(โโ๐ต)) โ
โ) |
19 | 4, 18 | sylan2 594 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด ยท (โโ๐ต)) โ
โ) |
20 | 19 | addcjd 15106 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด ยท (โโ๐ต)) + (โโ(๐ด ยท (โโ๐ต)))) = (2 ยท
(โโ(๐ด ยท
(โโ๐ต))))) |
21 | | cjmul 15036 |
. . . . . . 7
โข ((๐ด โ โ โง
(โโ๐ต) โ
โ) โ (โโ(๐ด ยท (โโ๐ต))) = ((โโ๐ด) ยท
(โโ(โโ๐ต)))) |
22 | 4, 21 | sylan2 594 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ(๐ด ยท
(โโ๐ต))) =
((โโ๐ด)
ยท (โโ(โโ๐ต)))) |
23 | | cjcj 15034 |
. . . . . . . 8
โข (๐ต โ โ โ
(โโ(โโ๐ต)) = ๐ต) |
24 | 23 | adantl 483 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ(โโ๐ต)) = ๐ต) |
25 | 24 | oveq2d 7377 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ
((โโ๐ด)
ยท (โโ(โโ๐ต))) = ((โโ๐ด) ยท ๐ต)) |
26 | 22, 25 | eqtrd 2773 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ(๐ด ยท
(โโ๐ต))) =
((โโ๐ด)
ยท ๐ต)) |
27 | 26 | oveq2d 7377 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด ยท (โโ๐ต)) + (โโ(๐ด ยท (โโ๐ต)))) = ((๐ด ยท (โโ๐ต)) + ((โโ๐ด) ยท ๐ต))) |
28 | 20, 27 | eqtr3d 2775 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ (2
ยท (โโ(๐ด
ยท (โโ๐ต)))) = ((๐ด ยท (โโ๐ต)) + ((โโ๐ด) ยท ๐ต))) |
29 | 17, 28 | oveq12d 7379 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ) โ
((((absโ๐ด)โ2) +
((absโ๐ต)โ2))
โ (2 ยท (โโ(๐ด ยท (โโ๐ต))))) = (((๐ด ยท (โโ๐ด)) + ((โโ๐ต) ยท ๐ต)) โ ((๐ด ยท (โโ๐ต)) + ((โโ๐ด) ยท ๐ต)))) |
30 | 8, 11, 29 | 3eqtr4d 2783 |
1
โข ((๐ด โ โ โง ๐ต โ โ) โ
((absโ(๐ด โ
๐ต))โ2) =
((((absโ๐ด)โ2) +
((absโ๐ต)โ2))
โ (2 ยท (โโ(๐ด ยท (โโ๐ต)))))) |