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

Metamath Proof Explorer

Theorem rec11ii

Description: Reciprocal is one-to-one. (Contributed by NM, 16-Sep-1999)

	Ref	Expression
Hypotheses	divclz.1	$⊢ A \in ℂ$
	divclz.2	$⊢ B \in ℂ$
	divneq0.3	$⊢ A \neq 0$
	divneq0.4	$⊢ B \neq 0$
Assertion	rec11ii	$⊢ \frac{1}{A} = \frac{1}{B} \leftrightarrow A = B$

Step	Hyp	Ref	Expression
1		divclz.1	$⊢ A \in ℂ$
2		divclz.2	$⊢ B \in ℂ$
3		divneq0.3	$⊢ A \neq 0$
4		divneq0.4	$⊢ B \neq 0$
5	1 2	rec11i	$⊢ (A \neq 0 \land B \neq 0) \to (\frac{1}{A} = \frac{1}{B} \leftrightarrow A = B)$
6	3 4 5	mp2an	$⊢ \frac{1}{A} = \frac{1}{B} \leftrightarrow A = B$