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	⊢ ( ( 𝐵 ∈ ( ℝ+ ∖ { 1 } ) ∧ 𝐴 ∈ ℝ+ ) → ( 𝐵 logb ( 𝐴 / 𝐵 ) ) = ( ( 𝐵 logb 𝐴 ) − 1 ) )

Proof

Step	Hyp	Ref	Expression
1		eldifsn	⊢ ( 𝐵 ∈ ( ℝ+ ∖ { 1 } ) ↔ ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1 ) )
2		rpcn	⊢ ( 𝐵 ∈ ℝ+ → 𝐵 ∈ ℂ )
3	2	adantr	⊢ ( ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1 ) → 𝐵 ∈ ℂ )
4		rpne0	⊢ ( 𝐵 ∈ ℝ+ → 𝐵 ≠ 0 )
5	4	adantr	⊢ ( ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1 ) → 𝐵 ≠ 0 )
6		simpr	⊢ ( ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1 ) → 𝐵 ≠ 1 )
7	3 5 6	3jca	⊢ ( ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1 ) → ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) )
8	1 7	sylbi	⊢ ( 𝐵 ∈ ( ℝ+ ∖ { 1 } ) → ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) )
9		eldifpr	⊢ ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ↔ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) )
10	8 9	sylibr	⊢ ( 𝐵 ∈ ( ℝ+ ∖ { 1 } ) → 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) )
11	10	adantr	⊢ ( ( 𝐵 ∈ ( ℝ+ ∖ { 1 } ) ∧ 𝐴 ∈ ℝ+ ) → 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) )
12		simpr	⊢ ( ( 𝐵 ∈ ( ℝ+ ∖ { 1 } ) ∧ 𝐴 ∈ ℝ+ ) → 𝐴 ∈ ℝ+ )
13		eldifi	⊢ ( 𝐵 ∈ ( ℝ+ ∖ { 1 } ) → 𝐵 ∈ ℝ+ )
14	13	adantr	⊢ ( ( 𝐵 ∈ ( ℝ+ ∖ { 1 } ) ∧ 𝐴 ∈ ℝ+ ) → 𝐵 ∈ ℝ+ )
15		relogbdiv	⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ) → ( 𝐵 logb ( 𝐴 / 𝐵 ) ) = ( ( 𝐵 logb 𝐴 ) − ( 𝐵 logb 𝐵 ) ) )
16	11 12 14 15	syl12anc	⊢ ( ( 𝐵 ∈ ( ℝ+ ∖ { 1 } ) ∧ 𝐴 ∈ ℝ+ ) → ( 𝐵 logb ( 𝐴 / 𝐵 ) ) = ( ( 𝐵 logb 𝐴 ) − ( 𝐵 logb 𝐵 ) ) )
17		logbid1	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) → ( 𝐵 logb 𝐵 ) = 1 )
18	8 17	syl	⊢ ( 𝐵 ∈ ( ℝ+ ∖ { 1 } ) → ( 𝐵 logb 𝐵 ) = 1 )
19	18	adantr	⊢ ( ( 𝐵 ∈ ( ℝ+ ∖ { 1 } ) ∧ 𝐴 ∈ ℝ+ ) → ( 𝐵 logb 𝐵 ) = 1 )
20	19	oveq2d	⊢ ( ( 𝐵 ∈ ( ℝ+ ∖ { 1 } ) ∧ 𝐴 ∈ ℝ+ ) → ( ( 𝐵 logb 𝐴 ) − ( 𝐵 logb 𝐵 ) ) = ( ( 𝐵 logb 𝐴 ) − 1 ) )
21	16 20	eqtrd	⊢ ( ( 𝐵 ∈ ( ℝ+ ∖ { 1 } ) ∧ 𝐴 ∈ ℝ+ ) → ( 𝐵 logb ( 𝐴 / 𝐵 ) ) = ( ( 𝐵 logb 𝐴 ) − 1 ) )