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	⊢ / = ( 𝑥 ∈ ℂ , 𝑦 ∈ ( ℂ ∖ { 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 ) = ∅