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

Metamath Proof Explorer

Theorem elogb

Description: The general logarithm of a number to the base being Euler's constant is the natural logarithm of the number. Put another way, using _e as the base in logb is the same as log . Definition in Cohen4 p. 352. (Contributed by David A. Wheeler, 17-Oct-2017) (Revised by David A. Wheeler and AV, 16-Jun-2020)

Ref Expression
Assertion elogb ⊢ A ∈ ℂ ∖ 0 → log e A = log ⁡ A

Proof

Step Hyp Ref Expression
1 ere ⊢ e ∈ ℝ
2 1 recni ⊢ e ∈ ℂ
3 ene0 ⊢ e ≠ 0
4 ene1 ⊢ e ≠ 1
5 eldifpr ⊢ e ∈ ℂ ∖ 0 1 ↔ e ∈ ℂ ∧ e ≠ 0 ∧ e ≠ 1
6 2 3 4 5 mpbir3an ⊢ e ∈ ℂ ∖ 0 1
7 logbval ⊢ e ∈ ℂ ∖ 0 1 ∧ A ∈ ℂ ∖ 0 → log e A = log ⁡ A log ⁡ e
8 6 7 mpan ⊢ A ∈ ℂ ∖ 0 → log e A = log ⁡ A log ⁡ e
9 loge ⊢ log ⁡ e = 1
10 9 oveq2i ⊢ log ⁡ A log ⁡ e = log ⁡ A 1
11 eldifsn ⊢ A ∈ ℂ ∖ 0 ↔ A ∈ ℂ ∧ A ≠ 0
12 logcl ⊢ A ∈ ℂ ∧ A ≠ 0 → log ⁡ A ∈ ℂ
13 11 12 sylbi ⊢ A ∈ ℂ ∖ 0 → log ⁡ A ∈ ℂ
14 13 div1d ⊢ A ∈ ℂ ∖ 0 → log ⁡ A 1 = log ⁡ A
15 10 14 eqtrid ⊢ A ∈ ℂ ∖ 0 → log ⁡ A log ⁡ e = log ⁡ A
16 8 15 eqtrd ⊢ A ∈ ℂ ∖ 0 → log e A = log ⁡ A