ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  xrmaxadd GIF version
Theorem xrmaxadd 11224
Description: Distributing addition over maximum. (Contributed by Jim Kingdon, 11-May-2023.)
Assertion
Ref Expression
xrmaxadd ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )))
Proof of Theorem xrmaxadd
StepHypRef Expression
1 simpr 109 . . 3 (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ∈ ℝ) → 𝐴 ∈ ℝ)
2 simpl2 996 . . 3 (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ∈ ℝ) → 𝐵 ∈ ℝ*)
3 simpl3 997 . . 3 (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ∈ ℝ) → 𝐶 ∈ ℝ*)
4 xrmaxaddlem 11223 . . 3 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )))
51, 2, 3, 4syl3anc 1233 . 2 (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ∈ ℝ) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )))
6 simpllr 529 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → 𝐴 = +∞)
7 simpr 109 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → 𝐶 = -∞)
86, 7oveq12d 5871 . . . . 5 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → (𝐴 +𝑒 𝐶) = (+∞ +𝑒 -∞))
9 simp1 992 . . . . . . . . 9 ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → 𝐴 ∈ ℝ*)
109ad3antrrr 489 . . . . . . . 8 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → 𝐴 ∈ ℝ*)
11 simp2 993 . . . . . . . . 9 ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → 𝐵 ∈ ℝ*)
1211ad3antrrr 489 . . . . . . . 8 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → 𝐵 ∈ ℝ*)
1310, 12xaddcld 9841 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → (𝐴 +𝑒 𝐵) ∈ ℝ*)
14 simp3 994 . . . . . . . . 9 ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → 𝐶 ∈ ℝ*)
1514ad3antrrr 489 . . . . . . . 8 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → 𝐶 ∈ ℝ*)
1610, 15xaddcld 9841 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → (𝐴 +𝑒 𝐶) ∈ ℝ*)
1713, 16jca 304 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → ((𝐴 +𝑒 𝐵) ∈ ℝ* ∧ (𝐴 +𝑒 𝐶) ∈ ℝ*))
18 simplr 525 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) → 𝐴 = +∞)
19 simpr 109 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) → 𝐵 = -∞)
2018, 19oveq12d 5871 . . . . . . . . . 10 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) → (𝐴 +𝑒 𝐵) = (+∞ +𝑒 -∞))
21 pnfaddmnf 9807 . . . . . . . . . 10 (+∞ +𝑒 -∞) = 0
2220, 21eqtrdi 2219 . . . . . . . . 9 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) → (𝐴 +𝑒 𝐵) = 0)
2322adantr 274 . . . . . . . 8 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → (𝐴 +𝑒 𝐵) = 0)
248, 21eqtrdi 2219 . . . . . . . 8 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → (𝐴 +𝑒 𝐶) = 0)
2523, 24eqtr4d 2206 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → (𝐴 +𝑒 𝐵) = (𝐴 +𝑒 𝐶))
2616xrleidd 9758 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → (𝐴 +𝑒 𝐶) ≤ (𝐴 +𝑒 𝐶))
2725, 26eqbrtrd 4011 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → (𝐴 +𝑒 𝐵) ≤ (𝐴 +𝑒 𝐶))
28 xrmaxleim 11207 . . . . . 6 (((𝐴 +𝑒 𝐵) ∈ ℝ* ∧ (𝐴 +𝑒 𝐶) ∈ ℝ*) → ((𝐴 +𝑒 𝐵) ≤ (𝐴 +𝑒 𝐶) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 𝐶)))
2917, 27, 28sylc 62 . . . . 5 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 𝐶))
3012, 15jca 304 . . . . . . . 8 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → (𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*))
31 simplr 525 . . . . . . . . . 10 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → 𝐵 = -∞)
3231, 7eqtr4d 2206 . . . . . . . . 9 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → 𝐵 = 𝐶)
3315xrleidd 9758 . . . . . . . . 9 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → 𝐶 ≤ 𝐶)
3432, 33eqbrtrd 4011 . . . . . . . 8 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → 𝐵 ≤ 𝐶)
35 xrmaxleim 11207 . . . . . . . 8 ((𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (𝐵 ≤ 𝐶 → sup({𝐵, 𝐶}, ℝ*, < ) = 𝐶))
3630, 34, 35sylc 62 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → sup({𝐵, 𝐶}, ℝ*, < ) = 𝐶)
3736, 7eqtrd 2203 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → sup({𝐵, 𝐶}, ℝ*, < ) = -∞)
386, 37oveq12d 5871 . . . . 5 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )) = (+∞ +𝑒 -∞))
398, 29, 383eqtr4d 2213 . . . 4 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )))
40 simpllr 529 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → 𝐴 = +∞)
4140oveq1d 5868 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → (𝐴 +𝑒 𝐶) = (+∞ +𝑒 𝐶))
4214ad3antrrr 489 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → 𝐶 ∈ ℝ*)
43 xaddpnf2 9804 . . . . . . 7 ((𝐶 ∈ ℝ* ∧ 𝐶 ≠ -∞) → (+∞ +𝑒 𝐶) = +∞)
4442, 43sylancom 418 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → (+∞ +𝑒 𝐶) = +∞)
4541, 44eqtrd 2203 . . . . 5 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → (𝐴 +𝑒 𝐶) = +∞)
469, 11xaddcld 9841 . . . . . . . . 9 ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (𝐴 +𝑒 𝐵) ∈ ℝ*)
4746ad3antrrr 489 . . . . . . . 8 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → (𝐴 +𝑒 𝐵) ∈ ℝ*)
48 pnfge 9746 . . . . . . . 8 ((𝐴 +𝑒 𝐵) ∈ ℝ* → (𝐴 +𝑒 𝐵) ≤ +∞)
4947, 48syl 14 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → (𝐴 +𝑒 𝐵) ≤ +∞)
5049, 45breqtrrd 4017 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → (𝐴 +𝑒 𝐵) ≤ (𝐴 +𝑒 𝐶))
519, 14xaddcld 9841 . . . . . . . 8 ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (𝐴 +𝑒 𝐶) ∈ ℝ*)
5251ad3antrrr 489 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → (𝐴 +𝑒 𝐶) ∈ ℝ*)
5347, 52, 28syl2anc 409 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → ((𝐴 +𝑒 𝐵) ≤ (𝐴 +𝑒 𝐶) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 𝐶)))
5450, 53mpd 13 . . . . 5 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 𝐶))
5540oveq1d 5868 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )) = (+∞ +𝑒 sup({𝐵, 𝐶}, ℝ*, < )))
5611ad3antrrr 489 . . . . . . . 8 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → 𝐵 ∈ ℝ*)
57 xrmaxcl 11215 . . . . . . . 8 ((𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → sup({𝐵, 𝐶}, ℝ*, < ) ∈ ℝ*)
5856, 42, 57syl2anc 409 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → sup({𝐵, 𝐶}, ℝ*, < ) ∈ ℝ*)
59 simpr 109 . . . . . . . . . . 11 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → 𝐶 ≠ -∞)
60 nmnfgt 9775 . . . . . . . . . . . 12 (𝐶 ∈ ℝ* → (-∞ < 𝐶 ↔ 𝐶 ≠ -∞))
6142, 60syl 14 . . . . . . . . . . 11 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → (-∞ < 𝐶 ↔ 𝐶 ≠ -∞))
6259, 61mpbird 166 . . . . . . . . . 10 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → -∞ < 𝐶)
6362olcd 729 . . . . . . . . 9 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → (-∞ < 𝐵 ∨ -∞ < 𝐶))
64 mnfxr 7976 . . . . . . . . . . 11 -∞ ∈ ℝ*
6564a1i 9 . . . . . . . . . 10 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → -∞ ∈ ℝ*)
66 xrltmaxsup 11220 . . . . . . . . . 10 ((𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ -∞ ∈ ℝ*) → (-∞ < sup({𝐵, 𝐶}, ℝ*, < ) ↔ (-∞ < 𝐵 ∨ -∞ < 𝐶)))
6756, 42, 65, 66syl3anc 1233 . . . . . . . . 9 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → (-∞ < sup({𝐵, 𝐶}, ℝ*, < ) ↔ (-∞ < 𝐵 ∨ -∞ < 𝐶)))
6863, 67mpbird 166 . . . . . . . 8 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → -∞ < sup({𝐵, 𝐶}, ℝ*, < ))
69 nmnfgt 9775 . . . . . . . . 9 (sup({𝐵, 𝐶}, ℝ*, < ) ∈ ℝ* → (-∞ < sup({𝐵, 𝐶}, ℝ*, < ) ↔ sup({𝐵, 𝐶}, ℝ*, < ) ≠ -∞))
7058, 69syl 14 . . . . . . . 8 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → (-∞ < sup({𝐵, 𝐶}, ℝ*, < ) ↔ sup({𝐵, 𝐶}, ℝ*, < ) ≠ -∞))
7168, 70mpbid 146 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → sup({𝐵, 𝐶}, ℝ*, < ) ≠ -∞)
72 xaddpnf2 9804 . . . . . . 7 ((sup({𝐵, 𝐶}, ℝ*, < ) ∈ ℝ* ∧ sup({𝐵, 𝐶}, ℝ*, < ) ≠ -∞) → (+∞ +𝑒 sup({𝐵, 𝐶}, ℝ*, < )) = +∞)
7358, 71, 72syl2anc 409 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → (+∞ +𝑒 sup({𝐵, 𝐶}, ℝ*, < )) = +∞)
7455, 73eqtrd 2203 . . . . 5 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )) = +∞)
7545, 54, 743eqtr4d 2213 . . . 4 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )))
76 xrmnfdc 9800 . . . . . . 7 (𝐶 ∈ ℝ* → DECID 𝐶 = -∞)
77763ad2ant3 1015 . . . . . 6 ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → DECID 𝐶 = -∞)
7877ad2antrr 485 . . . . 5 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) → DECID 𝐶 = -∞)
79 dcne 2351 . . . . 5 (DECID 𝐶 = -∞ ↔ (𝐶 = -∞ ∨ 𝐶 ≠ -∞))
8078, 79sylib 121 . . . 4 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) → (𝐶 = -∞ ∨ 𝐶 ≠ -∞))
8139, 75, 80mpjaodan 793 . . 3 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )))
8211ad2antrr 485 . . . . . 6 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → 𝐵 ∈ ℝ*)
8314ad2antrr 485 . . . . . 6 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → 𝐶 ∈ ℝ*)
8482, 83, 57syl2anc 409 . . . . 5 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → sup({𝐵, 𝐶}, ℝ*, < ) ∈ ℝ*)
85 simpr 109 . . . . . . . . 9 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → 𝐵 ≠ -∞)
86 nmnfgt 9775 . . . . . . . . . 10 (𝐵 ∈ ℝ* → (-∞ < 𝐵 ↔ 𝐵 ≠ -∞))
8782, 86syl 14 . . . . . . . . 9 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → (-∞ < 𝐵 ↔ 𝐵 ≠ -∞))
8885, 87mpbird 166 . . . . . . . 8 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → -∞ < 𝐵)
8988orcd 728 . . . . . . 7 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → (-∞ < 𝐵 ∨ -∞ < 𝐶))
9064a1i 9 . . . . . . . 8 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → -∞ ∈ ℝ*)
9182, 83, 90, 66syl3anc 1233 . . . . . . 7 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → (-∞ < sup({𝐵, 𝐶}, ℝ*, < ) ↔ (-∞ < 𝐵 ∨ -∞ < 𝐶)))
9289, 91mpbird 166 . . . . . 6 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → -∞ < sup({𝐵, 𝐶}, ℝ*, < ))
9384, 69syl 14 . . . . . 6 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → (-∞ < sup({𝐵, 𝐶}, ℝ*, < ) ↔ sup({𝐵, 𝐶}, ℝ*, < ) ≠ -∞))
9492, 93mpbid 146 . . . . 5 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → sup({𝐵, 𝐶}, ℝ*, < ) ≠ -∞)
9584, 94, 72syl2anc 409 . . . 4 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → (+∞ +𝑒 sup({𝐵, 𝐶}, ℝ*, < )) = +∞)
96 simplr 525 . . . . 5 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → 𝐴 = +∞)
9796oveq1d 5868 . . . 4 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )) = (+∞ +𝑒 sup({𝐵, 𝐶}, ℝ*, < )))
98 prcom 3659 . . . . . 6 {(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)} = {(𝐴 +𝑒 𝐶), (𝐴 +𝑒 𝐵)}
9998supeq1i 6965 . . . . 5 sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = sup({(𝐴 +𝑒 𝐶), (𝐴 +𝑒 𝐵)}, ℝ*, < )
10051ad2antrr 485 . . . . . . . 8 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → (𝐴 +𝑒 𝐶) ∈ ℝ*)
10146ad2antrr 485 . . . . . . . 8 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → (𝐴 +𝑒 𝐵) ∈ ℝ*)
102100, 101jca 304 . . . . . . 7 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → ((𝐴 +𝑒 𝐶) ∈ ℝ* ∧ (𝐴 +𝑒 𝐵) ∈ ℝ*))
103 pnfge 9746 . . . . . . . . 9 ((𝐴 +𝑒 𝐶) ∈ ℝ* → (𝐴 +𝑒 𝐶) ≤ +∞)
104100, 103syl 14 . . . . . . . 8 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → (𝐴 +𝑒 𝐶) ≤ +∞)
10596oveq1d 5868 . . . . . . . . 9 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → (𝐴 +𝑒 𝐵) = (+∞ +𝑒 𝐵))
106 xaddpnf2 9804 . . . . . . . . . 10 ((𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞) → (+∞ +𝑒 𝐵) = +∞)
10782, 106sylancom 418 . . . . . . . . 9 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → (+∞ +𝑒 𝐵) = +∞)
108105, 107eqtrd 2203 . . . . . . . 8 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → (𝐴 +𝑒 𝐵) = +∞)
109104, 108breqtrrd 4017 . . . . . . 7 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → (𝐴 +𝑒 𝐶) ≤ (𝐴 +𝑒 𝐵))
110 xrmaxleim 11207 . . . . . . 7 (((𝐴 +𝑒 𝐶) ∈ ℝ* ∧ (𝐴 +𝑒 𝐵) ∈ ℝ*) → ((𝐴 +𝑒 𝐶) ≤ (𝐴 +𝑒 𝐵) → sup({(𝐴 +𝑒 𝐶), (𝐴 +𝑒 𝐵)}, ℝ*, < ) = (𝐴 +𝑒 𝐵)))
111102, 109, 110sylc 62 . . . . . 6 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → sup({(𝐴 +𝑒 𝐶), (𝐴 +𝑒 𝐵)}, ℝ*, < ) = (𝐴 +𝑒 𝐵))
112111, 108eqtrd 2203 . . . . 5 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → sup({(𝐴 +𝑒 𝐶), (𝐴 +𝑒 𝐵)}, ℝ*, < ) = +∞)
11399, 112eqtrid 2215 . . . 4 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = +∞)
11495, 97, 1133eqtr4rd 2214 . . 3 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )))
115 xrmnfdc 9800 . . . . . 6 (𝐵 ∈ ℝ* → DECID 𝐵 = -∞)
116 dcne 2351 . . . . . 6 (DECID 𝐵 = -∞ ↔ (𝐵 = -∞ ∨ 𝐵 ≠ -∞))
117115, 116sylib 121 . . . . 5 (𝐵 ∈ ℝ* → (𝐵 = -∞ ∨ 𝐵 ≠ -∞))
1181173ad2ant2 1014 . . . 4 ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (𝐵 = -∞ ∨ 𝐵 ≠ -∞))
119118adantr 274 . . 3 (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) → (𝐵 = -∞ ∨ 𝐵 ≠ -∞))
12081, 114, 119mpjaodan 793 . 2 (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )))
121 simpllr 529 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 = +∞) → 𝐴 = -∞)
122 simpr 109 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 = +∞) → 𝐶 = +∞)
123121, 122oveq12d 5871 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 = +∞) → (𝐴 +𝑒 𝐶) = (-∞ +𝑒 +∞))
124 mnfaddpnf 9808 . . . . . 6 (-∞ +𝑒 +∞) = 0
125123, 124eqtrdi 2219 . . . . 5 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 = +∞) → (𝐴 +𝑒 𝐶) = 0)
12646ad3antrrr 489 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 = +∞) → (𝐴 +𝑒 𝐵) ∈ ℝ*)
12751ad3antrrr 489 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 = +∞) → (𝐴 +𝑒 𝐶) ∈ ℝ*)
128126, 127jca 304 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 = +∞) → ((𝐴 +𝑒 𝐵) ∈ ℝ* ∧ (𝐴 +𝑒 𝐶) ∈ ℝ*))
129 0le0 8967 . . . . . . . 8 0 ≤ 0
130129a1i 9 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 = +∞) → 0 ≤ 0)
131 simplr 525 . . . . . . . . . 10 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → 𝐴 = -∞)
132 simpr 109 . . . . . . . . . 10 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → 𝐵 = +∞)
133131, 132oveq12d 5871 . . . . . . . . 9 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → (𝐴 +𝑒 𝐵) = (-∞ +𝑒 +∞))
134133, 124eqtrdi 2219 . . . . . . . 8 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → (𝐴 +𝑒 𝐵) = 0)
135134adantr 274 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 = +∞) → (𝐴 +𝑒 𝐵) = 0)
136130, 135, 1253brtr4d 4021 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 = +∞) → (𝐴 +𝑒 𝐵) ≤ (𝐴 +𝑒 𝐶))
137128, 136, 28sylc 62 . . . . 5 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 = +∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 𝐶))
138 prcom 3659 . . . . . . . . . . 11 {𝐶, 𝐵} = {𝐵, 𝐶}
139138supeq1i 6965 . . . . . . . . . 10 sup({𝐶, 𝐵}, ℝ*, < ) = sup({𝐵, 𝐶}, ℝ*, < )
14014ad2antrr 485 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → 𝐶 ∈ ℝ*)
14111ad2antrr 485 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → 𝐵 ∈ ℝ*)
142140, 141jca 304 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → (𝐶 ∈ ℝ* ∧ 𝐵 ∈ ℝ*))
143 pnfge 9746 . . . . . . . . . . . . . 14 (𝐶 ∈ ℝ* → 𝐶 ≤ +∞)
1441433ad2ant3 1015 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → 𝐶 ≤ +∞)
145144ad2antrr 485 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → 𝐶 ≤ +∞)
146145, 132breqtrrd 4017 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → 𝐶 ≤ 𝐵)
147 xrmaxleim 11207 . . . . . . . . . . 11 ((𝐶 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ≤ 𝐵 → sup({𝐶, 𝐵}, ℝ*, < ) = 𝐵))
148142, 146, 147sylc 62 . . . . . . . . . 10 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → sup({𝐶, 𝐵}, ℝ*, < ) = 𝐵)
149139, 148eqtr3id 2217 . . . . . . . . 9 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → sup({𝐵, 𝐶}, ℝ*, < ) = 𝐵)
150149, 132eqtrd 2203 . . . . . . . 8 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → sup({𝐵, 𝐶}, ℝ*, < ) = +∞)
151150oveq2d 5869 . . . . . . 7 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )) = (𝐴 +𝑒 +∞))
152131oveq1d 5868 . . . . . . . 8 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → (𝐴 +𝑒 +∞) = (-∞ +𝑒 +∞))
153152, 124eqtrdi 2219 . . . . . . 7 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → (𝐴 +𝑒 +∞) = 0)
154151, 153eqtrd 2203 . . . . . 6 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )) = 0)
155154adantr 274 . . . . 5 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 = +∞) → (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )) = 0)
156125, 137, 1553eqtr4d 2213 . . . 4 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 = +∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )))
15751ad3antrrr 489 . . . . . . . . 9 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → (𝐴 +𝑒 𝐶) ∈ ℝ*)
15846ad3antrrr 489 . . . . . . . . 9 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → (𝐴 +𝑒 𝐵) ∈ ℝ*)
159157, 158jca 304 . . . . . . . 8 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → ((𝐴 +𝑒 𝐶) ∈ ℝ* ∧ (𝐴 +𝑒 𝐵) ∈ ℝ*))
160 0xr 7966 . . . . . . . . . 10 0 ∈ ℝ*
161 mnfle 9749 . . . . . . . . . 10 (0 ∈ ℝ* → -∞ ≤ 0)
162160, 161mp1i 10 . . . . . . . . 9 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → -∞ ≤ 0)
163 simpllr 529 . . . . . . . . . . 11 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → 𝐴 = -∞)
164163oveq1d 5868 . . . . . . . . . 10 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → (𝐴 +𝑒 𝐶) = (-∞ +𝑒 𝐶))
165 xaddmnf2 9806 . . . . . . . . . . 11 ((𝐶 ∈ ℝ* ∧ 𝐶 ≠ +∞) → (-∞ +𝑒 𝐶) = -∞)
166140, 165sylan 281 . . . . . . . . . 10 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → (-∞ +𝑒 𝐶) = -∞)
167164, 166eqtrd 2203 . . . . . . . . 9 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → (𝐴 +𝑒 𝐶) = -∞)
168134adantr 274 . . . . . . . . 9 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → (𝐴 +𝑒 𝐵) = 0)
169162, 167, 1683brtr4d 4021 . . . . . . . 8 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → (𝐴 +𝑒 𝐶) ≤ (𝐴 +𝑒 𝐵))
170159, 169, 110sylc 62 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → sup({(𝐴 +𝑒 𝐶), (𝐴 +𝑒 𝐵)}, ℝ*, < ) = (𝐴 +𝑒 𝐵))
171170, 168eqtrd 2203 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → sup({(𝐴 +𝑒 𝐶), (𝐴 +𝑒 𝐵)}, ℝ*, < ) = 0)
17299, 171eqtrid 2215 . . . . 5 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = 0)
173154adantr 274 . . . . 5 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )) = 0)
174172, 173eqtr4d 2206 . . . 4 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )))
175 xrpnfdc 9799 . . . . . . 7 (𝐶 ∈ ℝ* → DECID 𝐶 = +∞)
176 dcne 2351 . . . . . . 7 (DECID 𝐶 = +∞ ↔ (𝐶 = +∞ ∨ 𝐶 ≠ +∞))
177175, 176sylib 121 . . . . . 6 (𝐶 ∈ ℝ* → (𝐶 = +∞ ∨ 𝐶 ≠ +∞))
1781773ad2ant3 1015 . . . . 5 ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (𝐶 = +∞ ∨ 𝐶 ≠ +∞))
179178ad2antrr 485 . . . 4 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → (𝐶 = +∞ ∨ 𝐶 ≠ +∞))
180156, 174, 179mpjaodan 793 . . 3 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )))
181 simpllr 529 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → 𝐴 = -∞)
182 simpr 109 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → 𝐶 = +∞)
183181, 182oveq12d 5871 . . . . 5 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → (𝐴 +𝑒 𝐶) = (-∞ +𝑒 +∞))
18446ad2antrr 485 . . . . . . . 8 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) → (𝐴 +𝑒 𝐵) ∈ ℝ*)
18551ad2antrr 485 . . . . . . . 8 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) → (𝐴 +𝑒 𝐶) ∈ ℝ*)
186184, 185jca 304 . . . . . . 7 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) → ((𝐴 +𝑒 𝐵) ∈ ℝ* ∧ (𝐴 +𝑒 𝐶) ∈ ℝ*))
187 simplr 525 . . . . . . . . . 10 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) → 𝐴 = -∞)
188187oveq1d 5868 . . . . . . . . 9 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) → (𝐴 +𝑒 𝐵) = (-∞ +𝑒 𝐵))
18911ad2antrr 485 . . . . . . . . . 10 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) → 𝐵 ∈ ℝ*)
190 xaddmnf2 9806 . . . . . . . . . 10 ((𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞) → (-∞ +𝑒 𝐵) = -∞)
191189, 190sylancom 418 . . . . . . . . 9 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) → (-∞ +𝑒 𝐵) = -∞)
192188, 191eqtrd 2203 . . . . . . . 8 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) → (𝐴 +𝑒 𝐵) = -∞)
193 mnfle 9749 . . . . . . . . 9 ((𝐴 +𝑒 𝐶) ∈ ℝ* → -∞ ≤ (𝐴 +𝑒 𝐶))
194185, 193syl 14 . . . . . . . 8 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) → -∞ ≤ (𝐴 +𝑒 𝐶))
195192, 194eqbrtrd 4011 . . . . . . 7 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) → (𝐴 +𝑒 𝐵) ≤ (𝐴 +𝑒 𝐶))
196186, 195, 28sylc 62 . . . . . 6 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 𝐶))
197196adantr 274 . . . . 5 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 𝐶))
198189adantr 274 . . . . . . . . 9 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → 𝐵 ∈ ℝ*)
19914ad3antrrr 489 . . . . . . . . 9 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → 𝐶 ∈ ℝ*)
200198, 199jca 304 . . . . . . . 8 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → (𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*))
201 simpr 109 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) → 𝐵 ≠ +∞)
202 npnflt 9772 . . . . . . . . . . . . 13 (𝐵 ∈ ℝ* → (𝐵 < +∞ ↔ 𝐵 ≠ +∞))
203189, 202syl 14 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) → (𝐵 < +∞ ↔ 𝐵 ≠ +∞))
204201, 203mpbird 166 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) → 𝐵 < +∞)
205204adantr 274 . . . . . . . . . 10 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → 𝐵 < +∞)
206205, 182breqtrrd 4017 . . . . . . . . 9 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → 𝐵 < 𝐶)
207198, 199, 206xrltled 9756 . . . . . . . 8 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → 𝐵 ≤ 𝐶)
208200, 207, 35sylc 62 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → sup({𝐵, 𝐶}, ℝ*, < ) = 𝐶)
209208, 182eqtrd 2203 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → sup({𝐵, 𝐶}, ℝ*, < ) = +∞)
210181, 209oveq12d 5871 . . . . 5 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )) = (-∞ +𝑒 +∞))
211183, 197, 2103eqtr4d 2213 . . . 4 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )))
212189adantr 274 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → 𝐵 ∈ ℝ*)
21314ad3antrrr 489 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → 𝐶 ∈ ℝ*)
214212, 213, 57syl2anc 409 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → sup({𝐵, 𝐶}, ℝ*, < ) ∈ ℝ*)
215204adantr 274 . . . . . . . . 9 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → 𝐵 < +∞)
216 simpr 109 . . . . . . . . . 10 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → 𝐶 ≠ +∞)
217 npnflt 9772 . . . . . . . . . . 11 (𝐶 ∈ ℝ* → (𝐶 < +∞ ↔ 𝐶 ≠ +∞))
218213, 217syl 14 . . . . . . . . . 10 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → (𝐶 < +∞ ↔ 𝐶 ≠ +∞))
219216, 218mpbird 166 . . . . . . . . 9 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → 𝐶 < +∞)
220215, 219jca 304 . . . . . . . 8 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → (𝐵 < +∞ ∧ 𝐶 < +∞))
221 pnfxr 7972 . . . . . . . . . 10 +∞ ∈ ℝ*
222221a1i 9 . . . . . . . . 9 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → +∞ ∈ ℝ*)
223 xrmaxltsup 11221 . . . . . . . . 9 ((𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (sup({𝐵, 𝐶}, ℝ*, < ) < +∞ ↔ (𝐵 < +∞ ∧ 𝐶 < +∞)))
224212, 213, 222, 223syl3anc 1233 . . . . . . . 8 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → (sup({𝐵, 𝐶}, ℝ*, < ) < +∞ ↔ (𝐵 < +∞ ∧ 𝐶 < +∞)))
225220, 224mpbird 166 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → sup({𝐵, 𝐶}, ℝ*, < ) < +∞)
226 npnflt 9772 . . . . . . . 8 (sup({𝐵, 𝐶}, ℝ*, < ) ∈ ℝ* → (sup({𝐵, 𝐶}, ℝ*, < ) < +∞ ↔ sup({𝐵, 𝐶}, ℝ*, < ) ≠ +∞))
227214, 226syl 14 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → (sup({𝐵, 𝐶}, ℝ*, < ) < +∞ ↔ sup({𝐵, 𝐶}, ℝ*, < ) ≠ +∞))
228225, 227mpbid 146 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → sup({𝐵, 𝐶}, ℝ*, < ) ≠ +∞)
229 xaddmnf2 9806 . . . . . 6 ((sup({𝐵, 𝐶}, ℝ*, < ) ∈ ℝ* ∧ sup({𝐵, 𝐶}, ℝ*, < ) ≠ +∞) → (-∞ +𝑒 sup({𝐵, 𝐶}, ℝ*, < )) = -∞)
230214, 228, 229syl2anc 409 . . . . 5 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → (-∞ +𝑒 sup({𝐵, 𝐶}, ℝ*, < )) = -∞)
231 simpllr 529 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → 𝐴 = -∞)
232231oveq1d 5868 . . . . 5 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )) = (-∞ +𝑒 sup({𝐵, 𝐶}, ℝ*, < )))
233196adantr 274 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 𝐶))
234231oveq1d 5868 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → (𝐴 +𝑒 𝐶) = (-∞ +𝑒 𝐶))
235233, 234eqtrd 2203 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (-∞ +𝑒 𝐶))
236213, 165sylancom 418 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → (-∞ +𝑒 𝐶) = -∞)
237235, 236eqtrd 2203 . . . . 5 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = -∞)
238230, 232, 2373eqtr4rd 2214 . . . 4 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )))
239178ad2antrr 485 . . . 4 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) → (𝐶 = +∞ ∨ 𝐶 ≠ +∞))
240211, 238, 239mpjaodan 793 . . 3 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )))
241 xrpnfdc 9799 . . . . . 6 (𝐵 ∈ ℝ* → DECID 𝐵 = +∞)
2422413ad2ant2 1014 . . . . 5 ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → DECID 𝐵 = +∞)
243 dcne 2351 . . . . 5 (DECID 𝐵 = +∞ ↔ (𝐵 = +∞ ∨ 𝐵 ≠ +∞))
244242, 243sylib 121 . . . 4 ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (𝐵 = +∞ ∨ 𝐵 ≠ +∞))
245244adantr 274 . . 3 (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) → (𝐵 = +∞ ∨ 𝐵 ≠ +∞))
246180, 240, 245mpjaodan 793 . 2 (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )))
247 elxr 9733 . . . 4 (𝐴 ∈ ℝ* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
248247biimpi 119 . . 3 (𝐴 ∈ ℝ* → (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
2492483ad2ant1 1013 . 2 ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
2505, 120, 246, 249mpjao3dan 1302 1 ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )))
Colors of variables: wff set class
Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 703  DECID wdc 829   ∨ w3o 972   ∧ w3a 973   = wceq 1348   ∈ wcel 2141   ≠ wne 2340  {cpr 3584   class class class wbr 3989  (class class class)co 5853  supcsup 6959  ℝcr 7773  0cc0 7774  +∞cpnf 7951  -∞cmnf 7952  ℝ*cxr 7953   < clt 7954   ≤ cle 7955   +𝑒 cxad 9727
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-13 2143  ax-14 2144  ax-ext 2152  ax-coll 4104  ax-sep 4107  ax-nul 4115  ax-pow 4160  ax-pr 4194  ax-un 4418  ax-setind 4521  ax-iinf 4572  ax-cnex 7865  ax-resscn 7866  ax-1cn 7867  ax-1re 7868  ax-icn 7869  ax-addcl 7870  ax-addrcl 7871  ax-mulcl 7872  ax-mulrcl 7873  ax-addcom 7874  ax-mulcom 7875  ax-addass 7876  ax-mulass 7877  ax-distr 7878  ax-i2m1 7879  ax-0lt1 7880  ax-1rid 7881  ax-0id 7882  ax-rnegex 7883  ax-precex 7884  ax-cnre 7885  ax-pre-ltirr 7886  ax-pre-ltwlin 7887  ax-pre-lttrn 7888  ax-pre-apti 7889  ax-pre-ltadd 7890  ax-pre-mulgt0 7891  ax-pre-mulext 7892  ax-arch 7893  ax-caucvg 7894
This theorem depends on definitions:  df-bi 116  df-dc 830  df-3or 974  df-3an 975  df-tru 1351  df-fal 1354  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ne 2341  df-nel 2436  df-ral 2453  df-rex 2454  df-reu 2455  df-rmo 2456  df-rab 2457  df-v 2732  df-sbc 2956  df-csb 3050  df-dif 3123  df-un 3125  df-in 3127  df-ss 3134  df-nul 3415  df-if 3527  df-pw 3568  df-sn 3589  df-pr 3590  df-op 3592  df-uni 3797  df-int 3832  df-iun 3875  df-br 3990  df-opab 4051  df-mpt 4052  df-tr 4088  df-id 4278  df-po 4281  df-iso 4282  df-iord 4351  df-on 4353  df-ilim 4354  df-suc 4356  df-iom 4575  df-xp 4617  df-rel 4618  df-cnv 4619  df-co 4620  df-dm 4621  df-rn 4622  df-res 4623  df-ima 4624  df-iota 5160  df-fun 5200  df-fn 5201  df-f 5202  df-f1 5203  df-fo 5204  df-f1o 5205  df-fv 5206  df-riota 5809  df-ov 5856  df-oprab 5857  df-mpo 5858  df-1st 6119  df-2nd 6120  df-recs 6284  df-frec 6370  df-sup 6961  df-pnf 7956  df-mnf 7957  df-xr 7958  df-ltxr 7959  df-le 7960  df-sub 8092  df-neg 8093  df-reap 8494  df-ap 8501  df-div 8590  df-inn 8879  df-2 8937  df-3 8938  df-4 8939  df-n0 9136  df-z 9213  df-uz 9488  df-rp 9611  df-xneg 9729  df-xadd 9730  df-seqfrec 10402  df-exp 10476  df-cj 10806  df-re 10807  df-im 10808  df-rsqrt 10962  df-abs 10963
This theorem is referenced by:  xrminadd  11238
  Copyright terms: Public domain W3C validator