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 e. ( RR+ \ { 1 } ) /\ A e. RR+ ) -> ( B logb ( A / B ) ) = ( ( B logb A ) - 1 ) )

Proof

Step	Hyp	Ref	Expression
1		eldifsn	|- ( B e. ( RR+ \ { 1 } ) <-> ( B e. RR+ /\ B =/= 1 ) )
2		rpcn	|- ( B e. RR+ -> B e. CC )
3	2	adantr	|- ( ( B e. RR+ /\ B =/= 1 ) -> B e. CC )
4		rpne0	|- ( B e. RR+ -> B =/= 0 )
5	4	adantr	|- ( ( B e. RR+ /\ B =/= 1 ) -> B =/= 0 )
6		simpr	|- ( ( B e. RR+ /\ B =/= 1 ) -> B =/= 1 )
7	3 5 6	3jca	|- ( ( B e. RR+ /\ B =/= 1 ) -> ( B e. CC /\ B =/= 0 /\ B =/= 1 ) )
8	1 7	sylbi	|- ( B e. ( RR+ \ { 1 } ) -> ( B e. CC /\ B =/= 0 /\ B =/= 1 ) )
9		eldifpr	|- ( B e. ( CC \ { 0 , 1 } ) <-> ( B e. CC /\ B =/= 0 /\ B =/= 1 ) )
10	8 9	sylibr	|- ( B e. ( RR+ \ { 1 } ) -> B e. ( CC \ { 0 , 1 } ) )
11	10	adantr	|- ( ( B e. ( RR+ \ { 1 } ) /\ A e. RR+ ) -> B e. ( CC \ { 0 , 1 } ) )
12		simpr	|- ( ( B e. ( RR+ \ { 1 } ) /\ A e. RR+ ) -> A e. RR+ )
13		eldifi	|- ( B e. ( RR+ \ { 1 } ) -> B e. RR+ )
14	13	adantr	|- ( ( B e. ( RR+ \ { 1 } ) /\ A e. RR+ ) -> B e. RR+ )
15		relogbdiv	|- ( ( B e. ( CC \ { 0 , 1 } ) /\ ( A e. RR+ /\ B e. RR+ ) ) -> ( B logb ( A / B ) ) = ( ( B logb A ) - ( B logb B ) ) )
16	11 12 14 15	syl12anc	|- ( ( B e. ( RR+ \ { 1 } ) /\ A e. RR+ ) -> ( B logb ( A / B ) ) = ( ( B logb A ) - ( B logb B ) ) )
17		logbid1	|- ( ( B e. CC /\ B =/= 0 /\ B =/= 1 ) -> ( B logb B ) = 1 )
18	8 17	syl	|- ( B e. ( RR+ \ { 1 } ) -> ( B logb B ) = 1 )
19	18	adantr	|- ( ( B e. ( RR+ \ { 1 } ) /\ A e. RR+ ) -> ( B logb B ) = 1 )
20	19	oveq2d	|- ( ( B e. ( RR+ \ { 1 } ) /\ A e. RR+ ) -> ( ( B logb A ) - ( B logb B ) ) = ( ( B logb A ) - 1 ) )
21	16 20	eqtrd	|- ( ( B e. ( RR+ \ { 1 } ) /\ A e. RR+ ) -> ( B logb ( A / B ) ) = ( ( B logb A ) - 1 ) )