Proof of Theorem xrmaxltsup
Step | Hyp | Ref
| Expression |
1 | | simpl1 995 |
. . . 4
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ sup({𝐴, 𝐵}, ℝ*, < ) < 𝐶) → 𝐴 ∈
ℝ*) |
2 | | simpl2 996 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ sup({𝐴, 𝐵}, ℝ*, < ) < 𝐶) → 𝐵 ∈
ℝ*) |
3 | | xrmaxcl 11202 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → sup({𝐴, 𝐵}, ℝ*, < ) ∈
ℝ*) |
4 | 1, 2, 3 | syl2anc 409 |
. . . 4
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ sup({𝐴, 𝐵}, ℝ*, < ) < 𝐶) → sup({𝐴, 𝐵}, ℝ*, < ) ∈
ℝ*) |
5 | | simpl3 997 |
. . . 4
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ sup({𝐴, 𝐵}, ℝ*, < ) < 𝐶) → 𝐶 ∈
ℝ*) |
6 | | xrmax1sup 11203 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → 𝐴 ≤ sup({𝐴, 𝐵}, ℝ*, <
)) |
7 | 6 | 3adant3 1012 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) → 𝐴 ≤ sup({𝐴, 𝐵}, ℝ*, <
)) |
8 | 7 | adantr 274 |
. . . 4
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ sup({𝐴, 𝐵}, ℝ*, < ) < 𝐶) → 𝐴 ≤ sup({𝐴, 𝐵}, ℝ*, <
)) |
9 | | simpr 109 |
. . . 4
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ sup({𝐴, 𝐵}, ℝ*, < ) < 𝐶) → sup({𝐴, 𝐵}, ℝ*, < ) < 𝐶) |
10 | 1, 4, 5, 8, 9 | xrlelttrd 9754 |
. . 3
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ sup({𝐴, 𝐵}, ℝ*, < ) < 𝐶) → 𝐴 < 𝐶) |
11 | | xrmax2sup 11204 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → 𝐵 ≤ sup({𝐴, 𝐵}, ℝ*, <
)) |
12 | 1, 2, 11 | syl2anc 409 |
. . . 4
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ sup({𝐴, 𝐵}, ℝ*, < ) < 𝐶) → 𝐵 ≤ sup({𝐴, 𝐵}, ℝ*, <
)) |
13 | 2, 4, 5, 12, 9 | xrlelttrd 9754 |
. . 3
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ sup({𝐴, 𝐵}, ℝ*, < ) < 𝐶) → 𝐵 < 𝐶) |
14 | 10, 13 | jca 304 |
. 2
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ sup({𝐴, 𝐵}, ℝ*, < ) < 𝐶) → (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) |
15 | | simplr 525 |
. . . . . . 7
⊢
((((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ℝ) ∧ 𝐶 ∈ ℝ) → 𝐴 ∈ ℝ) |
16 | | simpllr 529 |
. . . . . . 7
⊢
((((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ℝ) ∧ 𝐶 ∈ ℝ) → 𝐵 ∈ ℝ) |
17 | | xrmaxrecl 11205 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
sup({𝐴, 𝐵}, ℝ*, < ) = sup({𝐴, 𝐵}, ℝ, < )) |
18 | 15, 16, 17 | syl2anc 409 |
. . . . . 6
⊢
((((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ℝ) ∧ 𝐶 ∈ ℝ) → sup({𝐴, 𝐵}, ℝ*, < ) = sup({𝐴, 𝐵}, ℝ, < )) |
19 | | simp-4r 537 |
. . . . . . 7
⊢
((((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ℝ) ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) |
20 | | simpr 109 |
. . . . . . . 8
⊢
((((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ℝ) ∧ 𝐶 ∈ ℝ) → 𝐶 ∈ ℝ) |
21 | | maxltsup 11169 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) →
(sup({𝐴, 𝐵}, ℝ, < ) < 𝐶 ↔ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶))) |
22 | 15, 16, 20, 21 | syl3anc 1233 |
. . . . . . 7
⊢
((((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ℝ) ∧ 𝐶 ∈ ℝ) → (sup({𝐴, 𝐵}, ℝ, < ) < 𝐶 ↔ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶))) |
23 | 19, 22 | mpbird 166 |
. . . . . 6
⊢
((((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ℝ) ∧ 𝐶 ∈ ℝ) → sup({𝐴, 𝐵}, ℝ, < ) < 𝐶) |
24 | 18, 23 | eqbrtrd 4009 |
. . . . 5
⊢
((((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ℝ) ∧ 𝐶 ∈ ℝ) → sup({𝐴, 𝐵}, ℝ*, < ) < 𝐶) |
25 | | simplr 525 |
. . . . . . . . 9
⊢
((((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ℝ) ∧ 𝐶 = +∞) → 𝐴 ∈ ℝ) |
26 | | simpllr 529 |
. . . . . . . . 9
⊢
((((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ℝ) ∧ 𝐶 = +∞) → 𝐵 ∈ ℝ) |
27 | | maxcl 11161 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
sup({𝐴, 𝐵}, ℝ, < ) ∈
ℝ) |
28 | 25, 26, 27 | syl2anc 409 |
. . . . . . . 8
⊢
((((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ℝ) ∧ 𝐶 = +∞) → sup({𝐴, 𝐵}, ℝ, < ) ∈
ℝ) |
29 | 17 | eleq1d 2239 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
(sup({𝐴, 𝐵}, ℝ*, < ) ∈
ℝ ↔ sup({𝐴,
𝐵}, ℝ, < ) ∈
ℝ)) |
30 | 25, 26, 29 | syl2anc 409 |
. . . . . . . 8
⊢
((((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ℝ) ∧ 𝐶 = +∞) → (sup({𝐴, 𝐵}, ℝ*, < ) ∈
ℝ ↔ sup({𝐴,
𝐵}, ℝ, < ) ∈
ℝ)) |
31 | 28, 30 | mpbird 166 |
. . . . . . 7
⊢
((((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ℝ) ∧ 𝐶 = +∞) → sup({𝐴, 𝐵}, ℝ*, < ) ∈
ℝ) |
32 | | ltpnf 9724 |
. . . . . . 7
⊢
(sup({𝐴, 𝐵}, ℝ*, < )
∈ ℝ → sup({𝐴, 𝐵}, ℝ*, < ) <
+∞) |
33 | 31, 32 | syl 14 |
. . . . . 6
⊢
((((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ℝ) ∧ 𝐶 = +∞) → sup({𝐴, 𝐵}, ℝ*, < ) <
+∞) |
34 | | simpr 109 |
. . . . . 6
⊢
((((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ℝ) ∧ 𝐶 = +∞) → 𝐶 = +∞) |
35 | 33, 34 | breqtrrd 4015 |
. . . . 5
⊢
((((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ℝ) ∧ 𝐶 = +∞) → sup({𝐴, 𝐵}, ℝ*, < ) < 𝐶) |
36 | | simprl 526 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) → 𝐴 < 𝐶) |
37 | 36 | ad3antrrr 489 |
. . . . . 6
⊢
((((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ℝ) ∧ 𝐶 = -∞) → 𝐴 < 𝐶) |
38 | | nltmnf 9732 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ*
→ ¬ 𝐴 <
-∞) |
39 | 38 | 3ad2ant1 1013 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) → ¬ 𝐴 < -∞) |
40 | 39 | ad4antr 491 |
. . . . . . 7
⊢
((((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ℝ) ∧ 𝐶 = -∞) → ¬ 𝐴 < -∞) |
41 | | simpr 109 |
. . . . . . . 8
⊢
((((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ℝ) ∧ 𝐶 = -∞) → 𝐶 = -∞) |
42 | 41 | breq2d 3999 |
. . . . . . 7
⊢
((((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ℝ) ∧ 𝐶 = -∞) → (𝐴 < 𝐶 ↔ 𝐴 < -∞)) |
43 | 40, 42 | mtbird 668 |
. . . . . 6
⊢
((((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ℝ) ∧ 𝐶 = -∞) → ¬ 𝐴 < 𝐶) |
44 | 37, 43 | pm2.21dd 615 |
. . . . 5
⊢
((((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ℝ) ∧ 𝐶 = -∞) → sup({𝐴, 𝐵}, ℝ*, < ) < 𝐶) |
45 | | elxr 9720 |
. . . . . . . 8
⊢ (𝐶 ∈ ℝ*
↔ (𝐶 ∈ ℝ
∨ 𝐶 = +∞ ∨
𝐶 =
-∞)) |
46 | 45 | biimpi 119 |
. . . . . . 7
⊢ (𝐶 ∈ ℝ*
→ (𝐶 ∈ ℝ
∨ 𝐶 = +∞ ∨
𝐶 =
-∞)) |
47 | 46 | 3ad2ant3 1015 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) → (𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞)) |
48 | 47 | ad3antrrr 489 |
. . . . 5
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ℝ) → (𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞)) |
49 | 24, 35, 44, 48 | mpjao3dan 1302 |
. . . 4
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ℝ) → sup({𝐴, 𝐵}, ℝ*, < ) < 𝐶) |
50 | 36 | ad2antrr 485 |
. . . . 5
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) ∧ 𝐵 ∈ ℝ) ∧ 𝐴 = +∞) → 𝐴 < 𝐶) |
51 | | pnfnlt 9731 |
. . . . . . . 8
⊢ (𝐶 ∈ ℝ*
→ ¬ +∞ < 𝐶) |
52 | 51 | 3ad2ant3 1015 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) → ¬ +∞ < 𝐶) |
53 | 52 | ad3antrrr 489 |
. . . . . 6
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) ∧ 𝐵 ∈ ℝ) ∧ 𝐴 = +∞) → ¬ +∞ <
𝐶) |
54 | | simpr 109 |
. . . . . . 7
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) ∧ 𝐵 ∈ ℝ) ∧ 𝐴 = +∞) → 𝐴 = +∞) |
55 | 54 | breq1d 3997 |
. . . . . 6
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) ∧ 𝐵 ∈ ℝ) ∧ 𝐴 = +∞) → (𝐴 < 𝐶 ↔ +∞ < 𝐶)) |
56 | 53, 55 | mtbird 668 |
. . . . 5
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) ∧ 𝐵 ∈ ℝ) ∧ 𝐴 = +∞) → ¬ 𝐴 < 𝐶) |
57 | 50, 56 | pm2.21dd 615 |
. . . 4
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) ∧ 𝐵 ∈ ℝ) ∧ 𝐴 = +∞) → sup({𝐴, 𝐵}, ℝ*, < ) < 𝐶) |
58 | | simpr 109 |
. . . . . . 7
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) ∧ 𝐵 ∈ ℝ) ∧ 𝐴 = -∞) → 𝐴 = -∞) |
59 | | mnfle 9736 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℝ*
→ -∞ ≤ 𝐵) |
60 | 59 | 3ad2ant2 1014 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) → -∞ ≤ 𝐵) |
61 | 60 | ad3antrrr 489 |
. . . . . . 7
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) ∧ 𝐵 ∈ ℝ) ∧ 𝐴 = -∞) → -∞ ≤ 𝐵) |
62 | 58, 61 | eqbrtrd 4009 |
. . . . . 6
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) ∧ 𝐵 ∈ ℝ) ∧ 𝐴 = -∞) → 𝐴 ≤ 𝐵) |
63 | | simp1 992 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) → 𝐴 ∈
ℝ*) |
64 | 63 | ad3antrrr 489 |
. . . . . . 7
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) ∧ 𝐵 ∈ ℝ) ∧ 𝐴 = -∞) → 𝐴 ∈
ℝ*) |
65 | | simp2 993 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) → 𝐵 ∈
ℝ*) |
66 | 65 | ad3antrrr 489 |
. . . . . . 7
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) ∧ 𝐵 ∈ ℝ) ∧ 𝐴 = -∞) → 𝐵 ∈
ℝ*) |
67 | | xrmaxleim 11194 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝐴 ≤ 𝐵 → sup({𝐴, 𝐵}, ℝ*, < ) = 𝐵)) |
68 | 64, 66, 67 | syl2anc 409 |
. . . . . 6
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) ∧ 𝐵 ∈ ℝ) ∧ 𝐴 = -∞) → (𝐴 ≤ 𝐵 → sup({𝐴, 𝐵}, ℝ*, < ) = 𝐵)) |
69 | 62, 68 | mpd 13 |
. . . . 5
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) ∧ 𝐵 ∈ ℝ) ∧ 𝐴 = -∞) → sup({𝐴, 𝐵}, ℝ*, < ) = 𝐵) |
70 | | simprr 527 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) → 𝐵 < 𝐶) |
71 | 70 | ad2antrr 485 |
. . . . 5
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) ∧ 𝐵 ∈ ℝ) ∧ 𝐴 = -∞) → 𝐵 < 𝐶) |
72 | 69, 71 | eqbrtrd 4009 |
. . . 4
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) ∧ 𝐵 ∈ ℝ) ∧ 𝐴 = -∞) → sup({𝐴, 𝐵}, ℝ*, < ) < 𝐶) |
73 | | elxr 9720 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ*
↔ (𝐴 ∈ ℝ
∨ 𝐴 = +∞ ∨
𝐴 =
-∞)) |
74 | 73 | biimpi 119 |
. . . . . 6
⊢ (𝐴 ∈ ℝ*
→ (𝐴 ∈ ℝ
∨ 𝐴 = +∞ ∨
𝐴 =
-∞)) |
75 | 74 | 3ad2ant1 1013 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) → (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞)) |
76 | 75 | ad2antrr 485 |
. . . 4
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) ∧ 𝐵 ∈ ℝ) → (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞)) |
77 | 49, 57, 72, 76 | mpjao3dan 1302 |
. . 3
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) ∧ 𝐵 ∈ ℝ) → sup({𝐴, 𝐵}, ℝ*, < ) < 𝐶) |
78 | | simplrr 531 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) ∧ 𝐵 = +∞) → 𝐵 < 𝐶) |
79 | | breq1 3990 |
. . . . . 6
⊢ (𝐵 = +∞ → (𝐵 < 𝐶 ↔ +∞ < 𝐶)) |
80 | 79 | adantl 275 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) ∧ 𝐵 = +∞) → (𝐵 < 𝐶 ↔ +∞ < 𝐶)) |
81 | 78, 80 | mpbid 146 |
. . . 4
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) ∧ 𝐵 = +∞) → +∞ < 𝐶) |
82 | 52 | ad2antrr 485 |
. . . 4
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) ∧ 𝐵 = +∞) → ¬ +∞ <
𝐶) |
83 | 81, 82 | pm2.21dd 615 |
. . 3
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) ∧ 𝐵 = +∞) → sup({𝐴, 𝐵}, ℝ*, < ) < 𝐶) |
84 | | prcom 3657 |
. . . . . 6
⊢ {𝐵, 𝐴} = {𝐴, 𝐵} |
85 | 84 | supeq1i 6961 |
. . . . 5
⊢
sup({𝐵, 𝐴}, ℝ*, < ) =
sup({𝐴, 𝐵}, ℝ*, <
) |
86 | | simpr 109 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) ∧ 𝐵 = -∞) → 𝐵 = -∞) |
87 | | mnfle 9736 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ*
→ -∞ ≤ 𝐴) |
88 | 87 | 3ad2ant1 1013 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) → -∞ ≤ 𝐴) |
89 | 88 | ad2antrr 485 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) ∧ 𝐵 = -∞) → -∞ ≤ 𝐴) |
90 | 86, 89 | eqbrtrd 4009 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) ∧ 𝐵 = -∞) → 𝐵 ≤ 𝐴) |
91 | | simpll2 1032 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) ∧ 𝐵 = -∞) → 𝐵 ∈
ℝ*) |
92 | | simpll1 1031 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) ∧ 𝐵 = -∞) → 𝐴 ∈
ℝ*) |
93 | | xrmaxleim 11194 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ*
∧ 𝐴 ∈
ℝ*) → (𝐵 ≤ 𝐴 → sup({𝐵, 𝐴}, ℝ*, < ) = 𝐴)) |
94 | 91, 92, 93 | syl2anc 409 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) ∧ 𝐵 = -∞) → (𝐵 ≤ 𝐴 → sup({𝐵, 𝐴}, ℝ*, < ) = 𝐴)) |
95 | 90, 94 | mpd 13 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) ∧ 𝐵 = -∞) → sup({𝐵, 𝐴}, ℝ*, < ) = 𝐴) |
96 | 85, 95 | eqtr3id 2217 |
. . . 4
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) ∧ 𝐵 = -∞) → sup({𝐴, 𝐵}, ℝ*, < ) = 𝐴) |
97 | | simplrl 530 |
. . . 4
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) ∧ 𝐵 = -∞) → 𝐴 < 𝐶) |
98 | 96, 97 | eqbrtrd 4009 |
. . 3
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) ∧ 𝐵 = -∞) → sup({𝐴, 𝐵}, ℝ*, < ) < 𝐶) |
99 | | elxr 9720 |
. . . . . 6
⊢ (𝐵 ∈ ℝ*
↔ (𝐵 ∈ ℝ
∨ 𝐵 = +∞ ∨
𝐵 =
-∞)) |
100 | 99 | biimpi 119 |
. . . . 5
⊢ (𝐵 ∈ ℝ*
→ (𝐵 ∈ ℝ
∨ 𝐵 = +∞ ∨
𝐵 =
-∞)) |
101 | 100 | 3ad2ant2 1014 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) → (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞)) |
102 | 101 | adantr 274 |
. . 3
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) → (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞)) |
103 | 77, 83, 98, 102 | mpjao3dan 1302 |
. 2
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)) → sup({𝐴, 𝐵}, ℝ*, < ) < 𝐶) |
104 | 14, 103 | impbida 591 |
1
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) → (sup({𝐴, 𝐵}, ℝ*, < ) < 𝐶 ↔ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶))) |