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 A \in ℂ \land \log B \in ℂ) \to e^{\log A F \log B} = e^{\log A} G e^{\log B}$
		relogoprlem.2	$⊢ (\log A \in ℝ \land \log B \in ℝ) \to \log A F \log B \in ℝ$
	Assertion	relogoprlem	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+}) \to \log (A G B) = \log A F \log B$

Proof

Step	Hyp	Ref	Expression
1		relogoprlem.1	$⊢ (\log A \in ℂ \land \log B \in ℂ) \to e^{\log A F \log B} = e^{\log A} G e^{\log B}$
2		relogoprlem.2	$⊢ (\log A \in ℝ \land \log B \in ℝ) \to \log A F \log B \in ℝ$
3		reeflog	$⊢ A \in ℝ^{+} \to e^{\log A} = A$
4		reeflog	$⊢ B \in ℝ^{+} \to e^{\log B} = B$
5	3 4	oveqan12d	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+}) \to e^{\log A} G e^{\log B} = A G B$
6	5	fveq2d	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+}) \to \log (e^{\log A} G e^{\log B}) = \log (A G B)$
7		relogcl	$⊢ A \in ℝ^{+} \to \log A \in ℝ$
8		relogcl	$⊢ B \in ℝ^{+} \to \log B \in ℝ$
9		recn	$⊢ \log A \in ℝ \to \log A \in ℂ$
10		recn	$⊢ \log B \in ℝ \to \log B \in ℂ$
11	1	fveq2d	$⊢ (\log A \in ℂ \land \log B \in ℂ) \to \log e^{\log A F \log B} = \log (e^{\log A} G e^{\log B})$
12	9 10 11	syl2an	$⊢ (\log A \in ℝ \land \log B \in ℝ) \to \log e^{\log A F \log B} = \log (e^{\log A} G e^{\log B})$
13		relogef	$⊢ \log A F \log B \in ℝ \to \log e^{\log A F \log B} = \log A F \log B$
14	2 13	syl	$⊢ (\log A \in ℝ \land \log B \in ℝ) \to \log e^{\log A F \log B} = \log A F \log B$
15	12 14	eqtr3d	$⊢ (\log A \in ℝ \land \log B \in ℝ) \to \log (e^{\log A} G e^{\log B}) = \log A F \log B$
16	7 8 15	syl2an	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+}) \to \log (e^{\log A} G e^{\log B}) = \log A F \log B$
17	6 16	eqtr3d	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+}) \to \log (A G B) = \log A F \log B$