Step | Hyp | Ref
| Expression |
1 | | rerpdivcl 12953 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ+)
โ (๐ด / ๐ต) โ
โ) |
2 | 1 | adantlr 714 |
. . . . 5
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ต โ โ+) โ (๐ด / ๐ต) โ โ) |
3 | | elrp 12925 |
. . . . . 6
โข (๐ต โ โ+
โ (๐ต โ โ
โง 0 < ๐ต)) |
4 | | divge0 12032 |
. . . . . 6
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 < ๐ต)) โ 0 โค (๐ด / ๐ต)) |
5 | 3, 4 | sylan2b 595 |
. . . . 5
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ต โ โ+) โ 0 โค
(๐ด / ๐ต)) |
6 | | resqrtcl 15147 |
. . . . 5
โข (((๐ด / ๐ต) โ โ โง 0 โค (๐ด / ๐ต)) โ (โโ(๐ด / ๐ต)) โ โ) |
7 | 2, 5, 6 | syl2anc 585 |
. . . 4
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ต โ โ+) โ
(โโ(๐ด / ๐ต)) โ
โ) |
8 | 7 | recnd 11191 |
. . 3
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ต โ โ+) โ
(โโ(๐ด / ๐ต)) โ
โ) |
9 | | rpsqrtcl 15158 |
. . . . 5
โข (๐ต โ โ+
โ (โโ๐ต)
โ โ+) |
10 | 9 | adantl 483 |
. . . 4
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ต โ โ+) โ
(โโ๐ต) โ
โ+) |
11 | 10 | rpcnd 12967 |
. . 3
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ต โ โ+) โ
(โโ๐ต) โ
โ) |
12 | 10 | rpne0d 12970 |
. . 3
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ต โ โ+) โ
(โโ๐ต) โ
0) |
13 | 8, 11, 12 | divcan4d 11945 |
. 2
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ต โ โ+) โ
(((โโ(๐ด / ๐ต)) ยท (โโ๐ต)) / (โโ๐ต)) = (โโ(๐ด / ๐ต))) |
14 | | rprege0 12938 |
. . . . . 6
โข (๐ต โ โ+
โ (๐ต โ โ
โง 0 โค ๐ต)) |
15 | 14 | adantl 483 |
. . . . 5
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ต โ โ+) โ (๐ต โ โ โง 0 โค
๐ต)) |
16 | | sqrtmul 15153 |
. . . . 5
โข ((((๐ด / ๐ต) โ โ โง 0 โค (๐ด / ๐ต)) โง (๐ต โ โ โง 0 โค ๐ต)) โ (โโ((๐ด / ๐ต) ยท ๐ต)) = ((โโ(๐ด / ๐ต)) ยท (โโ๐ต))) |
17 | 2, 5, 15, 16 | syl21anc 837 |
. . . 4
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ต โ โ+) โ
(โโ((๐ด / ๐ต) ยท ๐ต)) = ((โโ(๐ด / ๐ต)) ยท (โโ๐ต))) |
18 | | simpll 766 |
. . . . . . 7
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ต โ โ+) โ ๐ด โ
โ) |
19 | 18 | recnd 11191 |
. . . . . 6
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ต โ โ+) โ ๐ด โ
โ) |
20 | | rpcn 12933 |
. . . . . . 7
โข (๐ต โ โ+
โ ๐ต โ
โ) |
21 | 20 | adantl 483 |
. . . . . 6
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ต โ โ+) โ ๐ต โ
โ) |
22 | | rpne0 12939 |
. . . . . . 7
โข (๐ต โ โ+
โ ๐ต โ
0) |
23 | 22 | adantl 483 |
. . . . . 6
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ต โ โ+) โ ๐ต โ 0) |
24 | 19, 21, 23 | divcan1d 11940 |
. . . . 5
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ต โ โ+) โ ((๐ด / ๐ต) ยท ๐ต) = ๐ด) |
25 | 24 | fveq2d 6850 |
. . . 4
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ต โ โ+) โ
(โโ((๐ด / ๐ต) ยท ๐ต)) = (โโ๐ด)) |
26 | 17, 25 | eqtr3d 2775 |
. . 3
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ต โ โ+) โ
((โโ(๐ด / ๐ต)) ยท (โโ๐ต)) = (โโ๐ด)) |
27 | 26 | oveq1d 7376 |
. 2
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ต โ โ+) โ
(((โโ(๐ด / ๐ต)) ยท (โโ๐ต)) / (โโ๐ต)) = ((โโ๐ด) / (โโ๐ต))) |
28 | 13, 27 | eqtr3d 2775 |
1
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ต โ โ+) โ
(โโ(๐ด / ๐ต)) = ((โโ๐ด) / (โโ๐ต))) |