Description: A number in the continuous domain of log is nonzero. (Contributed by Mario Carneiro, 18-Feb-2015)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | logcn.d | ⊢ 𝐷 = ( ℂ ∖ ( -∞ (,] 0 ) ) | |
| Assertion | logdmn0 | ⊢ ( 𝐴 ∈ 𝐷 → 𝐴 ≠ 0 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | logcn.d | ⊢ 𝐷 = ( ℂ ∖ ( -∞ (,] 0 ) ) | |
| 2 | 0nrp | ⊢ ¬ 0 ∈ ℝ+ | |
| 3 | 0re | ⊢ 0 ∈ ℝ | |
| 4 | 1 | ellogdm | ⊢ ( 0 ∈ 𝐷 ↔ ( 0 ∈ ℂ ∧ ( 0 ∈ ℝ → 0 ∈ ℝ+ ) ) ) |
| 5 | 4 | simprbi | ⊢ ( 0 ∈ 𝐷 → ( 0 ∈ ℝ → 0 ∈ ℝ+ ) ) |
| 6 | 3 5 | mpi | ⊢ ( 0 ∈ 𝐷 → 0 ∈ ℝ+ ) |
| 7 | 2 6 | mto | ⊢ ¬ 0 ∈ 𝐷 |
| 8 | eleq1 | ⊢ ( 𝐴 = 0 → ( 𝐴 ∈ 𝐷 ↔ 0 ∈ 𝐷 ) ) | |
| 9 | 7 8 | mtbiri | ⊢ ( 𝐴 = 0 → ¬ 𝐴 ∈ 𝐷 ) |
| 10 | 9 | necon2ai | ⊢ ( 𝐴 ∈ 𝐷 → 𝐴 ≠ 0 ) |