This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝐶 ) ) )