Description: A number in the continuous domain of log is nonzero. (Contributed by Mario Carneiro, 18-Feb-2015)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | logcn.d | |- D = ( CC \ ( -oo (,] 0 ) ) |
|
| Assertion | logdmn0 | |- ( A e. D -> A =/= 0 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | logcn.d | |- D = ( CC \ ( -oo (,] 0 ) ) |
|
| 2 | 0nrp | |- -. 0 e. RR+ |
|
| 3 | 0re | |- 0 e. RR |
|
| 4 | 1 | ellogdm | |- ( 0 e. D <-> ( 0 e. CC /\ ( 0 e. RR -> 0 e. RR+ ) ) ) |
| 5 | 4 | simprbi | |- ( 0 e. D -> ( 0 e. RR -> 0 e. RR+ ) ) |
| 6 | 3 5 | mpi | |- ( 0 e. D -> 0 e. RR+ ) |
| 7 | 2 6 | mto | |- -. 0 e. D |
| 8 | eleq1 | |- ( A = 0 -> ( A e. D <-> 0 e. D ) ) |
|
| 9 | 7 8 | mtbiri | |- ( A = 0 -> -. A e. D ) |
| 10 | 9 | necon2ai | |- ( A e. D -> A =/= 0 ) |