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

Metamath Proof Explorer

Theorem recne0

Description: The reciprocal of a nonzero number is nonzero. (Contributed by NM, 9-Feb-2006) (Proof shortened by Mario Carneiro, 27-May-2016)

		Ref	Expression
	Assertion	recne0	$⊢ (A \in ℂ \land A \neq 0) \to \frac{1}{A} \neq 0$

Step	Hyp	Ref	Expression
1		ax-1cn	$⊢ 1 \in ℂ$
2		ax-1ne0	$⊢ 1 \neq 0$
3		divne0	$⊢ ((1 \in ℂ \land 1 \neq 0) \land (A \in ℂ \land A \neq 0)) \to \frac{1}{A} \neq 0$
4	1 2 3	mpanl12	$⊢ (A \in ℂ \land A \neq 0) \to \frac{1}{A} \neq 0$