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 e. R. -> E. x e. R. ( A +R x ) = 0R )

Proof

Step	Hyp	Ref	Expression
1		m1r	|- -1R e. R.
2		mulclsr	|- ( ( A e. R. /\ -1R e. R. ) -> ( A .R -1R ) e. R. )
3	1 2	mpan2	|- ( A e. R. -> ( A .R -1R ) e. R. )
4		pn0sr	|- ( A e. R. -> ( A +R ( A .R -1R ) ) = 0R )
5		oveq2	|- ( x = ( A .R -1R ) -> ( A +R x ) = ( A +R ( A .R -1R ) ) )
6	5	eqeq1d	|- ( x = ( A .R -1R ) -> ( ( A +R x ) = 0R <-> ( A +R ( A .R -1R ) ) = 0R ) )
7	6	rspcev	|- ( ( ( A .R -1R ) e. R. /\ ( A +R ( A .R -1R ) ) = 0R ) -> E. x e. R. ( A +R x ) = 0R )
8	3 4 7	syl2anc	|- ( A e. R. -> E. x e. R. ( A +R x ) = 0R )