This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )