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	⊢ ( 𝐴 ∈ R → ∃ 𝑥 ∈ R ( 𝐴 +R 𝑥 ) = 0R )

Proof

Step	Hyp	Ref	Expression
1		m1r	⊢ -1R ∈ R
2		mulclsr	⊢ ( ( 𝐴 ∈ R ∧ -1R ∈ R ) → ( 𝐴 ·R -1R ) ∈ R )
3	1 2	mpan2	⊢ ( 𝐴 ∈ R → ( 𝐴 ·R -1R ) ∈ R )
4		pn0sr	⊢ ( 𝐴 ∈ R → ( 𝐴 +R ( 𝐴 ·R -1R ) ) = 0R )
5		oveq2	⊢ ( 𝑥 = ( 𝐴 ·R -1R ) → ( 𝐴 +R 𝑥 ) = ( 𝐴 +R ( 𝐴 ·R -1R ) ) )
6	5	eqeq1d	⊢ ( 𝑥 = ( 𝐴 ·R -1R ) → ( ( 𝐴 +R 𝑥 ) = 0R ↔ ( 𝐴 +R ( 𝐴 ·R -1R ) ) = 0R ) )
7	6	rspcev	⊢ ( ( ( 𝐴 ·R -1R ) ∈ R ∧ ( 𝐴 +R ( 𝐴 ·R -1R ) ) = 0R ) → ∃ 𝑥 ∈ R ( 𝐴 +R 𝑥 ) = 0R )
8	3 4 7	syl2anc	⊢ ( 𝐴 ∈ R → ∃ 𝑥 ∈ R ( 𝐴 +R 𝑥 ) = 0R )