This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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