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 e. CC /\ A =/= 0 ) -> ( 1 / ( 1 / A ) ) = A )

Proof

Step	Hyp	Ref	Expression
1		recid2	|- ( ( A e. CC /\ A =/= 0 ) -> ( ( 1 / A ) x. A ) = 1 )
2		1cnd	|- ( ( A e. CC /\ A =/= 0 ) -> 1 e. CC )
3		simpl	|- ( ( A e. CC /\ A =/= 0 ) -> A e. CC )
4		reccl	|- ( ( A e. CC /\ A =/= 0 ) -> ( 1 / A ) e. CC )
5		recne0	|- ( ( A e. CC /\ A =/= 0 ) -> ( 1 / A ) =/= 0 )
6		divmul	|- ( ( 1 e. CC /\ A e. CC /\ ( ( 1 / A ) e. CC /\ ( 1 / A ) =/= 0 ) ) -> ( ( 1 / ( 1 / A ) ) = A <-> ( ( 1 / A ) x. A ) = 1 ) )
7	2 3 4 5 6	syl112anc	|- ( ( A e. CC /\ A =/= 0 ) -> ( ( 1 / ( 1 / A ) ) = A <-> ( ( 1 / A ) x. A ) = 1 ) )
8	1 7	mpbird	|- ( ( A e. CC /\ A =/= 0 ) -> ( 1 / ( 1 / A ) ) = A )