Theorem negrebd

Description: The negative of a real is real. (Contributed by Mario Carneiro, 28-May-2016)

	Ref	Expression
Hypotheses	negidd.1	|- ( ph -> A e. CC )
	negrebd.2	|- ( ph -> -u A e. RR )
Assertion	negrebd	|- ( ph -> A e. RR )

Proof

Step	Hyp	Ref	Expression
1		negidd.1	|- ( ph -> A e. CC )
2		negrebd.2	|- ( ph -> -u A e. RR )
3		negreb	|- ( A e. CC -> ( -u A e. RR <-> A e. RR ) )
4	1 3	syl	|- ( ph -> ( -u A e. RR <-> A e. RR ) )
5	2 4	mpbid	|- ( ph -> A e. RR )