Metamath Proof Explorer

Theorem logbcl

Description: General logarithm closure. (Contributed by David A. Wheeler, 17-Jul-2017)

Ref Expression
Assertion logbcl ⊢ B ∈ ℂ ∖ 0 1 ∧ X ∈ ℂ ∖ 0 → log B X ∈ ℂ

Proof

Step Hyp Ref Expression
1 logbval ⊢ B ∈ ℂ ∖ 0 1 ∧ X ∈ ℂ ∖ 0 → log B X = log ⁡ X log ⁡ B
2 eldifsn ⊢ X ∈ ℂ ∖ 0 ↔ X ∈ ℂ ∧ X ≠ 0
3 logcl ⊢ X ∈ ℂ ∧ X ≠ 0 → log ⁡ X ∈ ℂ
4 2 3 sylbi ⊢ X ∈ ℂ ∖ 0 → log ⁡ X ∈ ℂ
5 4 adantl ⊢ B ∈ ℂ ∖ 0 1 ∧ X ∈ ℂ ∖ 0 → log ⁡ X ∈ ℂ
6 eldifi ⊢ B ∈ ℂ ∖ 0 1 → B ∈ ℂ
7 eldifpr ⊢ B ∈ ℂ ∖ 0 1 ↔ B ∈ ℂ ∧ B ≠ 0 ∧ B ≠ 1
8 7 simp2bi ⊢ B ∈ ℂ ∖ 0 1 → B ≠ 0
9 6 8 logcld ⊢ B ∈ ℂ ∖ 0 1 → log ⁡ B ∈ ℂ
10 9 adantr ⊢ B ∈ ℂ ∖ 0 1 ∧ X ∈ ℂ ∖ 0 → log ⁡ B ∈ ℂ
11 logccne0 ⊢ B ∈ ℂ ∧ B ≠ 0 ∧ B ≠ 1 → log ⁡ B ≠ 0
12 7 11 sylbi ⊢ B ∈ ℂ ∖ 0 1 → log ⁡ B ≠ 0
13 12 adantr ⊢ B ∈ ℂ ∖ 0 1 ∧ X ∈ ℂ ∖ 0 → log ⁡ B ≠ 0
14 5 10 13 divcld ⊢ B ∈ ℂ ∖ 0 1 ∧ X ∈ ℂ ∖ 0 → log ⁡ X log ⁡ B ∈ ℂ
15 1 14 eqeltrd ⊢ B ∈ ℂ ∖ 0 1 ∧ X ∈ ℂ ∖ 0 → log B X ∈ ℂ