Theorem xsubge0

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

	Ref	Expression
Assertion	xsubge0	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 0 ≤ ( 𝐴 +𝑒 -𝑒 𝐵 ) ↔ 𝐵 ≤ 𝐴 ) )

Proof

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