Metamath Proof Explorer

Theorem 1div0OLD

Description: Obsolete version of 1div0 as of 5-Jun-2025. (Contributed by Mario Carneiro, 1-Apr-2014) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion 1div0OLD 
|- ( 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 ) = (/)