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 )