This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

Step	Hyp	Ref	Expression
1		df-div	$⊢ \div = (x \in ℂ, y \in (ℂ ∖ \{0\}) ⟼ (ι z \in ℂ \| y z = x))$
2		riotaex	$⊢ (ι z \in ℂ \| y z = x) \in V$
3	1 2	dmmpo	$⊢ dom \div = ℂ \times (ℂ ∖ \{0\})$
4		eqid	$⊢ 0 = 0$
5		eldifsni	$⊢ 0 \in (ℂ ∖ \{0\}) \to 0 \neq 0$
6	5	adantl	$⊢ (1 \in ℂ \land 0 \in (ℂ ∖ \{0\})) \to 0 \neq 0$
7	6	necon2bi	$⊢ 0 = 0 \to \neg (1 \in ℂ \land 0 \in (ℂ ∖ \{0\}))$
8	4 7	ax-mp	$⊢ \neg (1 \in ℂ \land 0 \in (ℂ ∖ \{0\}))$
9		ndmovg	$⊢ (dom \div = ℂ \times (ℂ ∖ \{0\}) \land \neg (1 \in ℂ \land 0 \in (ℂ ∖ \{0\}))) \to \frac{1}{0} = \emptyset$
10	3 8 9	mp2an	$⊢ \frac{1}{0} = \emptyset$