Metamath Proof Explorer


Theorem xleadd1a

Description: Extended real version of leadd1 ; note that the converse implication is not true, unlike the real version (for example 0 < 1 but ( 1 +e +oo ) <_ ( 0 +e +oo ) ). (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xleadd1a ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) → ( 𝐴 +𝑒 𝐶 ) ≤ ( 𝐵 +𝑒 𝐶 ) )

Proof

Step Hyp Ref Expression
1 simplrr ( ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ ) ) ∧ 𝐵 ∈ ℝ ) → 𝐴 ∈ ℝ )
2 simpr ( ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ ) ) ∧ 𝐵 ∈ ℝ ) → 𝐵 ∈ ℝ )
3 simplrl ( ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ ) ) ∧ 𝐵 ∈ ℝ ) → 𝐶 ∈ ℝ )
4 simpllr ( ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ ) ) ∧ 𝐵 ∈ ℝ ) → 𝐴𝐵 )
5 1 2 3 4 leadd1dd ( ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ ) ) ∧ 𝐵 ∈ ℝ ) → ( 𝐴 + 𝐶 ) ≤ ( 𝐵 + 𝐶 ) )
6 1 3 rexaddd ( ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ ) ) ∧ 𝐵 ∈ ℝ ) → ( 𝐴 +𝑒 𝐶 ) = ( 𝐴 + 𝐶 ) )
7 2 3 rexaddd ( ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ ) ) ∧ 𝐵 ∈ ℝ ) → ( 𝐵 +𝑒 𝐶 ) = ( 𝐵 + 𝐶 ) )
8 5 6 7 3brtr4d ( ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ ) ) ∧ 𝐵 ∈ ℝ ) → ( 𝐴 +𝑒 𝐶 ) ≤ ( 𝐵 +𝑒 𝐶 ) )
9 simpl1 ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) → 𝐴 ∈ ℝ* )
10 simpl3 ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) → 𝐶 ∈ ℝ* )
11 xaddcl ( ( 𝐴 ∈ ℝ*𝐶 ∈ ℝ* ) → ( 𝐴 +𝑒 𝐶 ) ∈ ℝ* )
12 9 10 11 syl2anc ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) → ( 𝐴 +𝑒 𝐶 ) ∈ ℝ* )
13 12 ad2antrr ( ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ ) ) ∧ 𝐵 = +∞ ) → ( 𝐴 +𝑒 𝐶 ) ∈ ℝ* )
14 pnfge ( ( 𝐴 +𝑒 𝐶 ) ∈ ℝ* → ( 𝐴 +𝑒 𝐶 ) ≤ +∞ )
15 13 14 syl ( ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ ) ) ∧ 𝐵 = +∞ ) → ( 𝐴 +𝑒 𝐶 ) ≤ +∞ )
16 oveq1 ( 𝐵 = +∞ → ( 𝐵 +𝑒 𝐶 ) = ( +∞ +𝑒 𝐶 ) )
17 rexr ( 𝐶 ∈ ℝ → 𝐶 ∈ ℝ* )
18 renemnf ( 𝐶 ∈ ℝ → 𝐶 ≠ -∞ )
19 xaddpnf2 ( ( 𝐶 ∈ ℝ*𝐶 ≠ -∞ ) → ( +∞ +𝑒 𝐶 ) = +∞ )
20 17 18 19 syl2anc ( 𝐶 ∈ ℝ → ( +∞ +𝑒 𝐶 ) = +∞ )
21 20 ad2antrl ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ ) ) → ( +∞ +𝑒 𝐶 ) = +∞ )
22 16 21 sylan9eqr ( ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ ) ) ∧ 𝐵 = +∞ ) → ( 𝐵 +𝑒 𝐶 ) = +∞ )
23 15 22 breqtrrd ( ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ ) ) ∧ 𝐵 = +∞ ) → ( 𝐴 +𝑒 𝐶 ) ≤ ( 𝐵 +𝑒 𝐶 ) )
24 12 adantr ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ 𝐵 = -∞ ) → ( 𝐴 +𝑒 𝐶 ) ∈ ℝ* )
25 24 xrleidd ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ 𝐵 = -∞ ) → ( 𝐴 +𝑒 𝐶 ) ≤ ( 𝐴 +𝑒 𝐶 ) )
26 simplr ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ 𝐵 = -∞ ) → 𝐴𝐵 )
27 simpr ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ 𝐵 = -∞ ) → 𝐵 = -∞ )
28 9 adantr ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ 𝐵 = -∞ ) → 𝐴 ∈ ℝ* )
29 mnfle ( 𝐴 ∈ ℝ* → -∞ ≤ 𝐴 )
30 28 29 syl ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ 𝐵 = -∞ ) → -∞ ≤ 𝐴 )
31 27 30 eqbrtrd ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ 𝐵 = -∞ ) → 𝐵𝐴 )
32 simpl2 ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) → 𝐵 ∈ ℝ* )
33 xrletri3 ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) → ( 𝐴 = 𝐵 ↔ ( 𝐴𝐵𝐵𝐴 ) ) )
34 9 32 33 syl2anc ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) → ( 𝐴 = 𝐵 ↔ ( 𝐴𝐵𝐵𝐴 ) ) )
35 34 adantr ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ 𝐵 = -∞ ) → ( 𝐴 = 𝐵 ↔ ( 𝐴𝐵𝐵𝐴 ) ) )
36 26 31 35 mpbir2and ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ 𝐵 = -∞ ) → 𝐴 = 𝐵 )
37 36 oveq1d ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ 𝐵 = -∞ ) → ( 𝐴 +𝑒 𝐶 ) = ( 𝐵 +𝑒 𝐶 ) )
38 25 37 breqtrd ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ 𝐵 = -∞ ) → ( 𝐴 +𝑒 𝐶 ) ≤ ( 𝐵 +𝑒 𝐶 ) )
39 38 adantlr ( ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ ) ) ∧ 𝐵 = -∞ ) → ( 𝐴 +𝑒 𝐶 ) ≤ ( 𝐵 +𝑒 𝐶 ) )
40 elxr ( 𝐵 ∈ ℝ* ↔ ( 𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞ ) )
41 32 40 sylib ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) → ( 𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞ ) )
42 41 adantr ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ ) ) → ( 𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞ ) )
43 8 23 39 42 mpjao3dan ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ ) ) → ( 𝐴 +𝑒 𝐶 ) ≤ ( 𝐵 +𝑒 𝐶 ) )
44 43 anassrs ( ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝐴 ∈ ℝ ) → ( 𝐴 +𝑒 𝐶 ) ≤ ( 𝐵 +𝑒 𝐶 ) )
45 12 adantr ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ 𝐴 = +∞ ) → ( 𝐴 +𝑒 𝐶 ) ∈ ℝ* )
46 45 xrleidd ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ 𝐴 = +∞ ) → ( 𝐴 +𝑒 𝐶 ) ≤ ( 𝐴 +𝑒 𝐶 ) )
47 simplr ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ 𝐴 = +∞ ) → 𝐴𝐵 )
48 pnfge ( 𝐵 ∈ ℝ*𝐵 ≤ +∞ )
49 32 48 syl ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) → 𝐵 ≤ +∞ )
50 49 adantr ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ 𝐴 = +∞ ) → 𝐵 ≤ +∞ )
51 simpr ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ 𝐴 = +∞ ) → 𝐴 = +∞ )
52 50 51 breqtrrd ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ 𝐴 = +∞ ) → 𝐵𝐴 )
53 34 adantr ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ 𝐴 = +∞ ) → ( 𝐴 = 𝐵 ↔ ( 𝐴𝐵𝐵𝐴 ) ) )
54 47 52 53 mpbir2and ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ 𝐴 = +∞ ) → 𝐴 = 𝐵 )
55 54 oveq1d ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ 𝐴 = +∞ ) → ( 𝐴 +𝑒 𝐶 ) = ( 𝐵 +𝑒 𝐶 ) )
56 46 55 breqtrd ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ 𝐴 = +∞ ) → ( 𝐴 +𝑒 𝐶 ) ≤ ( 𝐵 +𝑒 𝐶 ) )
57 56 adantlr ( ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝐴 = +∞ ) → ( 𝐴 +𝑒 𝐶 ) ≤ ( 𝐵 +𝑒 𝐶 ) )
58 oveq1 ( 𝐴 = -∞ → ( 𝐴 +𝑒 𝐶 ) = ( -∞ +𝑒 𝐶 ) )
59 renepnf ( 𝐶 ∈ ℝ → 𝐶 ≠ +∞ )
60 xaddmnf2 ( ( 𝐶 ∈ ℝ*𝐶 ≠ +∞ ) → ( -∞ +𝑒 𝐶 ) = -∞ )
61 17 59 60 syl2anc ( 𝐶 ∈ ℝ → ( -∞ +𝑒 𝐶 ) = -∞ )
62 61 adantl ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ 𝐶 ∈ ℝ ) → ( -∞ +𝑒 𝐶 ) = -∞ )
63 58 62 sylan9eqr ( ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝐴 = -∞ ) → ( 𝐴 +𝑒 𝐶 ) = -∞ )
64 xaddcl ( ( 𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) → ( 𝐵 +𝑒 𝐶 ) ∈ ℝ* )
65 32 10 64 syl2anc ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) → ( 𝐵 +𝑒 𝐶 ) ∈ ℝ* )
66 65 ad2antrr ( ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝐴 = -∞ ) → ( 𝐵 +𝑒 𝐶 ) ∈ ℝ* )
67 mnfle ( ( 𝐵 +𝑒 𝐶 ) ∈ ℝ* → -∞ ≤ ( 𝐵 +𝑒 𝐶 ) )
68 66 67 syl ( ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝐴 = -∞ ) → -∞ ≤ ( 𝐵 +𝑒 𝐶 ) )
69 63 68 eqbrtrd ( ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝐴 = -∞ ) → ( 𝐴 +𝑒 𝐶 ) ≤ ( 𝐵 +𝑒 𝐶 ) )
70 elxr ( 𝐴 ∈ ℝ* ↔ ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞ ) )
71 9 70 sylib ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) → ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞ ) )
72 71 adantr ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ 𝐶 ∈ ℝ ) → ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞ ) )
73 44 57 69 72 mpjao3dan ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ 𝐶 ∈ ℝ ) → ( 𝐴 +𝑒 𝐶 ) ≤ ( 𝐵 +𝑒 𝐶 ) )
74 38 adantlr ( ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ 𝐶 = +∞ ) ∧ 𝐵 = -∞ ) → ( 𝐴 +𝑒 𝐶 ) ≤ ( 𝐵 +𝑒 𝐶 ) )
75 12 ad2antrr ( ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ 𝐶 = +∞ ) ∧ 𝐵 ≠ -∞ ) → ( 𝐴 +𝑒 𝐶 ) ∈ ℝ* )
76 75 14 syl ( ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ 𝐶 = +∞ ) ∧ 𝐵 ≠ -∞ ) → ( 𝐴 +𝑒 𝐶 ) ≤ +∞ )
77 simplr ( ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ 𝐶 = +∞ ) ∧ 𝐵 ≠ -∞ ) → 𝐶 = +∞ )
78 77 oveq2d ( ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ 𝐶 = +∞ ) ∧ 𝐵 ≠ -∞ ) → ( 𝐵 +𝑒 𝐶 ) = ( 𝐵 +𝑒 +∞ ) )
79 32 adantr ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ 𝐶 = +∞ ) → 𝐵 ∈ ℝ* )
80 xaddpnf1 ( ( 𝐵 ∈ ℝ*𝐵 ≠ -∞ ) → ( 𝐵 +𝑒 +∞ ) = +∞ )
81 79 80 sylan ( ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ 𝐶 = +∞ ) ∧ 𝐵 ≠ -∞ ) → ( 𝐵 +𝑒 +∞ ) = +∞ )
82 78 81 eqtrd ( ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ 𝐶 = +∞ ) ∧ 𝐵 ≠ -∞ ) → ( 𝐵 +𝑒 𝐶 ) = +∞ )
83 76 82 breqtrrd ( ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ 𝐶 = +∞ ) ∧ 𝐵 ≠ -∞ ) → ( 𝐴 +𝑒 𝐶 ) ≤ ( 𝐵 +𝑒 𝐶 ) )
84 74 83 pm2.61dane ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ 𝐶 = +∞ ) → ( 𝐴 +𝑒 𝐶 ) ≤ ( 𝐵 +𝑒 𝐶 ) )
85 56 adantlr ( ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ 𝐶 = -∞ ) ∧ 𝐴 = +∞ ) → ( 𝐴 +𝑒 𝐶 ) ≤ ( 𝐵 +𝑒 𝐶 ) )
86 simplr ( ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ 𝐶 = -∞ ) ∧ 𝐴 ≠ +∞ ) → 𝐶 = -∞ )
87 86 oveq2d ( ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ 𝐶 = -∞ ) ∧ 𝐴 ≠ +∞ ) → ( 𝐴 +𝑒 𝐶 ) = ( 𝐴 +𝑒 -∞ ) )
88 9 adantr ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ 𝐶 = -∞ ) → 𝐴 ∈ ℝ* )
89 xaddmnf1 ( ( 𝐴 ∈ ℝ*𝐴 ≠ +∞ ) → ( 𝐴 +𝑒 -∞ ) = -∞ )
90 88 89 sylan ( ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ 𝐶 = -∞ ) ∧ 𝐴 ≠ +∞ ) → ( 𝐴 +𝑒 -∞ ) = -∞ )
91 87 90 eqtrd ( ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ 𝐶 = -∞ ) ∧ 𝐴 ≠ +∞ ) → ( 𝐴 +𝑒 𝐶 ) = -∞ )
92 65 ad2antrr ( ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ 𝐶 = -∞ ) ∧ 𝐴 ≠ +∞ ) → ( 𝐵 +𝑒 𝐶 ) ∈ ℝ* )
93 92 67 syl ( ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ 𝐶 = -∞ ) ∧ 𝐴 ≠ +∞ ) → -∞ ≤ ( 𝐵 +𝑒 𝐶 ) )
94 91 93 eqbrtrd ( ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ 𝐶 = -∞ ) ∧ 𝐴 ≠ +∞ ) → ( 𝐴 +𝑒 𝐶 ) ≤ ( 𝐵 +𝑒 𝐶 ) )
95 85 94 pm2.61dane ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) ∧ 𝐶 = -∞ ) → ( 𝐴 +𝑒 𝐶 ) ≤ ( 𝐵 +𝑒 𝐶 ) )
96 elxr ( 𝐶 ∈ ℝ* ↔ ( 𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞ ) )
97 10 96 sylib ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) → ( 𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞ ) )
98 73 84 95 97 mpjao3dan ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ 𝐴𝐵 ) → ( 𝐴 +𝑒 𝐶 ) ≤ ( 𝐵 +𝑒 𝐶 ) )