Metamath Proof Explorer

Theorem relogoprlem

Description: Lemma for relogmul and relogdiv . Remark of Cohen p. 301 ("The proof of Property 3 is quite similar to the proof given for Property 2"). (Contributed by Steve Rodriguez, 25-Nov-2007)

Ref Expression
Hypotheses relogoprlem.1 ⊢ ( ( ( log ‘ 𝐴 ) ∈ ℂ ∧ ( log ‘ 𝐵 ) ∈ ℂ ) → ( exp ‘ ( ( log ‘ 𝐴 ) 𝐹 ( log ‘ 𝐵 ) ) ) = ( ( exp ‘ ( log ‘ 𝐴 ) ) 𝐺 ( exp ‘ ( log ‘ 𝐵 ) ) ) )
relogoprlem.2 ⊢ ( ( ( log ‘ 𝐴 ) ∈ ℝ ∧ ( log ‘ 𝐵 ) ∈ ℝ ) → ( ( log ‘ 𝐴 ) 𝐹 ( log ‘ 𝐵 ) ) ∈ ℝ )
Assertion relogoprlem ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) → ( log ‘ ( 𝐴 𝐺 𝐵 ) ) = ( ( log ‘ 𝐴 ) 𝐹 ( log ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 relogoprlem.1 ⊢ ( ( ( log ‘ 𝐴 ) ∈ ℂ ∧ ( log ‘ 𝐵 ) ∈ ℂ ) → ( exp ‘ ( ( log ‘ 𝐴 ) 𝐹 ( log ‘ 𝐵 ) ) ) = ( ( exp ‘ ( log ‘ 𝐴 ) ) 𝐺 ( exp ‘ ( log ‘ 𝐵 ) ) ) )
2 relogoprlem.2 ⊢ ( ( ( log ‘ 𝐴 ) ∈ ℝ ∧ ( log ‘ 𝐵 ) ∈ ℝ ) → ( ( log ‘ 𝐴 ) 𝐹 ( log ‘ 𝐵 ) ) ∈ ℝ )
3 reeflog ⊢ ( 𝐴 ∈ ℝ+ → ( exp ‘ ( log ‘ 𝐴 ) ) = 𝐴 )
4 reeflog ⊢ ( 𝐵 ∈ ℝ+ → ( exp ‘ ( log ‘ 𝐵 ) ) = 𝐵 )
5 3 4 oveqan12d ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) → ( ( exp ‘ ( log ‘ 𝐴 ) ) 𝐺 ( exp ‘ ( log ‘ 𝐵 ) ) ) = ( 𝐴 𝐺 𝐵 ) )
6 5 fveq2d ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) → ( log ‘ ( ( exp ‘ ( log ‘ 𝐴 ) ) 𝐺 ( exp ‘ ( log ‘ 𝐵 ) ) ) ) = ( log ‘ ( 𝐴 𝐺 𝐵 ) ) )
7 relogcl ⊢ ( 𝐴 ∈ ℝ+ → ( log ‘ 𝐴 ) ∈ ℝ )
8 relogcl ⊢ ( 𝐵 ∈ ℝ+ → ( log ‘ 𝐵 ) ∈ ℝ )
9 recn ⊢ ( ( log ‘ 𝐴 ) ∈ ℝ → ( log ‘ 𝐴 ) ∈ ℂ )
10 recn ⊢ ( ( log ‘ 𝐵 ) ∈ ℝ → ( log ‘ 𝐵 ) ∈ ℂ )
11 1 fveq2d ⊢ ( ( ( log ‘ 𝐴 ) ∈ ℂ ∧ ( log ‘ 𝐵 ) ∈ ℂ ) → ( log ‘ ( exp ‘ ( ( log ‘ 𝐴 ) 𝐹 ( log ‘ 𝐵 ) ) ) ) = ( log ‘ ( ( exp ‘ ( log ‘ 𝐴 ) ) 𝐺 ( exp ‘ ( log ‘ 𝐵 ) ) ) ) )
12 9 10 11 syl2an ⊢ ( ( ( log ‘ 𝐴 ) ∈ ℝ ∧ ( log ‘ 𝐵 ) ∈ ℝ ) → ( log ‘ ( exp ‘ ( ( log ‘ 𝐴 ) 𝐹 ( log ‘ 𝐵 ) ) ) ) = ( log ‘ ( ( exp ‘ ( log ‘ 𝐴 ) ) 𝐺 ( exp ‘ ( log ‘ 𝐵 ) ) ) ) )
13 relogef ⊢ ( ( ( log ‘ 𝐴 ) 𝐹 ( log ‘ 𝐵 ) ) ∈ ℝ → ( log ‘ ( exp ‘ ( ( log ‘ 𝐴 ) 𝐹 ( log ‘ 𝐵 ) ) ) ) = ( ( log ‘ 𝐴 ) 𝐹 ( log ‘ 𝐵 ) ) )
14 2 13 syl ⊢ ( ( ( log ‘ 𝐴 ) ∈ ℝ ∧ ( log ‘ 𝐵 ) ∈ ℝ ) → ( log ‘ ( exp ‘ ( ( log ‘ 𝐴 ) 𝐹 ( log ‘ 𝐵 ) ) ) ) = ( ( log ‘ 𝐴 ) 𝐹 ( log ‘ 𝐵 ) ) )
15 12 14 eqtr3d ⊢ ( ( ( log ‘ 𝐴 ) ∈ ℝ ∧ ( log ‘ 𝐵 ) ∈ ℝ ) → ( log ‘ ( ( exp ‘ ( log ‘ 𝐴 ) ) 𝐺 ( exp ‘ ( log ‘ 𝐵 ) ) ) ) = ( ( log ‘ 𝐴 ) 𝐹 ( log ‘ 𝐵 ) ) )
16 7 8 15 syl2an ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) → ( log ‘ ( ( exp ‘ ( log ‘ 𝐴 ) ) 𝐺 ( exp ‘ ( log ‘ 𝐵 ) ) ) ) = ( ( log ‘ 𝐴 ) 𝐹 ( log ‘ 𝐵 ) ) )
17 6 16 eqtr3d ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) → ( log ‘ ( 𝐴 𝐺 𝐵 ) ) = ( ( log ‘ 𝐴 ) 𝐹 ( log ‘ 𝐵 ) ) )