Step | Hyp | Ref
| Expression |
1 | | iocval 13116 |
. . 3
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝐴(,]𝐵) = {𝑥 ∈ ℝ* ∣ (𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵)}) |
2 | 1 | eqeq1d 2740 |
. 2
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → ((𝐴(,]𝐵) = ∅ ↔ {𝑥 ∈ ℝ* ∣ (𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵)} = ∅)) |
3 | | df-ne 2944 |
. . . . . 6
⊢ ({𝑥 ∈ ℝ*
∣ (𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵)} ≠ ∅ ↔ ¬ {𝑥 ∈ ℝ*
∣ (𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵)} = ∅) |
4 | | rabn0 4319 |
. . . . . 6
⊢ ({𝑥 ∈ ℝ*
∣ (𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵)} ≠ ∅ ↔ ∃𝑥 ∈ ℝ*
(𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵)) |
5 | 3, 4 | bitr3i 276 |
. . . . 5
⊢ (¬
{𝑥 ∈
ℝ* ∣ (𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵)} = ∅ ↔ ∃𝑥 ∈ ℝ*
(𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵)) |
6 | | xrltletr 12891 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ*
∧ 𝑥 ∈
ℝ* ∧ 𝐵
∈ ℝ*) → ((𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵) → 𝐴 < 𝐵)) |
7 | 6 | 3com23 1125 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝑥
∈ ℝ*) → ((𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵) → 𝐴 < 𝐵)) |
8 | 7 | 3expa 1117 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ ℝ*) → ((𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵) → 𝐴 < 𝐵)) |
9 | 8 | rexlimdva 3213 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (∃𝑥 ∈ ℝ* (𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵) → 𝐴 < 𝐵)) |
10 | | qbtwnxr 12934 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)) |
11 | | qre 12693 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℚ → 𝑥 ∈
ℝ) |
12 | 11 | rexrd 11025 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℚ → 𝑥 ∈
ℝ*) |
13 | 12 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ*
∧ (𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐴 < 𝐵)) → (𝑥 ∈ ℚ → 𝑥 ∈
ℝ*)) |
14 | | xrltle 12883 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝑥 < 𝐵 → 𝑥 ≤ 𝐵)) |
15 | 14 | 3ad2antr2 1188 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ*
∧ (𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐴 < 𝐵)) → (𝑥 < 𝐵 → 𝑥 ≤ 𝐵)) |
16 | 15 | anim2d 612 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ*
∧ (𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐴 < 𝐵)) → ((𝐴 < 𝑥 ∧ 𝑥 < 𝐵) → (𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵))) |
17 | 13, 16 | anim12d 609 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ*
∧ (𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐴 < 𝐵)) → ((𝑥 ∈ ℚ ∧ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)) → (𝑥 ∈ ℝ* ∧ (𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵)))) |
18 | 17 | ex 413 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ*
→ ((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐴 < 𝐵) → ((𝑥 ∈ ℚ ∧ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)) → (𝑥 ∈ ℝ* ∧ (𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵))))) |
19 | 12, 18 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℚ → ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) → ((𝑥 ∈ ℚ ∧ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)) → (𝑥 ∈ ℝ* ∧ (𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵))))) |
20 | 19 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℚ ∧ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)) → ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐴 < 𝐵) → ((𝑥 ∈ ℚ ∧ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)) → (𝑥 ∈ ℝ* ∧ (𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵))))) |
21 | 20 | pm2.43b 55 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) → ((𝑥 ∈ ℚ ∧ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)) → (𝑥 ∈ ℝ* ∧ (𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵)))) |
22 | 21 | reximdv2 3199 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) →
(∃𝑥 ∈ ℚ
(𝐴 < 𝑥 ∧ 𝑥 < 𝐵) → ∃𝑥 ∈ ℝ* (𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵))) |
23 | 10, 22 | mpd 15 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) → ∃𝑥 ∈ ℝ*
(𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵)) |
24 | 23 | 3expia 1120 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℝ* (𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵))) |
25 | 9, 24 | impbid 211 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (∃𝑥 ∈ ℝ* (𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵) ↔ 𝐴 < 𝐵)) |
26 | 5, 25 | bitrid 282 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (¬ {𝑥 ∈ ℝ* ∣ (𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵)} = ∅ ↔ 𝐴 < 𝐵)) |
27 | | xrltnle 11042 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴)) |
28 | 26, 27 | bitrd 278 |
. . 3
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (¬ {𝑥 ∈ ℝ* ∣ (𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵)} = ∅ ↔ ¬ 𝐵 ≤ 𝐴)) |
29 | 28 | con4bid 317 |
. 2
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → ({𝑥 ∈ ℝ* ∣ (𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵)} = ∅ ↔ 𝐵 ≤ 𝐴)) |
30 | 2, 29 | bitrd 278 |
1
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → ((𝐴(,]𝐵) = ∅ ↔ 𝐵 ≤ 𝐴)) |