Proof of Theorem qextltlem
Step | Hyp | Ref
| Expression |
1 | | qbtwnxr 11905 |
. . 3
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)) |
2 | 1 | 3expia 1259 |
. 2
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))) |
3 | | simprl 790 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ ℚ) ∧ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)) → 𝐴 < 𝑥) |
4 | | simplll 794 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ ℚ) ∧ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)) → 𝐴 ∈
ℝ*) |
5 | | qre 11669 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℚ → 𝑥 ∈
ℝ) |
6 | 5 | rexrd 9968 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℚ → 𝑥 ∈
ℝ*) |
7 | 6 | ad2antlr 759 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ ℚ) ∧ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)) → 𝑥 ∈ ℝ*) |
8 | | xrltnle 9984 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ*
∧ 𝑥 ∈
ℝ*) → (𝐴 < 𝑥 ↔ ¬ 𝑥 ≤ 𝐴)) |
9 | 4, 7, 8 | syl2anc 691 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ ℚ) ∧ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)) → (𝐴 < 𝑥 ↔ ¬ 𝑥 ≤ 𝐴)) |
10 | 3, 9 | mpbid 221 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ ℚ) ∧ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)) → ¬ 𝑥 ≤ 𝐴) |
11 | | xrltle 11858 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ*
∧ 𝐴 ∈
ℝ*) → (𝑥 < 𝐴 → 𝑥 ≤ 𝐴)) |
12 | 7, 4, 11 | syl2anc 691 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ ℚ) ∧ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)) → (𝑥 < 𝐴 → 𝑥 ≤ 𝐴)) |
13 | 10, 12 | mtod 188 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ ℚ) ∧ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)) → ¬ 𝑥 < 𝐴) |
14 | | simprr 792 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ ℚ) ∧ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)) → 𝑥 < 𝐵) |
15 | 13, 14 | 2thd 254 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ ℚ) ∧ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)) → (¬ 𝑥 < 𝐴 ↔ 𝑥 < 𝐵)) |
16 | | nbbn 372 |
. . . . . 6
⊢ ((¬
𝑥 < 𝐴 ↔ 𝑥 < 𝐵) ↔ ¬ (𝑥 < 𝐴 ↔ 𝑥 < 𝐵)) |
17 | 15, 16 | sylib 207 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ ℚ) ∧ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)) → ¬ (𝑥 < 𝐴 ↔ 𝑥 < 𝐵)) |
18 | | simpllr 795 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ ℚ) ∧ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)) → 𝐵 ∈
ℝ*) |
19 | | xrltle 11858 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝑥 < 𝐵 → 𝑥 ≤ 𝐵)) |
20 | 7, 18, 19 | syl2anc 691 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ ℚ) ∧ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)) → (𝑥 < 𝐵 → 𝑥 ≤ 𝐵)) |
21 | 14, 20 | mpd 15 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ ℚ) ∧ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)) → 𝑥 ≤ 𝐵) |
22 | 10, 21 | 2thd 254 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ ℚ) ∧ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)) → (¬ 𝑥 ≤ 𝐴 ↔ 𝑥 ≤ 𝐵)) |
23 | | nbbn 372 |
. . . . . 6
⊢ ((¬
𝑥 ≤ 𝐴 ↔ 𝑥 ≤ 𝐵) ↔ ¬ (𝑥 ≤ 𝐴 ↔ 𝑥 ≤ 𝐵)) |
24 | 22, 23 | sylib 207 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ ℚ) ∧ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)) → ¬ (𝑥 ≤ 𝐴 ↔ 𝑥 ≤ 𝐵)) |
25 | 17, 24 | jca 553 |
. . . 4
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ ℚ) ∧ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)) → (¬ (𝑥 < 𝐴 ↔ 𝑥 < 𝐵) ∧ ¬ (𝑥 ≤ 𝐴 ↔ 𝑥 ≤ 𝐵))) |
26 | 25 | ex 449 |
. . 3
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ ℚ) → ((𝐴 < 𝑥 ∧ 𝑥 < 𝐵) → (¬ (𝑥 < 𝐴 ↔ 𝑥 < 𝐵) ∧ ¬ (𝑥 ≤ 𝐴 ↔ 𝑥 ≤ 𝐵)))) |
27 | 26 | reximdva 3000 |
. 2
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵) → ∃𝑥 ∈ ℚ (¬ (𝑥 < 𝐴 ↔ 𝑥 < 𝐵) ∧ ¬ (𝑥 ≤ 𝐴 ↔ 𝑥 ≤ 𝐵)))) |
28 | 2, 27 | syld 46 |
1
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (¬ (𝑥 < 𝐴 ↔ 𝑥 < 𝐵) ∧ ¬ (𝑥 ≤ 𝐴 ↔ 𝑥 ≤ 𝐵)))) |