Theorem xsubge0

Description: Extended real version of subge0 . (Contributed by Mario Carneiro, 24-Aug-2015)

	Ref	Expression
Assertion	xsubge0	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(0\le A{+}_{𝑒}\left(-B\right)\leftrightarrow B\le A\right)$$

Proof

Step	Hyp	Ref	Expression
1		elxr	$$⊢B\in {ℝ}^{*}\leftrightarrow \left(B\in ℝ\vee B=\mathrm{+\infty }\vee B=\mathrm{-\infty }\right)$$
2		0xr	$$⊢0\in {ℝ}^{*}$$
3		rexr	$$⊢B\in ℝ\to B\in {ℝ}^{*}$$
4		xnegcl	$$⊢B\in {ℝ}^{*}\to -B\in {ℝ}^{*}$$
5		xaddcl	$$⊢\left(A\in {ℝ}^{*}\wedge -B\in {ℝ}^{*}\right)\to A{+}_{𝑒}\left(-B\right)\in {ℝ}^{*}$$
6	4 5	sylan2	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to A{+}_{𝑒}\left(-B\right)\in {ℝ}^{*}$$
7	3 6	sylan2	$$⊢\left(A\in {ℝ}^{*}\wedge B\in ℝ\right)\to A{+}_{𝑒}\left(-B\right)\in {ℝ}^{*}$$
8		simpr	$$⊢\left(A\in {ℝ}^{*}\wedge B\in ℝ\right)\to B\in ℝ$$
9		xleadd1	$$⊢\left(0\in {ℝ}^{*}\wedge A{+}_{𝑒}\left(-B\right)\in {ℝ}^{*}\wedge B\in ℝ\right)\to \left(0\le A{+}_{𝑒}\left(-B\right)\leftrightarrow 0{+}_{𝑒}B\le \left(A{+}_{𝑒}\left(-B\right)\right){+}_{𝑒}B\right)$$
10	2 7 8 9	mp3an2i	$$⊢\left(A\in {ℝ}^{*}\wedge B\in ℝ\right)\to \left(0\le A{+}_{𝑒}\left(-B\right)\leftrightarrow 0{+}_{𝑒}B\le \left(A{+}_{𝑒}\left(-B\right)\right){+}_{𝑒}B\right)$$
11	3	adantl	$$⊢\left(A\in {ℝ}^{*}\wedge B\in ℝ\right)\to B\in {ℝ}^{*}$$
12		xaddlid	$$⊢B\in {ℝ}^{*}\to 0{+}_{𝑒}B=B$$
13	11 12	syl	$$⊢\left(A\in {ℝ}^{*}\wedge B\in ℝ\right)\to 0{+}_{𝑒}B=B$$
14		xnpcan	$$⊢\left(A\in {ℝ}^{*}\wedge B\in ℝ\right)\to \left(A{+}_{𝑒}\left(-B\right)\right){+}_{𝑒}B=A$$
15	13 14	breq12d	$$⊢\left(A\in {ℝ}^{*}\wedge B\in ℝ\right)\to \left(0{+}_{𝑒}B\le \left(A{+}_{𝑒}\left(-B\right)\right){+}_{𝑒}B\leftrightarrow B\le A\right)$$
16	10 15	bitrd	$$⊢\left(A\in {ℝ}^{*}\wedge B\in ℝ\right)\to \left(0\le A{+}_{𝑒}\left(-B\right)\leftrightarrow B\le A\right)$$
17		pnfxr	$$⊢\mathrm{+\infty }\in {ℝ}^{*}$$
18		xrletri3	$$⊢\left(A\in {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\right)\to \left(A=\mathrm{+\infty }\leftrightarrow \left(A\le \mathrm{+\infty }\wedge \mathrm{+\infty }\le A\right)\right)$$
19	17 18	mpan2	$$⊢A\in {ℝ}^{*}\to \left(A=\mathrm{+\infty }\leftrightarrow \left(A\le \mathrm{+\infty }\wedge \mathrm{+\infty }\le A\right)\right)$$
20		mnflt0	$$⊢\mathrm{-\infty }<0$$
21		mnfxr	$$⊢\mathrm{-\infty }\in {ℝ}^{*}$$
22		xrltnle	$$⊢\left(\mathrm{-\infty }\in {ℝ}^{*}\wedge 0\in {ℝ}^{*}\right)\to \left(\mathrm{-\infty }<0\leftrightarrow \neg 0\le \mathrm{-\infty }\right)$$
23	21 2 22	mp2an	$$⊢\mathrm{-\infty }<0\leftrightarrow \neg 0\le \mathrm{-\infty }$$
24	20 23	mpbi	$$⊢\neg 0\le \mathrm{-\infty }$$
25		xaddmnf1	$$⊢\left(A\in {ℝ}^{*}\wedge A\ne \mathrm{+\infty }\right)\to A{+}_{𝑒}\mathrm{-\infty }=\mathrm{-\infty }$$
26	25	breq2d	$$⊢\left(A\in {ℝ}^{*}\wedge A\ne \mathrm{+\infty }\right)\to \left(0\le A{+}_{𝑒}\mathrm{-\infty }\leftrightarrow 0\le \mathrm{-\infty }\right)$$
27	24 26	mtbiri	$$⊢\left(A\in {ℝ}^{*}\wedge A\ne \mathrm{+\infty }\right)\to \neg 0\le A{+}_{𝑒}\mathrm{-\infty }$$
28	27	ex	$$⊢A\in {ℝ}^{*}\to \left(A\ne \mathrm{+\infty }\to \neg 0\le A{+}_{𝑒}\mathrm{-\infty }\right)$$
29	28	necon4ad	$$⊢A\in {ℝ}^{*}\to \left(0\le A{+}_{𝑒}\mathrm{-\infty }\to A=\mathrm{+\infty }\right)$$
30		0le0	$$⊢0\le 0$$
31		oveq1	$$⊢A=\mathrm{+\infty }\to A{+}_{𝑒}\mathrm{-\infty }=\mathrm{+\infty }{+}_{𝑒}\mathrm{-\infty }$$
32		pnfaddmnf	$$⊢\mathrm{+\infty }{+}_{𝑒}\mathrm{-\infty }=0$$
33	31 32	eqtrdi	$$⊢A=\mathrm{+\infty }\to A{+}_{𝑒}\mathrm{-\infty }=0$$
34	30 33	breqtrrid	$$⊢A=\mathrm{+\infty }\to 0\le A{+}_{𝑒}\mathrm{-\infty }$$
35	29 34	impbid1	$$⊢A\in {ℝ}^{*}\to \left(0\le A{+}_{𝑒}\mathrm{-\infty }\leftrightarrow A=\mathrm{+\infty }\right)$$
36		pnfge	$$⊢A\in {ℝ}^{*}\to A\le \mathrm{+\infty }$$
37	36	biantrurd	$$⊢A\in {ℝ}^{*}\to \left(\mathrm{+\infty }\le A\leftrightarrow \left(A\le \mathrm{+\infty }\wedge \mathrm{+\infty }\le A\right)\right)$$
38	19 35 37	3bitr4d	$$⊢A\in {ℝ}^{*}\to \left(0\le A{+}_{𝑒}\mathrm{-\infty }\leftrightarrow \mathrm{+\infty }\le A\right)$$
39	38	adantr	$$⊢\left(A\in {ℝ}^{*}\wedge B=\mathrm{+\infty }\right)\to \left(0\le A{+}_{𝑒}\mathrm{-\infty }\leftrightarrow \mathrm{+\infty }\le A\right)$$
40		xnegeq	$$⊢B=\mathrm{+\infty }\to -B=-\mathrm{+\infty }$$
41		xnegpnf	$$⊢-\mathrm{+\infty }=\mathrm{-\infty }$$
42	40 41	eqtrdi	$$⊢B=\mathrm{+\infty }\to -B=\mathrm{-\infty }$$
43	42	adantl	$$⊢\left(A\in {ℝ}^{*}\wedge B=\mathrm{+\infty }\right)\to -B=\mathrm{-\infty }$$
44	43	oveq2d	$$⊢\left(A\in {ℝ}^{*}\wedge B=\mathrm{+\infty }\right)\to A{+}_{𝑒}\left(-B\right)=A{+}_{𝑒}\mathrm{-\infty }$$
45	44	breq2d	$$⊢\left(A\in {ℝ}^{*}\wedge B=\mathrm{+\infty }\right)\to \left(0\le A{+}_{𝑒}\left(-B\right)\leftrightarrow 0\le A{+}_{𝑒}\mathrm{-\infty }\right)$$
46		breq1	$$⊢B=\mathrm{+\infty }\to \left(B\le A\leftrightarrow \mathrm{+\infty }\le A\right)$$
47	46	adantl	$$⊢\left(A\in {ℝ}^{*}\wedge B=\mathrm{+\infty }\right)\to \left(B\le A\leftrightarrow \mathrm{+\infty }\le A\right)$$
48	39 45 47	3bitr4d	$$⊢\left(A\in {ℝ}^{*}\wedge B=\mathrm{+\infty }\right)\to \left(0\le A{+}_{𝑒}\left(-B\right)\leftrightarrow B\le A\right)$$
49		oveq1	$$⊢A=\mathrm{-\infty }\to A{+}_{𝑒}\mathrm{+\infty }=\mathrm{-\infty }{+}_{𝑒}\mathrm{+\infty }$$
50		mnfaddpnf	$$⊢\mathrm{-\infty }{+}_{𝑒}\mathrm{+\infty }=0$$
51	49 50	eqtrdi	$$⊢A=\mathrm{-\infty }\to A{+}_{𝑒}\mathrm{+\infty }=0$$
52	51	adantl	$$⊢\left(A\in {ℝ}^{*}\wedge A=\mathrm{-\infty }\right)\to A{+}_{𝑒}\mathrm{+\infty }=0$$
53	30 52	breqtrrid	$$⊢\left(A\in {ℝ}^{*}\wedge A=\mathrm{-\infty }\right)\to 0\le A{+}_{𝑒}\mathrm{+\infty }$$
54		0lepnf	$$⊢0\le \mathrm{+\infty }$$
55		xaddpnf1	$$⊢\left(A\in {ℝ}^{*}\wedge A\ne \mathrm{-\infty }\right)\to A{+}_{𝑒}\mathrm{+\infty }=\mathrm{+\infty }$$
56	54 55	breqtrrid	$$⊢\left(A\in {ℝ}^{*}\wedge A\ne \mathrm{-\infty }\right)\to 0\le A{+}_{𝑒}\mathrm{+\infty }$$
57	53 56	pm2.61dane	$$⊢A\in {ℝ}^{*}\to 0\le A{+}_{𝑒}\mathrm{+\infty }$$
58		mnfle	$$⊢A\in {ℝ}^{*}\to \mathrm{-\infty }\le A$$
59	57 58	2thd	$$⊢A\in {ℝ}^{*}\to \left(0\le A{+}_{𝑒}\mathrm{+\infty }\leftrightarrow \mathrm{-\infty }\le A\right)$$
60	59	adantr	$$⊢\left(A\in {ℝ}^{*}\wedge B=\mathrm{-\infty }\right)\to \left(0\le A{+}_{𝑒}\mathrm{+\infty }\leftrightarrow \mathrm{-\infty }\le A\right)$$
61		xnegeq	$$⊢B=\mathrm{-\infty }\to -B=-\mathrm{-\infty }$$
62		xnegmnf	$$⊢-\mathrm{-\infty }=\mathrm{+\infty }$$
63	61 62	eqtrdi	$$⊢B=\mathrm{-\infty }\to -B=\mathrm{+\infty }$$
64	63	adantl	$$⊢\left(A\in {ℝ}^{*}\wedge B=\mathrm{-\infty }\right)\to -B=\mathrm{+\infty }$$
65	64	oveq2d	$$⊢\left(A\in {ℝ}^{*}\wedge B=\mathrm{-\infty }\right)\to A{+}_{𝑒}\left(-B\right)=A{+}_{𝑒}\mathrm{+\infty }$$
66	65	breq2d	$$⊢\left(A\in {ℝ}^{*}\wedge B=\mathrm{-\infty }\right)\to \left(0\le A{+}_{𝑒}\left(-B\right)\leftrightarrow 0\le A{+}_{𝑒}\mathrm{+\infty }\right)$$
67		breq1	$$⊢B=\mathrm{-\infty }\to \left(B\le A\leftrightarrow \mathrm{-\infty }\le A\right)$$
68	67	adantl	$$⊢\left(A\in {ℝ}^{*}\wedge B=\mathrm{-\infty }\right)\to \left(B\le A\leftrightarrow \mathrm{-\infty }\le A\right)$$
69	60 66 68	3bitr4d	$$⊢\left(A\in {ℝ}^{*}\wedge B=\mathrm{-\infty }\right)\to \left(0\le A{+}_{𝑒}\left(-B\right)\leftrightarrow B\le A\right)$$
70	16 48 69	3jaodan	$$⊢\left(A\in {ℝ}^{*}\wedge \left(B\in ℝ\vee B=\mathrm{+\infty }\vee B=\mathrm{-\infty }\right)\right)\to \left(0\le A{+}_{𝑒}\left(-B\right)\leftrightarrow B\le A\right)$$
71	1 70	sylan2b	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(0\le A{+}_{𝑒}\left(-B\right)\leftrightarrow B\le A\right)$$