Metamath Proof Explorer

Theorem reglogmul

Description: Multiplication law for general log. (Contributed by Stefan O'Rear, 19-Sep-2014) (New usage is discouraged.) Use relogbmul instead.

		Ref	Expression
	Assertion	reglogmul	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℝ⁺ ∧ ( 𝐶 ∈ ℝ⁺ ∧ 𝐶 ≠ 1 ) ) → ( ( log ‘ ( 𝐴 · 𝐵 ) ) / ( log ‘ 𝐶 ) ) = ( ( ( log ‘ 𝐴 ) / ( log ‘ 𝐶 ) ) + ( ( log ‘ 𝐵 ) / ( log ‘ 𝐶 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		relogmul	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℝ⁺ ) → ( log ‘ ( 𝐴 · 𝐵 ) ) = ( ( log ‘ 𝐴 ) + ( log ‘ 𝐵 ) ) )
2	1	3adant3	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℝ⁺ ∧ ( 𝐶 ∈ ℝ⁺ ∧ 𝐶 ≠ 1 ) ) → ( log ‘ ( 𝐴 · 𝐵 ) ) = ( ( log ‘ 𝐴 ) + ( log ‘ 𝐵 ) ) )
3	2	oveq1d	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℝ⁺ ∧ ( 𝐶 ∈ ℝ⁺ ∧ 𝐶 ≠ 1 ) ) → ( ( log ‘ ( 𝐴 · 𝐵 ) ) / ( log ‘ 𝐶 ) ) = ( ( ( log ‘ 𝐴 ) + ( log ‘ 𝐵 ) ) / ( log ‘ 𝐶 ) ) )
4		relogcl	⊢ ( 𝐴 ∈ ℝ⁺ → ( log ‘ 𝐴 ) ∈ ℝ )
5	4	recnd	⊢ ( 𝐴 ∈ ℝ⁺ → ( log ‘ 𝐴 ) ∈ ℂ )
6	5	3ad2ant1	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℝ⁺ ∧ ( 𝐶 ∈ ℝ⁺ ∧ 𝐶 ≠ 1 ) ) → ( log ‘ 𝐴 ) ∈ ℂ )
7		relogcl	⊢ ( 𝐵 ∈ ℝ⁺ → ( log ‘ 𝐵 ) ∈ ℝ )
8	7	recnd	⊢ ( 𝐵 ∈ ℝ⁺ → ( log ‘ 𝐵 ) ∈ ℂ )
9	8	3ad2ant2	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℝ⁺ ∧ ( 𝐶 ∈ ℝ⁺ ∧ 𝐶 ≠ 1 ) ) → ( log ‘ 𝐵 ) ∈ ℂ )
10		relogcl	⊢ ( 𝐶 ∈ ℝ⁺ → ( log ‘ 𝐶 ) ∈ ℝ )
11	10	recnd	⊢ ( 𝐶 ∈ ℝ⁺ → ( log ‘ 𝐶 ) ∈ ℂ )
12	11	adantr	⊢ ( ( 𝐶 ∈ ℝ⁺ ∧ 𝐶 ≠ 1 ) → ( log ‘ 𝐶 ) ∈ ℂ )
13	12	3ad2ant3	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℝ⁺ ∧ ( 𝐶 ∈ ℝ⁺ ∧ 𝐶 ≠ 1 ) ) → ( log ‘ 𝐶 ) ∈ ℂ )
14		logne0	⊢ ( ( 𝐶 ∈ ℝ⁺ ∧ 𝐶 ≠ 1 ) → ( log ‘ 𝐶 ) ≠ 0 )
15	14	3ad2ant3	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℝ⁺ ∧ ( 𝐶 ∈ ℝ⁺ ∧ 𝐶 ≠ 1 ) ) → ( log ‘ 𝐶 ) ≠ 0 )
16	6 9 13 15	divdird	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℝ⁺ ∧ ( 𝐶 ∈ ℝ⁺ ∧ 𝐶 ≠ 1 ) ) → ( ( ( log ‘ 𝐴 ) + ( log ‘ 𝐵 ) ) / ( log ‘ 𝐶 ) ) = ( ( ( log ‘ 𝐴 ) / ( log ‘ 𝐶 ) ) + ( ( log ‘ 𝐵 ) / ( log ‘ 𝐶 ) ) ) )
17	3 16	eqtrd	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℝ⁺ ∧ ( 𝐶 ∈ ℝ⁺ ∧ 𝐶 ≠ 1 ) ) → ( ( log ‘ ( 𝐴 · 𝐵 ) ) / ( log ‘ 𝐶 ) ) = ( ( ( log ‘ 𝐴 ) / ( log ‘ 𝐶 ) ) + ( ( log ‘ 𝐵 ) / ( log ‘ 𝐶 ) ) ) )