Metamath Proof Explorer


Theorem relogbdiv

Description: The logarithm of the quotient of two positive real numbers is the difference of logarithms. Property 3 of Cohen4 p. 361. (Contributed by AV, 29-May-2020)

Ref Expression
Assertion relogbdiv ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ ( 𝐴 ∈ ℝ+𝐶 ∈ ℝ+ ) ) → ( 𝐵 logb ( 𝐴 / 𝐶 ) ) = ( ( 𝐵 logb 𝐴 ) − ( 𝐵 logb 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 neg1rr - 1 ∈ ℝ
2 relogbmulexp ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ ( 𝐴 ∈ ℝ+𝐶 ∈ ℝ+ ∧ - 1 ∈ ℝ ) ) → ( 𝐵 logb ( 𝐴 · ( 𝐶𝑐 - 1 ) ) ) = ( ( 𝐵 logb 𝐴 ) + ( - 1 · ( 𝐵 logb 𝐶 ) ) ) )
3 1 2 mp3anr3 ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ ( 𝐴 ∈ ℝ+𝐶 ∈ ℝ+ ) ) → ( 𝐵 logb ( 𝐴 · ( 𝐶𝑐 - 1 ) ) ) = ( ( 𝐵 logb 𝐴 ) + ( - 1 · ( 𝐵 logb 𝐶 ) ) ) )
4 rpcn ( 𝐴 ∈ ℝ+𝐴 ∈ ℂ )
5 4 adantr ( ( 𝐴 ∈ ℝ+𝐶 ∈ ℝ+ ) → 𝐴 ∈ ℂ )
6 rpcn ( 𝐶 ∈ ℝ+𝐶 ∈ ℂ )
7 6 adantl ( ( 𝐴 ∈ ℝ+𝐶 ∈ ℝ+ ) → 𝐶 ∈ ℂ )
8 rpne0 ( 𝐶 ∈ ℝ+𝐶 ≠ 0 )
9 8 adantl ( ( 𝐴 ∈ ℝ+𝐶 ∈ ℝ+ ) → 𝐶 ≠ 0 )
10 5 7 9 divrecd ( ( 𝐴 ∈ ℝ+𝐶 ∈ ℝ+ ) → ( 𝐴 / 𝐶 ) = ( 𝐴 · ( 1 / 𝐶 ) ) )
11 1cnd ( 𝐶 ∈ ℝ+ → 1 ∈ ℂ )
12 6 8 11 cxpnegd ( 𝐶 ∈ ℝ+ → ( 𝐶𝑐 - 1 ) = ( 1 / ( 𝐶𝑐 1 ) ) )
13 6 cxp1d ( 𝐶 ∈ ℝ+ → ( 𝐶𝑐 1 ) = 𝐶 )
14 13 oveq2d ( 𝐶 ∈ ℝ+ → ( 1 / ( 𝐶𝑐 1 ) ) = ( 1 / 𝐶 ) )
15 12 14 eqtrd ( 𝐶 ∈ ℝ+ → ( 𝐶𝑐 - 1 ) = ( 1 / 𝐶 ) )
16 15 adantl ( ( 𝐴 ∈ ℝ+𝐶 ∈ ℝ+ ) → ( 𝐶𝑐 - 1 ) = ( 1 / 𝐶 ) )
17 16 oveq2d ( ( 𝐴 ∈ ℝ+𝐶 ∈ ℝ+ ) → ( 𝐴 · ( 𝐶𝑐 - 1 ) ) = ( 𝐴 · ( 1 / 𝐶 ) ) )
18 10 17 eqtr4d ( ( 𝐴 ∈ ℝ+𝐶 ∈ ℝ+ ) → ( 𝐴 / 𝐶 ) = ( 𝐴 · ( 𝐶𝑐 - 1 ) ) )
19 18 adantl ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ ( 𝐴 ∈ ℝ+𝐶 ∈ ℝ+ ) ) → ( 𝐴 / 𝐶 ) = ( 𝐴 · ( 𝐶𝑐 - 1 ) ) )
20 19 oveq2d ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ ( 𝐴 ∈ ℝ+𝐶 ∈ ℝ+ ) ) → ( 𝐵 logb ( 𝐴 / 𝐶 ) ) = ( 𝐵 logb ( 𝐴 · ( 𝐶𝑐 - 1 ) ) ) )
21 rpcndif0 ( 𝐶 ∈ ℝ+𝐶 ∈ ( ℂ ∖ { 0 } ) )
22 21 adantl ( ( 𝐴 ∈ ℝ+𝐶 ∈ ℝ+ ) → 𝐶 ∈ ( ℂ ∖ { 0 } ) )
23 logbcl ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝐶 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝐵 logb 𝐶 ) ∈ ℂ )
24 22 23 sylan2 ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ ( 𝐴 ∈ ℝ+𝐶 ∈ ℝ+ ) ) → ( 𝐵 logb 𝐶 ) ∈ ℂ )
25 mulm1 ( ( 𝐵 logb 𝐶 ) ∈ ℂ → ( - 1 · ( 𝐵 logb 𝐶 ) ) = - ( 𝐵 logb 𝐶 ) )
26 25 oveq2d ( ( 𝐵 logb 𝐶 ) ∈ ℂ → ( ( 𝐵 logb 𝐴 ) + ( - 1 · ( 𝐵 logb 𝐶 ) ) ) = ( ( 𝐵 logb 𝐴 ) + - ( 𝐵 logb 𝐶 ) ) )
27 24 26 syl ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ ( 𝐴 ∈ ℝ+𝐶 ∈ ℝ+ ) ) → ( ( 𝐵 logb 𝐴 ) + ( - 1 · ( 𝐵 logb 𝐶 ) ) ) = ( ( 𝐵 logb 𝐴 ) + - ( 𝐵 logb 𝐶 ) ) )
28 rpcndif0 ( 𝐴 ∈ ℝ+𝐴 ∈ ( ℂ ∖ { 0 } ) )
29 28 adantr ( ( 𝐴 ∈ ℝ+𝐶 ∈ ℝ+ ) → 𝐴 ∈ ( ℂ ∖ { 0 } ) )
30 logbcl ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝐵 logb 𝐴 ) ∈ ℂ )
31 29 30 sylan2 ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ ( 𝐴 ∈ ℝ+𝐶 ∈ ℝ+ ) ) → ( 𝐵 logb 𝐴 ) ∈ ℂ )
32 31 24 negsubd ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ ( 𝐴 ∈ ℝ+𝐶 ∈ ℝ+ ) ) → ( ( 𝐵 logb 𝐴 ) + - ( 𝐵 logb 𝐶 ) ) = ( ( 𝐵 logb 𝐴 ) − ( 𝐵 logb 𝐶 ) ) )
33 27 32 eqtr2d ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ ( 𝐴 ∈ ℝ+𝐶 ∈ ℝ+ ) ) → ( ( 𝐵 logb 𝐴 ) − ( 𝐵 logb 𝐶 ) ) = ( ( 𝐵 logb 𝐴 ) + ( - 1 · ( 𝐵 logb 𝐶 ) ) ) )
34 3 20 33 3eqtr4d ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ ( 𝐴 ∈ ℝ+𝐶 ∈ ℝ+ ) ) → ( 𝐵 logb ( 𝐴 / 𝐶 ) ) = ( ( 𝐵 logb 𝐴 ) − ( 𝐵 logb 𝐶 ) ) )