Theorem rexneg

Description: Minus a real number. Remark BourbakiTop1 p. IV.15. (Contributed by FL, 26-Dec-2011) (Proof shortened by Mario Carneiro, 20-Aug-2015)

	Ref	Expression
Assertion	rexneg	$$⊢A\in ℝ\to -A=-A$$

Proof

Step	Hyp	Ref	Expression
1		df-xneg	$$⊢-A=if\left(A=\mathrm{+\infty },\mathrm{-\infty },if\left(A=\mathrm{-\infty },\mathrm{+\infty },-A\right)\right)$$
2		renepnf	$$⊢A\in ℝ\to A\ne \mathrm{+\infty }$$
3		ifnefalse	$$⊢A\ne \mathrm{+\infty }\to if\left(A=\mathrm{+\infty },\mathrm{-\infty },if\left(A=\mathrm{-\infty },\mathrm{+\infty },-A\right)\right)=if\left(A=\mathrm{-\infty },\mathrm{+\infty },-A\right)$$
4	2 3	syl	$$⊢A\in ℝ\to if\left(A=\mathrm{+\infty },\mathrm{-\infty },if\left(A=\mathrm{-\infty },\mathrm{+\infty },-A\right)\right)=if\left(A=\mathrm{-\infty },\mathrm{+\infty },-A\right)$$
5		renemnf	$$⊢A\in ℝ\to A\ne \mathrm{-\infty }$$
6		ifnefalse	$$⊢A\ne \mathrm{-\infty }\to if\left(A=\mathrm{-\infty },\mathrm{+\infty },-A\right)=-A$$
7	5 6	syl	$$⊢A\in ℝ\to if\left(A=\mathrm{-\infty },\mathrm{+\infty },-A\right)=-A$$
8	4 7	eqtrd	$$⊢A\in ℝ\to if\left(A=\mathrm{+\infty },\mathrm{-\infty },if\left(A=\mathrm{-\infty },\mathrm{+\infty },-A\right)\right)=-A$$
9	1 8	eqtrid	$$⊢A\in ℝ\to -A=-A$$