Theorem xnegpnf

Description: Minus +oo . Remark of BourbakiTop1 p. IV.15. (Contributed by FL, 26-Dec-2011)

	Ref	Expression
Assertion	xnegpnf	$$⊢-\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		eqid	$$⊢\mathrm{+\infty }=\mathrm{+\infty }$$
3	2	iftruei	$$⊢if\left(\mathrm{+\infty }=\mathrm{+\infty },\mathrm{-\infty },if\left(\mathrm{+\infty }=\mathrm{-\infty },\mathrm{+\infty },-\mathrm{+\infty }\right)\right)=\mathrm{-\infty }$$
4	1 3	eqtri	$$⊢-\mathrm{+\infty }=\mathrm{-\infty }$$