Theorem negexsr

Description: Existence of negative signed real. Part of Proposition 9-4.3 of Gleason p. 126. (Contributed by NM, 2-May-1996) (New usage is discouraged.)

	Ref	Expression
Assertion	negexsr	$$⊢A\in 𝑹\to \exists x\in 𝑹A{+}_{𝑹}x=0_{𝑹}$$

Proof

Step	Hyp	Ref	Expression
1		m1r	$$⊢{-1}_{𝑹}\in 𝑹$$
2		mulclsr	$$⊢\left(A\in 𝑹\wedge {-1}_{𝑹}\in 𝑹\right)\to A{\cdot }_{𝑹}{-1}_{𝑹}\in 𝑹$$
3	1 2	mpan2	$$⊢A\in 𝑹\to A{\cdot }_{𝑹}{-1}_{𝑹}\in 𝑹$$
4		pn0sr	$$⊢A\in 𝑹\to A{+}_{𝑹}\left(A{\cdot }_{𝑹}{-1}_{𝑹}\right)=0_{𝑹}$$
5		oveq2	$$⊢x=A{\cdot }_{𝑹}{-1}_{𝑹}\to A{+}_{𝑹}x=A{+}_{𝑹}\left(A{\cdot }_{𝑹}{-1}_{𝑹}\right)$$
6	5	eqeq1d	$$⊢x=A{\cdot }_{𝑹}{-1}_{𝑹}\to \left(A{+}_{𝑹}x=0_{𝑹}\leftrightarrow A{+}_{𝑹}\left(A{\cdot }_{𝑹}{-1}_{𝑹}\right)=0_{𝑹}\right)$$
7	6	rspcev	$$⊢\left(A{\cdot }_{𝑹}{-1}_{𝑹}\in 𝑹\wedge A{+}_{𝑹}\left(A{\cdot }_{𝑹}{-1}_{𝑹}\right)=0_{𝑹}\right)\to \exists x\in 𝑹A{+}_{𝑹}x=0_{𝑹}$$
8	3 4 7	syl2anc	$$⊢A\in 𝑹\to \exists x\in 𝑹A{+}_{𝑹}x=0_{𝑹}$$