Proof of Theorem qextltlem
Step | Hyp | Ref
| Expression |
1 | | qbtwnxr 12031 |
. . 3
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)) |
2 | 1 | 3expia 1267 |
. 2
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))) |
3 | | simprl 794 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ ℚ) ∧ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)) → 𝐴 < 𝑥) |
4 | | simplll 798 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ ℚ) ∧ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)) → 𝐴 ∈
ℝ*) |
5 | | qre 11793 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℚ → 𝑥 ∈
ℝ) |
6 | 5 | rexrd 10089 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℚ → 𝑥 ∈
ℝ*) |
7 | 6 | ad2antlr 763 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ ℚ) ∧ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)) → 𝑥 ∈ ℝ*) |
8 | | xrltnle 10105 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ*
∧ 𝑥 ∈
ℝ*) → (𝐴 < 𝑥 ↔ ¬ 𝑥 ≤ 𝐴)) |
9 | 4, 7, 8 | syl2anc 693 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ ℚ) ∧ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)) → (𝐴 < 𝑥 ↔ ¬ 𝑥 ≤ 𝐴)) |
10 | 3, 9 | mpbid 222 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ ℚ) ∧ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)) → ¬ 𝑥 ≤ 𝐴) |
11 | | xrltle 11982 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ*
∧ 𝐴 ∈
ℝ*) → (𝑥 < 𝐴 → 𝑥 ≤ 𝐴)) |
12 | 7, 4, 11 | syl2anc 693 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ ℚ) ∧ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)) → (𝑥 < 𝐴 → 𝑥 ≤ 𝐴)) |
13 | 10, 12 | mtod 189 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ ℚ) ∧ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)) → ¬ 𝑥 < 𝐴) |
14 | | simprr 796 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ ℚ) ∧ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)) → 𝑥 < 𝐵) |
15 | 13, 14 | 2thd 255 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ ℚ) ∧ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)) → (¬ 𝑥 < 𝐴 ↔ 𝑥 < 𝐵)) |
16 | | nbbn 373 |
. . . . . 6
⊢ ((¬
𝑥 < 𝐴 ↔ 𝑥 < 𝐵) ↔ ¬ (𝑥 < 𝐴 ↔ 𝑥 < 𝐵)) |
17 | 15, 16 | sylib 208 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ ℚ) ∧ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)) → ¬ (𝑥 < 𝐴 ↔ 𝑥 < 𝐵)) |
18 | | simpllr 799 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ ℚ) ∧ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)) → 𝐵 ∈
ℝ*) |
19 | | xrltle 11982 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝑥 < 𝐵 → 𝑥 ≤ 𝐵)) |
20 | 7, 18, 19 | syl2anc 693 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ ℚ) ∧ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)) → (𝑥 < 𝐵 → 𝑥 ≤ 𝐵)) |
21 | 14, 20 | mpd 15 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ ℚ) ∧ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)) → 𝑥 ≤ 𝐵) |
22 | 10, 21 | 2thd 255 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ ℚ) ∧ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)) → (¬ 𝑥 ≤ 𝐴 ↔ 𝑥 ≤ 𝐵)) |
23 | | nbbn 373 |
. . . . . 6
⊢ ((¬
𝑥 ≤ 𝐴 ↔ 𝑥 ≤ 𝐵) ↔ ¬ (𝑥 ≤ 𝐴 ↔ 𝑥 ≤ 𝐵)) |
24 | 22, 23 | sylib 208 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ ℚ) ∧ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)) → ¬ (𝑥 ≤ 𝐴 ↔ 𝑥 ≤ 𝐵)) |
25 | 17, 24 | jca 554 |
. . . 4
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ ℚ) ∧ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)) → (¬ (𝑥 < 𝐴 ↔ 𝑥 < 𝐵) ∧ ¬ (𝑥 ≤ 𝐴 ↔ 𝑥 ≤ 𝐵))) |
26 | 25 | ex 450 |
. . 3
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝑥 ∈ ℚ) → ((𝐴 < 𝑥 ∧ 𝑥 < 𝐵) → (¬ (𝑥 < 𝐴 ↔ 𝑥 < 𝐵) ∧ ¬ (𝑥 ≤ 𝐴 ↔ 𝑥 ≤ 𝐵)))) |
27 | 26 | reximdva 3017 |
. 2
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵) → ∃𝑥 ∈ ℚ (¬ (𝑥 < 𝐴 ↔ 𝑥 < 𝐵) ∧ ¬ (𝑥 ≤ 𝐴 ↔ 𝑥 ≤ 𝐵)))) |
28 | 2, 27 | syld 47 |
1
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (¬ (𝑥 < 𝐴 ↔ 𝑥 < 𝐵) ∧ ¬ (𝑥 ≤ 𝐴 ↔ 𝑥 ≤ 𝐵)))) |