Theorem xnegmnf

Description: Minus -oo . Remark of BourbakiTop1 p. IV.15. (Contributed by FL, 26-Dec-2011) (Revised by Mario Carneiro, 20-Aug-2015)

	Ref	Expression
Assertion	xnegmnf	$$⊢-\mathrm{-\infty }=\mathrm{+\infty }$$

Proof

Step	Hyp	Ref	Expression
1		df-xneg	$$⊢-\mathrm{-\infty }=if\left(\mathrm{-\infty }=\mathrm{+\infty },\mathrm{-\infty },if\left(\mathrm{-\infty }=\mathrm{-\infty },\mathrm{+\infty },-\mathrm{-\infty }\right)\right)$$
2		mnfnepnf	$$⊢\mathrm{-\infty }\ne \mathrm{+\infty }$$
3		ifnefalse	$$⊢\mathrm{-\infty }\ne \mathrm{+\infty }\to if\left(\mathrm{-\infty }=\mathrm{+\infty },\mathrm{-\infty },if\left(\mathrm{-\infty }=\mathrm{-\infty },\mathrm{+\infty },-\mathrm{-\infty }\right)\right)=if\left(\mathrm{-\infty }=\mathrm{-\infty },\mathrm{+\infty },-\mathrm{-\infty }\right)$$
4	2 3	ax-mp	$$⊢if\left(\mathrm{-\infty }=\mathrm{+\infty },\mathrm{-\infty },if\left(\mathrm{-\infty }=\mathrm{-\infty },\mathrm{+\infty },-\mathrm{-\infty }\right)\right)=if\left(\mathrm{-\infty }=\mathrm{-\infty },\mathrm{+\infty },-\mathrm{-\infty }\right)$$
5		eqid	$$⊢\mathrm{-\infty }=\mathrm{-\infty }$$
6	5	iftruei	$$⊢if\left(\mathrm{-\infty }=\mathrm{-\infty },\mathrm{+\infty },-\mathrm{-\infty }\right)=\mathrm{+\infty }$$
7	1 4 6	3eqtri	$$⊢-\mathrm{-\infty }=\mathrm{+\infty }$$