Theorem renegcli

Description: Closure law for negative of reals. (Note: this inference proof style and the deduction theorem usage in renegcl is deprecated, but is retained for its demonstration value.) (Contributed by NM, 17-Jan-1997) (Proof shortened by Andrew Salmon, 22-Oct-2011)

	Ref	Expression
Hypothesis	renegcl.1	|- A e. RR
Assertion	renegcli	|- -u A e. RR

Proof

Step	Hyp	Ref	Expression
1		renegcl.1	|- A e. RR
2		ax-rnegex	|- ( A e. RR -> E. x e. RR ( A + x ) = 0 )
3		recn	|- ( x e. RR -> x e. CC )
4		df-neg	|- -u A = ( 0 - A )
5	4	eqeq1i	|- ( -u A = x <-> ( 0 - A ) = x )
6		0cn	|- 0 e. CC
7	1	recni	|- A e. CC
8		subadd	|- ( ( 0 e. CC /\ A e. CC /\ x e. CC ) -> ( ( 0 - A ) = x <-> ( A + x ) = 0 ) )
9	6 7 8	mp3an12	|- ( x e. CC -> ( ( 0 - A ) = x <-> ( A + x ) = 0 ) )
10	5 9	bitrid	|- ( x e. CC -> ( -u A = x <-> ( A + x ) = 0 ) )
11	3 10	syl	|- ( x e. RR -> ( -u A = x <-> ( A + x ) = 0 ) )
12		eleq1a	|- ( x e. RR -> ( -u A = x -> -u A e. RR ) )
13	11 12	sylbird	|- ( x e. RR -> ( ( A + x ) = 0 -> -u A e. RR ) )
14	13	rexlimiv	|- ( E. x e. RR ( A + x ) = 0 -> -u A e. RR )
15	1 2 14	mp2b	|- -u A e. RR