Theorem 1div0

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 ) = ∅

Proof

Step	Hyp	Ref	Expression
1		df-div	⊢ / = ( 𝑥 ∈ ℂ , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℩ 𝑧 ∈ ℂ ( 𝑦 · 𝑧 ) = 𝑥 ) )
2		riotaex	⊢ ( ℩ 𝑧 ∈ ℂ ( 𝑦 · 𝑧 ) = 𝑥 ) ∈ V
3	1 2	dmmpo	⊢ dom / = ( ℂ × ( ℂ ∖ { 0 } ) )
4		eqid	⊢ 0 = 0
5		eldifsni	⊢ ( 0 ∈ ( ℂ ∖ { 0 } ) → 0 ≠ 0 )
6	5	adantl	⊢ ( ( 1 ∈ ℂ ∧ 0 ∈ ( ℂ ∖ { 0 } ) ) → 0 ≠ 0 )
7	6	necon2bi	⊢ ( 0 = 0 → ¬ ( 1 ∈ ℂ ∧ 0 ∈ ( ℂ ∖ { 0 } ) ) )
8	4 7	ax-mp	⊢ ¬ ( 1 ∈ ℂ ∧ 0 ∈ ( ℂ ∖ { 0 } ) )
9		ndmovg	⊢ ( ( dom / = ( ℂ × ( ℂ ∖ { 0 } ) ) ∧ ¬ ( 1 ∈ ℂ ∧ 0 ∈ ( ℂ ∖ { 0 } ) ) ) → ( 1 / 0 ) = ∅ )
10	3 8 9	mp2an	⊢ ( 1 / 0 ) = ∅