Metamath Proof Explorer


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 eqtrdi ( 𝐴 = +∞ → ( 𝐴 +𝑒 -∞ ) = 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 eqtrdi ( 𝐵 = +∞ → -𝑒 𝐵 = -∞ )
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 ≤ 𝐶 ) ) → ( ( 𝐴 +𝑒 -𝑒 𝐵 ) ≤ 𝐶𝐴 ≤ ( 𝐶 +𝑒 𝐵 ) ) )