Description: The continuity domain of log is a subset of the regular domain of log . (Contributed by Mario Carneiro, 1-Mar-2015)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | logcn.d | |- D = ( CC \ ( -oo (,] 0 ) ) |
|
| Assertion | logdmss | |- D C_ ( CC \ { 0 } ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | logcn.d | |- D = ( CC \ ( -oo (,] 0 ) ) |
|
| 2 | 1 | ellogdm | |- ( x e. D <-> ( x e. CC /\ ( x e. RR -> x e. RR+ ) ) ) |
| 3 | 2 | simplbi | |- ( x e. D -> x e. CC ) |
| 4 | 1 | logdmn0 | |- ( x e. D -> x =/= 0 ) |
| 5 | eldifsn | |- ( x e. ( CC \ { 0 } ) <-> ( x e. CC /\ x =/= 0 ) ) |
|
| 6 | 3 4 5 | sylanbrc | |- ( x e. D -> x e. ( CC \ { 0 } ) ) |
| 7 | 6 | ssriv | |- D C_ ( CC \ { 0 } ) |