Metamath Proof Explorer


Theorem relogbdivb

Description: The logarithm of the quotient of a positive real number and the base is the logarithm of the number minus 1. (Contributed by AV, 29-May-2020)

Ref Expression
Assertion relogbdivb B + 1 A + log B A B = log B A 1

Proof

Step Hyp Ref Expression
1 eldifsn B + 1 B + B 1
2 rpcn B + B
3 2 adantr B + B 1 B
4 rpne0 B + B 0
5 4 adantr B + B 1 B 0
6 simpr B + B 1 B 1
7 3 5 6 3jca B + B 1 B B 0 B 1
8 1 7 sylbi B + 1 B B 0 B 1
9 eldifpr B 0 1 B B 0 B 1
10 8 9 sylibr B + 1 B 0 1
11 10 adantr B + 1 A + B 0 1
12 simpr B + 1 A + A +
13 eldifi B + 1 B +
14 13 adantr B + 1 A + B +
15 relogbdiv B 0 1 A + B + log B A B = log B A log B B
16 11 12 14 15 syl12anc B + 1 A + log B A B = log B A log B B
17 logbid1 B B 0 B 1 log B B = 1
18 8 17 syl B + 1 log B B = 1
19 18 adantr B + 1 A + log B B = 1
20 19 oveq2d B + 1 A + log B A log B B = log B A 1
21 16 20 eqtrd B + 1 A + log B A B = log B A 1