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	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 𝐴 logb 𝐴 ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		eldifpr	⊢ ( 𝐴 ∈ ( ℂ ∖ { 0 , 1 } ) ↔ ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) )
2	1	biimpri	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → 𝐴 ∈ ( ℂ ∖ { 0 , 1 } ) )
3		eldifsn	⊢ ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) )
4	3	biimpri	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → 𝐴 ∈ ( ℂ ∖ { 0 } ) )
5	4	3adant3	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → 𝐴 ∈ ( ℂ ∖ { 0 } ) )
6		logbval	⊢ ( ( 𝐴 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝐴 logb 𝐴 ) = ( ( log ‘ 𝐴 ) / ( log ‘ 𝐴 ) ) )
7	2 5 6	syl2anc	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 𝐴 logb 𝐴 ) = ( ( log ‘ 𝐴 ) / ( log ‘ 𝐴 ) ) )
8		logcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( log ‘ 𝐴 ) ∈ ℂ )
9	8	3adant3	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( log ‘ 𝐴 ) ∈ ℂ )
10		logccne0	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( log ‘ 𝐴 ) ≠ 0 )
11	9 10	dividd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( log ‘ 𝐴 ) / ( log ‘ 𝐴 ) ) = 1 )
12	7 11	eqtrd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 𝐴 logb 𝐴 ) = 1 )