This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 𝐴 ≤ 𝐵 ) → ( 𝐴 +𝑒 𝐶 ) ≤ ( 𝐵 +𝑒 𝐶 ) )