Step | Hyp | Ref
| Expression |
1 | | simpll 766 |
. . . 4
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ๐ด โ โ) |
2 | | simprl 770 |
. . . 4
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ๐ต โ โ) |
3 | 1, 2 | remulcld 11193 |
. . 3
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (๐ด ยท ๐ต) โ โ) |
4 | | mulge0 11681 |
. . 3
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ 0 โค (๐ด ยท ๐ต)) |
5 | | resqrtcl 15147 |
. . 3
โข (((๐ด ยท ๐ต) โ โ โง 0 โค (๐ด ยท ๐ต)) โ (โโ(๐ด ยท ๐ต)) โ โ) |
6 | 3, 4, 5 | syl2anc 585 |
. 2
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (โโ(๐ด ยท ๐ต)) โ โ) |
7 | | resqrtcl 15147 |
. . . 4
โข ((๐ด โ โ โง 0 โค
๐ด) โ
(โโ๐ด) โ
โ) |
8 | 7 | adantr 482 |
. . 3
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (โโ๐ด) โ
โ) |
9 | | resqrtcl 15147 |
. . . 4
โข ((๐ต โ โ โง 0 โค
๐ต) โ
(โโ๐ต) โ
โ) |
10 | 9 | adantl 483 |
. . 3
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (โโ๐ต) โ
โ) |
11 | 8, 10 | remulcld 11193 |
. 2
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((โโ๐ด) ยท (โโ๐ต)) โ
โ) |
12 | | sqrtge0 15151 |
. . 3
โข (((๐ด ยท ๐ต) โ โ โง 0 โค (๐ด ยท ๐ต)) โ 0 โค (โโ(๐ด ยท ๐ต))) |
13 | 3, 4, 12 | syl2anc 585 |
. 2
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ 0 โค
(โโ(๐ด ยท
๐ต))) |
14 | | sqrtge0 15151 |
. . . 4
โข ((๐ด โ โ โง 0 โค
๐ด) โ 0 โค
(โโ๐ด)) |
15 | 14 | adantr 482 |
. . 3
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ 0 โค
(โโ๐ด)) |
16 | | sqrtge0 15151 |
. . . 4
โข ((๐ต โ โ โง 0 โค
๐ต) โ 0 โค
(โโ๐ต)) |
17 | 16 | adantl 483 |
. . 3
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ 0 โค
(โโ๐ต)) |
18 | 8, 10, 15, 17 | mulge0d 11740 |
. 2
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ 0 โค
((โโ๐ด) ยท
(โโ๐ต))) |
19 | | resqrtth 15149 |
. . . 4
โข ((๐ด โ โ โง 0 โค
๐ด) โ
((โโ๐ด)โ2)
= ๐ด) |
20 | | resqrtth 15149 |
. . . 4
โข ((๐ต โ โ โง 0 โค
๐ต) โ
((โโ๐ต)โ2)
= ๐ต) |
21 | 19, 20 | oveqan12d 7380 |
. . 3
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (((โโ๐ด)โ2) ยท
((โโ๐ต)โ2))
= (๐ด ยท ๐ต)) |
22 | 8 | recnd 11191 |
. . . 4
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (โโ๐ด) โ
โ) |
23 | 10 | recnd 11191 |
. . . 4
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (โโ๐ต) โ
โ) |
24 | 22, 23 | sqmuld 14072 |
. . 3
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (((โโ๐ด) ยท (โโ๐ต))โ2) =
(((โโ๐ด)โ2)
ยท ((โโ๐ต)โ2))) |
25 | | resqrtth 15149 |
. . . 4
โข (((๐ด ยท ๐ต) โ โ โง 0 โค (๐ด ยท ๐ต)) โ ((โโ(๐ด ยท ๐ต))โ2) = (๐ด ยท ๐ต)) |
26 | 3, 4, 25 | syl2anc 585 |
. . 3
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((โโ(๐ด ยท ๐ต))โ2) = (๐ด ยท ๐ต)) |
27 | 21, 24, 26 | 3eqtr4rd 2784 |
. 2
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((โโ(๐ด ยท ๐ต))โ2) = (((โโ๐ด) ยท (โโ๐ต))โ2)) |
28 | 6, 11, 13, 18, 27 | sq11d 14170 |
1
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (โโ(๐ด ยท ๐ต)) = ((โโ๐ด) ยท (โโ๐ต))) |