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	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 1 / ( 1 / 𝐴 ) ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		recid2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( 1 / 𝐴 ) · 𝐴 ) = 1 )
2		1cnd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → 1 ∈ ℂ )
3		simpl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → 𝐴 ∈ ℂ )
4		reccl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 1 / 𝐴 ) ∈ ℂ )
5		recne0	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 1 / 𝐴 ) ≠ 0 )
6		divmul	⊢ ( ( 1 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ ( ( 1 / 𝐴 ) ∈ ℂ ∧ ( 1 / 𝐴 ) ≠ 0 ) ) → ( ( 1 / ( 1 / 𝐴 ) ) = 𝐴 ↔ ( ( 1 / 𝐴 ) · 𝐴 ) = 1 ) )
7	2 3 4 5 6	syl112anc	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( 1 / ( 1 / 𝐴 ) ) = 𝐴 ↔ ( ( 1 / 𝐴 ) · 𝐴 ) = 1 ) )
8	1 7	mpbird	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 1 / ( 1 / 𝐴 ) ) = 𝐴 )