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 ( ( ๐ด โˆˆ R โˆง ๐ด โ‰  0R ) โ†’ โˆƒ ๐‘ฅ โˆˆ R ( ๐ด ยทR ๐‘ฅ ) = 1R )

Proof

Step Hyp Ref Expression
1 sqgt0sr โŠข ( ( ๐ด โˆˆ R โˆง ๐ด โ‰  0R ) โ†’ 0R <R ( ๐ด ยทR ๐ด ) )
2 mulclsr โŠข ( ( ๐ด โˆˆ R โˆง ๐‘ฆ โˆˆ R ) โ†’ ( ๐ด ยทR ๐‘ฆ ) โˆˆ R )
3 mulasssr โŠข ( ( ๐ด ยทR ๐ด ) ยทR ๐‘ฆ ) = ( ๐ด ยทR ( ๐ด ยทR ๐‘ฆ ) )
4 3 eqeq1i โŠข ( ( ( ๐ด ยทR ๐ด ) ยทR ๐‘ฆ ) = 1R โ†” ( ๐ด ยทR ( ๐ด ยทR ๐‘ฆ ) ) = 1R )
5 oveq2 โŠข ( ๐‘ฅ = ( ๐ด ยทR ๐‘ฆ ) โ†’ ( ๐ด ยทR ๐‘ฅ ) = ( ๐ด ยทR ( ๐ด ยทR ๐‘ฆ ) ) )
6 5 eqeq1d โŠข ( ๐‘ฅ = ( ๐ด ยทR ๐‘ฆ ) โ†’ ( ( ๐ด ยทR ๐‘ฅ ) = 1R โ†” ( ๐ด ยทR ( ๐ด ยทR ๐‘ฆ ) ) = 1R ) )
7 6 rspcev โŠข ( ( ( ๐ด ยทR ๐‘ฆ ) โˆˆ R โˆง ( ๐ด ยทR ( ๐ด ยทR ๐‘ฆ ) ) = 1R ) โ†’ โˆƒ ๐‘ฅ โˆˆ R ( ๐ด ยทR ๐‘ฅ ) = 1R )
8 4 7 sylan2b โŠข ( ( ( ๐ด ยทR ๐‘ฆ ) โˆˆ R โˆง ( ( ๐ด ยทR ๐ด ) ยทR ๐‘ฆ ) = 1R ) โ†’ โˆƒ ๐‘ฅ โˆˆ R ( ๐ด ยทR ๐‘ฅ ) = 1R )
9 2 8 sylan โŠข ( ( ( ๐ด โˆˆ R โˆง ๐‘ฆ โˆˆ R ) โˆง ( ( ๐ด ยทR ๐ด ) ยทR ๐‘ฆ ) = 1R ) โ†’ โˆƒ ๐‘ฅ โˆˆ R ( ๐ด ยทR ๐‘ฅ ) = 1R )
10 9 rexlimdva2 โŠข ( ๐ด โˆˆ R โ†’ ( โˆƒ ๐‘ฆ โˆˆ R ( ( ๐ด ยทR ๐ด ) ยทR ๐‘ฆ ) = 1R โ†’ โˆƒ ๐‘ฅ โˆˆ R ( ๐ด ยทR ๐‘ฅ ) = 1R ) )
11 recexsrlem โŠข ( 0R <R ( ๐ด ยทR ๐ด ) โ†’ โˆƒ ๐‘ฆ โˆˆ R ( ( ๐ด ยทR ๐ด ) ยทR ๐‘ฆ ) = 1R )
12 10 11 impel โŠข ( ( ๐ด โˆˆ R โˆง 0R <R ( ๐ด ยทR ๐ด ) ) โ†’ โˆƒ ๐‘ฅ โˆˆ R ( ๐ด ยทR ๐‘ฅ ) = 1R )
13 1 12 syldan โŠข ( ( ๐ด โˆˆ R โˆง ๐ด โ‰  0R ) โ†’ โˆƒ ๐‘ฅ โˆˆ R ( ๐ด ยทR ๐‘ฅ ) = 1R )