ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  xrmaxadd GIF version
Theorem xrmaxadd 11202
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 991 . . 3 (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ∈ ℝ) → 𝐵 ∈ ℝ*)
3 simpl3 992 . . 3 (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ∈ ℝ) → 𝐶 ∈ ℝ*)
4 xrmaxaddlem 11201 . . 3 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )))
51, 2, 3, 4syl3anc 1228 . 2 (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ∈ ℝ) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )))
6 simpllr 524 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → 𝐴 = +∞)
7 simpr 109 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → 𝐶 = -∞)
86, 7oveq12d 5860 . . . . 5 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → (𝐴 +𝑒 𝐶) = (+∞ +𝑒 -∞))
9 simp1 987 . . . . . . . . 9 ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → 𝐴 ∈ ℝ*)
109ad3antrrr 484 . . . . . . . 8 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → 𝐴 ∈ ℝ*)
11 simp2 988 . . . . . . . . 9 ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → 𝐵 ∈ ℝ*)
1211ad3antrrr 484 . . . . . . . 8 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → 𝐵 ∈ ℝ*)
1310, 12xaddcld 9820 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → (𝐴 +𝑒 𝐵) ∈ ℝ*)
14 simp3 989 . . . . . . . . 9 ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → 𝐶 ∈ ℝ*)
1514ad3antrrr 484 . . . . . . . 8 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → 𝐶 ∈ ℝ*)
1610, 15xaddcld 9820 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → (𝐴 +𝑒 𝐶) ∈ ℝ*)
1713, 16jca 304 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → ((𝐴 +𝑒 𝐵) ∈ ℝ* ∧ (𝐴 +𝑒 𝐶) ∈ ℝ*))
18 simplr 520 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) → 𝐴 = +∞)
19 simpr 109 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) → 𝐵 = -∞)
2018, 19oveq12d 5860 . . . . . . . . . 10 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) → (𝐴 +𝑒 𝐵) = (+∞ +𝑒 -∞))
21 pnfaddmnf 9786 . . . . . . . . . 10 (+∞ +𝑒 -∞) = 0
2220, 21eqtrdi 2215 . . . . . . . . 9 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) → (𝐴 +𝑒 𝐵) = 0)
2322adantr 274 . . . . . . . 8 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → (𝐴 +𝑒 𝐵) = 0)
248, 21eqtrdi 2215 . . . . . . . 8 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → (𝐴 +𝑒 𝐶) = 0)
2523, 24eqtr4d 2201 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → (𝐴 +𝑒 𝐵) = (𝐴 +𝑒 𝐶))
2616xrleidd 9737 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → (𝐴 +𝑒 𝐶) ≤ (𝐴 +𝑒 𝐶))
2725, 26eqbrtrd 4004 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → (𝐴 +𝑒 𝐵) ≤ (𝐴 +𝑒 𝐶))
28 xrmaxleim 11185 . . . . . 6 (((𝐴 +𝑒 𝐵) ∈ ℝ* ∧ (𝐴 +𝑒 𝐶) ∈ ℝ*) → ((𝐴 +𝑒 𝐵) ≤ (𝐴 +𝑒 𝐶) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 𝐶)))
2917, 27, 28sylc 62 . . . . 5 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 𝐶))
3012, 15jca 304 . . . . . . . 8 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → (𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*))
31 simplr 520 . . . . . . . . . 10 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → 𝐵 = -∞)
3231, 7eqtr4d 2201 . . . . . . . . 9 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → 𝐵 = 𝐶)
3315xrleidd 9737 . . . . . . . . 9 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → 𝐶 ≤ 𝐶)
3432, 33eqbrtrd 4004 . . . . . . . 8 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → 𝐵 ≤ 𝐶)
35 xrmaxleim 11185 . . . . . . . 8 ((𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (𝐵 ≤ 𝐶 → sup({𝐵, 𝐶}, ℝ*, < ) = 𝐶))
3630, 34, 35sylc 62 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → sup({𝐵, 𝐶}, ℝ*, < ) = 𝐶)
3736, 7eqtrd 2198 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → sup({𝐵, 𝐶}, ℝ*, < ) = -∞)
386, 37oveq12d 5860 . . . . 5 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )) = (+∞ +𝑒 -∞))
398, 29, 383eqtr4d 2208 . . . 4 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )))
40 simpllr 524 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → 𝐴 = +∞)
4140oveq1d 5857 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → (𝐴 +𝑒 𝐶) = (+∞ +𝑒 𝐶))
4214ad3antrrr 484 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → 𝐶 ∈ ℝ*)
43 xaddpnf2 9783 . . . . . . 7 ((𝐶 ∈ ℝ* ∧ 𝐶 ≠ -∞) → (+∞ +𝑒 𝐶) = +∞)
4442, 43sylancom 417 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → (+∞ +𝑒 𝐶) = +∞)
4541, 44eqtrd 2198 . . . . 5 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → (𝐴 +𝑒 𝐶) = +∞)
469, 11xaddcld 9820 . . . . . . . . 9 ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (𝐴 +𝑒 𝐵) ∈ ℝ*)
4746ad3antrrr 484 . . . . . . . 8 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → (𝐴 +𝑒 𝐵) ∈ ℝ*)
48 pnfge 9725 . . . . . . . 8 ((𝐴 +𝑒 𝐵) ∈ ℝ* → (𝐴 +𝑒 𝐵) ≤ +∞)
4947, 48syl 14 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → (𝐴 +𝑒 𝐵) ≤ +∞)
5049, 45breqtrrd 4010 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → (𝐴 +𝑒 𝐵) ≤ (𝐴 +𝑒 𝐶))
519, 14xaddcld 9820 . . . . . . . 8 ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (𝐴 +𝑒 𝐶) ∈ ℝ*)
5251ad3antrrr 484 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → (𝐴 +𝑒 𝐶) ∈ ℝ*)
5347, 52, 28syl2anc 409 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → ((𝐴 +𝑒 𝐵) ≤ (𝐴 +𝑒 𝐶) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 𝐶)))
5450, 53mpd 13 . . . . 5 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 𝐶))
5540oveq1d 5857 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )) = (+∞ +𝑒 sup({𝐵, 𝐶}, ℝ*, < )))
5611ad3antrrr 484 . . . . . . . 8 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → 𝐵 ∈ ℝ*)
57 xrmaxcl 11193 . . . . . . . 8 ((𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → sup({𝐵, 𝐶}, ℝ*, < ) ∈ ℝ*)
5856, 42, 57syl2anc 409 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → sup({𝐵, 𝐶}, ℝ*, < ) ∈ ℝ*)
59 simpr 109 . . . . . . . . . . 11 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → 𝐶 ≠ -∞)
60 nmnfgt 9754 . . . . . . . . . . . 12 (𝐶 ∈ ℝ* → (-∞ < 𝐶 ↔ 𝐶 ≠ -∞))
6142, 60syl 14 . . . . . . . . . . 11 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → (-∞ < 𝐶 ↔ 𝐶 ≠ -∞))
6259, 61mpbird 166 . . . . . . . . . 10 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → -∞ < 𝐶)
6362olcd 724 . . . . . . . . 9 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → (-∞ < 𝐵 ∨ -∞ < 𝐶))
64 mnfxr 7955 . . . . . . . . . . 11 -∞ ∈ ℝ*
6564a1i 9 . . . . . . . . . 10 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → -∞ ∈ ℝ*)
66 xrltmaxsup 11198 . . . . . . . . . 10 ((𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ -∞ ∈ ℝ*) → (-∞ < sup({𝐵, 𝐶}, ℝ*, < ) ↔ (-∞ < 𝐵 ∨ -∞ < 𝐶)))
6756, 42, 65, 66syl3anc 1228 . . . . . . . . 9 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → (-∞ < sup({𝐵, 𝐶}, ℝ*, < ) ↔ (-∞ < 𝐵 ∨ -∞ < 𝐶)))
6863, 67mpbird 166 . . . . . . . 8 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → -∞ < sup({𝐵, 𝐶}, ℝ*, < ))
69 nmnfgt 9754 . . . . . . . . 9 (sup({𝐵, 𝐶}, ℝ*, < ) ∈ ℝ* → (-∞ < sup({𝐵, 𝐶}, ℝ*, < ) ↔ sup({𝐵, 𝐶}, ℝ*, < ) ≠ -∞))
7058, 69syl 14 . . . . . . . 8 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → (-∞ < sup({𝐵, 𝐶}, ℝ*, < ) ↔ sup({𝐵, 𝐶}, ℝ*, < ) ≠ -∞))
7168, 70mpbid 146 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → sup({𝐵, 𝐶}, ℝ*, < ) ≠ -∞)
72 xaddpnf2 9783 . . . . . . 7 ((sup({𝐵, 𝐶}, ℝ*, < ) ∈ ℝ* ∧ sup({𝐵, 𝐶}, ℝ*, < ) ≠ -∞) → (+∞ +𝑒 sup({𝐵, 𝐶}, ℝ*, < )) = +∞)
7358, 71, 72syl2anc 409 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → (+∞ +𝑒 sup({𝐵, 𝐶}, ℝ*, < )) = +∞)
7455, 73eqtrd 2198 . . . . 5 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )) = +∞)
7545, 54, 743eqtr4d 2208 . . . 4 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )))
76 xrmnfdc 9779 . . . . . . 7 (𝐶 ∈ ℝ* → DECID 𝐶 = -∞)
77763ad2ant3 1010 . . . . . 6 ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → DECID 𝐶 = -∞)
7877ad2antrr 480 . . . . 5 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) → DECID 𝐶 = -∞)
79 dcne 2347 . . . . 5 (DECID 𝐶 = -∞ ↔ (𝐶 = -∞ ∨ 𝐶 ≠ -∞))
8078, 79sylib 121 . . . 4 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) → (𝐶 = -∞ ∨ 𝐶 ≠ -∞))
8139, 75, 80mpjaodan 788 . . 3 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )))
8211ad2antrr 480 . . . . . 6 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → 𝐵 ∈ ℝ*)
8314ad2antrr 480 . . . . . 6 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → 𝐶 ∈ ℝ*)
8482, 83, 57syl2anc 409 . . . . 5 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → sup({𝐵, 𝐶}, ℝ*, < ) ∈ ℝ*)
85 simpr 109 . . . . . . . . 9 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → 𝐵 ≠ -∞)
86 nmnfgt 9754 . . . . . . . . . 10 (𝐵 ∈ ℝ* → (-∞ < 𝐵 ↔ 𝐵 ≠ -∞))
8782, 86syl 14 . . . . . . . . 9 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → (-∞ < 𝐵 ↔ 𝐵 ≠ -∞))
8885, 87mpbird 166 . . . . . . . 8 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → -∞ < 𝐵)
8988orcd 723 . . . . . . 7 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → (-∞ < 𝐵 ∨ -∞ < 𝐶))
9064a1i 9 . . . . . . . 8 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → -∞ ∈ ℝ*)
9182, 83, 90, 66syl3anc 1228 . . . . . . 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 520 . . . . 5 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → 𝐴 = +∞)
9796oveq1d 5857 . . . 4 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )) = (+∞ +𝑒 sup({𝐵, 𝐶}, ℝ*, < )))
98 prcom 3652 . . . . . 6 {(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)} = {(𝐴 +𝑒 𝐶), (𝐴 +𝑒 𝐵)}
9998supeq1i 6953 . . . . 5 sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = sup({(𝐴 +𝑒 𝐶), (𝐴 +𝑒 𝐵)}, ℝ*, < )
10051ad2antrr 480 . . . . . . . 8 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → (𝐴 +𝑒 𝐶) ∈ ℝ*)
10146ad2antrr 480 . . . . . . . 8 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → (𝐴 +𝑒 𝐵) ∈ ℝ*)
102100, 101jca 304 . . . . . . 7 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → ((𝐴 +𝑒 𝐶) ∈ ℝ* ∧ (𝐴 +𝑒 𝐵) ∈ ℝ*))
103 pnfge 9725 . . . . . . . . 9 ((𝐴 +𝑒 𝐶) ∈ ℝ* → (𝐴 +𝑒 𝐶) ≤ +∞)
104100, 103syl 14 . . . . . . . 8 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → (𝐴 +𝑒 𝐶) ≤ +∞)
10596oveq1d 5857 . . . . . . . . 9 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → (𝐴 +𝑒 𝐵) = (+∞ +𝑒 𝐵))
106 xaddpnf2 9783 . . . . . . . . . 10 ((𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞) → (+∞ +𝑒 𝐵) = +∞)
10782, 106sylancom 417 . . . . . . . . 9 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → (+∞ +𝑒 𝐵) = +∞)
108105, 107eqtrd 2198 . . . . . . . 8 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → (𝐴 +𝑒 𝐵) = +∞)
109104, 108breqtrrd 4010 . . . . . . 7 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → (𝐴 +𝑒 𝐶) ≤ (𝐴 +𝑒 𝐵))
110 xrmaxleim 11185 . . . . . . 7 (((𝐴 +𝑒 𝐶) ∈ ℝ* ∧ (𝐴 +𝑒 𝐵) ∈ ℝ*) → ((𝐴 +𝑒 𝐶) ≤ (𝐴 +𝑒 𝐵) → sup({(𝐴 +𝑒 𝐶), (𝐴 +𝑒 𝐵)}, ℝ*, < ) = (𝐴 +𝑒 𝐵)))
111102, 109, 110sylc 62 . . . . . 6 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → sup({(𝐴 +𝑒 𝐶), (𝐴 +𝑒 𝐵)}, ℝ*, < ) = (𝐴 +𝑒 𝐵))
112111, 108eqtrd 2198 . . . . 5 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → sup({(𝐴 +𝑒 𝐶), (𝐴 +𝑒 𝐵)}, ℝ*, < ) = +∞)
11399, 112syl5eq 2211 . . . 4 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = +∞)
11495, 97, 1133eqtr4rd 2209 . . 3 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )))
115 xrmnfdc 9779 . . . . . 6 (𝐵 ∈ ℝ* → DECID 𝐵 = -∞)
116 dcne 2347 . . . . . 6 (DECID 𝐵 = -∞ ↔ (𝐵 = -∞ ∨ 𝐵 ≠ -∞))
117115, 116sylib 121 . . . . 5 (𝐵 ∈ ℝ* → (𝐵 = -∞ ∨ 𝐵 ≠ -∞))
1181173ad2ant2 1009 . . . 4 ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (𝐵 = -∞ ∨ 𝐵 ≠ -∞))
119118adantr 274 . . 3 (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) → (𝐵 = -∞ ∨ 𝐵 ≠ -∞))
12081, 114, 119mpjaodan 788 . 2 (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )))
121 simpllr 524 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 = +∞) → 𝐴 = -∞)
122 simpr 109 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 = +∞) → 𝐶 = +∞)
123121, 122oveq12d 5860 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 = +∞) → (𝐴 +𝑒 𝐶) = (-∞ +𝑒 +∞))
124 mnfaddpnf 9787 . . . . . 6 (-∞ +𝑒 +∞) = 0
125123, 124eqtrdi 2215 . . . . 5 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 = +∞) → (𝐴 +𝑒 𝐶) = 0)
12646ad3antrrr 484 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 = +∞) → (𝐴 +𝑒 𝐵) ∈ ℝ*)
12751ad3antrrr 484 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 = +∞) → (𝐴 +𝑒 𝐶) ∈ ℝ*)
128126, 127jca 304 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 = +∞) → ((𝐴 +𝑒 𝐵) ∈ ℝ* ∧ (𝐴 +𝑒 𝐶) ∈ ℝ*))
129 0le0 8946 . . . . . . . 8 0 ≤ 0
130129a1i 9 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 = +∞) → 0 ≤ 0)
131 simplr 520 . . . . . . . . . 10 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → 𝐴 = -∞)
132 simpr 109 . . . . . . . . . 10 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → 𝐵 = +∞)
133131, 132oveq12d 5860 . . . . . . . . 9 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → (𝐴 +𝑒 𝐵) = (-∞ +𝑒 +∞))
134133, 124eqtrdi 2215 . . . . . . . 8 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → (𝐴 +𝑒 𝐵) = 0)
135134adantr 274 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 = +∞) → (𝐴 +𝑒 𝐵) = 0)
136130, 135, 1253brtr4d 4014 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 = +∞) → (𝐴 +𝑒 𝐵) ≤ (𝐴 +𝑒 𝐶))
137128, 136, 28sylc 62 . . . . 5 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 = +∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 𝐶))
138 prcom 3652 . . . . . . . . . . 11 {𝐶, 𝐵} = {𝐵, 𝐶}
139138supeq1i 6953 . . . . . . . . . 10 sup({𝐶, 𝐵}, ℝ*, < ) = sup({𝐵, 𝐶}, ℝ*, < )
14014ad2antrr 480 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → 𝐶 ∈ ℝ*)
14111ad2antrr 480 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → 𝐵 ∈ ℝ*)
142140, 141jca 304 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → (𝐶 ∈ ℝ* ∧ 𝐵 ∈ ℝ*))
143 pnfge 9725 . . . . . . . . . . . . . 14 (𝐶 ∈ ℝ* → 𝐶 ≤ +∞)
1441433ad2ant3 1010 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → 𝐶 ≤ +∞)
145144ad2antrr 480 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → 𝐶 ≤ +∞)
146145, 132breqtrrd 4010 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → 𝐶 ≤ 𝐵)
147 xrmaxleim 11185 . . . . . . . . . . 11 ((𝐶 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ≤ 𝐵 → sup({𝐶, 𝐵}, ℝ*, < ) = 𝐵))
148142, 146, 147sylc 62 . . . . . . . . . 10 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → sup({𝐶, 𝐵}, ℝ*, < ) = 𝐵)
149139, 148eqtr3id 2213 . . . . . . . . 9 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → sup({𝐵, 𝐶}, ℝ*, < ) = 𝐵)
150149, 132eqtrd 2198 . . . . . . . 8 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → sup({𝐵, 𝐶}, ℝ*, < ) = +∞)
151150oveq2d 5858 . . . . . . 7 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )) = (𝐴 +𝑒 +∞))
152131oveq1d 5857 . . . . . . . 8 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → (𝐴 +𝑒 +∞) = (-∞ +𝑒 +∞))
153152, 124eqtrdi 2215 . . . . . . 7 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → (𝐴 +𝑒 +∞) = 0)
154151, 153eqtrd 2198 . . . . . 6 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )) = 0)
155154adantr 274 . . . . 5 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 = +∞) → (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )) = 0)
156125, 137, 1553eqtr4d 2208 . . . 4 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 = +∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )))
15751ad3antrrr 484 . . . . . . . . 9 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → (𝐴 +𝑒 𝐶) ∈ ℝ*)
15846ad3antrrr 484 . . . . . . . . 9 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → (𝐴 +𝑒 𝐵) ∈ ℝ*)
159157, 158jca 304 . . . . . . . 8 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → ((𝐴 +𝑒 𝐶) ∈ ℝ* ∧ (𝐴 +𝑒 𝐵) ∈ ℝ*))
160 0xr 7945 . . . . . . . . . 10 0 ∈ ℝ*
161 mnfle 9728 . . . . . . . . . 10 (0 ∈ ℝ* → -∞ ≤ 0)
162160, 161mp1i 10 . . . . . . . . 9 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → -∞ ≤ 0)
163 simpllr 524 . . . . . . . . . . 11 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → 𝐴 = -∞)
164163oveq1d 5857 . . . . . . . . . 10 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → (𝐴 +𝑒 𝐶) = (-∞ +𝑒 𝐶))
165 xaddmnf2 9785 . . . . . . . . . . 11 ((𝐶 ∈ ℝ* ∧ 𝐶 ≠ +∞) → (-∞ +𝑒 𝐶) = -∞)
166140, 165sylan 281 . . . . . . . . . 10 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → (-∞ +𝑒 𝐶) = -∞)
167164, 166eqtrd 2198 . . . . . . . . 9 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → (𝐴 +𝑒 𝐶) = -∞)
168134adantr 274 . . . . . . . . 9 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → (𝐴 +𝑒 𝐵) = 0)
169162, 167, 1683brtr4d 4014 . . . . . . . 8 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → (𝐴 +𝑒 𝐶) ≤ (𝐴 +𝑒 𝐵))
170159, 169, 110sylc 62 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → sup({(𝐴 +𝑒 𝐶), (𝐴 +𝑒 𝐵)}, ℝ*, < ) = (𝐴 +𝑒 𝐵))
171170, 168eqtrd 2198 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → sup({(𝐴 +𝑒 𝐶), (𝐴 +𝑒 𝐵)}, ℝ*, < ) = 0)
17299, 171syl5eq 2211 . . . . 5 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = 0)
173154adantr 274 . . . . 5 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )) = 0)
174172, 173eqtr4d 2201 . . . 4 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )))
175 xrpnfdc 9778 . . . . . . 7 (𝐶 ∈ ℝ* → DECID 𝐶 = +∞)
176 dcne 2347 . . . . . . 7 (DECID 𝐶 = +∞ ↔ (𝐶 = +∞ ∨ 𝐶 ≠ +∞))
177175, 176sylib 121 . . . . . 6 (𝐶 ∈ ℝ* → (𝐶 = +∞ ∨ 𝐶 ≠ +∞))
1781773ad2ant3 1010 . . . . 5 ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (𝐶 = +∞ ∨ 𝐶 ≠ +∞))
179178ad2antrr 480 . . . 4 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → (𝐶 = +∞ ∨ 𝐶 ≠ +∞))
180156, 174, 179mpjaodan 788 . . 3 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )))
181 simpllr 524 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → 𝐴 = -∞)
182 simpr 109 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → 𝐶 = +∞)
183181, 182oveq12d 5860 . . . . 5 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → (𝐴 +𝑒 𝐶) = (-∞ +𝑒 +∞))
18446ad2antrr 480 . . . . . . . 8 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) → (𝐴 +𝑒 𝐵) ∈ ℝ*)
18551ad2antrr 480 . . . . . . . 8 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) → (𝐴 +𝑒 𝐶) ∈ ℝ*)
186184, 185jca 304 . . . . . . 7 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) → ((𝐴 +𝑒 𝐵) ∈ ℝ* ∧ (𝐴 +𝑒 𝐶) ∈ ℝ*))
187 simplr 520 . . . . . . . . . 10 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) → 𝐴 = -∞)
188187oveq1d 5857 . . . . . . . . 9 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) → (𝐴 +𝑒 𝐵) = (-∞ +𝑒 𝐵))
18911ad2antrr 480 . . . . . . . . . 10 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) → 𝐵 ∈ ℝ*)
190 xaddmnf2 9785 . . . . . . . . . 10 ((𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞) → (-∞ +𝑒 𝐵) = -∞)
191189, 190sylancom 417 . . . . . . . . 9 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) → (-∞ +𝑒 𝐵) = -∞)
192188, 191eqtrd 2198 . . . . . . . 8 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) → (𝐴 +𝑒 𝐵) = -∞)
193 mnfle 9728 . . . . . . . . 9 ((𝐴 +𝑒 𝐶) ∈ ℝ* → -∞ ≤ (𝐴 +𝑒 𝐶))
194185, 193syl 14 . . . . . . . 8 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) → -∞ ≤ (𝐴 +𝑒 𝐶))
195192, 194eqbrtrd 4004 . . . . . . 7 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) → (𝐴 +𝑒 𝐵) ≤ (𝐴 +𝑒 𝐶))
196186, 195, 28sylc 62 . . . . . 6 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 𝐶))
197196adantr 274 . . . . 5 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 𝐶))
198189adantr 274 . . . . . . . . 9 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → 𝐵 ∈ ℝ*)
19914ad3antrrr 484 . . . . . . . . 9 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → 𝐶 ∈ ℝ*)
200198, 199jca 304 . . . . . . . 8 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → (𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*))
201 simpr 109 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) → 𝐵 ≠ +∞)
202 npnflt 9751 . . . . . . . . . . . . 13 (𝐵 ∈ ℝ* → (𝐵 < +∞ ↔ 𝐵 ≠ +∞))
203189, 202syl 14 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) → (𝐵 < +∞ ↔ 𝐵 ≠ +∞))
204201, 203mpbird 166 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) → 𝐵 < +∞)
205204adantr 274 . . . . . . . . . 10 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → 𝐵 < +∞)
206205, 182breqtrrd 4010 . . . . . . . . 9 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → 𝐵 < 𝐶)
207198, 199, 206xrltled 9735 . . . . . . . 8 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → 𝐵 ≤ 𝐶)
208200, 207, 35sylc 62 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → sup({𝐵, 𝐶}, ℝ*, < ) = 𝐶)
209208, 182eqtrd 2198 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → sup({𝐵, 𝐶}, ℝ*, < ) = +∞)
210181, 209oveq12d 5860 . . . . 5 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )) = (-∞ +𝑒 +∞))
211183, 197, 2103eqtr4d 2208 . . . 4 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )))
212189adantr 274 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → 𝐵 ∈ ℝ*)
21314ad3antrrr 484 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → 𝐶 ∈ ℝ*)
214212, 213, 57syl2anc 409 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → sup({𝐵, 𝐶}, ℝ*, < ) ∈ ℝ*)
215204adantr 274 . . . . . . . . 9 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → 𝐵 < +∞)
216 simpr 109 . . . . . . . . . 10 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → 𝐶 ≠ +∞)
217 npnflt 9751 . . . . . . . . . . 11 (𝐶 ∈ ℝ* → (𝐶 < +∞ ↔ 𝐶 ≠ +∞))
218213, 217syl 14 . . . . . . . . . 10 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → (𝐶 < +∞ ↔ 𝐶 ≠ +∞))
219216, 218mpbird 166 . . . . . . . . 9 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → 𝐶 < +∞)
220215, 219jca 304 . . . . . . . 8 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → (𝐵 < +∞ ∧ 𝐶 < +∞))
221 pnfxr 7951 . . . . . . . . . 10 +∞ ∈ ℝ*
222221a1i 9 . . . . . . . . 9 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → +∞ ∈ ℝ*)
223 xrmaxltsup 11199 . . . . . . . . 9 ((𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (sup({𝐵, 𝐶}, ℝ*, < ) < +∞ ↔ (𝐵 < +∞ ∧ 𝐶 < +∞)))
224212, 213, 222, 223syl3anc 1228 . . . . . . . 8 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → (sup({𝐵, 𝐶}, ℝ*, < ) < +∞ ↔ (𝐵 < +∞ ∧ 𝐶 < +∞)))
225220, 224mpbird 166 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → sup({𝐵, 𝐶}, ℝ*, < ) < +∞)
226 npnflt 9751 . . . . . . . 8 (sup({𝐵, 𝐶}, ℝ*, < ) ∈ ℝ* → (sup({𝐵, 𝐶}, ℝ*, < ) < +∞ ↔ sup({𝐵, 𝐶}, ℝ*, < ) ≠ +∞))
227214, 226syl 14 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → (sup({𝐵, 𝐶}, ℝ*, < ) < +∞ ↔ sup({𝐵, 𝐶}, ℝ*, < ) ≠ +∞))
228225, 227mpbid 146 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → sup({𝐵, 𝐶}, ℝ*, < ) ≠ +∞)
229 xaddmnf2 9785 . . . . . 6 ((sup({𝐵, 𝐶}, ℝ*, < ) ∈ ℝ* ∧ sup({𝐵, 𝐶}, ℝ*, < ) ≠ +∞) → (-∞ +𝑒 sup({𝐵, 𝐶}, ℝ*, < )) = -∞)
230214, 228, 229syl2anc 409 . . . . 5 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → (-∞ +𝑒 sup({𝐵, 𝐶}, ℝ*, < )) = -∞)
231 simpllr 524 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → 𝐴 = -∞)
232231oveq1d 5857 . . . . 5 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )) = (-∞ +𝑒 sup({𝐵, 𝐶}, ℝ*, < )))
233196adantr 274 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 𝐶))
234231oveq1d 5857 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → (𝐴 +𝑒 𝐶) = (-∞ +𝑒 𝐶))
235233, 234eqtrd 2198 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (-∞ +𝑒 𝐶))
236213, 165sylancom 417 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → (-∞ +𝑒 𝐶) = -∞)
237235, 236eqtrd 2198 . . . . 5 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = -∞)
238230, 232, 2373eqtr4rd 2209 . . . 4 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )))
239178ad2antrr 480 . . . 4 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) → (𝐶 = +∞ ∨ 𝐶 ≠ +∞))
240211, 238, 239mpjaodan 788 . . 3 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )))
241 xrpnfdc 9778 . . . . . 6 (𝐵 ∈ ℝ* → DECID 𝐵 = +∞)
2422413ad2ant2 1009 . . . . 5 ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → DECID 𝐵 = +∞)
243 dcne 2347 . . . . 5 (DECID 𝐵 = +∞ ↔ (𝐵 = +∞ ∨ 𝐵 ≠ +∞))
244242, 243sylib 121 . . . 4 ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (𝐵 = +∞ ∨ 𝐵 ≠ +∞))
245244adantr 274 . . 3 (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) → (𝐵 = +∞ ∨ 𝐵 ≠ +∞))
246180, 240, 245mpjaodan 788 . 2 (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )))
247 elxr 9712 . . . 4 (𝐴 ∈ ℝ* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
248247biimpi 119 . . 3 (𝐴 ∈ ℝ* → (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
2492483ad2ant1 1008 . 2 ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
2505, 120, 246, 249mpjao3dan 1297 1 ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )))
Colors of variables: wff set class
Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 698  DECID wdc 824   ∨ w3o 967   ∧ w3a 968   = wceq 1343   ∈ wcel 2136   ≠ wne 2336  {cpr 3577   class class class wbr 3982  (class class class)co 5842  supcsup 6947  ℝcr 7752  0cc0 7753  +∞cpnf 7930  -∞cmnf 7931  ℝ*cxr 7932   < clt 7933   ≤ cle 7934   +𝑒 cxad 9706
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 604  ax-in2 605  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-13 2138  ax-14 2139  ax-ext 2147  ax-coll 4097  ax-sep 4100  ax-nul 4108  ax-pow 4153  ax-pr 4187  ax-un 4411  ax-setind 4514  ax-iinf 4565  ax-cnex 7844  ax-resscn 7845  ax-1cn 7846  ax-1re 7847  ax-icn 7848  ax-addcl 7849  ax-addrcl 7850  ax-mulcl 7851  ax-mulrcl 7852  ax-addcom 7853  ax-mulcom 7854  ax-addass 7855  ax-mulass 7856  ax-distr 7857  ax-i2m1 7858  ax-0lt1 7859  ax-1rid 7860  ax-0id 7861  ax-rnegex 7862  ax-precex 7863  ax-cnre 7864  ax-pre-ltirr 7865  ax-pre-ltwlin 7866  ax-pre-lttrn 7867  ax-pre-apti 7868  ax-pre-ltadd 7869  ax-pre-mulgt0 7870  ax-pre-mulext 7871  ax-arch 7872  ax-caucvg 7873
This theorem depends on definitions:  df-bi 116  df-dc 825  df-3or 969  df-3an 970  df-tru 1346  df-fal 1349  df-nf 1449  df-sb 1751  df-eu 2017  df-mo 2018  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2297  df-ne 2337  df-nel 2432  df-ral 2449  df-rex 2450  df-reu 2451  df-rmo 2452  df-rab 2453  df-v 2728  df-sbc 2952  df-csb 3046  df-dif 3118  df-un 3120  df-in 3122  df-ss 3129  df-nul 3410  df-if 3521  df-pw 3561  df-sn 3582  df-pr 3583  df-op 3585  df-uni 3790  df-int 3825  df-iun 3868  df-br 3983  df-opab 4044  df-mpt 4045  df-tr 4081  df-id 4271  df-po 4274  df-iso 4275  df-iord 4344  df-on 4346  df-ilim 4347  df-suc 4349  df-iom 4568  df-xp 4610  df-rel 4611  df-cnv 4612  df-co 4613  df-dm 4614  df-rn 4615  df-res 4616  df-ima 4617  df-iota 5153  df-fun 5190  df-fn 5191  df-f 5192  df-f1 5193  df-fo 5194  df-f1o 5195  df-fv 5196  df-riota 5798  df-ov 5845  df-oprab 5846  df-mpo 5847  df-1st 6108  df-2nd 6109  df-recs 6273  df-frec 6359  df-sup 6949  df-pnf 7935  df-mnf 7936  df-xr 7937  df-ltxr 7938  df-le 7939  df-sub 8071  df-neg 8072  df-reap 8473  df-ap 8480  df-div 8569  df-inn 8858  df-2 8916  df-3 8917  df-4 8918  df-n0 9115  df-z 9192  df-uz 9467  df-rp 9590  df-xneg 9708  df-xadd 9709  df-seqfrec 10381  df-exp 10455  df-cj 10784  df-re 10785  df-im 10786  df-rsqrt 10940  df-abs 10941
This theorem is referenced by:  xrminadd  11216
  Copyright terms: Public domain W3C validator