ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  xrmaxadd GIF version
Theorem xrmaxadd 11815
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 110 . . 3 (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ∈ ℝ) → 𝐴 ∈ ℝ)
2 simpl2 1025 . . 3 (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ∈ ℝ) → 𝐵 ∈ ℝ*)
3 simpl3 1026 . . 3 (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ∈ ℝ) → 𝐶 ∈ ℝ*)
4 xrmaxaddlem 11814 . . 3 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )))
51, 2, 3, 4syl3anc 1271 . 2 (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ∈ ℝ) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )))
6 simpllr 534 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → 𝐴 = +∞)
7 simpr 110 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → 𝐶 = -∞)
86, 7oveq12d 6031 . . . . 5 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → (𝐴 +𝑒 𝐶) = (+∞ +𝑒 -∞))
9 simp1 1021 . . . . . . . . 9 ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → 𝐴 ∈ ℝ*)
109ad3antrrr 492 . . . . . . . 8 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → 𝐴 ∈ ℝ*)
11 simp2 1022 . . . . . . . . 9 ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → 𝐵 ∈ ℝ*)
1211ad3antrrr 492 . . . . . . . 8 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → 𝐵 ∈ ℝ*)
1310, 12xaddcld 10112 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → (𝐴 +𝑒 𝐵) ∈ ℝ*)
14 simp3 1023 . . . . . . . . 9 ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → 𝐶 ∈ ℝ*)
1514ad3antrrr 492 . . . . . . . 8 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → 𝐶 ∈ ℝ*)
1610, 15xaddcld 10112 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → (𝐴 +𝑒 𝐶) ∈ ℝ*)
1713, 16jca 306 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → ((𝐴 +𝑒 𝐵) ∈ ℝ* ∧ (𝐴 +𝑒 𝐶) ∈ ℝ*))
18 simplr 528 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) → 𝐴 = +∞)
19 simpr 110 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) → 𝐵 = -∞)
2018, 19oveq12d 6031 . . . . . . . . . 10 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) → (𝐴 +𝑒 𝐵) = (+∞ +𝑒 -∞))
21 pnfaddmnf 10078 . . . . . . . . . 10 (+∞ +𝑒 -∞) = 0
2220, 21eqtrdi 2278 . . . . . . . . 9 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) → (𝐴 +𝑒 𝐵) = 0)
2322adantr 276 . . . . . . . 8 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → (𝐴 +𝑒 𝐵) = 0)
248, 21eqtrdi 2278 . . . . . . . 8 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → (𝐴 +𝑒 𝐶) = 0)
2523, 24eqtr4d 2265 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → (𝐴 +𝑒 𝐵) = (𝐴 +𝑒 𝐶))
2616xrleidd 10029 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → (𝐴 +𝑒 𝐶) ≤ (𝐴 +𝑒 𝐶))
2725, 26eqbrtrd 4108 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → (𝐴 +𝑒 𝐵) ≤ (𝐴 +𝑒 𝐶))
28 xrmaxleim 11798 . . . . . 6 (((𝐴 +𝑒 𝐵) ∈ ℝ* ∧ (𝐴 +𝑒 𝐶) ∈ ℝ*) → ((𝐴 +𝑒 𝐵) ≤ (𝐴 +𝑒 𝐶) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 𝐶)))
2917, 27, 28sylc 62 . . . . 5 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 𝐶))
3012, 15jca 306 . . . . . . . 8 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → (𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*))
31 simplr 528 . . . . . . . . . 10 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → 𝐵 = -∞)
3231, 7eqtr4d 2265 . . . . . . . . 9 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → 𝐵 = 𝐶)
3315xrleidd 10029 . . . . . . . . 9 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → 𝐶 ≤ 𝐶)
3432, 33eqbrtrd 4108 . . . . . . . 8 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → 𝐵 ≤ 𝐶)
35 xrmaxleim 11798 . . . . . . . 8 ((𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (𝐵 ≤ 𝐶 → sup({𝐵, 𝐶}, ℝ*, < ) = 𝐶))
3630, 34, 35sylc 62 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → sup({𝐵, 𝐶}, ℝ*, < ) = 𝐶)
3736, 7eqtrd 2262 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → sup({𝐵, 𝐶}, ℝ*, < ) = -∞)
386, 37oveq12d 6031 . . . . 5 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )) = (+∞ +𝑒 -∞))
398, 29, 383eqtr4d 2272 . . . 4 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )))
40 simpllr 534 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → 𝐴 = +∞)
4140oveq1d 6028 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → (𝐴 +𝑒 𝐶) = (+∞ +𝑒 𝐶))
4214ad3antrrr 492 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → 𝐶 ∈ ℝ*)
43 xaddpnf2 10075 . . . . . . 7 ((𝐶 ∈ ℝ* ∧ 𝐶 ≠ -∞) → (+∞ +𝑒 𝐶) = +∞)
4442, 43sylancom 420 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → (+∞ +𝑒 𝐶) = +∞)
4541, 44eqtrd 2262 . . . . 5 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → (𝐴 +𝑒 𝐶) = +∞)
469, 11xaddcld 10112 . . . . . . . . 9 ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (𝐴 +𝑒 𝐵) ∈ ℝ*)
4746ad3antrrr 492 . . . . . . . 8 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → (𝐴 +𝑒 𝐵) ∈ ℝ*)
48 pnfge 10017 . . . . . . . 8 ((𝐴 +𝑒 𝐵) ∈ ℝ* → (𝐴 +𝑒 𝐵) ≤ +∞)
4947, 48syl 14 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → (𝐴 +𝑒 𝐵) ≤ +∞)
5049, 45breqtrrd 4114 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → (𝐴 +𝑒 𝐵) ≤ (𝐴 +𝑒 𝐶))
519, 14xaddcld 10112 . . . . . . . 8 ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (𝐴 +𝑒 𝐶) ∈ ℝ*)
5251ad3antrrr 492 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → (𝐴 +𝑒 𝐶) ∈ ℝ*)
5347, 52, 28syl2anc 411 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → ((𝐴 +𝑒 𝐵) ≤ (𝐴 +𝑒 𝐶) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 𝐶)))
5450, 53mpd 13 . . . . 5 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 𝐶))
5540oveq1d 6028 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )) = (+∞ +𝑒 sup({𝐵, 𝐶}, ℝ*, < )))
5611ad3antrrr 492 . . . . . . . 8 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → 𝐵 ∈ ℝ*)
57 xrmaxcl 11806 . . . . . . . 8 ((𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → sup({𝐵, 𝐶}, ℝ*, < ) ∈ ℝ*)
5856, 42, 57syl2anc 411 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → sup({𝐵, 𝐶}, ℝ*, < ) ∈ ℝ*)
59 simpr 110 . . . . . . . . . . 11 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → 𝐶 ≠ -∞)
60 nmnfgt 10046 . . . . . . . . . . . 12 (𝐶 ∈ ℝ* → (-∞ < 𝐶 ↔ 𝐶 ≠ -∞))
6142, 60syl 14 . . . . . . . . . . 11 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → (-∞ < 𝐶 ↔ 𝐶 ≠ -∞))
6259, 61mpbird 167 . . . . . . . . . 10 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → -∞ < 𝐶)
6362olcd 739 . . . . . . . . 9 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → (-∞ < 𝐵 ∨ -∞ < 𝐶))
64 mnfxr 8229 . . . . . . . . . . 11 -∞ ∈ ℝ*
6564a1i 9 . . . . . . . . . 10 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → -∞ ∈ ℝ*)
66 xrltmaxsup 11811 . . . . . . . . . 10 ((𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ -∞ ∈ ℝ*) → (-∞ < sup({𝐵, 𝐶}, ℝ*, < ) ↔ (-∞ < 𝐵 ∨ -∞ < 𝐶)))
6756, 42, 65, 66syl3anc 1271 . . . . . . . . 9 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → (-∞ < sup({𝐵, 𝐶}, ℝ*, < ) ↔ (-∞ < 𝐵 ∨ -∞ < 𝐶)))
6863, 67mpbird 167 . . . . . . . 8 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → -∞ < sup({𝐵, 𝐶}, ℝ*, < ))
69 nmnfgt 10046 . . . . . . . . 9 (sup({𝐵, 𝐶}, ℝ*, < ) ∈ ℝ* → (-∞ < sup({𝐵, 𝐶}, ℝ*, < ) ↔ sup({𝐵, 𝐶}, ℝ*, < ) ≠ -∞))
7058, 69syl 14 . . . . . . . 8 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → (-∞ < sup({𝐵, 𝐶}, ℝ*, < ) ↔ sup({𝐵, 𝐶}, ℝ*, < ) ≠ -∞))
7168, 70mpbid 147 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → sup({𝐵, 𝐶}, ℝ*, < ) ≠ -∞)
72 xaddpnf2 10075 . . . . . . 7 ((sup({𝐵, 𝐶}, ℝ*, < ) ∈ ℝ* ∧ sup({𝐵, 𝐶}, ℝ*, < ) ≠ -∞) → (+∞ +𝑒 sup({𝐵, 𝐶}, ℝ*, < )) = +∞)
7358, 71, 72syl2anc 411 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → (+∞ +𝑒 sup({𝐵, 𝐶}, ℝ*, < )) = +∞)
7455, 73eqtrd 2262 . . . . 5 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )) = +∞)
7545, 54, 743eqtr4d 2272 . . . 4 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) ∧ 𝐶 ≠ -∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )))
76 xrmnfdc 10071 . . . . . . 7 (𝐶 ∈ ℝ* → DECID 𝐶 = -∞)
77763ad2ant3 1044 . . . . . 6 ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → DECID 𝐶 = -∞)
7877ad2antrr 488 . . . . 5 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) → DECID 𝐶 = -∞)
79 dcne 2411 . . . . 5 (DECID 𝐶 = -∞ ↔ (𝐶 = -∞ ∨ 𝐶 ≠ -∞))
8078, 79sylib 122 . . . 4 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) → (𝐶 = -∞ ∨ 𝐶 ≠ -∞))
8139, 75, 80mpjaodan 803 . . 3 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 = -∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )))
8211ad2antrr 488 . . . . . 6 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → 𝐵 ∈ ℝ*)
8314ad2antrr 488 . . . . . 6 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → 𝐶 ∈ ℝ*)
8482, 83, 57syl2anc 411 . . . . 5 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → sup({𝐵, 𝐶}, ℝ*, < ) ∈ ℝ*)
85 simpr 110 . . . . . . . . 9 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → 𝐵 ≠ -∞)
86 nmnfgt 10046 . . . . . . . . . 10 (𝐵 ∈ ℝ* → (-∞ < 𝐵 ↔ 𝐵 ≠ -∞))
8782, 86syl 14 . . . . . . . . 9 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → (-∞ < 𝐵 ↔ 𝐵 ≠ -∞))
8885, 87mpbird 167 . . . . . . . 8 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → -∞ < 𝐵)
8988orcd 738 . . . . . . 7 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → (-∞ < 𝐵 ∨ -∞ < 𝐶))
9064a1i 9 . . . . . . . 8 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → -∞ ∈ ℝ*)
9182, 83, 90, 66syl3anc 1271 . . . . . . 7 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → (-∞ < sup({𝐵, 𝐶}, ℝ*, < ) ↔ (-∞ < 𝐵 ∨ -∞ < 𝐶)))
9289, 91mpbird 167 . . . . . 6 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → -∞ < sup({𝐵, 𝐶}, ℝ*, < ))
9384, 69syl 14 . . . . . 6 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → (-∞ < sup({𝐵, 𝐶}, ℝ*, < ) ↔ sup({𝐵, 𝐶}, ℝ*, < ) ≠ -∞))
9492, 93mpbid 147 . . . . 5 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → sup({𝐵, 𝐶}, ℝ*, < ) ≠ -∞)
9584, 94, 72syl2anc 411 . . . 4 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → (+∞ +𝑒 sup({𝐵, 𝐶}, ℝ*, < )) = +∞)
96 simplr 528 . . . . 5 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → 𝐴 = +∞)
9796oveq1d 6028 . . . 4 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )) = (+∞ +𝑒 sup({𝐵, 𝐶}, ℝ*, < )))
98 prcom 3745 . . . . . 6 {(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)} = {(𝐴 +𝑒 𝐶), (𝐴 +𝑒 𝐵)}
9998supeq1i 7181 . . . . 5 sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = sup({(𝐴 +𝑒 𝐶), (𝐴 +𝑒 𝐵)}, ℝ*, < )
10051ad2antrr 488 . . . . . . . 8 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → (𝐴 +𝑒 𝐶) ∈ ℝ*)
10146ad2antrr 488 . . . . . . . 8 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → (𝐴 +𝑒 𝐵) ∈ ℝ*)
102100, 101jca 306 . . . . . . 7 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → ((𝐴 +𝑒 𝐶) ∈ ℝ* ∧ (𝐴 +𝑒 𝐵) ∈ ℝ*))
103 pnfge 10017 . . . . . . . . 9 ((𝐴 +𝑒 𝐶) ∈ ℝ* → (𝐴 +𝑒 𝐶) ≤ +∞)
104100, 103syl 14 . . . . . . . 8 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → (𝐴 +𝑒 𝐶) ≤ +∞)
10596oveq1d 6028 . . . . . . . . 9 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → (𝐴 +𝑒 𝐵) = (+∞ +𝑒 𝐵))
106 xaddpnf2 10075 . . . . . . . . . 10 ((𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞) → (+∞ +𝑒 𝐵) = +∞)
10782, 106sylancom 420 . . . . . . . . 9 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → (+∞ +𝑒 𝐵) = +∞)
108105, 107eqtrd 2262 . . . . . . . 8 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → (𝐴 +𝑒 𝐵) = +∞)
109104, 108breqtrrd 4114 . . . . . . 7 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → (𝐴 +𝑒 𝐶) ≤ (𝐴 +𝑒 𝐵))
110 xrmaxleim 11798 . . . . . . 7 (((𝐴 +𝑒 𝐶) ∈ ℝ* ∧ (𝐴 +𝑒 𝐵) ∈ ℝ*) → ((𝐴 +𝑒 𝐶) ≤ (𝐴 +𝑒 𝐵) → sup({(𝐴 +𝑒 𝐶), (𝐴 +𝑒 𝐵)}, ℝ*, < ) = (𝐴 +𝑒 𝐵)))
111102, 109, 110sylc 62 . . . . . 6 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → sup({(𝐴 +𝑒 𝐶), (𝐴 +𝑒 𝐵)}, ℝ*, < ) = (𝐴 +𝑒 𝐵))
112111, 108eqtrd 2262 . . . . 5 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → sup({(𝐴 +𝑒 𝐶), (𝐴 +𝑒 𝐵)}, ℝ*, < ) = +∞)
11399, 112eqtrid 2274 . . . 4 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = +∞)
11495, 97, 1133eqtr4rd 2273 . . 3 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) ∧ 𝐵 ≠ -∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )))
115 xrmnfdc 10071 . . . . . 6 (𝐵 ∈ ℝ* → DECID 𝐵 = -∞)
116 dcne 2411 . . . . . 6 (DECID 𝐵 = -∞ ↔ (𝐵 = -∞ ∨ 𝐵 ≠ -∞))
117115, 116sylib 122 . . . . 5 (𝐵 ∈ ℝ* → (𝐵 = -∞ ∨ 𝐵 ≠ -∞))
1181173ad2ant2 1043 . . . 4 ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (𝐵 = -∞ ∨ 𝐵 ≠ -∞))
119118adantr 276 . . 3 (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) → (𝐵 = -∞ ∨ 𝐵 ≠ -∞))
12081, 114, 119mpjaodan 803 . 2 (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = +∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )))
121 simpllr 534 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 = +∞) → 𝐴 = -∞)
122 simpr 110 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 = +∞) → 𝐶 = +∞)
123121, 122oveq12d 6031 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 = +∞) → (𝐴 +𝑒 𝐶) = (-∞ +𝑒 +∞))
124 mnfaddpnf 10079 . . . . . 6 (-∞ +𝑒 +∞) = 0
125123, 124eqtrdi 2278 . . . . 5 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 = +∞) → (𝐴 +𝑒 𝐶) = 0)
12646ad3antrrr 492 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 = +∞) → (𝐴 +𝑒 𝐵) ∈ ℝ*)
12751ad3antrrr 492 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 = +∞) → (𝐴 +𝑒 𝐶) ∈ ℝ*)
128126, 127jca 306 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 = +∞) → ((𝐴 +𝑒 𝐵) ∈ ℝ* ∧ (𝐴 +𝑒 𝐶) ∈ ℝ*))
129 0le0 9225 . . . . . . . 8 0 ≤ 0
130129a1i 9 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 = +∞) → 0 ≤ 0)
131 simplr 528 . . . . . . . . . 10 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → 𝐴 = -∞)
132 simpr 110 . . . . . . . . . 10 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → 𝐵 = +∞)
133131, 132oveq12d 6031 . . . . . . . . 9 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → (𝐴 +𝑒 𝐵) = (-∞ +𝑒 +∞))
134133, 124eqtrdi 2278 . . . . . . . 8 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → (𝐴 +𝑒 𝐵) = 0)
135134adantr 276 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 = +∞) → (𝐴 +𝑒 𝐵) = 0)
136130, 135, 1253brtr4d 4118 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 = +∞) → (𝐴 +𝑒 𝐵) ≤ (𝐴 +𝑒 𝐶))
137128, 136, 28sylc 62 . . . . 5 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 = +∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 𝐶))
138 prcom 3745 . . . . . . . . . . 11 {𝐶, 𝐵} = {𝐵, 𝐶}
139138supeq1i 7181 . . . . . . . . . 10 sup({𝐶, 𝐵}, ℝ*, < ) = sup({𝐵, 𝐶}, ℝ*, < )
14014ad2antrr 488 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → 𝐶 ∈ ℝ*)
14111ad2antrr 488 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → 𝐵 ∈ ℝ*)
142140, 141jca 306 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → (𝐶 ∈ ℝ* ∧ 𝐵 ∈ ℝ*))
143 pnfge 10017 . . . . . . . . . . . . . 14 (𝐶 ∈ ℝ* → 𝐶 ≤ +∞)
1441433ad2ant3 1044 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → 𝐶 ≤ +∞)
145144ad2antrr 488 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → 𝐶 ≤ +∞)
146145, 132breqtrrd 4114 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → 𝐶 ≤ 𝐵)
147 xrmaxleim 11798 . . . . . . . . . . 11 ((𝐶 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ≤ 𝐵 → sup({𝐶, 𝐵}, ℝ*, < ) = 𝐵))
148142, 146, 147sylc 62 . . . . . . . . . 10 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → sup({𝐶, 𝐵}, ℝ*, < ) = 𝐵)
149139, 148eqtr3id 2276 . . . . . . . . 9 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → sup({𝐵, 𝐶}, ℝ*, < ) = 𝐵)
150149, 132eqtrd 2262 . . . . . . . 8 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → sup({𝐵, 𝐶}, ℝ*, < ) = +∞)
151150oveq2d 6029 . . . . . . 7 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )) = (𝐴 +𝑒 +∞))
152131oveq1d 6028 . . . . . . . 8 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → (𝐴 +𝑒 +∞) = (-∞ +𝑒 +∞))
153152, 124eqtrdi 2278 . . . . . . 7 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → (𝐴 +𝑒 +∞) = 0)
154151, 153eqtrd 2262 . . . . . 6 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )) = 0)
155154adantr 276 . . . . 5 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 = +∞) → (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )) = 0)
156125, 137, 1553eqtr4d 2272 . . . 4 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 = +∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )))
15751ad3antrrr 492 . . . . . . . . 9 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → (𝐴 +𝑒 𝐶) ∈ ℝ*)
15846ad3antrrr 492 . . . . . . . . 9 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → (𝐴 +𝑒 𝐵) ∈ ℝ*)
159157, 158jca 306 . . . . . . . 8 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → ((𝐴 +𝑒 𝐶) ∈ ℝ* ∧ (𝐴 +𝑒 𝐵) ∈ ℝ*))
160 0xr 8219 . . . . . . . . . 10 0 ∈ ℝ*
161 mnfle 10020 . . . . . . . . . 10 (0 ∈ ℝ* → -∞ ≤ 0)
162160, 161mp1i 10 . . . . . . . . 9 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → -∞ ≤ 0)
163 simpllr 534 . . . . . . . . . . 11 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → 𝐴 = -∞)
164163oveq1d 6028 . . . . . . . . . 10 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → (𝐴 +𝑒 𝐶) = (-∞ +𝑒 𝐶))
165 xaddmnf2 10077 . . . . . . . . . . 11 ((𝐶 ∈ ℝ* ∧ 𝐶 ≠ +∞) → (-∞ +𝑒 𝐶) = -∞)
166140, 165sylan 283 . . . . . . . . . 10 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → (-∞ +𝑒 𝐶) = -∞)
167164, 166eqtrd 2262 . . . . . . . . 9 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → (𝐴 +𝑒 𝐶) = -∞)
168134adantr 276 . . . . . . . . 9 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → (𝐴 +𝑒 𝐵) = 0)
169162, 167, 1683brtr4d 4118 . . . . . . . 8 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → (𝐴 +𝑒 𝐶) ≤ (𝐴 +𝑒 𝐵))
170159, 169, 110sylc 62 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → sup({(𝐴 +𝑒 𝐶), (𝐴 +𝑒 𝐵)}, ℝ*, < ) = (𝐴 +𝑒 𝐵))
171170, 168eqtrd 2262 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → sup({(𝐴 +𝑒 𝐶), (𝐴 +𝑒 𝐵)}, ℝ*, < ) = 0)
17299, 171eqtrid 2274 . . . . 5 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = 0)
173154adantr 276 . . . . 5 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )) = 0)
174172, 173eqtr4d 2265 . . . 4 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )))
175 xrpnfdc 10070 . . . . . . 7 (𝐶 ∈ ℝ* → DECID 𝐶 = +∞)
176 dcne 2411 . . . . . . 7 (DECID 𝐶 = +∞ ↔ (𝐶 = +∞ ∨ 𝐶 ≠ +∞))
177175, 176sylib 122 . . . . . 6 (𝐶 ∈ ℝ* → (𝐶 = +∞ ∨ 𝐶 ≠ +∞))
1781773ad2ant3 1044 . . . . 5 ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (𝐶 = +∞ ∨ 𝐶 ≠ +∞))
179178ad2antrr 488 . . . 4 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → (𝐶 = +∞ ∨ 𝐶 ≠ +∞))
180156, 174, 179mpjaodan 803 . . 3 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )))
181 simpllr 534 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → 𝐴 = -∞)
182 simpr 110 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → 𝐶 = +∞)
183181, 182oveq12d 6031 . . . . 5 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → (𝐴 +𝑒 𝐶) = (-∞ +𝑒 +∞))
18446ad2antrr 488 . . . . . . . 8 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) → (𝐴 +𝑒 𝐵) ∈ ℝ*)
18551ad2antrr 488 . . . . . . . 8 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) → (𝐴 +𝑒 𝐶) ∈ ℝ*)
186184, 185jca 306 . . . . . . 7 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) → ((𝐴 +𝑒 𝐵) ∈ ℝ* ∧ (𝐴 +𝑒 𝐶) ∈ ℝ*))
187 simplr 528 . . . . . . . . . 10 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) → 𝐴 = -∞)
188187oveq1d 6028 . . . . . . . . 9 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) → (𝐴 +𝑒 𝐵) = (-∞ +𝑒 𝐵))
18911ad2antrr 488 . . . . . . . . . 10 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) → 𝐵 ∈ ℝ*)
190 xaddmnf2 10077 . . . . . . . . . 10 ((𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞) → (-∞ +𝑒 𝐵) = -∞)
191189, 190sylancom 420 . . . . . . . . 9 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) → (-∞ +𝑒 𝐵) = -∞)
192188, 191eqtrd 2262 . . . . . . . 8 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) → (𝐴 +𝑒 𝐵) = -∞)
193 mnfle 10020 . . . . . . . . 9 ((𝐴 +𝑒 𝐶) ∈ ℝ* → -∞ ≤ (𝐴 +𝑒 𝐶))
194185, 193syl 14 . . . . . . . 8 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) → -∞ ≤ (𝐴 +𝑒 𝐶))
195192, 194eqbrtrd 4108 . . . . . . 7 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) → (𝐴 +𝑒 𝐵) ≤ (𝐴 +𝑒 𝐶))
196186, 195, 28sylc 62 . . . . . 6 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 𝐶))
197196adantr 276 . . . . 5 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 𝐶))
198189adantr 276 . . . . . . . . 9 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → 𝐵 ∈ ℝ*)
19914ad3antrrr 492 . . . . . . . . 9 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → 𝐶 ∈ ℝ*)
200198, 199jca 306 . . . . . . . 8 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → (𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*))
201 simpr 110 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) → 𝐵 ≠ +∞)
202 npnflt 10043 . . . . . . . . . . . . 13 (𝐵 ∈ ℝ* → (𝐵 < +∞ ↔ 𝐵 ≠ +∞))
203189, 202syl 14 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) → (𝐵 < +∞ ↔ 𝐵 ≠ +∞))
204201, 203mpbird 167 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) → 𝐵 < +∞)
205204adantr 276 . . . . . . . . . 10 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → 𝐵 < +∞)
206205, 182breqtrrd 4114 . . . . . . . . 9 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → 𝐵 < 𝐶)
207198, 199, 206xrltled 10027 . . . . . . . 8 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → 𝐵 ≤ 𝐶)
208200, 207, 35sylc 62 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → sup({𝐵, 𝐶}, ℝ*, < ) = 𝐶)
209208, 182eqtrd 2262 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → sup({𝐵, 𝐶}, ℝ*, < ) = +∞)
210181, 209oveq12d 6031 . . . . 5 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )) = (-∞ +𝑒 +∞))
211183, 197, 2103eqtr4d 2272 . . . 4 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )))
212189adantr 276 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → 𝐵 ∈ ℝ*)
21314ad3antrrr 492 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → 𝐶 ∈ ℝ*)
214212, 213, 57syl2anc 411 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → sup({𝐵, 𝐶}, ℝ*, < ) ∈ ℝ*)
215204adantr 276 . . . . . . . . 9 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → 𝐵 < +∞)
216 simpr 110 . . . . . . . . . 10 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → 𝐶 ≠ +∞)
217 npnflt 10043 . . . . . . . . . . 11 (𝐶 ∈ ℝ* → (𝐶 < +∞ ↔ 𝐶 ≠ +∞))
218213, 217syl 14 . . . . . . . . . 10 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → (𝐶 < +∞ ↔ 𝐶 ≠ +∞))
219216, 218mpbird 167 . . . . . . . . 9 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → 𝐶 < +∞)
220215, 219jca 306 . . . . . . . 8 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → (𝐵 < +∞ ∧ 𝐶 < +∞))
221 pnfxr 8225 . . . . . . . . . 10 +∞ ∈ ℝ*
222221a1i 9 . . . . . . . . 9 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → +∞ ∈ ℝ*)
223 xrmaxltsup 11812 . . . . . . . . 9 ((𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (sup({𝐵, 𝐶}, ℝ*, < ) < +∞ ↔ (𝐵 < +∞ ∧ 𝐶 < +∞)))
224212, 213, 222, 223syl3anc 1271 . . . . . . . 8 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → (sup({𝐵, 𝐶}, ℝ*, < ) < +∞ ↔ (𝐵 < +∞ ∧ 𝐶 < +∞)))
225220, 224mpbird 167 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → sup({𝐵, 𝐶}, ℝ*, < ) < +∞)
226 npnflt 10043 . . . . . . . 8 (sup({𝐵, 𝐶}, ℝ*, < ) ∈ ℝ* → (sup({𝐵, 𝐶}, ℝ*, < ) < +∞ ↔ sup({𝐵, 𝐶}, ℝ*, < ) ≠ +∞))
227214, 226syl 14 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → (sup({𝐵, 𝐶}, ℝ*, < ) < +∞ ↔ sup({𝐵, 𝐶}, ℝ*, < ) ≠ +∞))
228225, 227mpbid 147 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → sup({𝐵, 𝐶}, ℝ*, < ) ≠ +∞)
229 xaddmnf2 10077 . . . . . 6 ((sup({𝐵, 𝐶}, ℝ*, < ) ∈ ℝ* ∧ sup({𝐵, 𝐶}, ℝ*, < ) ≠ +∞) → (-∞ +𝑒 sup({𝐵, 𝐶}, ℝ*, < )) = -∞)
230214, 228, 229syl2anc 411 . . . . 5 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → (-∞ +𝑒 sup({𝐵, 𝐶}, ℝ*, < )) = -∞)
231 simpllr 534 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → 𝐴 = -∞)
232231oveq1d 6028 . . . . 5 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )) = (-∞ +𝑒 sup({𝐵, 𝐶}, ℝ*, < )))
233196adantr 276 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 𝐶))
234231oveq1d 6028 . . . . . . 7 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → (𝐴 +𝑒 𝐶) = (-∞ +𝑒 𝐶))
235233, 234eqtrd 2262 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (-∞ +𝑒 𝐶))
236213, 165sylancom 420 . . . . . 6 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → (-∞ +𝑒 𝐶) = -∞)
237235, 236eqtrd 2262 . . . . 5 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = -∞)
238230, 232, 2373eqtr4rd 2273 . . . 4 (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )))
239178ad2antrr 488 . . . 4 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) → (𝐶 = +∞ ∨ 𝐶 ≠ +∞))
240211, 238, 239mpjaodan 803 . . 3 ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) ∧ 𝐵 ≠ +∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )))
241 xrpnfdc 10070 . . . . . 6 (𝐵 ∈ ℝ* → DECID 𝐵 = +∞)
2422413ad2ant2 1043 . . . . 5 ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → DECID 𝐵 = +∞)
243 dcne 2411 . . . . 5 (DECID 𝐵 = +∞ ↔ (𝐵 = +∞ ∨ 𝐵 ≠ +∞))
244242, 243sylib 122 . . . 4 ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (𝐵 = +∞ ∨ 𝐵 ≠ +∞))
245244adantr 276 . . 3 (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) → (𝐵 = +∞ ∨ 𝐵 ≠ +∞))
246180, 240, 245mpjaodan 803 . 2 (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 = -∞) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )))
247 elxr 10004 . . . 4 (𝐴 ∈ ℝ* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
248247biimpi 120 . . 3 (𝐴 ∈ ℝ* → (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
2492483ad2ant1 1042 . 2 ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
2505, 120, 246, 249mpjao3dan 1341 1 ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → sup({(𝐴 +𝑒 𝐵), (𝐴 +𝑒 𝐶)}, ℝ*, < ) = (𝐴 +𝑒 sup({𝐵, 𝐶}, ℝ*, < )))
Colors of variables: wff set class
Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   ∨ wo 713  DECID wdc 839   ∨ w3o 1001   ∧ w3a 1002   = wceq 1395   ∈ wcel 2200   ≠ wne 2400  {cpr 3668   class class class wbr 4086  (class class class)co 6013  supcsup 7175  ℝcr 8024  0cc0 8025  +∞cpnf 8204  -∞cmnf 8205  ℝ*cxr 8206   < clt 8207   ≤ cle 8208   +𝑒 cxad 9998
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-coll 4202  ax-sep 4205  ax-nul 4213  ax-pow 4262  ax-pr 4297  ax-un 4528  ax-setind 4633  ax-iinf 4684  ax-cnex 8116  ax-resscn 8117  ax-1cn 8118  ax-1re 8119  ax-icn 8120  ax-addcl 8121  ax-addrcl 8122  ax-mulcl 8123  ax-mulrcl 8124  ax-addcom 8125  ax-mulcom 8126  ax-addass 8127  ax-mulass 8128  ax-distr 8129  ax-i2m1 8130  ax-0lt1 8131  ax-1rid 8132  ax-0id 8133  ax-rnegex 8134  ax-precex 8135  ax-cnre 8136  ax-pre-ltirr 8137  ax-pre-ltwlin 8138  ax-pre-lttrn 8139  ax-pre-apti 8140  ax-pre-ltadd 8141  ax-pre-mulgt0 8142  ax-pre-mulext 8143  ax-arch 8144  ax-caucvg 8145
This theorem depends on definitions:  df-bi 117  df-dc 840  df-3or 1003  df-3an 1004  df-tru 1398  df-fal 1401  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ne 2401  df-nel 2496  df-ral 2513  df-rex 2514  df-reu 2515  df-rmo 2516  df-rab 2517  df-v 2802  df-sbc 3030  df-csb 3126  df-dif 3200  df-un 3202  df-in 3204  df-ss 3211  df-nul 3493  df-if 3604  df-pw 3652  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3892  df-int 3927  df-iun 3970  df-br 4087  df-opab 4149  df-mpt 4150  df-tr 4186  df-id 4388  df-po 4391  df-iso 4392  df-iord 4461  df-on 4463  df-ilim 4464  df-suc 4466  df-iom 4687  df-xp 4729  df-rel 4730  df-cnv 4731  df-co 4732  df-dm 4733  df-rn 4734  df-res 4735  df-ima 4736  df-iota 5284  df-fun 5326  df-fn 5327  df-f 5328  df-f1 5329  df-fo 5330  df-f1o 5331  df-fv 5332  df-riota 5966  df-ov 6016  df-oprab 6017  df-mpo 6018  df-1st 6298  df-2nd 6299  df-recs 6466  df-frec 6552  df-sup 7177  df-pnf 8209  df-mnf 8210  df-xr 8211  df-ltxr 8212  df-le 8213  df-sub 8345  df-neg 8346  df-reap 8748  df-ap 8755  df-div 8846  df-inn 9137  df-2 9195  df-3 9196  df-4 9197  df-n0 9396  df-z 9473  df-uz 9749  df-rp 9882  df-xneg 10000  df-xadd 10001  df-seqfrec 10703  df-exp 10794  df-cj 11396  df-re 11397  df-im 11398  df-rsqrt 11552  df-abs 11553
This theorem is referenced by:  xrminadd  11829
  Copyright terms: Public domain W3C validator