Metamath Proof Explorer


Theorem relogbmulbexp

Description: The logarithm of the product of a positive real number and the base to the power of a real number is the logarithm of the positive real number plus the real number. (Contributed by AV, 29-May-2020)

Ref Expression
Assertion relogbmulbexp B + 1 A + C log B A B C = log B A + C

Proof

Step Hyp Ref Expression
1 rpcn B + B
2 1 adantr B + B 1 B
3 rpne0 B + B 0
4 3 adantr B + B 1 B 0
5 simpr B + B 1 B 1
6 2 4 5 3jca B + B 1 B B 0 B 1
7 eldifsn B + 1 B + B 1
8 eldifpr B 0 1 B B 0 B 1
9 6 7 8 3imtr4i B + 1 B 0 1
10 9 adantr B + 1 A + C B 0 1
11 simprl B + 1 A + C A +
12 eldifi B + 1 B +
13 12 adantr B + 1 A + C B +
14 simpr A + C C
15 14 adantl B + 1 A + C C
16 relogbmulexp B 0 1 A + B + C log B A B C = log B A + C log B B
17 10 11 13 15 16 syl13anc B + 1 A + C log B A B C = log B A + C log B B
18 7 6 sylbi B + 1 B B 0 B 1
19 logbid1 B B 0 B 1 log B B = 1
20 18 19 syl B + 1 log B B = 1
21 20 adantr B + 1 A + C log B B = 1
22 21 oveq2d B + 1 A + C C log B B = C 1
23 ax-1rid C C 1 = C
24 23 adantl A + C C 1 = C
25 24 adantl B + 1 A + C C 1 = C
26 22 25 eqtrd B + 1 A + C C log B B = C
27 26 oveq2d B + 1 A + C log B A + C log B B = log B A + C
28 17 27 eqtrd B + 1 A + C log B A B C = log B A + C