Metamath Proof Explorer


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 𝐶 ) ) )