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 ) |
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 ) |