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 ⊢B∈ℂ∖01∧C∈ℝ+∧E∈ℝ→logBCE=E⁢logBC

Proof

Step Hyp Ref Expression
1 logcxp ⊢C∈ℝ+∧E∈ℝ→log⁡CE=E⁢log⁡C
2 1 3adant1 ⊢B∈ℂ∖01∧C∈ℝ+∧E∈ℝ→log⁡CE=E⁢log⁡C
3 2 oveq1d ⊢B∈ℂ∖01∧C∈ℝ+∧E∈ℝ→log⁡CElog⁡B=E⁢log⁡Clog⁡B
4 recn ⊢E∈ℝ→E∈ℂ
5 4 3ad2ant3 ⊢B∈ℂ∖01∧C∈ℝ+∧E∈ℝ→E∈ℂ
6 rpcn ⊢C∈ℝ+→C∈ℂ
7 rpne0 ⊢C∈ℝ+→C≠0
8 6 7 logcld ⊢C∈ℝ+→log⁡C∈ℂ
9 8 3ad2ant2 ⊢B∈ℂ∖01∧C∈ℝ+∧E∈ℝ→log⁡C∈ℂ
10 eldifi ⊢B∈ℂ∖01→B∈ℂ
11 eldifpr ⊢B∈ℂ∖01↔B∈ℂ∧B≠0∧B≠1
12 11 simp2bi ⊢B∈ℂ∖01→B≠0
13 10 12 logcld ⊢B∈ℂ∖01→log⁡B∈ℂ
14 logccne0 ⊢B∈ℂ∧B≠0∧B≠1→log⁡B≠0
15 11 14 sylbi ⊢B∈ℂ∖01→log⁡B≠0
16 13 15 jca ⊢B∈ℂ∖01→log⁡B∈ℂ∧log⁡B≠0
17 16 3ad2ant1 ⊢B∈ℂ∖01∧C∈ℝ+∧E∈ℝ→log⁡B∈ℂ∧log⁡B≠0
18 divass ⊢E∈ℂ∧log⁡C∈ℂ∧log⁡B∈ℂ∧log⁡B≠0→E⁢log⁡Clog⁡B=E⁢log⁡Clog⁡B
19 5 9 17 18 syl3anc ⊢B∈ℂ∖01∧C∈ℝ+∧E∈ℝ→E⁢log⁡Clog⁡B=E⁢log⁡Clog⁡B
20 3 19 eqtrd ⊢B∈ℂ∖01∧C∈ℝ+∧E∈ℝ→log⁡CElog⁡B=E⁢log⁡Clog⁡B
21 simp1 ⊢B∈ℂ∖01∧C∈ℝ+∧E∈ℝ→B∈ℂ∖01
22 6 adantr ⊢C∈ℝ+∧E∈ℝ→C∈ℂ
23 4 adantl ⊢C∈ℝ+∧E∈ℝ→E∈ℂ
24 22 23 cxpcld ⊢C∈ℝ+∧E∈ℝ→CE∈ℂ
25 7 adantr ⊢C∈ℝ+∧E∈ℝ→C≠0
26 22 25 23 cxpne0d ⊢C∈ℝ+∧E∈ℝ→CE≠0
27 eldifsn ⊢CE∈ℂ∖0↔CE∈ℂ∧CE≠0
28 24 26 27 sylanbrc ⊢C∈ℝ+∧E∈ℝ→CE∈ℂ∖0
29 28 3adant1 ⊢B∈ℂ∖01∧C∈ℝ+∧E∈ℝ→CE∈ℂ∖0
30 logbval ⊢B∈ℂ∖01∧CE∈ℂ∖0→logBCE=log⁡CElog⁡B
31 21 29 30 syl2anc ⊢B∈ℂ∖01∧C∈ℝ+∧E∈ℝ→logBCE=log⁡CElog⁡B
32 rpcndif0 ⊢C∈ℝ+→C∈ℂ∖0
33 32 anim2i ⊢B∈ℂ∖01∧C∈ℝ+→B∈ℂ∖01∧C∈ℂ∖0
34 33 3adant3 ⊢B∈ℂ∖01∧C∈ℝ+∧E∈ℝ→B∈ℂ∖01∧C∈ℂ∖0
35 logbval ⊢B∈ℂ∖01∧C∈ℂ∖0→logBC=log⁡Clog⁡B
36 34 35 syl ⊢B∈ℂ∖01∧C∈ℝ+∧E∈ℝ→logBC=log⁡Clog⁡B
37 36 oveq2d ⊢B∈ℂ∖01∧C∈ℝ+∧E∈ℝ→E⁢logBC=E⁢log⁡Clog⁡B
38 20 31 37 3eqtr4d ⊢B∈ℂ∖01∧C∈ℝ+∧E∈ℝ→logBCE=E⁢logBC