Step | Hyp | Ref
| Expression |
1 | | neg1rr 9025 |
. . 3
โข -1 โ
โ |
2 | | rprelogbmulexp 14377 |
. . 3
โข (((๐ต โ โ+
โง ๐ต # 1) โง (๐ด โ โ+
โง ๐ถ โ
โ+ โง -1 โ โ)) โ (๐ต logb (๐ด ยท (๐ถโ๐-1))) = ((๐ต logb ๐ด) + (-1 ยท (๐ต logb ๐ถ)))) |
3 | 1, 2 | mp3anr3 1336 |
. 2
โข (((๐ต โ โ+
โง ๐ต # 1) โง (๐ด โ โ+
โง ๐ถ โ
โ+)) โ (๐ต logb (๐ด ยท (๐ถโ๐-1))) = ((๐ต logb ๐ด) + (-1 ยท (๐ต logb ๐ถ)))) |
4 | | rpcn 9662 |
. . . . . . 7
โข (๐ด โ โ+
โ ๐ด โ
โ) |
5 | 4 | adantr 276 |
. . . . . 6
โข ((๐ด โ โ+
โง ๐ถ โ
โ+) โ ๐ด โ โ) |
6 | | rpcn 9662 |
. . . . . . 7
โข (๐ถ โ โ+
โ ๐ถ โ
โ) |
7 | 6 | adantl 277 |
. . . . . 6
โข ((๐ด โ โ+
โง ๐ถ โ
โ+) โ ๐ถ โ โ) |
8 | | rpap0 9670 |
. . . . . . 7
โข (๐ถ โ โ+
โ ๐ถ #
0) |
9 | 8 | adantl 277 |
. . . . . 6
โข ((๐ด โ โ+
โง ๐ถ โ
โ+) โ ๐ถ # 0) |
10 | 5, 7, 9 | divrecapd 8750 |
. . . . 5
โข ((๐ด โ โ+
โง ๐ถ โ
โ+) โ (๐ด / ๐ถ) = (๐ด ยท (1 / ๐ถ))) |
11 | | ax-1cn 7904 |
. . . . . . . . 9
โข 1 โ
โ |
12 | | rpcxpneg 14331 |
. . . . . . . . 9
โข ((๐ถ โ โ+
โง 1 โ โ) โ (๐ถโ๐-1) = (1 / (๐ถโ๐1))) |
13 | 11, 12 | mpan2 425 |
. . . . . . . 8
โข (๐ถ โ โ+
โ (๐ถโ๐-1) = (1 / (๐ถโ๐1))) |
14 | | rpcxp1 14323 |
. . . . . . . . 9
โข (๐ถ โ โ+
โ (๐ถโ๐1) = ๐ถ) |
15 | 14 | oveq2d 5891 |
. . . . . . . 8
โข (๐ถ โ โ+
โ (1 / (๐ถโ๐1)) = (1 / ๐ถ)) |
16 | 13, 15 | eqtrd 2210 |
. . . . . . 7
โข (๐ถ โ โ+
โ (๐ถโ๐-1) = (1 / ๐ถ)) |
17 | 16 | adantl 277 |
. . . . . 6
โข ((๐ด โ โ+
โง ๐ถ โ
โ+) โ (๐ถโ๐-1) = (1 / ๐ถ)) |
18 | 17 | oveq2d 5891 |
. . . . 5
โข ((๐ด โ โ+
โง ๐ถ โ
โ+) โ (๐ด ยท (๐ถโ๐-1)) = (๐ด ยท (1 / ๐ถ))) |
19 | 10, 18 | eqtr4d 2213 |
. . . 4
โข ((๐ด โ โ+
โง ๐ถ โ
โ+) โ (๐ด / ๐ถ) = (๐ด ยท (๐ถโ๐-1))) |
20 | 19 | adantl 277 |
. . 3
โข (((๐ต โ โ+
โง ๐ต # 1) โง (๐ด โ โ+
โง ๐ถ โ
โ+)) โ (๐ด / ๐ถ) = (๐ด ยท (๐ถโ๐-1))) |
21 | 20 | oveq2d 5891 |
. 2
โข (((๐ต โ โ+
โง ๐ต # 1) โง (๐ด โ โ+
โง ๐ถ โ
โ+)) โ (๐ต logb (๐ด / ๐ถ)) = (๐ต logb (๐ด ยท (๐ถโ๐-1)))) |
22 | | simpll 527 |
. . . . 5
โข (((๐ต โ โ+
โง ๐ต # 1) โง (๐ด โ โ+
โง ๐ถ โ
โ+)) โ ๐ต โ
โ+) |
23 | | simplr 528 |
. . . . 5
โข (((๐ต โ โ+
โง ๐ต # 1) โง (๐ด โ โ+
โง ๐ถ โ
โ+)) โ ๐ต # 1) |
24 | | simprr 531 |
. . . . 5
โข (((๐ต โ โ+
โง ๐ต # 1) โง (๐ด โ โ+
โง ๐ถ โ
โ+)) โ ๐ถ โ
โ+) |
25 | | rplogbcl 14367 |
. . . . 5
โข ((๐ต โ โ+
โง ๐ต # 1 โง ๐ถ โ โ+)
โ (๐ต logb
๐ถ) โ
โ) |
26 | 22, 23, 24, 25 | syl3anc 1238 |
. . . 4
โข (((๐ต โ โ+
โง ๐ต # 1) โง (๐ด โ โ+
โง ๐ถ โ
โ+)) โ (๐ต logb ๐ถ) โ โ) |
27 | | recn 7944 |
. . . 4
โข ((๐ต logb ๐ถ) โ โ โ (๐ต logb ๐ถ) โ
โ) |
28 | | mulm1 8357 |
. . . . 5
โข ((๐ต logb ๐ถ) โ โ โ (-1
ยท (๐ต logb
๐ถ)) = -(๐ต logb ๐ถ)) |
29 | 28 | oveq2d 5891 |
. . . 4
โข ((๐ต logb ๐ถ) โ โ โ ((๐ต logb ๐ด) + (-1 ยท (๐ต logb ๐ถ))) = ((๐ต logb ๐ด) + -(๐ต logb ๐ถ))) |
30 | 26, 27, 29 | 3syl 17 |
. . 3
โข (((๐ต โ โ+
โง ๐ต # 1) โง (๐ด โ โ+
โง ๐ถ โ
โ+)) โ ((๐ต logb ๐ด) + (-1 ยท (๐ต logb ๐ถ))) = ((๐ต logb ๐ด) + -(๐ต logb ๐ถ))) |
31 | | simprl 529 |
. . . . . 6
โข (((๐ต โ โ+
โง ๐ต # 1) โง (๐ด โ โ+
โง ๐ถ โ
โ+)) โ ๐ด โ
โ+) |
32 | | rplogbcl 14367 |
. . . . . 6
โข ((๐ต โ โ+
โง ๐ต # 1 โง ๐ด โ โ+)
โ (๐ต logb
๐ด) โ
โ) |
33 | 22, 23, 31, 32 | syl3anc 1238 |
. . . . 5
โข (((๐ต โ โ+
โง ๐ต # 1) โง (๐ด โ โ+
โง ๐ถ โ
โ+)) โ (๐ต logb ๐ด) โ โ) |
34 | 33 | recnd 7986 |
. . . 4
โข (((๐ต โ โ+
โง ๐ต # 1) โง (๐ด โ โ+
โง ๐ถ โ
โ+)) โ (๐ต logb ๐ด) โ โ) |
35 | 26 | recnd 7986 |
. . . 4
โข (((๐ต โ โ+
โง ๐ต # 1) โง (๐ด โ โ+
โง ๐ถ โ
โ+)) โ (๐ต logb ๐ถ) โ โ) |
36 | 34, 35 | negsubd 8274 |
. . 3
โข (((๐ต โ โ+
โง ๐ต # 1) โง (๐ด โ โ+
โง ๐ถ โ
โ+)) โ ((๐ต logb ๐ด) + -(๐ต logb ๐ถ)) = ((๐ต logb ๐ด) โ (๐ต logb ๐ถ))) |
37 | 30, 36 | eqtr2d 2211 |
. 2
โข (((๐ต โ โ+
โง ๐ต # 1) โง (๐ด โ โ+
โง ๐ถ โ
โ+)) โ ((๐ต logb ๐ด) โ (๐ต logb ๐ถ)) = ((๐ต logb ๐ด) + (-1 ยท (๐ต logb ๐ถ)))) |
38 | 3, 21, 37 | 3eqtr4d 2220 |
1
โข (((๐ต โ โ+
โง ๐ต # 1) โง (๐ด โ โ+
โง ๐ถ โ
โ+)) โ (๐ต logb (๐ด / ๐ถ)) = ((๐ต logb ๐ด) โ (๐ต logb ๐ถ))) |