Theorem recreci

Description: A number is equal to the reciprocal of its reciprocal. Theorem I.10 of Apostol p. 18. (Contributed by NM, 9-Feb-1995)

	Ref	Expression
Hypotheses	divclz.1	⊢ 𝐴 ∈ ℂ
	reccl.2	⊢ 𝐴 ≠ 0
Assertion	recreci	⊢ ( 1 / ( 1 / 𝐴 ) ) = 𝐴

Proof

Step	Hyp	Ref	Expression
1		divclz.1	⊢ 𝐴 ∈ ℂ
2		reccl.2	⊢ 𝐴 ≠ 0
3		recrec	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 1 / ( 1 / 𝐴 ) ) = 𝐴 )
4	1 2 3	mp2an	⊢ ( 1 / ( 1 / 𝐴 ) ) = 𝐴