Metamath Proof Explorer

Theorem cxplogb

Description: Identity law for the general logarithm. (Contributed by AV, 22-May-2020)

Ref Expression
Assertion cxplogb ⊢B∈ℂ∖01∧X∈ℂ∖0→BlogBX=X

Proof

Step Hyp Ref Expression
1 logbval ⊢B∈ℂ∖01∧X∈ℂ∖0→logBX=log⁡Xlog⁡B
2 1 oveq2d ⊢B∈ℂ∖01∧X∈ℂ∖0→BlogBX=Blog⁡Xlog⁡B
3 eldifi ⊢B∈ℂ∖01→B∈ℂ
4 3 adantr ⊢B∈ℂ∖01∧X∈ℂ∖0→B∈ℂ
5 eldif ⊢B∈ℂ∖01↔B∈ℂ∧¬B∈01
6 c0ex ⊢0∈V
7 6 prid1 ⊢0∈01
8 eleq1 ⊢B=0→B∈01↔0∈01
9 7 8 mpbiri ⊢B=0→B∈01
10 9 necon3bi ⊢¬B∈01→B≠0
11 10 adantl ⊢B∈ℂ∧¬B∈01→B≠0
12 5 11 sylbi ⊢B∈ℂ∖01→B≠0
13 12 adantr ⊢B∈ℂ∖01∧X∈ℂ∖0→B≠0
14 eldif ⊢X∈ℂ∖0↔X∈ℂ∧¬X∈0
15 6 snid ⊢0∈0
16 eleq1 ⊢X=0→X∈0↔0∈0
17 15 16 mpbiri ⊢X=0→X∈0
18 17 necon3bi ⊢¬X∈0→X≠0
19 18 anim2i ⊢X∈ℂ∧¬X∈0→X∈ℂ∧X≠0
20 14 19 sylbi ⊢X∈ℂ∖0→X∈ℂ∧X≠0
21 logcl ⊢X∈ℂ∧X≠0→log⁡X∈ℂ
22 20 21 syl ⊢X∈ℂ∖0→log⁡X∈ℂ
23 22 adantl ⊢B∈ℂ∖01∧X∈ℂ∖0→log⁡X∈ℂ
24 10 anim2i ⊢B∈ℂ∧¬B∈01→B∈ℂ∧B≠0
25 5 24 sylbi ⊢B∈ℂ∖01→B∈ℂ∧B≠0
26 logcl ⊢B∈ℂ∧B≠0→log⁡B∈ℂ
27 25 26 syl ⊢B∈ℂ∖01→log⁡B∈ℂ
28 27 adantr ⊢B∈ℂ∖01∧X∈ℂ∖0→log⁡B∈ℂ
29 eldifpr ⊢B∈ℂ∖01↔B∈ℂ∧B≠0∧B≠1
30 29 biimpi ⊢B∈ℂ∖01→B∈ℂ∧B≠0∧B≠1
31 30 adantr ⊢B∈ℂ∖01∧X∈ℂ∖0→B∈ℂ∧B≠0∧B≠1
32 logccne0 ⊢B∈ℂ∧B≠0∧B≠1→log⁡B≠0
33 31 32 syl ⊢B∈ℂ∖01∧X∈ℂ∖0→log⁡B≠0
34 23 28 33 divcld ⊢B∈ℂ∖01∧X∈ℂ∖0→log⁡Xlog⁡B∈ℂ
35 4 13 34 cxpefd ⊢B∈ℂ∖01∧X∈ℂ∖0→Blog⁡Xlog⁡B=elog⁡Xlog⁡B⁢log⁡B
36 eldifsn ⊢X∈ℂ∖0↔X∈ℂ∧X≠0
37 36 21 sylbi ⊢X∈ℂ∖0→log⁡X∈ℂ
38 37 adantl ⊢B∈ℂ∖01∧X∈ℂ∖0→log⁡X∈ℂ
39 29 32 sylbi ⊢B∈ℂ∖01→log⁡B≠0
40 39 adantr ⊢B∈ℂ∖01∧X∈ℂ∖0→log⁡B≠0
41 38 28 40 divcan1d ⊢B∈ℂ∖01∧X∈ℂ∖0→log⁡Xlog⁡B⁢log⁡B=log⁡X
42 41 fveq2d ⊢B∈ℂ∖01∧X∈ℂ∖0→elog⁡Xlog⁡B⁢log⁡B=elog⁡X
43 eflog ⊢X∈ℂ∧X≠0→elog⁡X=X
44 36 43 sylbi ⊢X∈ℂ∖0→elog⁡X=X
45 44 adantl ⊢B∈ℂ∖01∧X∈ℂ∖0→elog⁡X=X
46 42 45 eqtrd ⊢B∈ℂ∖01∧X∈ℂ∖0→elog⁡Xlog⁡B⁢log⁡B=X
47 2 35 46 3eqtrd ⊢B∈ℂ∖01∧X∈ℂ∖0→BlogBX=X