relogbreexp

Description: Power law for the general logarithm for real powers: The logarithm of a positive real number to the power of a real number is equal to the product of the exponent and the logarithm of the base of the power. Property 4 of Cohen4 p. 361. (Contributed by AV, 9-Jun-2020)

		Ref	Expression
	Assertion	relogbreexp	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land C \in ℝ^{+} \land E \in ℝ) \to \log_{B} C^{E} = E \log_{B} C$

Proof

Step	Hyp	Ref	Expression
1		logcxp	$⊢ (C \in ℝ^{+} \land E \in ℝ) \to \log C^{E} = E \log C$
2	1	3adant1	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land C \in ℝ^{+} \land E \in ℝ) \to \log C^{E} = E \log C$
3	2	oveq1d	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land C \in ℝ^{+} \land E \in ℝ) \to \frac{\log C^{E}}{\log B} = \frac{E \log C}{\log B}$
4		recn	$⊢ E \in ℝ \to E \in ℂ$
5	4	3ad2ant3	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land C \in ℝ^{+} \land E \in ℝ) \to E \in ℂ$
6		rpcn	$⊢ C \in ℝ^{+} \to C \in ℂ$
7		rpne0	$⊢ C \in ℝ^{+} \to C \neq 0$
8	6 7	logcld	$⊢ C \in ℝ^{+} \to \log C \in ℂ$
9	8	3ad2ant2	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land C \in ℝ^{+} \land E \in ℝ) \to \log C \in ℂ$
10		eldifi	$⊢ B \in (ℂ ∖ \{0, 1\}) \to B \in ℂ$
11		eldifpr	$⊢ B \in (ℂ ∖ \{0, 1\}) \leftrightarrow (B \in ℂ \land B \neq 0 \land B \neq 1)$
12	11	simp2bi	$⊢ B \in (ℂ ∖ \{0, 1\}) \to B \neq 0$
13	10 12	logcld	$⊢ B \in (ℂ ∖ \{0, 1\}) \to \log B \in ℂ$
14		logccne0	$⊢ (B \in ℂ \land B \neq 0 \land B \neq 1) \to \log B \neq 0$
15	11 14	sylbi	$⊢ B \in (ℂ ∖ \{0, 1\}) \to \log B \neq 0$
16	13 15	jca	$⊢ B \in (ℂ ∖ \{0, 1\}) \to (\log B \in ℂ \land \log B \neq 0)$
17	16	3ad2ant1	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land C \in ℝ^{+} \land E \in ℝ) \to (\log B \in ℂ \land \log B \neq 0)$
18		divass	$⊢ (E \in ℂ \land \log C \in ℂ \land (\log B \in ℂ \land \log B \neq 0)) \to \frac{E \log C}{\log B} = E (\frac{\log C}{\log B})$
19	5 9 17 18	syl3anc	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land C \in ℝ^{+} \land E \in ℝ) \to \frac{E \log C}{\log B} = E (\frac{\log C}{\log B})$
20	3 19	eqtrd	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land C \in ℝ^{+} \land E \in ℝ) \to \frac{\log C^{E}}{\log B} = E (\frac{\log C}{\log B})$
21		simp1	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land C \in ℝ^{+} \land E \in ℝ) \to B \in (ℂ ∖ \{0, 1\})$
22	6	adantr	$⊢ (C \in ℝ^{+} \land E \in ℝ) \to C \in ℂ$
23	4	adantl	$⊢ (C \in ℝ^{+} \land E \in ℝ) \to E \in ℂ$
24	22 23	cxpcld	$⊢ (C \in ℝ^{+} \land E \in ℝ) \to C^{E} \in ℂ$
25	7	adantr	$⊢ (C \in ℝ^{+} \land E \in ℝ) \to C \neq 0$
26	22 25 23	cxpne0d	$⊢ (C \in ℝ^{+} \land E \in ℝ) \to C^{E} \neq 0$
27		eldifsn	$⊢ C^{E} \in (ℂ ∖ \{0\}) \leftrightarrow (C^{E} \in ℂ \land C^{E} \neq 0)$
28	24 26 27	sylanbrc	$⊢ (C \in ℝ^{+} \land E \in ℝ) \to C^{E} \in (ℂ ∖ \{0\})$
29	28	3adant1	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land C \in ℝ^{+} \land E \in ℝ) \to C^{E} \in (ℂ ∖ \{0\})$
30		logbval	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land C^{E} \in (ℂ ∖ \{0\})) \to \log_{B} C^{E} = \frac{\log C^{E}}{\log B}$
31	21 29 30	syl2anc	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land C \in ℝ^{+} \land E \in ℝ) \to \log_{B} C^{E} = \frac{\log C^{E}}{\log B}$
32		rpcndif0	$⊢ C \in ℝ^{+} \to C \in (ℂ ∖ \{0\})$
33	32	anim2i	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land C \in ℝ^{+}) \to (B \in (ℂ ∖ \{0, 1\}) \land C \in (ℂ ∖ \{0\}))$
34	33	3adant3	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land C \in ℝ^{+} \land E \in ℝ) \to (B \in (ℂ ∖ \{0, 1\}) \land C \in (ℂ ∖ \{0\}))$
35		logbval	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land C \in (ℂ ∖ \{0\})) \to \log_{B} C = \frac{\log C}{\log B}$
36	34 35	syl	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land C \in ℝ^{+} \land E \in ℝ) \to \log_{B} C = \frac{\log C}{\log B}$
37	36	oveq2d	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land C \in ℝ^{+} \land E \in ℝ) \to E \log_{B} C = E (\frac{\log C}{\log B})$
38	20 31 37	3eqtr4d	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land C \in ℝ^{+} \land E \in ℝ) \to \log_{B} C^{E} = E \log_{B} C$

Metamath Proof Explorer

Theorem relogbreexp

Proof