MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xleadd1a Structured version   Visualization version   GIF version

Theorem xleadd1a 12165
Description: Extended real version of leadd1 10577; note that the converse implication is not true, unlike the real version (for example 0 < 1 but (1 +𝑒 +∞) ≤ (0 +𝑒 +∞)). (Contributed by Mario Carneiro, 20-Aug-2015.)
Assertion
Ref Expression
xleadd1a (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶))

Proof of Theorem xleadd1a
StepHypRef Expression
1 simplrr 820 . . . . . . 7 (((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) ∧ 𝐵 ∈ ℝ) → 𝐴 ∈ ℝ)
2 simpr 479 . . . . . . 7 (((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) ∧ 𝐵 ∈ ℝ) → 𝐵 ∈ ℝ)
3 simplrl 819 . . . . . . 7 (((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) ∧ 𝐵 ∈ ℝ) → 𝐶 ∈ ℝ)
4 simpllr 817 . . . . . . 7 (((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) ∧ 𝐵 ∈ ℝ) → 𝐴𝐵)
51, 2, 3, 4leadd1dd 10722 . . . . . 6 (((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐶) ≤ (𝐵 + 𝐶))
6 rexadd 12145 . . . . . . 7 ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 +𝑒 𝐶) = (𝐴 + 𝐶))
71, 3, 6syl2anc 696 . . . . . 6 (((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) ∧ 𝐵 ∈ ℝ) → (𝐴 +𝑒 𝐶) = (𝐴 + 𝐶))
8 rexadd 12145 . . . . . . 7 ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 +𝑒 𝐶) = (𝐵 + 𝐶))
92, 3, 8syl2anc 696 . . . . . 6 (((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) ∧ 𝐵 ∈ ℝ) → (𝐵 +𝑒 𝐶) = (𝐵 + 𝐶))
105, 7, 93brtr4d 4760 . . . . 5 (((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) ∧ 𝐵 ∈ ℝ) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶))
11 simpl1 1146 . . . . . . . . 9 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) → 𝐴 ∈ ℝ*)
12 simpl3 1148 . . . . . . . . 9 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) → 𝐶 ∈ ℝ*)
13 xaddcl 12152 . . . . . . . . 9 ((𝐴 ∈ ℝ*𝐶 ∈ ℝ*) → (𝐴 +𝑒 𝐶) ∈ ℝ*)
1411, 12, 13syl2anc 696 . . . . . . . 8 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) → (𝐴 +𝑒 𝐶) ∈ ℝ*)
1514ad2antrr 764 . . . . . . 7 (((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) ∧ 𝐵 = +∞) → (𝐴 +𝑒 𝐶) ∈ ℝ*)
16 pnfge 12046 . . . . . . 7 ((𝐴 +𝑒 𝐶) ∈ ℝ* → (𝐴 +𝑒 𝐶) ≤ +∞)
1715, 16syl 17 . . . . . 6 (((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) ∧ 𝐵 = +∞) → (𝐴 +𝑒 𝐶) ≤ +∞)
18 oveq1 6740 . . . . . . 7 (𝐵 = +∞ → (𝐵 +𝑒 𝐶) = (+∞ +𝑒 𝐶))
19 rexr 10166 . . . . . . . . 9 (𝐶 ∈ ℝ → 𝐶 ∈ ℝ*)
20 renemnf 10169 . . . . . . . . 9 (𝐶 ∈ ℝ → 𝐶 ≠ -∞)
21 xaddpnf2 12140 . . . . . . . . 9 ((𝐶 ∈ ℝ*𝐶 ≠ -∞) → (+∞ +𝑒 𝐶) = +∞)
2219, 20, 21syl2anc 696 . . . . . . . 8 (𝐶 ∈ ℝ → (+∞ +𝑒 𝐶) = +∞)
2322ad2antrl 766 . . . . . . 7 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) → (+∞ +𝑒 𝐶) = +∞)
2418, 23sylan9eqr 2748 . . . . . 6 (((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) ∧ 𝐵 = +∞) → (𝐵 +𝑒 𝐶) = +∞)
2517, 24breqtrrd 4756 . . . . 5 (((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) ∧ 𝐵 = +∞) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶))
2614adantr 472 . . . . . . . 8 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ 𝐵 = -∞) → (𝐴 +𝑒 𝐶) ∈ ℝ*)
27 xrleid 12065 . . . . . . . 8 ((𝐴 +𝑒 𝐶) ∈ ℝ* → (𝐴 +𝑒 𝐶) ≤ (𝐴 +𝑒 𝐶))
2826, 27syl 17 . . . . . . 7 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ 𝐵 = -∞) → (𝐴 +𝑒 𝐶) ≤ (𝐴 +𝑒 𝐶))
29 simplr 809 . . . . . . . . 9 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ 𝐵 = -∞) → 𝐴𝐵)
30 simpr 479 . . . . . . . . . 10 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ 𝐵 = -∞) → 𝐵 = -∞)
3111adantr 472 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ 𝐵 = -∞) → 𝐴 ∈ ℝ*)
32 mnfle 12051 . . . . . . . . . . 11 (𝐴 ∈ ℝ* → -∞ ≤ 𝐴)
3331, 32syl 17 . . . . . . . . . 10 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ 𝐵 = -∞) → -∞ ≤ 𝐴)
3430, 33eqbrtrd 4750 . . . . . . . . 9 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ 𝐵 = -∞) → 𝐵𝐴)
35 simpl2 1147 . . . . . . . . . . 11 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) → 𝐵 ∈ ℝ*)
36 xrletri3 12067 . . . . . . . . . . 11 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴)))
3711, 35, 36syl2anc 696 . . . . . . . . . 10 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) → (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴)))
3837adantr 472 . . . . . . . . 9 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ 𝐵 = -∞) → (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴)))
3929, 34, 38mpbir2and 995 . . . . . . . 8 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ 𝐵 = -∞) → 𝐴 = 𝐵)
4039oveq1d 6748 . . . . . . 7 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ 𝐵 = -∞) → (𝐴 +𝑒 𝐶) = (𝐵 +𝑒 𝐶))
4128, 40breqtrd 4754 . . . . . 6 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ 𝐵 = -∞) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶))
4241adantlr 753 . . . . 5 (((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) ∧ 𝐵 = -∞) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶))
43 elxr 12032 . . . . . . 7 (𝐵 ∈ ℝ* ↔ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞))
4435, 43sylib 208 . . . . . 6 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) → (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞))
4544adantr 472 . . . . 5 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) → (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞))
4610, 25, 42, 45mpjao3dan 1476 . . . 4 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶))
4746anassrs 683 . . 3 (((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ∈ ℝ) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶))
4814adantr 472 . . . . . 6 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ 𝐴 = +∞) → (𝐴 +𝑒 𝐶) ∈ ℝ*)
4948, 27syl 17 . . . . 5 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ 𝐴 = +∞) → (𝐴 +𝑒 𝐶) ≤ (𝐴 +𝑒 𝐶))
50 simplr 809 . . . . . . 7 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ 𝐴 = +∞) → 𝐴𝐵)
51 pnfge 12046 . . . . . . . . . 10 (𝐵 ∈ ℝ*𝐵 ≤ +∞)
5235, 51syl 17 . . . . . . . . 9 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) → 𝐵 ≤ +∞)
5352adantr 472 . . . . . . . 8 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ 𝐴 = +∞) → 𝐵 ≤ +∞)
54 simpr 479 . . . . . . . 8 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ 𝐴 = +∞) → 𝐴 = +∞)
5553, 54breqtrrd 4756 . . . . . . 7 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ 𝐴 = +∞) → 𝐵𝐴)
5637adantr 472 . . . . . . 7 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ 𝐴 = +∞) → (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴)))
5750, 55, 56mpbir2and 995 . . . . . 6 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ 𝐴 = +∞) → 𝐴 = 𝐵)
5857oveq1d 6748 . . . . 5 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ 𝐴 = +∞) → (𝐴 +𝑒 𝐶) = (𝐵 +𝑒 𝐶))
5949, 58breqtrd 4754 . . . 4 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ 𝐴 = +∞) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶))
6059adantlr 753 . . 3 (((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ 𝐶 ∈ ℝ) ∧ 𝐴 = +∞) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶))
61 oveq1 6740 . . . . 5 (𝐴 = -∞ → (𝐴 +𝑒 𝐶) = (-∞ +𝑒 𝐶))
62 renepnf 10168 . . . . . . 7 (𝐶 ∈ ℝ → 𝐶 ≠ +∞)
63 xaddmnf2 12142 . . . . . . 7 ((𝐶 ∈ ℝ*𝐶 ≠ +∞) → (-∞ +𝑒 𝐶) = -∞)
6419, 62, 63syl2anc 696 . . . . . 6 (𝐶 ∈ ℝ → (-∞ +𝑒 𝐶) = -∞)
6564adantl 473 . . . . 5 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ 𝐶 ∈ ℝ) → (-∞ +𝑒 𝐶) = -∞)
6661, 65sylan9eqr 2748 . . . 4 (((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ 𝐶 ∈ ℝ) ∧ 𝐴 = -∞) → (𝐴 +𝑒 𝐶) = -∞)
67 xaddcl 12152 . . . . . . 7 ((𝐵 ∈ ℝ*𝐶 ∈ ℝ*) → (𝐵 +𝑒 𝐶) ∈ ℝ*)
6835, 12, 67syl2anc 696 . . . . . 6 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) → (𝐵 +𝑒 𝐶) ∈ ℝ*)
6968ad2antrr 764 . . . . 5 (((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ 𝐶 ∈ ℝ) ∧ 𝐴 = -∞) → (𝐵 +𝑒 𝐶) ∈ ℝ*)
70 mnfle 12051 . . . . 5 ((𝐵 +𝑒 𝐶) ∈ ℝ* → -∞ ≤ (𝐵 +𝑒 𝐶))
7169, 70syl 17 . . . 4 (((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ 𝐶 ∈ ℝ) ∧ 𝐴 = -∞) → -∞ ≤ (𝐵 +𝑒 𝐶))
7266, 71eqbrtrd 4750 . . 3 (((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ 𝐶 ∈ ℝ) ∧ 𝐴 = -∞) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶))
73 elxr 12032 . . . . 5 (𝐴 ∈ ℝ* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
7411, 73sylib 208 . . . 4 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) → (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
7574adantr 472 . . 3 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ 𝐶 ∈ ℝ) → (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
7647, 60, 72, 75mpjao3dan 1476 . 2 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ 𝐶 ∈ ℝ) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶))
7741adantlr 753 . . 3 (((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ 𝐶 = +∞) ∧ 𝐵 = -∞) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶))
7814ad2antrr 764 . . . . 5 (((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ 𝐶 = +∞) ∧ 𝐵 ≠ -∞) → (𝐴 +𝑒 𝐶) ∈ ℝ*)
7978, 16syl 17 . . . 4 (((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ 𝐶 = +∞) ∧ 𝐵 ≠ -∞) → (𝐴 +𝑒 𝐶) ≤ +∞)
80 simplr 809 . . . . . 6 (((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ 𝐶 = +∞) ∧ 𝐵 ≠ -∞) → 𝐶 = +∞)
8180oveq2d 6749 . . . . 5 (((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ 𝐶 = +∞) ∧ 𝐵 ≠ -∞) → (𝐵 +𝑒 𝐶) = (𝐵 +𝑒 +∞))
8235adantr 472 . . . . . 6 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ 𝐶 = +∞) → 𝐵 ∈ ℝ*)
83 xaddpnf1 12139 . . . . . 6 ((𝐵 ∈ ℝ*𝐵 ≠ -∞) → (𝐵 +𝑒 +∞) = +∞)
8482, 83sylan 489 . . . . 5 (((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ 𝐶 = +∞) ∧ 𝐵 ≠ -∞) → (𝐵 +𝑒 +∞) = +∞)
8581, 84eqtrd 2726 . . . 4 (((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ 𝐶 = +∞) ∧ 𝐵 ≠ -∞) → (𝐵 +𝑒 𝐶) = +∞)
8679, 85breqtrrd 4756 . . 3 (((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ 𝐶 = +∞) ∧ 𝐵 ≠ -∞) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶))
8777, 86pm2.61dane 2951 . 2 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ 𝐶 = +∞) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶))
8859adantlr 753 . . 3 (((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ 𝐶 = -∞) ∧ 𝐴 = +∞) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶))
89 simplr 809 . . . . . 6 (((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ 𝐶 = -∞) ∧ 𝐴 ≠ +∞) → 𝐶 = -∞)
9089oveq2d 6749 . . . . 5 (((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ 𝐶 = -∞) ∧ 𝐴 ≠ +∞) → (𝐴 +𝑒 𝐶) = (𝐴 +𝑒 -∞))
9111adantr 472 . . . . . 6 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ 𝐶 = -∞) → 𝐴 ∈ ℝ*)
92 xaddmnf1 12141 . . . . . 6 ((𝐴 ∈ ℝ*𝐴 ≠ +∞) → (𝐴 +𝑒 -∞) = -∞)
9391, 92sylan 489 . . . . 5 (((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ 𝐶 = -∞) ∧ 𝐴 ≠ +∞) → (𝐴 +𝑒 -∞) = -∞)
9490, 93eqtrd 2726 . . . 4 (((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ 𝐶 = -∞) ∧ 𝐴 ≠ +∞) → (𝐴 +𝑒 𝐶) = -∞)
9568ad2antrr 764 . . . . 5 (((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ 𝐶 = -∞) ∧ 𝐴 ≠ +∞) → (𝐵 +𝑒 𝐶) ∈ ℝ*)
9695, 70syl 17 . . . 4 (((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ 𝐶 = -∞) ∧ 𝐴 ≠ +∞) → -∞ ≤ (𝐵 +𝑒 𝐶))
9794, 96eqbrtrd 4750 . . 3 (((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ 𝐶 = -∞) ∧ 𝐴 ≠ +∞) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶))
9888, 97pm2.61dane 2951 . 2 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) ∧ 𝐶 = -∞) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶))
99 elxr 12032 . . 3 (𝐶 ∈ ℝ* ↔ (𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞))
10012, 99sylib 208 . 2 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) → (𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞))
10176, 87, 98, 100mpjao3dan 1476 1 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3o 1071  w3a 1072   = wceq 1564  wcel 2071  wne 2864   class class class wbr 4728  (class class class)co 6733  cr 10016   + caddc 10020  +∞cpnf 10152  -∞cmnf 10153  *cxr 10154  cle 10156   +𝑒 cxad 12026
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1818  ax-5 1920  ax-6 1986  ax-7 2022  ax-8 2073  ax-9 2080  ax-10 2100  ax-11 2115  ax-12 2128  ax-13 2323  ax-ext 2672  ax-sep 4857  ax-nul 4865  ax-pow 4916  ax-pr 4979  ax-un 7034  ax-cnex 10073  ax-resscn 10074  ax-1cn 10075  ax-icn 10076  ax-addcl 10077  ax-addrcl 10078  ax-mulcl 10079  ax-mulrcl 10080  ax-mulcom 10081  ax-addass 10082  ax-mulass 10083  ax-distr 10084  ax-i2m1 10085  ax-1ne0 10086  ax-1rid 10087  ax-rnegex 10088  ax-rrecex 10089  ax-cnre 10090  ax-pre-lttri 10091  ax-pre-lttrn 10092  ax-pre-ltadd 10093
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1567  df-ex 1786  df-nf 1791  df-sb 1979  df-eu 2543  df-mo 2544  df-clab 2679  df-cleq 2685  df-clel 2688  df-nfc 2823  df-ne 2865  df-nel 2968  df-ral 2987  df-rex 2988  df-rab 2991  df-v 3274  df-sbc 3510  df-csb 3608  df-dif 3651  df-un 3653  df-in 3655  df-ss 3662  df-nul 3992  df-if 4163  df-pw 4236  df-sn 4254  df-pr 4256  df-op 4260  df-uni 4513  df-iun 4598  df-br 4729  df-opab 4789  df-mpt 4806  df-id 5096  df-po 5107  df-so 5108  df-xp 5192  df-rel 5193  df-cnv 5194  df-co 5195  df-dm 5196  df-rn 5197  df-res 5198  df-ima 5199  df-iota 5932  df-fun 5971  df-fn 5972  df-f 5973  df-f1 5974  df-fo 5975  df-f1o 5976  df-fv 5977  df-ov 6736  df-oprab 6737  df-mpt2 6738  df-1st 7253  df-2nd 7254  df-er 7830  df-en 8041  df-dom 8042  df-sdom 8043  df-pnf 10157  df-mnf 10158  df-xr 10159  df-ltxr 10160  df-le 10161  df-xadd 12029
This theorem is referenced by:  xleadd2a  12166  xleadd1  12167  xaddge0  12170  xle2add  12171  imasdsf1olem  22268  xblss2ps  22296  xblss2  22297  stdbdxmet  22410  xrge0omnd  29909  measunl  30477  carsgclctunlem2  30579  xleadd1d  39928
  Copyright terms: Public domain W3C validator