Metamath Proof Explorer

Theorem rereccl

Description: Closure law for reciprocal. (Contributed by NM, 30-Apr-2005) (Revised by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion rereccl 
|- ( ( A e. RR /\ A =/= 0 ) -> ( 1 / A ) e. RR )

Proof

Step Hyp Ref Expression
1 ax-rrecex 
 |-  ( ( A e. RR /\ A =/= 0 ) -> E. x e. RR ( A x. x ) = 1 )
2 eqcom 
 |-  ( x = ( 1 / A ) <-> ( 1 / A ) = x )
3 1cnd 
 |-  ( ( ( A e. RR /\ A =/= 0 ) /\ x e. RR ) -> 1 e. CC )
4 simpr 
 |-  ( ( ( A e. RR /\ A =/= 0 ) /\ x e. RR ) -> x e. RR )
5 4 recnd 
 |-  ( ( ( A e. RR /\ A =/= 0 ) /\ x e. RR ) -> x e. CC )
6 simpll 
 |-  ( ( ( A e. RR /\ A =/= 0 ) /\ x e. RR ) -> A e. RR )
7 6 recnd 
 |-  ( ( ( A e. RR /\ A =/= 0 ) /\ x e. RR ) -> A e. CC )
8 simplr 
 |-  ( ( ( A e. RR /\ A =/= 0 ) /\ x e. RR ) -> A =/= 0 )
9 divmul 
 |-  ( ( 1 e. CC /\ x e. CC /\ ( A e. CC /\ A =/= 0 ) ) -> ( ( 1 / A ) = x <-> ( A x. x ) = 1 ) )
10 3 5 7 8 9 syl112anc 
 |-  ( ( ( A e. RR /\ A =/= 0 ) /\ x e. RR ) -> ( ( 1 / A ) = x <-> ( A x. x ) = 1 ) )
11 2 10 syl5bb 
 |-  ( ( ( A e. RR /\ A =/= 0 ) /\ x e. RR ) -> ( x = ( 1 / A ) <-> ( A x. x ) = 1 ) )
12 11 rexbidva 
 |-  ( ( A e. RR /\ A =/= 0 ) -> ( E. x e. RR x = ( 1 / A ) <-> E. x e. RR ( A x. x ) = 1 ) )
13 1 12 mpbird 
 |-  ( ( A e. RR /\ A =/= 0 ) -> E. x e. RR x = ( 1 / A ) )
14 risset 
 |-  ( ( 1 / A ) e. RR <-> E. x e. RR x = ( 1 / A ) )
15 13 14 sylibr 
 |-  ( ( A e. RR /\ A =/= 0 ) -> ( 1 / A ) e. RR )