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