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

Metamath Proof Explorer

Theorem recrec

Description: A number is equal to the reciprocal of its reciprocal. Theorem I.10 of Apostol p. 18. (Contributed by NM, 26-Sep-1999) (Proof shortened by Mario Carneiro, 27-May-2016)

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

Proof

Step	Hyp	Ref	Expression
1		recid2	$⊢ (A \in ℂ \land A \neq 0) \to (\frac{1}{A}) A = 1$
2		1cnd	$⊢ (A \in ℂ \land A \neq 0) \to 1 \in ℂ$
3		simpl	$⊢ (A \in ℂ \land A \neq 0) \to A \in ℂ$
4		reccl	$⊢ (A \in ℂ \land A \neq 0) \to \frac{1}{A} \in ℂ$
5		recne0	$⊢ (A \in ℂ \land A \neq 0) \to \frac{1}{A} \neq 0$
6		divmul	$⊢ (1 \in ℂ \land A \in ℂ \land (\frac{1}{A} \in ℂ \land \frac{1}{A} \neq 0)) \to (\frac{1}{\frac{1}{A}} = A \leftrightarrow (\frac{1}{A}) A = 1)$
7	2 3 4 5 6	syl112anc	$⊢ (A \in ℂ \land A \neq 0) \to (\frac{1}{\frac{1}{A}} = A \leftrightarrow (\frac{1}{A}) A = 1)$
8	1 7	mpbird	$⊢ (A \in ℂ \land A \neq 0) \to \frac{1}{\frac{1}{A}} = A$