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

Metamath Proof Explorer

Theorem logbid1

Description: General logarithm is 1 when base and arg match. Property 1(a) of Cohen4 p. 361. (Contributed by Stefan O'Rear, 19-Sep-2014) (Revised by David A. Wheeler, 22-Jul-2017)

Ref Expression
Assertion logbid1 ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ A ≠ 1 → log A A = 1

Proof

Step Hyp Ref Expression
1 eldifpr ⊢ A ∈ ℂ ∖ 0 1 ↔ A ∈ ℂ ∧ A ≠ 0 ∧ A ≠ 1
2 1 biimpri ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ A ≠ 1 → A ∈ ℂ ∖ 0 1
3 eldifsn ⊢ A ∈ ℂ ∖ 0 ↔ A ∈ ℂ ∧ A ≠ 0
4 3 biimpri ⊢ A ∈ ℂ ∧ A ≠ 0 → A ∈ ℂ ∖ 0
5 4 3adant3 ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ A ≠ 1 → A ∈ ℂ ∖ 0
6 logbval ⊢ A ∈ ℂ ∖ 0 1 ∧ A ∈ ℂ ∖ 0 → log A A = log ⁡ A log ⁡ A
7 2 5 6 syl2anc ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ A ≠ 1 → log A A = log ⁡ A log ⁡ A
8 logcl ⊢ A ∈ ℂ ∧ A ≠ 0 → log ⁡ A ∈ ℂ
9 8 3adant3 ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ A ≠ 1 → log ⁡ A ∈ ℂ
10 logccne0 ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ A ≠ 1 → log ⁡ A ≠ 0
11 9 10 dividd ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ A ≠ 1 → log ⁡ A log ⁡ A = 1
12 7 11 eqtrd ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ A ≠ 1 → log A A = 1