Step | Hyp | Ref
| Expression |
1 | | cjmul 15028 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ(๐ด ยท
๐ต)) =
((โโ๐ด)
ยท (โโ๐ต))) |
2 | 1 | oveq2d 7374 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด ยท ๐ต) ยท (โโ(๐ด ยท ๐ต))) = ((๐ด ยท ๐ต) ยท ((โโ๐ด) ยท (โโ๐ต)))) |
3 | | simpl 484 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ ๐ด โ
โ) |
4 | | simpr 486 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ ๐ต โ
โ) |
5 | 3 | cjcld 15082 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ๐ด) โ
โ) |
6 | 4 | cjcld 15082 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ๐ต) โ
โ) |
7 | 3, 4, 5, 6 | mul4d 11368 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด ยท ๐ต) ยท ((โโ๐ด) ยท (โโ๐ต))) = ((๐ด ยท (โโ๐ด)) ยท (๐ต ยท (โโ๐ต)))) |
8 | 2, 7 | eqtrd 2777 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด ยท ๐ต) ยท (โโ(๐ด ยท ๐ต))) = ((๐ด ยท (โโ๐ด)) ยท (๐ต ยท (โโ๐ต)))) |
9 | 8 | fveq2d 6847 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ((๐ด ยท
๐ต) ยท
(โโ(๐ด ยท
๐ต)))) =
(โโ((๐ด ยท
(โโ๐ด))
ยท (๐ต ยท
(โโ๐ต))))) |
10 | | cjmulrcl 15030 |
. . . . 5
โข (๐ด โ โ โ (๐ด ยท (โโ๐ด)) โ
โ) |
11 | | cjmulge0 15032 |
. . . . 5
โข (๐ด โ โ โ 0 โค
(๐ด ยท
(โโ๐ด))) |
12 | 10, 11 | jca 513 |
. . . 4
โข (๐ด โ โ โ ((๐ด ยท (โโ๐ด)) โ โ โง 0 โค
(๐ด ยท
(โโ๐ด)))) |
13 | | cjmulrcl 15030 |
. . . . 5
โข (๐ต โ โ โ (๐ต ยท (โโ๐ต)) โ
โ) |
14 | | cjmulge0 15032 |
. . . . 5
โข (๐ต โ โ โ 0 โค
(๐ต ยท
(โโ๐ต))) |
15 | 13, 14 | jca 513 |
. . . 4
โข (๐ต โ โ โ ((๐ต ยท (โโ๐ต)) โ โ โง 0 โค
(๐ต ยท
(โโ๐ต)))) |
16 | | sqrtmul 15145 |
. . . 4
โข ((((๐ด ยท (โโ๐ด)) โ โ โง 0 โค
(๐ด ยท
(โโ๐ด))) โง
((๐ต ยท
(โโ๐ต)) โ
โ โง 0 โค (๐ต
ยท (โโ๐ต)))) โ (โโ((๐ด ยท (โโ๐ด)) ยท (๐ต ยท (โโ๐ต)))) = ((โโ(๐ด ยท (โโ๐ด))) ยท (โโ(๐ต ยท (โโ๐ต))))) |
17 | 12, 15, 16 | syl2an 597 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ((๐ด ยท
(โโ๐ด))
ยท (๐ต ยท
(โโ๐ต)))) =
((โโ(๐ด ยท
(โโ๐ด)))
ยท (โโ(๐ต
ยท (โโ๐ต))))) |
18 | 9, 17 | eqtrd 2777 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ((๐ด ยท
๐ต) ยท
(โโ(๐ด ยท
๐ต)))) =
((โโ(๐ด ยท
(โโ๐ด)))
ยท (โโ(๐ต
ยท (โโ๐ต))))) |
19 | | mulcl 11136 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด ยท ๐ต) โ โ) |
20 | | absval 15124 |
. . 3
โข ((๐ด ยท ๐ต) โ โ โ (absโ(๐ด ยท ๐ต)) = (โโ((๐ด ยท ๐ต) ยท (โโ(๐ด ยท ๐ต))))) |
21 | 19, 20 | syl 17 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ) โ
(absโ(๐ด ยท
๐ต)) =
(โโ((๐ด ยท
๐ต) ยท
(โโ(๐ด ยท
๐ต))))) |
22 | | absval 15124 |
. . 3
โข (๐ด โ โ โ
(absโ๐ด) =
(โโ(๐ด ยท
(โโ๐ด)))) |
23 | | absval 15124 |
. . 3
โข (๐ต โ โ โ
(absโ๐ต) =
(โโ(๐ต ยท
(โโ๐ต)))) |
24 | 22, 23 | oveqan12d 7377 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ) โ
((absโ๐ด) ยท
(absโ๐ต)) =
((โโ(๐ด ยท
(โโ๐ด)))
ยท (โโ(๐ต
ยท (โโ๐ต))))) |
25 | 18, 21, 24 | 3eqtr4d 2787 |
1
โข ((๐ด โ โ โง ๐ต โ โ) โ
(absโ(๐ด ยท
๐ต)) = ((absโ๐ด) ยท (absโ๐ต))) |