Proof of Theorem ixxub
Step | Hyp | Ref
| Expression |
1 | | ixx.1 |
. . . . . . . . 9
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) |
2 | 1 | elixx1 12055 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝑤 ∈ (𝐴𝑂𝐵) ↔ (𝑤 ∈ ℝ* ∧ 𝐴𝑅𝑤 ∧ 𝑤𝑆𝐵))) |
3 | 2 | 3adant3 1074 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐴𝑂𝐵) ≠ ∅) → (𝑤 ∈ (𝐴𝑂𝐵) ↔ (𝑤 ∈ ℝ* ∧ 𝐴𝑅𝑤 ∧ 𝑤𝑆𝐵))) |
4 | 3 | biimpa 500 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ (𝐴𝑂𝐵)) → (𝑤 ∈ ℝ* ∧ 𝐴𝑅𝑤 ∧ 𝑤𝑆𝐵)) |
5 | 4 | simp3d 1068 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ (𝐴𝑂𝐵)) → 𝑤𝑆𝐵) |
6 | 4 | simp1d 1066 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ (𝐴𝑂𝐵)) → 𝑤 ∈ ℝ*) |
7 | | simp2 1055 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐴𝑂𝐵) ≠ ∅) → 𝐵 ∈
ℝ*) |
8 | 7 | adantr 480 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ (𝐴𝑂𝐵)) → 𝐵 ∈
ℝ*) |
9 | | ixxub.3 |
. . . . . 6
⊢ ((𝑤 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝑤𝑆𝐵 → 𝑤 ≤ 𝐵)) |
10 | 6, 8, 9 | syl2anc 691 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ (𝐴𝑂𝐵)) → (𝑤𝑆𝐵 → 𝑤 ≤ 𝐵)) |
11 | 5, 10 | mpd 15 |
. . . 4
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ (𝐴𝑂𝐵)) → 𝑤 ≤ 𝐵) |
12 | 11 | ralrimiva 2949 |
. . 3
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐴𝑂𝐵) ≠ ∅) → ∀𝑤 ∈ (𝐴𝑂𝐵)𝑤 ≤ 𝐵) |
13 | 6 | ex 449 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐴𝑂𝐵) ≠ ∅) → (𝑤 ∈ (𝐴𝑂𝐵) → 𝑤 ∈
ℝ*)) |
14 | 13 | ssrdv 3574 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐴𝑂𝐵) ≠ ∅) → (𝐴𝑂𝐵) ⊆
ℝ*) |
15 | | supxrleub 12028 |
. . . 4
⊢ (((𝐴𝑂𝐵) ⊆ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (sup((𝐴𝑂𝐵), ℝ*, < ) ≤ 𝐵 ↔ ∀𝑤 ∈ (𝐴𝑂𝐵)𝑤 ≤ 𝐵)) |
16 | 14, 7, 15 | syl2anc 691 |
. . 3
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐴𝑂𝐵) ≠ ∅) → (sup((𝐴𝑂𝐵), ℝ*, < ) ≤ 𝐵 ↔ ∀𝑤 ∈ (𝐴𝑂𝐵)𝑤 ≤ 𝐵)) |
17 | 12, 16 | mpbird 246 |
. 2
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐴𝑂𝐵) ≠ ∅) → sup((𝐴𝑂𝐵), ℝ*, < ) ≤ 𝐵) |
18 | | simprl 790 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ ℚ) ∧ (sup((𝐴𝑂𝐵), ℝ*, < ) < 𝑤 ∧ 𝑤 < 𝐵)) → sup((𝐴𝑂𝐵), ℝ*, < ) < 𝑤) |
19 | 14 | ad2antrr 758 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ ℚ) ∧ (sup((𝐴𝑂𝐵), ℝ*, < ) < 𝑤 ∧ 𝑤 < 𝐵)) → (𝐴𝑂𝐵) ⊆
ℝ*) |
20 | | qre 11669 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ ℚ → 𝑤 ∈
ℝ) |
21 | 20 | rexrd 9968 |
. . . . . . . . . 10
⊢ (𝑤 ∈ ℚ → 𝑤 ∈
ℝ*) |
22 | 21 | ad2antlr 759 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ ℚ) ∧ (sup((𝐴𝑂𝐵), ℝ*, < ) < 𝑤 ∧ 𝑤 < 𝐵)) → 𝑤 ∈ ℝ*) |
23 | | simp1 1054 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐴𝑂𝐵) ≠ ∅) → 𝐴 ∈
ℝ*) |
24 | 23 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ ℚ) ∧ (sup((𝐴𝑂𝐵), ℝ*, < ) < 𝑤 ∧ 𝑤 < 𝐵)) → 𝐴 ∈
ℝ*) |
25 | | supxrcl 12017 |
. . . . . . . . . . . . 13
⊢ ((𝐴𝑂𝐵) ⊆ ℝ* →
sup((𝐴𝑂𝐵), ℝ*, < ) ∈
ℝ*) |
26 | 14, 25 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐴𝑂𝐵) ≠ ∅) → sup((𝐴𝑂𝐵), ℝ*, < ) ∈
ℝ*) |
27 | 26 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ ℚ) ∧ (sup((𝐴𝑂𝐵), ℝ*, < ) < 𝑤 ∧ 𝑤 < 𝐵)) → sup((𝐴𝑂𝐵), ℝ*, < ) ∈
ℝ*) |
28 | | simp3 1056 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐴𝑂𝐵) ≠ ∅) → (𝐴𝑂𝐵) ≠ ∅) |
29 | | n0 3890 |
. . . . . . . . . . . . . 14
⊢ ((𝐴𝑂𝐵) ≠ ∅ ↔ ∃𝑤 𝑤 ∈ (𝐴𝑂𝐵)) |
30 | 28, 29 | sylib 207 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐴𝑂𝐵) ≠ ∅) → ∃𝑤 𝑤 ∈ (𝐴𝑂𝐵)) |
31 | 23 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ (𝐴𝑂𝐵)) → 𝐴 ∈
ℝ*) |
32 | 26 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ (𝐴𝑂𝐵)) → sup((𝐴𝑂𝐵), ℝ*, < ) ∈
ℝ*) |
33 | 4 | simp2d 1067 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ (𝐴𝑂𝐵)) → 𝐴𝑅𝑤) |
34 | | ixxub.5 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℝ*
∧ 𝑤 ∈
ℝ*) → (𝐴𝑅𝑤 → 𝐴 ≤ 𝑤)) |
35 | 31, 6, 34 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ (𝐴𝑂𝐵)) → (𝐴𝑅𝑤 → 𝐴 ≤ 𝑤)) |
36 | 33, 35 | mpd 15 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ (𝐴𝑂𝐵)) → 𝐴 ≤ 𝑤) |
37 | | supxrub 12026 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴𝑂𝐵) ⊆ ℝ* ∧ 𝑤 ∈ (𝐴𝑂𝐵)) → 𝑤 ≤ sup((𝐴𝑂𝐵), ℝ*, <
)) |
38 | 14, 37 | sylan 487 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ (𝐴𝑂𝐵)) → 𝑤 ≤ sup((𝐴𝑂𝐵), ℝ*, <
)) |
39 | 31, 6, 32, 36, 38 | xrletrd 11869 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ (𝐴𝑂𝐵)) → 𝐴 ≤ sup((𝐴𝑂𝐵), ℝ*, <
)) |
40 | 30, 39 | exlimddv 1850 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐴𝑂𝐵) ≠ ∅) → 𝐴 ≤ sup((𝐴𝑂𝐵), ℝ*, <
)) |
41 | 40 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ ℚ) ∧ (sup((𝐴𝑂𝐵), ℝ*, < ) < 𝑤 ∧ 𝑤 < 𝐵)) → 𝐴 ≤ sup((𝐴𝑂𝐵), ℝ*, <
)) |
42 | 24, 27, 22, 41, 18 | xrlelttrd 11867 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ ℚ) ∧ (sup((𝐴𝑂𝐵), ℝ*, < ) < 𝑤 ∧ 𝑤 < 𝐵)) → 𝐴 < 𝑤) |
43 | | ixxub.4 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ*
∧ 𝑤 ∈
ℝ*) → (𝐴 < 𝑤 → 𝐴𝑅𝑤)) |
44 | 24, 22, 43 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ ℚ) ∧ (sup((𝐴𝑂𝐵), ℝ*, < ) < 𝑤 ∧ 𝑤 < 𝐵)) → (𝐴 < 𝑤 → 𝐴𝑅𝑤)) |
45 | 42, 44 | mpd 15 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ ℚ) ∧ (sup((𝐴𝑂𝐵), ℝ*, < ) < 𝑤 ∧ 𝑤 < 𝐵)) → 𝐴𝑅𝑤) |
46 | | simprr 792 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ ℚ) ∧ (sup((𝐴𝑂𝐵), ℝ*, < ) < 𝑤 ∧ 𝑤 < 𝐵)) → 𝑤 < 𝐵) |
47 | 7 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ ℚ) ∧ (sup((𝐴𝑂𝐵), ℝ*, < ) < 𝑤 ∧ 𝑤 < 𝐵)) → 𝐵 ∈
ℝ*) |
48 | | ixxub.2 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝑤 < 𝐵 → 𝑤𝑆𝐵)) |
49 | 22, 47, 48 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ ℚ) ∧ (sup((𝐴𝑂𝐵), ℝ*, < ) < 𝑤 ∧ 𝑤 < 𝐵)) → (𝑤 < 𝐵 → 𝑤𝑆𝐵)) |
50 | 46, 49 | mpd 15 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ ℚ) ∧ (sup((𝐴𝑂𝐵), ℝ*, < ) < 𝑤 ∧ 𝑤 < 𝐵)) → 𝑤𝑆𝐵) |
51 | 3 | ad2antrr 758 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ ℚ) ∧ (sup((𝐴𝑂𝐵), ℝ*, < ) < 𝑤 ∧ 𝑤 < 𝐵)) → (𝑤 ∈ (𝐴𝑂𝐵) ↔ (𝑤 ∈ ℝ* ∧ 𝐴𝑅𝑤 ∧ 𝑤𝑆𝐵))) |
52 | 22, 45, 50, 51 | mpbir3and 1238 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ ℚ) ∧ (sup((𝐴𝑂𝐵), ℝ*, < ) < 𝑤 ∧ 𝑤 < 𝐵)) → 𝑤 ∈ (𝐴𝑂𝐵)) |
53 | 19, 52, 37 | syl2anc 691 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ ℚ) ∧ (sup((𝐴𝑂𝐵), ℝ*, < ) < 𝑤 ∧ 𝑤 < 𝐵)) → 𝑤 ≤ sup((𝐴𝑂𝐵), ℝ*, <
)) |
54 | | xrlenlt 9982 |
. . . . . . . 8
⊢ ((𝑤 ∈ ℝ*
∧ sup((𝐴𝑂𝐵), ℝ*, < ) ∈
ℝ*) → (𝑤 ≤ sup((𝐴𝑂𝐵), ℝ*, < ) ↔ ¬
sup((𝐴𝑂𝐵), ℝ*, < ) < 𝑤)) |
55 | 22, 27, 54 | syl2anc 691 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ ℚ) ∧ (sup((𝐴𝑂𝐵), ℝ*, < ) < 𝑤 ∧ 𝑤 < 𝐵)) → (𝑤 ≤ sup((𝐴𝑂𝐵), ℝ*, < ) ↔ ¬
sup((𝐴𝑂𝐵), ℝ*, < ) < 𝑤)) |
56 | 53, 55 | mpbid 221 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ ℚ) ∧ (sup((𝐴𝑂𝐵), ℝ*, < ) < 𝑤 ∧ 𝑤 < 𝐵)) → ¬ sup((𝐴𝑂𝐵), ℝ*, < ) < 𝑤) |
57 | 18, 56 | pm2.65da 598 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐴𝑂𝐵) ≠ ∅) ∧ 𝑤 ∈ ℚ) → ¬ (sup((𝐴𝑂𝐵), ℝ*, < ) < 𝑤 ∧ 𝑤 < 𝐵)) |
58 | 57 | nrexdv 2984 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐴𝑂𝐵) ≠ ∅) → ¬ ∃𝑤 ∈ ℚ (sup((𝐴𝑂𝐵), ℝ*, < ) < 𝑤 ∧ 𝑤 < 𝐵)) |
59 | | qbtwnxr 11905 |
. . . . . 6
⊢
((sup((𝐴𝑂𝐵), ℝ*, < ) ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ sup((𝐴𝑂𝐵), ℝ*, < ) < 𝐵) → ∃𝑤 ∈ ℚ (sup((𝐴𝑂𝐵), ℝ*, < ) < 𝑤 ∧ 𝑤 < 𝐵)) |
60 | 59 | 3expia 1259 |
. . . . 5
⊢
((sup((𝐴𝑂𝐵), ℝ*, < ) ∈
ℝ* ∧ 𝐵
∈ ℝ*) → (sup((𝐴𝑂𝐵), ℝ*, < ) < 𝐵 → ∃𝑤 ∈ ℚ (sup((𝐴𝑂𝐵), ℝ*, < ) < 𝑤 ∧ 𝑤 < 𝐵))) |
61 | 26, 7, 60 | syl2anc 691 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐴𝑂𝐵) ≠ ∅) → (sup((𝐴𝑂𝐵), ℝ*, < ) < 𝐵 → ∃𝑤 ∈ ℚ (sup((𝐴𝑂𝐵), ℝ*, < ) < 𝑤 ∧ 𝑤 < 𝐵))) |
62 | 58, 61 | mtod 188 |
. . 3
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐴𝑂𝐵) ≠ ∅) → ¬ sup((𝐴𝑂𝐵), ℝ*, < ) < 𝐵) |
63 | | xrlenlt 9982 |
. . . 4
⊢ ((𝐵 ∈ ℝ*
∧ sup((𝐴𝑂𝐵), ℝ*, < ) ∈
ℝ*) → (𝐵 ≤ sup((𝐴𝑂𝐵), ℝ*, < ) ↔ ¬
sup((𝐴𝑂𝐵), ℝ*, < ) < 𝐵)) |
64 | 7, 26, 63 | syl2anc 691 |
. . 3
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐴𝑂𝐵) ≠ ∅) → (𝐵 ≤ sup((𝐴𝑂𝐵), ℝ*, < ) ↔ ¬
sup((𝐴𝑂𝐵), ℝ*, < ) < 𝐵)) |
65 | 62, 64 | mpbird 246 |
. 2
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐴𝑂𝐵) ≠ ∅) → 𝐵 ≤ sup((𝐴𝑂𝐵), ℝ*, <
)) |
66 | | xrletri3 11861 |
. . 3
⊢
((sup((𝐴𝑂𝐵), ℝ*, < ) ∈
ℝ* ∧ 𝐵
∈ ℝ*) → (sup((𝐴𝑂𝐵), ℝ*, < ) = 𝐵 ↔ (sup((𝐴𝑂𝐵), ℝ*, < ) ≤ 𝐵 ∧ 𝐵 ≤ sup((𝐴𝑂𝐵), ℝ*, <
)))) |
67 | 26, 7, 66 | syl2anc 691 |
. 2
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐴𝑂𝐵) ≠ ∅) → (sup((𝐴𝑂𝐵), ℝ*, < ) = 𝐵 ↔ (sup((𝐴𝑂𝐵), ℝ*, < ) ≤ 𝐵 ∧ 𝐵 ≤ sup((𝐴𝑂𝐵), ℝ*, <
)))) |
68 | 17, 65, 67 | mpbir2and 959 |
1
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐴𝑂𝐵) ≠ ∅) → sup((𝐴𝑂𝐵), ℝ*, < ) = 𝐵) |