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	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \frac{1}{\frac{1}{A}}=A$$

Proof

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