Description: You can't divide by zero, because division explicitly excludes zero from the domain of the function. Thus, by the definition of function value, it evaluates to the empty set. (This theorem is for information only and normally is not referenced by other proofs. To be meaningful, it assumes that (/) is not a complex number, which depends on the particular complex number construction that is used.) (Contributed by Mario Carneiro, 1-Apr-2014) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | 1div0 | |- ( 1 / 0 ) = (/) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-div | |- / = ( x e. CC , y e. ( CC \ { 0 } ) |-> ( iota_ z e. CC ( y x. z ) = x ) ) |
|
| 2 | riotaex | |- ( iota_ z e. CC ( y x. z ) = x ) e. _V |
|
| 3 | 1 2 | dmmpo | |- dom / = ( CC X. ( CC \ { 0 } ) ) |
| 4 | eqid | |- 0 = 0 |
|
| 5 | eldifsni | |- ( 0 e. ( CC \ { 0 } ) -> 0 =/= 0 ) |
|
| 6 | 5 | adantl | |- ( ( 1 e. CC /\ 0 e. ( CC \ { 0 } ) ) -> 0 =/= 0 ) |
| 7 | 6 | necon2bi | |- ( 0 = 0 -> -. ( 1 e. CC /\ 0 e. ( CC \ { 0 } ) ) ) |
| 8 | 4 7 | ax-mp | |- -. ( 1 e. CC /\ 0 e. ( CC \ { 0 } ) ) |
| 9 | ndmovg | |- ( ( dom / = ( CC X. ( CC \ { 0 } ) ) /\ -. ( 1 e. CC /\ 0 e. ( CC \ { 0 } ) ) ) -> ( 1 / 0 ) = (/) ) |
|
| 10 | 3 8 9 | mp2an | |- ( 1 / 0 ) = (/) |