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