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 ( ( 𝐵 ∈ ( ℝ+ ∖ { 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 ) )