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\in ℝ$$
Assertion	renegcli	$$⊢-A\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		renegcl.1	$$⊢A\in ℝ$$
2		ax-rnegex	$$⊢A\in ℝ\to \exists x\in ℝA+x=0$$
3		recn	$$⊢x\in ℝ\to x\in ℂ$$
4		df-neg	$$⊢-A=0-A$$
5	4	eqeq1i	$$⊢-A=x\leftrightarrow 0-A=x$$
6		0cn	$$⊢0\in ℂ$$
7	1	recni	$$⊢A\in ℂ$$
8		subadd	$$⊢\left(0\in ℂ\wedge A\in ℂ\wedge x\in ℂ\right)\to \left(0-A=x\leftrightarrow A+x=0\right)$$
9	6 7 8	mp3an12	$$⊢x\in ℂ\to \left(0-A=x\leftrightarrow A+x=0\right)$$
10	5 9	bitrid	$$⊢x\in ℂ\to \left(-A=x\leftrightarrow A+x=0\right)$$
11	3 10	syl	$$⊢x\in ℝ\to \left(-A=x\leftrightarrow A+x=0\right)$$
12		eleq1a	$$⊢x\in ℝ\to \left(-A=x\to -A\in ℝ\right)$$
13	11 12	sylbird	$$⊢x\in ℝ\to \left(A+x=0\to -A\in ℝ\right)$$
14	13	rexlimiv	$$⊢\exists x\in ℝA+x=0\to -A\in ℝ$$
15	1 2 14	mp2b	$$⊢-A\in ℝ$$