Step | Hyp | Ref
| Expression |
1 | | simp1 998 |
. . . . . . 7
โข ((๐ด โ โ+
โง ๐ต โ
โ+ โง ๐ถ
โ โ) โ ๐ด
โ โ+) |
2 | | simp2 999 |
. . . . . . 7
โข ((๐ด โ โ+
โง ๐ต โ
โ+ โง ๐ถ
โ โ) โ ๐ต
โ โ+) |
3 | 1, 2 | relogmuld 14545 |
. . . . . 6
โข ((๐ด โ โ+
โง ๐ต โ
โ+ โง ๐ถ
โ โ) โ (logโ(๐ด ยท ๐ต)) = ((logโ๐ด) + (logโ๐ต))) |
4 | 3 | oveq2d 5904 |
. . . . 5
โข ((๐ด โ โ+
โง ๐ต โ
โ+ โง ๐ถ
โ โ) โ (๐ถ
ยท (logโ(๐ด
ยท ๐ต))) = (๐ถ ยท ((logโ๐ด) + (logโ๐ต)))) |
5 | | simp3 1000 |
. . . . . 6
โข ((๐ด โ โ+
โง ๐ต โ
โ+ โง ๐ถ
โ โ) โ ๐ถ
โ โ) |
6 | 1 | relogcld 14543 |
. . . . . . 7
โข ((๐ด โ โ+
โง ๐ต โ
โ+ โง ๐ถ
โ โ) โ (logโ๐ด) โ โ) |
7 | 6 | recnd 7999 |
. . . . . 6
โข ((๐ด โ โ+
โง ๐ต โ
โ+ โง ๐ถ
โ โ) โ (logโ๐ด) โ โ) |
8 | 2 | relogcld 14543 |
. . . . . . 7
โข ((๐ด โ โ+
โง ๐ต โ
โ+ โง ๐ถ
โ โ) โ (logโ๐ต) โ โ) |
9 | 8 | recnd 7999 |
. . . . . 6
โข ((๐ด โ โ+
โง ๐ต โ
โ+ โง ๐ถ
โ โ) โ (logโ๐ต) โ โ) |
10 | 5, 7, 9 | adddid 7995 |
. . . . 5
โข ((๐ด โ โ+
โง ๐ต โ
โ+ โง ๐ถ
โ โ) โ (๐ถ
ยท ((logโ๐ด) +
(logโ๐ต))) = ((๐ถ ยท (logโ๐ด)) + (๐ถ ยท (logโ๐ต)))) |
11 | 4, 10 | eqtrd 2220 |
. . . 4
โข ((๐ด โ โ+
โง ๐ต โ
โ+ โง ๐ถ
โ โ) โ (๐ถ
ยท (logโ(๐ด
ยท ๐ต))) = ((๐ถ ยท (logโ๐ด)) + (๐ถ ยท (logโ๐ต)))) |
12 | 11 | fveq2d 5531 |
. . 3
โข ((๐ด โ โ+
โง ๐ต โ
โ+ โง ๐ถ
โ โ) โ (expโ(๐ถ ยท (logโ(๐ด ยท ๐ต)))) = (expโ((๐ถ ยท (logโ๐ด)) + (๐ถ ยท (logโ๐ต))))) |
13 | 5, 7 | mulcld 7991 |
. . . 4
โข ((๐ด โ โ+
โง ๐ต โ
โ+ โง ๐ถ
โ โ) โ (๐ถ
ยท (logโ๐ด))
โ โ) |
14 | 5, 9 | mulcld 7991 |
. . . 4
โข ((๐ด โ โ+
โง ๐ต โ
โ+ โง ๐ถ
โ โ) โ (๐ถ
ยท (logโ๐ต))
โ โ) |
15 | | efadd 11696 |
. . . 4
โข (((๐ถ ยท (logโ๐ด)) โ โ โง (๐ถ ยท (logโ๐ต)) โ โ) โ
(expโ((๐ถ ยท
(logโ๐ด)) + (๐ถ ยท (logโ๐ต)))) = ((expโ(๐ถ ยท (logโ๐ด))) ยท (expโ(๐ถ ยท (logโ๐ต))))) |
16 | 13, 14, 15 | syl2anc 411 |
. . 3
โข ((๐ด โ โ+
โง ๐ต โ
โ+ โง ๐ถ
โ โ) โ (expโ((๐ถ ยท (logโ๐ด)) + (๐ถ ยท (logโ๐ต)))) = ((expโ(๐ถ ยท (logโ๐ด))) ยท (expโ(๐ถ ยท (logโ๐ต))))) |
17 | 12, 16 | eqtrd 2220 |
. 2
โข ((๐ด โ โ+
โง ๐ต โ
โ+ โง ๐ถ
โ โ) โ (expโ(๐ถ ยท (logโ(๐ด ยท ๐ต)))) = ((expโ(๐ถ ยท (logโ๐ด))) ยท (expโ(๐ถ ยท (logโ๐ต))))) |
18 | 1, 2 | rpmulcld 9726 |
. . 3
โข ((๐ด โ โ+
โง ๐ต โ
โ+ โง ๐ถ
โ โ) โ (๐ด
ยท ๐ต) โ
โ+) |
19 | | rpcxpef 14555 |
. . 3
โข (((๐ด ยท ๐ต) โ โ+ โง ๐ถ โ โ) โ ((๐ด ยท ๐ต)โ๐๐ถ) = (expโ(๐ถ ยท (logโ(๐ด ยท ๐ต))))) |
20 | 18, 5, 19 | syl2anc 411 |
. 2
โข ((๐ด โ โ+
โง ๐ต โ
โ+ โง ๐ถ
โ โ) โ ((๐ด
ยท ๐ต)โ๐๐ถ) = (expโ(๐ถ ยท (logโ(๐ด ยท ๐ต))))) |
21 | | rpcxpef 14555 |
. . . 4
โข ((๐ด โ โ+
โง ๐ถ โ โ)
โ (๐ดโ๐๐ถ) = (expโ(๐ถ ยท (logโ๐ด)))) |
22 | 1, 5, 21 | syl2anc 411 |
. . 3
โข ((๐ด โ โ+
โง ๐ต โ
โ+ โง ๐ถ
โ โ) โ (๐ดโ๐๐ถ) = (expโ(๐ถ ยท (logโ๐ด)))) |
23 | | rpcxpef 14555 |
. . . 4
โข ((๐ต โ โ+
โง ๐ถ โ โ)
โ (๐ตโ๐๐ถ) = (expโ(๐ถ ยท (logโ๐ต)))) |
24 | 2, 5, 23 | syl2anc 411 |
. . 3
โข ((๐ด โ โ+
โง ๐ต โ
โ+ โง ๐ถ
โ โ) โ (๐ตโ๐๐ถ) = (expโ(๐ถ ยท (logโ๐ต)))) |
25 | 22, 24 | oveq12d 5906 |
. 2
โข ((๐ด โ โ+
โง ๐ต โ
โ+ โง ๐ถ
โ โ) โ ((๐ดโ๐๐ถ) ยท (๐ตโ๐๐ถ)) = ((expโ(๐ถ ยท (logโ๐ด))) ยท (expโ(๐ถ ยท (logโ๐ต))))) |
26 | 17, 20, 25 | 3eqtr4d 2230 |
1
โข ((๐ด โ โ+
โง ๐ต โ
โ+ โง ๐ถ
โ โ) โ ((๐ด
ยท ๐ต)โ๐๐ถ) = ((๐ดโ๐๐ถ) ยท (๐ตโ๐๐ถ))) |