Step | Hyp | Ref
| Expression |
1 | | qre 8710 |
. . . 4
⊢ (𝐴 ∈ ℚ → 𝐴 ∈
ℝ) |
2 | | btwnz 8466 |
. . . 4
⊢ (𝐴 ∈ ℝ →
(∃𝑚 ∈ ℤ
𝑚 < 𝐴 ∧ ∃𝑛 ∈ ℤ 𝐴 < 𝑛)) |
3 | 1, 2 | syl 14 |
. . 3
⊢ (𝐴 ∈ ℚ →
(∃𝑚 ∈ ℤ
𝑚 < 𝐴 ∧ ∃𝑛 ∈ ℤ 𝐴 < 𝑛)) |
4 | | reeanv 2523 |
. . 3
⊢
(∃𝑚 ∈
ℤ ∃𝑛 ∈
ℤ (𝑚 < 𝐴 ∧ 𝐴 < 𝑛) ↔ (∃𝑚 ∈ ℤ 𝑚 < 𝐴 ∧ ∃𝑛 ∈ ℤ 𝐴 < 𝑛)) |
5 | 3, 4 | sylibr 132 |
. 2
⊢ (𝐴 ∈ ℚ →
∃𝑚 ∈ ℤ
∃𝑛 ∈ ℤ
(𝑚 < 𝐴 ∧ 𝐴 < 𝑛)) |
6 | | simpll 495 |
. . . . 5
⊢ (((𝐴 ∈ ℚ ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑚 < 𝐴 ∧ 𝐴 < 𝑛)) → 𝐴 ∈ ℚ) |
7 | | simplrl 501 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℚ ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑚 < 𝐴 ∧ 𝐴 < 𝑛)) → 𝑚 ∈ ℤ) |
8 | 7 | zred 8469 |
. . . . . . 7
⊢ (((𝐴 ∈ ℚ ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑚 < 𝐴 ∧ 𝐴 < 𝑛)) → 𝑚 ∈ ℝ) |
9 | 1 | ad2antrr 471 |
. . . . . . 7
⊢ (((𝐴 ∈ ℚ ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑚 < 𝐴 ∧ 𝐴 < 𝑛)) → 𝐴 ∈ ℝ) |
10 | | simplrr 502 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℚ ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑚 < 𝐴 ∧ 𝐴 < 𝑛)) → 𝑛 ∈ ℤ) |
11 | 10 | zred 8469 |
. . . . . . 7
⊢ (((𝐴 ∈ ℚ ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑚 < 𝐴 ∧ 𝐴 < 𝑛)) → 𝑛 ∈ ℝ) |
12 | | simprl 497 |
. . . . . . 7
⊢ (((𝐴 ∈ ℚ ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑚 < 𝐴 ∧ 𝐴 < 𝑛)) → 𝑚 < 𝐴) |
13 | | simprr 498 |
. . . . . . 7
⊢ (((𝐴 ∈ ℚ ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑚 < 𝐴 ∧ 𝐴 < 𝑛)) → 𝐴 < 𝑛) |
14 | 8, 9, 11, 12, 13 | lttrd 7235 |
. . . . . 6
⊢ (((𝐴 ∈ ℚ ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑚 < 𝐴 ∧ 𝐴 < 𝑛)) → 𝑚 < 𝑛) |
15 | | znnsub 8402 |
. . . . . . 7
⊢ ((𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑚 < 𝑛 ↔ (𝑛 − 𝑚) ∈ ℕ)) |
16 | 15 | ad2antlr 472 |
. . . . . 6
⊢ (((𝐴 ∈ ℚ ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑚 < 𝐴 ∧ 𝐴 < 𝑛)) → (𝑚 < 𝑛 ↔ (𝑛 − 𝑚) ∈ ℕ)) |
17 | 14, 16 | mpbid 145 |
. . . . 5
⊢ (((𝐴 ∈ ℚ ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑚 < 𝐴 ∧ 𝐴 < 𝑛)) → (𝑛 − 𝑚) ∈ ℕ) |
18 | 8, 9, 12 | ltled 7228 |
. . . . . 6
⊢ (((𝐴 ∈ ℚ ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑚 < 𝐴 ∧ 𝐴 < 𝑛)) → 𝑚 ≤ 𝐴) |
19 | 7 | zcnd 8470 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℚ ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑚 < 𝐴 ∧ 𝐴 < 𝑛)) → 𝑚 ∈ ℂ) |
20 | 10 | zcnd 8470 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℚ ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑚 < 𝐴 ∧ 𝐴 < 𝑛)) → 𝑛 ∈ ℂ) |
21 | 19, 20 | pncan3d 7422 |
. . . . . . 7
⊢ (((𝐴 ∈ ℚ ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑚 < 𝐴 ∧ 𝐴 < 𝑛)) → (𝑚 + (𝑛 − 𝑚)) = 𝑛) |
22 | 13, 21 | breqtrrd 3811 |
. . . . . 6
⊢ (((𝐴 ∈ ℚ ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑚 < 𝐴 ∧ 𝐴 < 𝑛)) → 𝐴 < (𝑚 + (𝑛 − 𝑚))) |
23 | | breq1 3788 |
. . . . . . . 8
⊢ (𝑦 = 𝑚 → (𝑦 ≤ 𝐴 ↔ 𝑚 ≤ 𝐴)) |
24 | | oveq1 5539 |
. . . . . . . . 9
⊢ (𝑦 = 𝑚 → (𝑦 + (𝑛 − 𝑚)) = (𝑚 + (𝑛 − 𝑚))) |
25 | 24 | breq2d 3797 |
. . . . . . . 8
⊢ (𝑦 = 𝑚 → (𝐴 < (𝑦 + (𝑛 − 𝑚)) ↔ 𝐴 < (𝑚 + (𝑛 − 𝑚)))) |
26 | 23, 25 | anbi12d 456 |
. . . . . . 7
⊢ (𝑦 = 𝑚 → ((𝑦 ≤ 𝐴 ∧ 𝐴 < (𝑦 + (𝑛 − 𝑚))) ↔ (𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + (𝑛 − 𝑚))))) |
27 | 26 | rspcev 2701 |
. . . . . 6
⊢ ((𝑚 ∈ ℤ ∧ (𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + (𝑛 − 𝑚)))) → ∃𝑦 ∈ ℤ (𝑦 ≤ 𝐴 ∧ 𝐴 < (𝑦 + (𝑛 − 𝑚)))) |
28 | 7, 18, 22, 27 | syl12anc 1167 |
. . . . 5
⊢ (((𝐴 ∈ ℚ ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑚 < 𝐴 ∧ 𝐴 < 𝑛)) → ∃𝑦 ∈ ℤ (𝑦 ≤ 𝐴 ∧ 𝐴 < (𝑦 + (𝑛 − 𝑚)))) |
29 | | qbtwnzlemshrink 9258 |
. . . . 5
⊢ ((𝐴 ∈ ℚ ∧ (𝑛 − 𝑚) ∈ ℕ ∧ ∃𝑦 ∈ ℤ (𝑦 ≤ 𝐴 ∧ 𝐴 < (𝑦 + (𝑛 − 𝑚)))) → ∃𝑥 ∈ ℤ (𝑥 ≤ 𝐴 ∧ 𝐴 < (𝑥 + 1))) |
30 | 6, 17, 28, 29 | syl3anc 1169 |
. . . 4
⊢ (((𝐴 ∈ ℚ ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑚 < 𝐴 ∧ 𝐴 < 𝑛)) → ∃𝑥 ∈ ℤ (𝑥 ≤ 𝐴 ∧ 𝐴 < (𝑥 + 1))) |
31 | 30 | ex 113 |
. . 3
⊢ ((𝐴 ∈ ℚ ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) → ((𝑚 < 𝐴 ∧ 𝐴 < 𝑛) → ∃𝑥 ∈ ℤ (𝑥 ≤ 𝐴 ∧ 𝐴 < (𝑥 + 1)))) |
32 | 31 | rexlimdvva 2484 |
. 2
⊢ (𝐴 ∈ ℚ →
(∃𝑚 ∈ ℤ
∃𝑛 ∈ ℤ
(𝑚 < 𝐴 ∧ 𝐴 < 𝑛) → ∃𝑥 ∈ ℤ (𝑥 ≤ 𝐴 ∧ 𝐴 < (𝑥 + 1)))) |
33 | 5, 32 | mpd 13 |
1
⊢ (𝐴 ∈ ℚ →
∃𝑥 ∈ ℤ
(𝑥 ≤ 𝐴 ∧ 𝐴 < (𝑥 + 1))) |