Theorem infm3lem

Description: Lemma for infm3 . (Contributed by NM, 14-Jun-2005)

	Ref	Expression
Assertion	infm3lem	$$⊢x\in ℝ\to \exists y\in ℝx=-y$$

Proof

Step	Hyp	Ref	Expression
1		renegcl	$$⊢x\in ℝ\to -x\in ℝ$$
2		recn	$$⊢x\in ℝ\to x\in ℂ$$
3	2	negnegd	$$⊢x\in ℝ\to -\left(-x\right)=x$$
4	3	eqcomd	$$⊢x\in ℝ\to x=-\left(-x\right)$$
5		negeq	$$⊢y=-x\to -y=-\left(-x\right)$$
6	5	rspceeqv	$$⊢\left(-x\in ℝ\wedge x=-\left(-x\right)\right)\to \exists y\in ℝx=-y$$
7	1 4 6	syl2anc	$$⊢x\in ℝ\to \exists y\in ℝx=-y$$