Theorem xlesubadd

Description: Under certain conditions, the conclusion of lesubadd is true even in the extended reals. (Contributed by Mario Carneiro, 4-Sep-2015)

	Ref	Expression
Assertion	xlesubadd	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶 ) ) → ( ( 𝐴 +𝑒 -𝑒 𝐵 ) ≤ 𝐶 ↔ 𝐴 ≤ ( 𝐶 +𝑒 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		simpl1	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶 ) ) → 𝐴 ∈ ℝ* )
2		simpl2	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶 ) ) → 𝐵 ∈ ℝ* )
3		xnegcl	⊢ ( 𝐵 ∈ ℝ* → -𝑒 𝐵 ∈ ℝ* )
4	2 3	syl	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶 ) ) → -𝑒 𝐵 ∈ ℝ* )
5		xaddcl	⊢ ( ( 𝐴 ∈ ℝ* ∧ -𝑒 𝐵 ∈ ℝ* ) → ( 𝐴 +𝑒 -𝑒 𝐵 ) ∈ ℝ* )
6	1 4 5	syl2anc	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶 ) ) → ( 𝐴 +𝑒 -𝑒 𝐵 ) ∈ ℝ* )
7	6	adantr	⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶 ) ) ∧ 𝐵 ∈ ℝ ) → ( 𝐴 +𝑒 -𝑒 𝐵 ) ∈ ℝ* )
8		simpll3	⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶 ) ) ∧ 𝐵 ∈ ℝ ) → 𝐶 ∈ ℝ* )
9		simpr	⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶 ) ) ∧ 𝐵 ∈ ℝ ) → 𝐵 ∈ ℝ )
10		xleadd1	⊢ ( ( ( 𝐴 +𝑒 -𝑒 𝐵 ) ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 +𝑒 -𝑒 𝐵 ) ≤ 𝐶 ↔ ( ( 𝐴 +𝑒 -𝑒 𝐵 ) +𝑒 𝐵 ) ≤ ( 𝐶 +𝑒 𝐵 ) ) )
11	7 8 9 10	syl3anc	⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶 ) ) ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 +𝑒 -𝑒 𝐵 ) ≤ 𝐶 ↔ ( ( 𝐴 +𝑒 -𝑒 𝐵 ) +𝑒 𝐵 ) ≤ ( 𝐶 +𝑒 𝐵 ) ) )
12		xnpcan	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 +𝑒 -𝑒 𝐵 ) +𝑒 𝐵 ) = 𝐴 )
13	1 12	sylan	⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶 ) ) ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 +𝑒 -𝑒 𝐵 ) +𝑒 𝐵 ) = 𝐴 )
14	13	breq1d	⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶 ) ) ∧ 𝐵 ∈ ℝ ) → ( ( ( 𝐴 +𝑒 -𝑒 𝐵 ) +𝑒 𝐵 ) ≤ ( 𝐶 +𝑒 𝐵 ) ↔ 𝐴 ≤ ( 𝐶 +𝑒 𝐵 ) ) )
15	11 14	bitrd	⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶 ) ) ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 +𝑒 -𝑒 𝐵 ) ≤ 𝐶 ↔ 𝐴 ≤ ( 𝐶 +𝑒 𝐵 ) ) )
16		simpr3	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶 ) ) → 0 ≤ 𝐶 )
17		oveq1	⊢ ( 𝐴 = +∞ → ( 𝐴 +𝑒 -∞ ) = ( +∞ +𝑒 -∞ ) )
18		pnfaddmnf	⊢ ( +∞ +𝑒 -∞ ) = 0
19	17 18	syl6eq	⊢ ( 𝐴 = +∞ → ( 𝐴 +𝑒 -∞ ) = 0 )
20	19	breq1d	⊢ ( 𝐴 = +∞ → ( ( 𝐴 +𝑒 -∞ ) ≤ 𝐶 ↔ 0 ≤ 𝐶 ) )
21	16 20	syl5ibrcom	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶 ) ) → ( 𝐴 = +∞ → ( 𝐴 +𝑒 -∞ ) ≤ 𝐶 ) )
22		xaddmnf1	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞ ) → ( 𝐴 +𝑒 -∞ ) = -∞ )
23	22	ex	⊢ ( 𝐴 ∈ ℝ* → ( 𝐴 ≠ +∞ → ( 𝐴 +𝑒 -∞ ) = -∞ ) )
24	1 23	syl	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶 ) ) → ( 𝐴 ≠ +∞ → ( 𝐴 +𝑒 -∞ ) = -∞ ) )
25		simpl3	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶 ) ) → 𝐶 ∈ ℝ* )
26		mnfle	⊢ ( 𝐶 ∈ ℝ* → -∞ ≤ 𝐶 )
27	25 26	syl	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶 ) ) → -∞ ≤ 𝐶 )
28		breq1	⊢ ( ( 𝐴 +𝑒 -∞ ) = -∞ → ( ( 𝐴 +𝑒 -∞ ) ≤ 𝐶 ↔ -∞ ≤ 𝐶 ) )
29	27 28	syl5ibrcom	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶 ) ) → ( ( 𝐴 +𝑒 -∞ ) = -∞ → ( 𝐴 +𝑒 -∞ ) ≤ 𝐶 ) )
30	24 29	syld	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶 ) ) → ( 𝐴 ≠ +∞ → ( 𝐴 +𝑒 -∞ ) ≤ 𝐶 ) )
31	21 30	pm2.61dne	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶 ) ) → ( 𝐴 +𝑒 -∞ ) ≤ 𝐶 )
32		pnfge	⊢ ( 𝐴 ∈ ℝ* → 𝐴 ≤ +∞ )
33	1 32	syl	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶 ) ) → 𝐴 ≤ +∞ )
34		ge0nemnf	⊢ ( ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) → 𝐶 ≠ -∞ )
35	25 16 34	syl2anc	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶 ) ) → 𝐶 ≠ -∞ )
36		xaddpnf1	⊢ ( ( 𝐶 ∈ ℝ* ∧ 𝐶 ≠ -∞ ) → ( 𝐶 +𝑒 +∞ ) = +∞ )
37	25 35 36	syl2anc	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶 ) ) → ( 𝐶 +𝑒 +∞ ) = +∞ )
38	33 37	breqtrrd	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶 ) ) → 𝐴 ≤ ( 𝐶 +𝑒 +∞ ) )
39	31 38	2thd	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶 ) ) → ( ( 𝐴 +𝑒 -∞ ) ≤ 𝐶 ↔ 𝐴 ≤ ( 𝐶 +𝑒 +∞ ) ) )
40		xnegeq	⊢ ( 𝐵 = +∞ → -𝑒 𝐵 = -𝑒 +∞ )
41		xnegpnf	⊢ -𝑒 +∞ = -∞
42	40 41	syl6eq	⊢ ( 𝐵 = +∞ → -𝑒 𝐵 = -∞ )
43	42	oveq2d	⊢ ( 𝐵 = +∞ → ( 𝐴 +𝑒 -𝑒 𝐵 ) = ( 𝐴 +𝑒 -∞ ) )
44	43	breq1d	⊢ ( 𝐵 = +∞ → ( ( 𝐴 +𝑒 -𝑒 𝐵 ) ≤ 𝐶 ↔ ( 𝐴 +𝑒 -∞ ) ≤ 𝐶 ) )
45		oveq2	⊢ ( 𝐵 = +∞ → ( 𝐶 +𝑒 𝐵 ) = ( 𝐶 +𝑒 +∞ ) )
46	45	breq2d	⊢ ( 𝐵 = +∞ → ( 𝐴 ≤ ( 𝐶 +𝑒 𝐵 ) ↔ 𝐴 ≤ ( 𝐶 +𝑒 +∞ ) ) )
47	44 46	bibi12d	⊢ ( 𝐵 = +∞ → ( ( ( 𝐴 +𝑒 -𝑒 𝐵 ) ≤ 𝐶 ↔ 𝐴 ≤ ( 𝐶 +𝑒 𝐵 ) ) ↔ ( ( 𝐴 +𝑒 -∞ ) ≤ 𝐶 ↔ 𝐴 ≤ ( 𝐶 +𝑒 +∞ ) ) ) )
48	39 47	syl5ibrcom	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶 ) ) → ( 𝐵 = +∞ → ( ( 𝐴 +𝑒 -𝑒 𝐵 ) ≤ 𝐶 ↔ 𝐴 ≤ ( 𝐶 +𝑒 𝐵 ) ) ) )
49	48	imp	⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶 ) ) ∧ 𝐵 = +∞ ) → ( ( 𝐴 +𝑒 -𝑒 𝐵 ) ≤ 𝐶 ↔ 𝐴 ≤ ( 𝐶 +𝑒 𝐵 ) ) )
50		simpr2	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶 ) ) → 𝐵 ≠ -∞ )
51	2 50	jca	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶 ) ) → ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞ ) )
52		xrnemnf	⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞ ) ↔ ( 𝐵 ∈ ℝ ∨ 𝐵 = +∞ ) )
53	51 52	sylib	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶 ) ) → ( 𝐵 ∈ ℝ ∨ 𝐵 = +∞ ) )
54	15 49 53	mpjaodan	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶 ) ) → ( ( 𝐴 +𝑒 -𝑒 𝐵 ) ≤ 𝐶 ↔ 𝐴 ≤ ( 𝐶 +𝑒 𝐵 ) ) )