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