Metamath Proof Explorer


Theorem logne0

Description: Logarithm of a non-1 positive real number is not zero and thus suitable as a divisor. (Contributed by Stefan O'Rear, 19-Sep-2014) (Proof shortened by AV, 14-Jun-2020)

Ref Expression
Assertion logne0 ( ( 𝐴 ∈ ℝ+𝐴 ≠ 1 ) → ( log ‘ 𝐴 ) ≠ 0 )

Proof

Step Hyp Ref Expression
1 rpcn ( 𝐴 ∈ ℝ+𝐴 ∈ ℂ )
2 1 adantr ( ( 𝐴 ∈ ℝ+𝐴 ≠ 1 ) → 𝐴 ∈ ℂ )
3 rpne0 ( 𝐴 ∈ ℝ+𝐴 ≠ 0 )
4 3 adantr ( ( 𝐴 ∈ ℝ+𝐴 ≠ 1 ) → 𝐴 ≠ 0 )
5 simpr ( ( 𝐴 ∈ ℝ+𝐴 ≠ 1 ) → 𝐴 ≠ 1 )
6 logccne0 ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( log ‘ 𝐴 ) ≠ 0 )
7 2 4 5 6 syl3anc ( ( 𝐴 ∈ ℝ+𝐴 ≠ 1 ) → ( log ‘ 𝐴 ) ≠ 0 )