Step | Hyp | Ref
| Expression |
1 | | 0red 11221 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ด = 0) โ 0 โ
โ) |
2 | | 0le0 12317 |
. . . . . 6
โข 0 โค
0 |
3 | 2 | a1i 11 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ด = 0) โ 0 โค
0) |
4 | | simplr 766 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ด = 0) โ ๐ต โ โ) |
5 | | recxpcl 26564 |
. . . . 5
โข ((0
โ โ โง 0 โค 0 โง ๐ต โ โ) โ
(0โ๐๐ต) โ โ) |
6 | 1, 3, 4, 5 | syl3anc 1368 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ด = 0) โ
(0โ๐๐ต) โ โ) |
7 | | cxpge0 26572 |
. . . . 5
โข ((0
โ โ โง 0 โค 0 โง ๐ต โ โ) โ 0 โค
(0โ๐๐ต)) |
8 | 1, 3, 4, 7 | syl3anc 1368 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ด = 0) โ 0 โค
(0โ๐๐ต)) |
9 | 6, 8 | absidd 15375 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ด = 0) โ
(absโ(0โ๐๐ต)) = (0โ๐๐ต)) |
10 | | simpr 484 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ด = 0) โ ๐ด = 0) |
11 | 10 | oveq1d 7420 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ด = 0) โ (๐ดโ๐๐ต) = (0โ๐๐ต)) |
12 | 11 | fveq2d 6889 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ด = 0) โ (absโ(๐ดโ๐๐ต)) =
(absโ(0โ๐๐ต))) |
13 | 10 | abs00bd 15244 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ด = 0) โ (absโ๐ด) = 0) |
14 | 13 | oveq1d 7420 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ด = 0) โ ((absโ๐ด)โ๐๐ต) =
(0โ๐๐ต)) |
15 | 9, 12, 14 | 3eqtr4d 2776 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ด = 0) โ (absโ(๐ดโ๐๐ต)) = ((absโ๐ด)โ๐๐ต)) |
16 | | simplr 766 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ด โ 0) โ ๐ต โ
โ) |
17 | 16 | recnd 11246 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ด โ 0) โ ๐ต โ
โ) |
18 | | logcl 26457 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ด โ 0) โ (logโ๐ด) โ
โ) |
19 | 18 | adantlr 712 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ด โ 0) โ (logโ๐ด) โ
โ) |
20 | 17, 19 | mulcld 11238 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ด โ 0) โ (๐ต ยท (logโ๐ด)) โ
โ) |
21 | | absef 16147 |
. . . . 5
โข ((๐ต ยท (logโ๐ด)) โ โ โ
(absโ(expโ(๐ต
ยท (logโ๐ด)))) =
(expโ(โโ(๐ต
ยท (logโ๐ด))))) |
22 | 20, 21 | syl 17 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ด โ 0) โ
(absโ(expโ(๐ต
ยท (logโ๐ด)))) =
(expโ(โโ(๐ต
ยท (logโ๐ด))))) |
23 | 16, 19 | remul2d 15180 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ด โ 0) โ
(โโ(๐ต ยท
(logโ๐ด))) = (๐ต ยท
(โโ(logโ๐ด)))) |
24 | | relog 26486 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ด โ 0) โ
(โโ(logโ๐ด)) = (logโ(absโ๐ด))) |
25 | 24 | adantlr 712 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ด โ 0) โ
(โโ(logโ๐ด)) = (logโ(absโ๐ด))) |
26 | 25 | oveq2d 7421 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ด โ 0) โ (๐ต ยท
(โโ(logโ๐ด))) = (๐ต ยท (logโ(absโ๐ด)))) |
27 | 23, 26 | eqtrd 2766 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ด โ 0) โ
(โโ(๐ต ยท
(logโ๐ด))) = (๐ต ยท
(logโ(absโ๐ด)))) |
28 | 27 | fveq2d 6889 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ด โ 0) โ
(expโ(โโ(๐ต
ยท (logโ๐ด)))) =
(expโ(๐ต ยท
(logโ(absโ๐ด))))) |
29 | 22, 28 | eqtrd 2766 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ด โ 0) โ
(absโ(expโ(๐ต
ยท (logโ๐ด)))) =
(expโ(๐ต ยท
(logโ(absโ๐ด))))) |
30 | | simpll 764 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ด โ 0) โ ๐ด โ
โ) |
31 | | simpr 484 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ด โ 0) โ ๐ด โ 0) |
32 | | cxpef 26554 |
. . . . 5
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ต โ โ) โ (๐ดโ๐๐ต) = (expโ(๐ต ยท (logโ๐ด)))) |
33 | 30, 31, 17, 32 | syl3anc 1368 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ด โ 0) โ (๐ดโ๐๐ต) = (expโ(๐ต ยท (logโ๐ด)))) |
34 | 33 | fveq2d 6889 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ด โ 0) โ
(absโ(๐ดโ๐๐ต)) = (absโ(expโ(๐ต ยท (logโ๐ด))))) |
35 | 30 | abscld 15389 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ด โ 0) โ (absโ๐ด) โ
โ) |
36 | 35 | recnd 11246 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ด โ 0) โ (absโ๐ด) โ
โ) |
37 | | abs00 15242 |
. . . . . . 7
โข (๐ด โ โ โ
((absโ๐ด) = 0 โ
๐ด = 0)) |
38 | 37 | adantr 480 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ
((absโ๐ด) = 0 โ
๐ด = 0)) |
39 | 38 | necon3bid 2979 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ
((absโ๐ด) โ 0
โ ๐ด โ
0)) |
40 | 39 | biimpar 477 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ด โ 0) โ (absโ๐ด) โ 0) |
41 | | cxpef 26554 |
. . . 4
โข
(((absโ๐ด)
โ โ โง (absโ๐ด) โ 0 โง ๐ต โ โ) โ ((absโ๐ด)โ๐๐ต) = (expโ(๐ต ยท
(logโ(absโ๐ด))))) |
42 | 36, 40, 17, 41 | syl3anc 1368 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ด โ 0) โ
((absโ๐ด)โ๐๐ต) = (expโ(๐ต ยท (logโ(absโ๐ด))))) |
43 | 29, 34, 42 | 3eqtr4d 2776 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ด โ 0) โ
(absโ(๐ดโ๐๐ต)) = ((absโ๐ด)โ๐๐ต)) |
44 | 15, 43 | pm2.61dane 3023 |
1
โข ((๐ด โ โ โง ๐ต โ โ) โ
(absโ(๐ดโ๐๐ต)) = ((absโ๐ด)โ๐๐ต)) |