This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem recexsr

Description: The reciprocal of a nonzero signed real exists. Part of Proposition 9-4.3 of Gleason p. 126. (Contributed by NM, 15-May-1996) (New usage is discouraged.)

Ref Expression
Assertion recexsr 
|- ( ( A e. R. /\ A =/= 0R ) -> E. x e. R. ( A .R x ) = 1R )

Proof

Step Hyp Ref Expression
1 sqgt0sr 
 |-  ( ( A e. R. /\ A =/= 0R ) -> 0R
2 mulclsr 
 |-  ( ( A e. R. /\ y e. R. ) -> ( A .R y ) e. R. )
3 mulasssr 
 |-  ( ( A .R A ) .R y ) = ( A .R ( A .R y ) )
4 3 eqeq1i 
 |-  ( ( ( A .R A ) .R y ) = 1R <-> ( A .R ( A .R y ) ) = 1R )
5 oveq2 
 |-  ( x = ( A .R y ) -> ( A .R x ) = ( A .R ( A .R y ) ) )
6 5 eqeq1d 
 |-  ( x = ( A .R y ) -> ( ( A .R x ) = 1R <-> ( A .R ( A .R y ) ) = 1R ) )
7 6 rspcev 
 |-  ( ( ( A .R y ) e. R. /\ ( A .R ( A .R y ) ) = 1R ) -> E. x e. R. ( A .R x ) = 1R )
8 4 7 sylan2b 
 |-  ( ( ( A .R y ) e. R. /\ ( ( A .R A ) .R y ) = 1R ) -> E. x e. R. ( A .R x ) = 1R )
9 2 8 sylan 
 |-  ( ( ( A e. R. /\ y e. R. ) /\ ( ( A .R A ) .R y ) = 1R ) -> E. x e. R. ( A .R x ) = 1R )
10 9 rexlimdva2 
 |-  ( A e. R. -> ( E. y e. R. ( ( A .R A ) .R y ) = 1R -> E. x e. R. ( A .R x ) = 1R ) )
11 recexsrlem 
 |-  ( 0R  E. y e. R. ( ( A .R A ) .R y ) = 1R )
12 10 11 impel 
 |-  ( ( A e. R. /\ 0R  E. x e. R. ( A .R x ) = 1R )
13 1 12 syldan 
 |-  ( ( A e. R. /\ A =/= 0R ) -> E. x e. R. ( A .R x ) = 1R )