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	$$⊢\left(A\in 𝑹\wedge A\ne 0_{𝑹}\right)\to \exists x\in 𝑹A{\cdot }_{𝑹}x=1_{𝑹}$$

Proof

Step	Hyp	Ref	Expression
1		sqgt0sr	$$⊢\left(A\in 𝑹\wedge A\ne 0_{𝑹}\right)\to 0_{𝑹}{<}_{𝑹}\left(A{\cdot }_{𝑹}A\right)$$
2		mulclsr	$$⊢\left(A\in 𝑹\wedge y\in 𝑹\right)\to A{\cdot }_{𝑹}y\in 𝑹$$
3		mulasssr	$$⊢\left(A{\cdot }_{𝑹}A\right){\cdot }_{𝑹}y=A{\cdot }_{𝑹}\left(A{\cdot }_{𝑹}y\right)$$
4	3	eqeq1i	$$⊢\left(A{\cdot }_{𝑹}A\right){\cdot }_{𝑹}y=1_{𝑹}\leftrightarrow A{\cdot }_{𝑹}\left(A{\cdot }_{𝑹}y\right)=1_{𝑹}$$
5		oveq2	$$⊢x=A{\cdot }_{𝑹}y\to A{\cdot }_{𝑹}x=A{\cdot }_{𝑹}\left(A{\cdot }_{𝑹}y\right)$$
6	5	eqeq1d	$$⊢x=A{\cdot }_{𝑹}y\to \left(A{\cdot }_{𝑹}x=1_{𝑹}\leftrightarrow A{\cdot }_{𝑹}\left(A{\cdot }_{𝑹}y\right)=1_{𝑹}\right)$$
7	6	rspcev	$$⊢\left(A{\cdot }_{𝑹}y\in 𝑹\wedge A{\cdot }_{𝑹}\left(A{\cdot }_{𝑹}y\right)=1_{𝑹}\right)\to \exists x\in 𝑹A{\cdot }_{𝑹}x=1_{𝑹}$$
8	4 7	sylan2b	$$⊢\left(A{\cdot }_{𝑹}y\in 𝑹\wedge \left(A{\cdot }_{𝑹}A\right){\cdot }_{𝑹}y=1_{𝑹}\right)\to \exists x\in 𝑹A{\cdot }_{𝑹}x=1_{𝑹}$$
9	2 8	sylan	$$⊢\left(\left(A\in 𝑹\wedge y\in 𝑹\right)\wedge \left(A{\cdot }_{𝑹}A\right){\cdot }_{𝑹}y=1_{𝑹}\right)\to \exists x\in 𝑹A{\cdot }_{𝑹}x=1_{𝑹}$$
10	9	rexlimdva2	$$⊢A\in 𝑹\to \left(\exists y\in 𝑹\left(A{\cdot }_{𝑹}A\right){\cdot }_{𝑹}y=1_{𝑹}\to \exists x\in 𝑹A{\cdot }_{𝑹}x=1_{𝑹}\right)$$
11		recexsrlem	$$⊢0_{𝑹}{<}_{𝑹}\left(A{\cdot }_{𝑹}A\right)\to \exists y\in 𝑹\left(A{\cdot }_{𝑹}A\right){\cdot }_{𝑹}y=1_{𝑹}$$
12	10 11	impel	$$⊢\left(A\in 𝑹\wedge 0_{𝑹}{<}_{𝑹}\left(A{\cdot }_{𝑹}A\right)\right)\to \exists x\in 𝑹A{\cdot }_{𝑹}x=1_{𝑹}$$
13	1 12	syldan	$$⊢\left(A\in 𝑹\wedge A\ne 0_{𝑹}\right)\to \exists x\in 𝑹A{\cdot }_{𝑹}x=1_{𝑹}$$