Proof of Theorem qbtwnxr
Step | Hyp | Ref
| Expression |
1 | | elxr 9661 |
. . 3
⊢ (𝐴 ∈ ℝ*
↔ (𝐴 ∈ ℝ
∨ 𝐴 = +∞ ∨
𝐴 =
-∞)) |
2 | | elxr 9661 |
. . . . 5
⊢ (𝐵 ∈ ℝ*
↔ (𝐵 ∈ ℝ
∨ 𝐵 = +∞ ∨
𝐵 =
-∞)) |
3 | | qbtwnre 10134 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)) |
4 | 3 | 3expia 1184 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))) |
5 | | simpl 108 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → 𝐴 ∈
ℝ) |
6 | | peano2re 7990 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ → (𝐴 + 1) ∈
ℝ) |
7 | 6 | adantr 274 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (𝐴 + 1) ∈
ℝ) |
8 | | ltp1 8694 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ → 𝐴 < (𝐴 + 1)) |
9 | 8 | adantr 274 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → 𝐴 < (𝐴 + 1)) |
10 | | qbtwnre 10134 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ (𝐴 + 1) ∈ ℝ ∧ 𝐴 < (𝐴 + 1)) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < (𝐴 + 1))) |
11 | 5, 7, 9, 10 | syl3anc 1217 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < (𝐴 + 1))) |
12 | | qre 9512 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℚ → 𝑥 ∈
ℝ) |
13 | | ltpnf 9665 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℝ → 𝑥 < +∞) |
14 | 12, 13 | syl 14 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℚ → 𝑥 < +∞) |
15 | 14 | adantl 275 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 = +∞) ∧ 𝑥 ∈ ℚ) → 𝑥 < +∞) |
16 | | simplr 520 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 = +∞) ∧ 𝑥 ∈ ℚ) → 𝐵 = +∞) |
17 | 15, 16 | breqtrrd 3988 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 = +∞) ∧ 𝑥 ∈ ℚ) → 𝑥 < 𝐵) |
18 | 17 | a1d 22 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 = +∞) ∧ 𝑥 ∈ ℚ) → (𝑥 < (𝐴 + 1) → 𝑥 < 𝐵)) |
19 | 18 | anim2d 335 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 = +∞) ∧ 𝑥 ∈ ℚ) → ((𝐴 < 𝑥 ∧ 𝑥 < (𝐴 + 1)) → (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))) |
20 | 19 | reximdva 2556 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) →
(∃𝑥 ∈ ℚ
(𝐴 < 𝑥 ∧ 𝑥 < (𝐴 + 1)) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))) |
21 | 11, 20 | mpd 13 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)) |
22 | 21 | a1d 22 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))) |
23 | | rexr 7902 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℝ*) |
24 | | breq2 3965 |
. . . . . . . . 9
⊢ (𝐵 = -∞ → (𝐴 < 𝐵 ↔ 𝐴 < -∞)) |
25 | 24 | adantl 275 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 = -∞) →
(𝐴 < 𝐵 ↔ 𝐴 < -∞)) |
26 | | nltmnf 9673 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ*
→ ¬ 𝐴 <
-∞) |
27 | 26 | adantr 274 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 = -∞) →
¬ 𝐴 <
-∞) |
28 | 27 | pm2.21d 609 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 = -∞) →
(𝐴 < -∞ →
∃𝑥 ∈ ℚ
(𝐴 < 𝑥 ∧ 𝑥 < 𝐵))) |
29 | 25, 28 | sylbid 149 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 = -∞) →
(𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))) |
30 | 23, 29 | sylan 281 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))) |
31 | 4, 22, 30 | 3jaodan 1285 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞)) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))) |
32 | 2, 31 | sylan2b 285 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*)
→ (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))) |
33 | | breq1 3964 |
. . . . . 6
⊢ (𝐴 = +∞ → (𝐴 < 𝐵 ↔ +∞ < 𝐵)) |
34 | 33 | adantr 274 |
. . . . 5
⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*)
→ (𝐴 < 𝐵 ↔ +∞ < 𝐵)) |
35 | | pnfnlt 9672 |
. . . . . . 7
⊢ (𝐵 ∈ ℝ*
→ ¬ +∞ < 𝐵) |
36 | 35 | adantl 275 |
. . . . . 6
⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*)
→ ¬ +∞ < 𝐵) |
37 | 36 | pm2.21d 609 |
. . . . 5
⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*)
→ (+∞ < 𝐵
→ ∃𝑥 ∈
ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))) |
38 | 34, 37 | sylbid 149 |
. . . 4
⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*)
→ (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))) |
39 | | peano2rem 8121 |
. . . . . . . . . 10
⊢ (𝐵 ∈ ℝ → (𝐵 − 1) ∈
ℝ) |
40 | 39 | adantl 275 |
. . . . . . . . 9
⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → (𝐵 − 1) ∈
ℝ) |
41 | | simpr 109 |
. . . . . . . . 9
⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → 𝐵 ∈
ℝ) |
42 | | ltm1 8696 |
. . . . . . . . . 10
⊢ (𝐵 ∈ ℝ → (𝐵 − 1) < 𝐵) |
43 | 42 | adantl 275 |
. . . . . . . . 9
⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → (𝐵 − 1) < 𝐵) |
44 | | qbtwnre 10134 |
. . . . . . . . 9
⊢ (((𝐵 − 1) ∈ ℝ ∧
𝐵 ∈ ℝ ∧
(𝐵 − 1) < 𝐵) → ∃𝑥 ∈ ℚ ((𝐵 − 1) < 𝑥 ∧ 𝑥 < 𝐵)) |
45 | 40, 41, 43, 44 | syl3anc 1217 |
. . . . . . . 8
⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) →
∃𝑥 ∈ ℚ
((𝐵 − 1) < 𝑥 ∧ 𝑥 < 𝐵)) |
46 | | simpll 519 |
. . . . . . . . . . . 12
⊢ (((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℚ) → 𝐴 = -∞) |
47 | 12 | adantl 275 |
. . . . . . . . . . . . 13
⊢ (((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℚ) → 𝑥 ∈
ℝ) |
48 | | mnflt 9668 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ → -∞
< 𝑥) |
49 | 47, 48 | syl 14 |
. . . . . . . . . . . 12
⊢ (((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℚ) → -∞
< 𝑥) |
50 | 46, 49 | eqbrtrd 3982 |
. . . . . . . . . . 11
⊢ (((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℚ) → 𝐴 < 𝑥) |
51 | 50 | a1d 22 |
. . . . . . . . . 10
⊢ (((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℚ) → ((𝐵 − 1) < 𝑥 → 𝐴 < 𝑥)) |
52 | 51 | anim1d 334 |
. . . . . . . . 9
⊢ (((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℚ) → (((𝐵 − 1) < 𝑥 ∧ 𝑥 < 𝐵) → (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))) |
53 | 52 | reximdva 2556 |
. . . . . . . 8
⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) →
(∃𝑥 ∈ ℚ
((𝐵 − 1) < 𝑥 ∧ 𝑥 < 𝐵) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))) |
54 | 45, 53 | mpd 13 |
. . . . . . 7
⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) →
∃𝑥 ∈ ℚ
(𝐴 < 𝑥 ∧ 𝑥 < 𝐵)) |
55 | 54 | a1d 22 |
. . . . . 6
⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))) |
56 | | 1re 7856 |
. . . . . . . . . 10
⊢ 1 ∈
ℝ |
57 | | mnflt 9668 |
. . . . . . . . . 10
⊢ (1 ∈
ℝ → -∞ < 1) |
58 | 56, 57 | ax-mp 5 |
. . . . . . . . 9
⊢ -∞
< 1 |
59 | | breq1 3964 |
. . . . . . . . 9
⊢ (𝐴 = -∞ → (𝐴 < 1 ↔ -∞ <
1)) |
60 | 58, 59 | mpbiri 167 |
. . . . . . . 8
⊢ (𝐴 = -∞ → 𝐴 < 1) |
61 | | ltpnf 9665 |
. . . . . . . . . 10
⊢ (1 ∈
ℝ → 1 < +∞) |
62 | 56, 61 | ax-mp 5 |
. . . . . . . . 9
⊢ 1 <
+∞ |
63 | | breq2 3965 |
. . . . . . . . 9
⊢ (𝐵 = +∞ → (1 < 𝐵 ↔ 1 <
+∞)) |
64 | 62, 63 | mpbiri 167 |
. . . . . . . 8
⊢ (𝐵 = +∞ → 1 < 𝐵) |
65 | | 1z 9172 |
. . . . . . . . . 10
⊢ 1 ∈
ℤ |
66 | | zq 9513 |
. . . . . . . . . 10
⊢ (1 ∈
ℤ → 1 ∈ ℚ) |
67 | 65, 66 | ax-mp 5 |
. . . . . . . . 9
⊢ 1 ∈
ℚ |
68 | | breq2 3965 |
. . . . . . . . . . 11
⊢ (𝑥 = 1 → (𝐴 < 𝑥 ↔ 𝐴 < 1)) |
69 | | breq1 3964 |
. . . . . . . . . . 11
⊢ (𝑥 = 1 → (𝑥 < 𝐵 ↔ 1 < 𝐵)) |
70 | 68, 69 | anbi12d 465 |
. . . . . . . . . 10
⊢ (𝑥 = 1 → ((𝐴 < 𝑥 ∧ 𝑥 < 𝐵) ↔ (𝐴 < 1 ∧ 1 < 𝐵))) |
71 | 70 | rspcev 2813 |
. . . . . . . . 9
⊢ ((1
∈ ℚ ∧ (𝐴
< 1 ∧ 1 < 𝐵))
→ ∃𝑥 ∈
ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)) |
72 | 67, 71 | mpan 421 |
. . . . . . . 8
⊢ ((𝐴 < 1 ∧ 1 < 𝐵) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)) |
73 | 60, 64, 72 | syl2an 287 |
. . . . . . 7
⊢ ((𝐴 = -∞ ∧ 𝐵 = +∞) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)) |
74 | 73 | a1d 22 |
. . . . . 6
⊢ ((𝐴 = -∞ ∧ 𝐵 = +∞) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))) |
75 | | 3mix3 1153 |
. . . . . . . 8
⊢ (𝐴 = -∞ → (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞)) |
76 | 75, 1 | sylibr 133 |
. . . . . . 7
⊢ (𝐴 = -∞ → 𝐴 ∈
ℝ*) |
77 | 76, 29 | sylan 281 |
. . . . . 6
⊢ ((𝐴 = -∞ ∧ 𝐵 = -∞) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))) |
78 | 55, 74, 77 | 3jaodan 1285 |
. . . . 5
⊢ ((𝐴 = -∞ ∧ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞)) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))) |
79 | 2, 78 | sylan2b 285 |
. . . 4
⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*)
→ (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))) |
80 | 32, 38, 79 | 3jaoian 1284 |
. . 3
⊢ (((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ∧ 𝐵 ∈ ℝ*)
→ (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))) |
81 | 1, 80 | sylanb 282 |
. 2
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))) |
82 | 81 | 3impia 1179 |
1
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)) |