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