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 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 )