Metamath Proof Explorer


Theorem 1div0apr

Description: Division by zero is forbidden! If we try, we encounter the DO NOT ENTER sign, which in mathematics means it is foolhardy to venture any further, possibly putting the underlying fabric of reality at risk. Based on a dare by David A. Wheeler. (Contributed by Mario Carneiro, 1-Apr-2014) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion 1div0apr
|- ( 1 / 0 ) = (/)

Proof

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 ) = (/)