Description: The set of nonzero complex numbers is open with respect to the standard topology on complex numbers. (Contributed by SN, 7-Oct-2025)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | cnn0opn | |- ( CC \ { 0 } ) e. ( TopOpen ` CCfld ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqid | |- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld ) |
|
| 2 | 1 | cnfldhaus | |- ( TopOpen ` CCfld ) e. Haus |
| 3 | 0cn | |- 0 e. CC |
|
| 4 | unicntop | |- CC = U. ( TopOpen ` CCfld ) |
|
| 5 | 4 | sncld | |- ( ( ( TopOpen ` CCfld ) e. Haus /\ 0 e. CC ) -> { 0 } e. ( Clsd ` ( TopOpen ` CCfld ) ) ) |
| 6 | 2 3 5 | mp2an | |- { 0 } e. ( Clsd ` ( TopOpen ` CCfld ) ) |
| 7 | 4 | cldopn | |- ( { 0 } e. ( Clsd ` ( TopOpen ` CCfld ) ) -> ( CC \ { 0 } ) e. ( TopOpen ` CCfld ) ) |
| 8 | 6 7 | ax-mp | |- ( CC \ { 0 } ) e. ( TopOpen ` CCfld ) |