Theorem 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	⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝐶 ∈ ℝ+ ∧ 𝐸 ∈ ℝ ) → ( 𝐵 logb ( 𝐶 ↑𝑐 𝐸 ) ) = ( 𝐸 · ( 𝐵 logb 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		logcxp	⊢ ( ( 𝐶 ∈ ℝ+ ∧ 𝐸 ∈ ℝ ) → ( log ‘ ( 𝐶 ↑𝑐 𝐸 ) ) = ( 𝐸 · ( log ‘ 𝐶 ) ) )
2	1	3adant1	⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝐶 ∈ ℝ+ ∧ 𝐸 ∈ ℝ ) → ( log ‘ ( 𝐶 ↑𝑐 𝐸 ) ) = ( 𝐸 · ( log ‘ 𝐶 ) ) )
3	2	oveq1d	⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝐶 ∈ ℝ+ ∧ 𝐸 ∈ ℝ ) → ( ( log ‘ ( 𝐶 ↑𝑐 𝐸 ) ) / ( log ‘ 𝐵 ) ) = ( ( 𝐸 · ( log ‘ 𝐶 ) ) / ( log ‘ 𝐵 ) ) )
4		recn	⊢ ( 𝐸 ∈ ℝ → 𝐸 ∈ ℂ )
5	4	3ad2ant3	⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝐶 ∈ ℝ+ ∧ 𝐸 ∈ ℝ ) → 𝐸 ∈ ℂ )
6		rpcn	⊢ ( 𝐶 ∈ ℝ+ → 𝐶 ∈ ℂ )
7		rpne0	⊢ ( 𝐶 ∈ ℝ+ → 𝐶 ≠ 0 )
8	6 7	logcld	⊢ ( 𝐶 ∈ ℝ+ → ( log ‘ 𝐶 ) ∈ ℂ )
9	8	3ad2ant2	⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝐶 ∈ ℝ+ ∧ 𝐸 ∈ ℝ ) → ( log ‘ 𝐶 ) ∈ ℂ )
10		eldifi	⊢ ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) → 𝐵 ∈ ℂ )
11		eldifpr	⊢ ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ↔ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) )
12	11	simp2bi	⊢ ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) → 𝐵 ≠ 0 )
13	10 12	logcld	⊢ ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) → ( log ‘ 𝐵 ) ∈ ℂ )
14		logccne0	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) → ( log ‘ 𝐵 ) ≠ 0 )
15	11 14	sylbi	⊢ ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) → ( log ‘ 𝐵 ) ≠ 0 )
16	13 15	jca	⊢ ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) → ( ( log ‘ 𝐵 ) ∈ ℂ ∧ ( log ‘ 𝐵 ) ≠ 0 ) )
17	16	3ad2ant1	⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝐶 ∈ ℝ+ ∧ 𝐸 ∈ ℝ ) → ( ( log ‘ 𝐵 ) ∈ ℂ ∧ ( log ‘ 𝐵 ) ≠ 0 ) )
18		divass	⊢ ( ( 𝐸 ∈ ℂ ∧ ( log ‘ 𝐶 ) ∈ ℂ ∧ ( ( log ‘ 𝐵 ) ∈ ℂ ∧ ( log ‘ 𝐵 ) ≠ 0 ) ) → ( ( 𝐸 · ( log ‘ 𝐶 ) ) / ( log ‘ 𝐵 ) ) = ( 𝐸 · ( ( log ‘ 𝐶 ) / ( log ‘ 𝐵 ) ) ) )
19	5 9 17 18	syl3anc	⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝐶 ∈ ℝ+ ∧ 𝐸 ∈ ℝ ) → ( ( 𝐸 · ( log ‘ 𝐶 ) ) / ( log ‘ 𝐵 ) ) = ( 𝐸 · ( ( log ‘ 𝐶 ) / ( log ‘ 𝐵 ) ) ) )
20	3 19	eqtrd	⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝐶 ∈ ℝ+ ∧ 𝐸 ∈ ℝ ) → ( ( log ‘ ( 𝐶 ↑𝑐 𝐸 ) ) / ( log ‘ 𝐵 ) ) = ( 𝐸 · ( ( log ‘ 𝐶 ) / ( log ‘ 𝐵 ) ) ) )
21		simp1	⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝐶 ∈ ℝ+ ∧ 𝐸 ∈ ℝ ) → 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) )
22	6	adantr	⊢ ( ( 𝐶 ∈ ℝ+ ∧ 𝐸 ∈ ℝ ) → 𝐶 ∈ ℂ )
23	4	adantl	⊢ ( ( 𝐶 ∈ ℝ+ ∧ 𝐸 ∈ ℝ ) → 𝐸 ∈ ℂ )
24	22 23	cxpcld	⊢ ( ( 𝐶 ∈ ℝ+ ∧ 𝐸 ∈ ℝ ) → ( 𝐶 ↑𝑐 𝐸 ) ∈ ℂ )
25	7	adantr	⊢ ( ( 𝐶 ∈ ℝ+ ∧ 𝐸 ∈ ℝ ) → 𝐶 ≠ 0 )
26	22 25 23	cxpne0d	⊢ ( ( 𝐶 ∈ ℝ+ ∧ 𝐸 ∈ ℝ ) → ( 𝐶 ↑𝑐 𝐸 ) ≠ 0 )
27		eldifsn	⊢ ( ( 𝐶 ↑𝑐 𝐸 ) ∈ ( ℂ ∖ { 0 } ) ↔ ( ( 𝐶 ↑𝑐 𝐸 ) ∈ ℂ ∧ ( 𝐶 ↑𝑐 𝐸 ) ≠ 0 ) )
28	24 26 27	sylanbrc	⊢ ( ( 𝐶 ∈ ℝ+ ∧ 𝐸 ∈ ℝ ) → ( 𝐶 ↑𝑐 𝐸 ) ∈ ( ℂ ∖ { 0 } ) )
29	28	3adant1	⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝐶 ∈ ℝ+ ∧ 𝐸 ∈ ℝ ) → ( 𝐶 ↑𝑐 𝐸 ) ∈ ( ℂ ∖ { 0 } ) )
30		logbval	⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ ( 𝐶 ↑𝑐 𝐸 ) ∈ ( ℂ ∖ { 0 } ) ) → ( 𝐵 logb ( 𝐶 ↑𝑐 𝐸 ) ) = ( ( log ‘ ( 𝐶 ↑𝑐 𝐸 ) ) / ( log ‘ 𝐵 ) ) )
31	21 29 30	syl2anc	⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝐶 ∈ ℝ+ ∧ 𝐸 ∈ ℝ ) → ( 𝐵 logb ( 𝐶 ↑𝑐 𝐸 ) ) = ( ( log ‘ ( 𝐶 ↑𝑐 𝐸 ) ) / ( log ‘ 𝐵 ) ) )
32		rpcndif0	⊢ ( 𝐶 ∈ ℝ+ → 𝐶 ∈ ( ℂ ∖ { 0 } ) )
33	32	anim2i	⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝐶 ∈ ℝ+ ) → ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝐶 ∈ ( ℂ ∖ { 0 } ) ) )
34	33	3adant3	⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝐶 ∈ ℝ+ ∧ 𝐸 ∈ ℝ ) → ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝐶 ∈ ( ℂ ∖ { 0 } ) ) )
35		logbval	⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝐶 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝐵 logb 𝐶 ) = ( ( log ‘ 𝐶 ) / ( log ‘ 𝐵 ) ) )
36	34 35	syl	⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝐶 ∈ ℝ+ ∧ 𝐸 ∈ ℝ ) → ( 𝐵 logb 𝐶 ) = ( ( log ‘ 𝐶 ) / ( log ‘ 𝐵 ) ) )
37	36	oveq2d	⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝐶 ∈ ℝ+ ∧ 𝐸 ∈ ℝ ) → ( 𝐸 · ( 𝐵 logb 𝐶 ) ) = ( 𝐸 · ( ( log ‘ 𝐶 ) / ( log ‘ 𝐵 ) ) ) )
38	20 31 37	3eqtr4d	⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝐶 ∈ ℝ+ ∧ 𝐸 ∈ ℝ ) → ( 𝐵 logb ( 𝐶 ↑𝑐 𝐸 ) ) = ( 𝐸 · ( 𝐵 logb 𝐶 ) ) )