Step | Hyp | Ref
| Expression |
1 | | iocval 9875 |
. . 3
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝐴(,]𝐵) = {𝑥 ∈ ℝ* ∣ (𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵)}) |
2 | 1 | eqeq1d 2179 |
. 2
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → ((𝐴(,]𝐵) = ∅ ↔ {𝑥 ∈ ℝ* ∣ (𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵)} = ∅)) |
3 | | xrltletr 9764 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ*
∧ 𝑥 ∈
ℝ* ∧ 𝐵
∈ ℝ*) → ((𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵) → 𝐴 < 𝐵)) |
4 | 3 | 3com23 1204 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝑥
∈ ℝ*) → ((𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵) → 𝐴 < 𝐵)) |
5 | 4 | 3expa 1198 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ ℝ*) → ((𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵) → 𝐴 < 𝐵)) |
6 | 5 | rexlimdva 2587 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (∃𝑥 ∈ ℝ* (𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵) → 𝐴 < 𝐵)) |
7 | | qbtwnxr 10214 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)) |
8 | | qre 9584 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℚ → 𝑥 ∈
ℝ) |
9 | 8 | rexrd 7969 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℚ → 𝑥 ∈
ℝ*) |
10 | 9 | a1i 9 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ*
∧ (𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐴 < 𝐵)) → (𝑥 ∈ ℚ → 𝑥 ∈
ℝ*)) |
11 | | xrltle 9755 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝑥 < 𝐵 → 𝑥 ≤ 𝐵)) |
12 | 11 | 3ad2antr2 1158 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ*
∧ (𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐴 < 𝐵)) → (𝑥 < 𝐵 → 𝑥 ≤ 𝐵)) |
13 | 12 | anim2d 335 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ*
∧ (𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐴 < 𝐵)) → ((𝐴 < 𝑥 ∧ 𝑥 < 𝐵) → (𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵))) |
14 | 10, 13 | anim12d 333 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ*
∧ (𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐴 < 𝐵)) → ((𝑥 ∈ ℚ ∧ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)) → (𝑥 ∈ ℝ* ∧ (𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵)))) |
15 | 14 | ex 114 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ*
→ ((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐴 < 𝐵) → ((𝑥 ∈ ℚ ∧ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)) → (𝑥 ∈ ℝ* ∧ (𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵))))) |
16 | 9, 15 | syl 14 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℚ → ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) → ((𝑥 ∈ ℚ ∧ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)) → (𝑥 ∈ ℝ* ∧ (𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵))))) |
17 | 16 | adantr 274 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℚ ∧ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)) → ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐴 < 𝐵) → ((𝑥 ∈ ℚ ∧ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)) → (𝑥 ∈ ℝ* ∧ (𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵))))) |
18 | 17 | pm2.43b 52 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) → ((𝑥 ∈ ℚ ∧ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)) → (𝑥 ∈ ℝ* ∧ (𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵)))) |
19 | 18 | reximdv2 2569 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) →
(∃𝑥 ∈ ℚ
(𝐴 < 𝑥 ∧ 𝑥 < 𝐵) → ∃𝑥 ∈ ℝ* (𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵))) |
20 | 7, 19 | mpd 13 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) → ∃𝑥 ∈ ℝ*
(𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵)) |
21 | 20 | 3expia 1200 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℝ* (𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵))) |
22 | 6, 21 | impbid 128 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (∃𝑥 ∈ ℝ* (𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵) ↔ 𝐴 < 𝐵)) |
23 | 22 | notbid 662 |
. . 3
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (¬ ∃𝑥 ∈ ℝ* (𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵) ↔ ¬ 𝐴 < 𝐵)) |
24 | | rabeq0 3444 |
. . . . 5
⊢ ({𝑥 ∈ ℝ*
∣ (𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵)} = ∅ ↔ ∀𝑥 ∈ ℝ*
¬ (𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵)) |
25 | | ralnex 2458 |
. . . . 5
⊢
(∀𝑥 ∈
ℝ* ¬ (𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵) ↔ ¬ ∃𝑥 ∈ ℝ* (𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵)) |
26 | 24, 25 | bitri 183 |
. . . 4
⊢ ({𝑥 ∈ ℝ*
∣ (𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵)} = ∅ ↔ ¬ ∃𝑥 ∈ ℝ*
(𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵)) |
27 | 26 | a1i 9 |
. . 3
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → ({𝑥 ∈ ℝ* ∣ (𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵)} = ∅ ↔ ¬ ∃𝑥 ∈ ℝ*
(𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵))) |
28 | | xrlenlt 7984 |
. . . 4
⊢ ((𝐵 ∈ ℝ*
∧ 𝐴 ∈
ℝ*) → (𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵)) |
29 | 28 | ancoms 266 |
. . 3
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵)) |
30 | 23, 27, 29 | 3bitr4d 219 |
. 2
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → ({𝑥 ∈ ℝ* ∣ (𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵)} = ∅ ↔ 𝐵 ≤ 𝐴)) |
31 | 2, 30 | bitrd 187 |
1
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → ((𝐴(,]𝐵) = ∅ ↔ 𝐵 ≤ 𝐴)) |