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	$$⊢\frac{1}{0}=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		df-div	$$⊢÷=\left(x\in ℂ,y\in \left(ℂ\setminus \left\{0\right\}\right)⟼\left(\iota z\in ℂ|yz=x\right)\right)$$
2		riotaex	$$⊢\left(\iota z\in ℂ|yz=x\right)\in \mathrm{V}$$
3	1 2	dmmpo	$$⊢\mathrm{dom}÷=ℂ\times \left(ℂ\setminus \left\{0\right\}\right)$$
4		eqid	$$⊢0=0$$
5		eldifsni	$$⊢0\in \left(ℂ\setminus \left\{0\right\}\right)\to 0\ne 0$$
6	5	adantl	$$⊢\left(1\in ℂ\wedge 0\in \left(ℂ\setminus \left\{0\right\}\right)\right)\to 0\ne 0$$
7	6	necon2bi	$$⊢0=0\to \neg \left(1\in ℂ\wedge 0\in \left(ℂ\setminus \left\{0\right\}\right)\right)$$
8	4 7	ax-mp	$$⊢\neg \left(1\in ℂ\wedge 0\in \left(ℂ\setminus \left\{0\right\}\right)\right)$$
9		ndmovg	$$⊢\left(\mathrm{dom}÷=ℂ\times \left(ℂ\setminus \left\{0\right\}\right)\wedge \neg \left(1\in ℂ\wedge 0\in \left(ℂ\setminus \left\{0\right\}\right)\right)\right)\to \frac{1}{0}=\varnothing$$
10	3 8 9	mp2an	$$⊢\frac{1}{0}=\varnothing$$