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