Theorem infm3lem

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

	Ref	Expression
Assertion	infm3lem	|- ( x e. RR -> E. y e. RR x = -u y )

Proof

Step	Hyp	Ref	Expression
1		renegcl	|- ( x e. RR -> -u x e. RR )
2		recn	|- ( x e. RR -> x e. CC )
3	2	negnegd	|- ( x e. RR -> -u -u x = x )
4	3	eqcomd	|- ( x e. RR -> x = -u -u x )
5		negeq	|- ( y = -u x -> -u y = -u -u x )
6	5	rspceeqv	|- ( ( -u x e. RR /\ x = -u -u x ) -> E. y e. RR x = -u y )
7	1 4 6	syl2anc	|- ( x e. RR -> E. y e. RR x = -u y )