Step | Hyp | Ref
| Expression |
1 | | btwnz 9331 |
. . 3
⊢ (𝐴 ∈ ℝ →
(∃𝑚 ∈ ℤ
𝑚 < 𝐴 ∧ ∃𝑛 ∈ ℤ 𝐴 < 𝑛)) |
2 | | reeanv 2639 |
. . 3
⊢
(∃𝑚 ∈
ℤ ∃𝑛 ∈
ℤ (𝑚 < 𝐴 ∧ 𝐴 < 𝑛) ↔ (∃𝑚 ∈ ℤ 𝑚 < 𝐴 ∧ ∃𝑛 ∈ ℤ 𝐴 < 𝑛)) |
3 | 1, 2 | sylibr 133 |
. 2
⊢ (𝐴 ∈ ℝ →
∃𝑚 ∈ ℤ
∃𝑛 ∈ ℤ
(𝑚 < 𝐴 ∧ 𝐴 < 𝑛)) |
4 | | simpll 524 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑚 < 𝐴 ∧ 𝐴 < 𝑛)) → 𝐴 ∈ ℝ) |
5 | | simplrl 530 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑚 < 𝐴 ∧ 𝐴 < 𝑛)) → 𝑚 ∈ ℤ) |
6 | 5 | zred 9334 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑚 < 𝐴 ∧ 𝐴 < 𝑛)) → 𝑚 ∈ ℝ) |
7 | | simplrr 531 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑚 < 𝐴 ∧ 𝐴 < 𝑛)) → 𝑛 ∈ ℤ) |
8 | 7 | zred 9334 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑚 < 𝐴 ∧ 𝐴 < 𝑛)) → 𝑛 ∈ ℝ) |
9 | | simprl 526 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑚 < 𝐴 ∧ 𝐴 < 𝑛)) → 𝑚 < 𝐴) |
10 | | simprr 527 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑚 < 𝐴 ∧ 𝐴 < 𝑛)) → 𝐴 < 𝑛) |
11 | 6, 4, 8, 9, 10 | lttrd 8045 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑚 < 𝐴 ∧ 𝐴 < 𝑛)) → 𝑚 < 𝑛) |
12 | | znnsub 9263 |
. . . . . . . 8
⊢ ((𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑚 < 𝑛 ↔ (𝑛 − 𝑚) ∈ ℕ)) |
13 | 12 | ad2antlr 486 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑚 < 𝐴 ∧ 𝐴 < 𝑛)) → (𝑚 < 𝑛 ↔ (𝑛 − 𝑚) ∈ ℕ)) |
14 | 11, 13 | mpbid 146 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑚 < 𝐴 ∧ 𝐴 < 𝑛)) → (𝑛 − 𝑚) ∈ ℕ) |
15 | | elnnuz 9523 |
. . . . . . . 8
⊢ ((𝑛 − 𝑚) ∈ ℕ ↔ (𝑛 − 𝑚) ∈
(ℤ≥‘1)) |
16 | | eluzp1p1 9512 |
. . . . . . . 8
⊢ ((𝑛 − 𝑚) ∈ (ℤ≥‘1)
→ ((𝑛 − 𝑚) + 1) ∈
(ℤ≥‘(1 + 1))) |
17 | 15, 16 | sylbi 120 |
. . . . . . 7
⊢ ((𝑛 − 𝑚) ∈ ℕ → ((𝑛 − 𝑚) + 1) ∈
(ℤ≥‘(1 + 1))) |
18 | | df-2 8937 |
. . . . . . . 8
⊢ 2 = (1 +
1) |
19 | 18 | fveq2i 5499 |
. . . . . . 7
⊢
(ℤ≥‘2) = (ℤ≥‘(1 +
1)) |
20 | 17, 19 | eleqtrrdi 2264 |
. . . . . 6
⊢ ((𝑛 − 𝑚) ∈ ℕ → ((𝑛 − 𝑚) + 1) ∈
(ℤ≥‘2)) |
21 | 14, 20 | syl 14 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑚 < 𝐴 ∧ 𝐴 < 𝑛)) → ((𝑛 − 𝑚) + 1) ∈
(ℤ≥‘2)) |
22 | 5 | zcnd 9335 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑚 < 𝐴 ∧ 𝐴 < 𝑛)) → 𝑚 ∈ ℂ) |
23 | 7 | zcnd 9335 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑚 < 𝐴 ∧ 𝐴 < 𝑛)) → 𝑛 ∈ ℂ) |
24 | 22, 23 | pncan3d 8233 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑚 < 𝐴 ∧ 𝐴 < 𝑛)) → (𝑚 + (𝑛 − 𝑚)) = 𝑛) |
25 | 24, 8 | eqeltrd 2247 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑚 < 𝐴 ∧ 𝐴 < 𝑛)) → (𝑚 + (𝑛 − 𝑚)) ∈ ℝ) |
26 | 8, 6 | resubcld 8300 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑚 < 𝐴 ∧ 𝐴 < 𝑛)) → (𝑛 − 𝑚) ∈ ℝ) |
27 | | 1red 7935 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑚 < 𝐴 ∧ 𝐴 < 𝑛)) → 1 ∈ ℝ) |
28 | 26, 27 | readdcld 7949 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑚 < 𝐴 ∧ 𝐴 < 𝑛)) → ((𝑛 − 𝑚) + 1) ∈ ℝ) |
29 | 6, 28 | readdcld 7949 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑚 < 𝐴 ∧ 𝐴 < 𝑛)) → (𝑚 + ((𝑛 − 𝑚) + 1)) ∈ ℝ) |
30 | 10, 24 | breqtrrd 4017 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑚 < 𝐴 ∧ 𝐴 < 𝑛)) → 𝐴 < (𝑚 + (𝑛 − 𝑚))) |
31 | 26 | ltp1d 8846 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑚 < 𝐴 ∧ 𝐴 < 𝑛)) → (𝑛 − 𝑚) < ((𝑛 − 𝑚) + 1)) |
32 | 26, 28, 6, 31 | ltadd2dd 8341 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑚 < 𝐴 ∧ 𝐴 < 𝑛)) → (𝑚 + (𝑛 − 𝑚)) < (𝑚 + ((𝑛 − 𝑚) + 1))) |
33 | 4, 25, 29, 30, 32 | lttrd 8045 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑚 < 𝐴 ∧ 𝐴 < 𝑛)) → 𝐴 < (𝑚 + ((𝑛 − 𝑚) + 1))) |
34 | | breq1 3992 |
. . . . . . . 8
⊢ (𝑦 = 𝑚 → (𝑦 < 𝐴 ↔ 𝑚 < 𝐴)) |
35 | | oveq1 5860 |
. . . . . . . . 9
⊢ (𝑦 = 𝑚 → (𝑦 + ((𝑛 − 𝑚) + 1)) = (𝑚 + ((𝑛 − 𝑚) + 1))) |
36 | 35 | breq2d 4001 |
. . . . . . . 8
⊢ (𝑦 = 𝑚 → (𝐴 < (𝑦 + ((𝑛 − 𝑚) + 1)) ↔ 𝐴 < (𝑚 + ((𝑛 − 𝑚) + 1)))) |
37 | 34, 36 | anbi12d 470 |
. . . . . . 7
⊢ (𝑦 = 𝑚 → ((𝑦 < 𝐴 ∧ 𝐴 < (𝑦 + ((𝑛 − 𝑚) + 1))) ↔ (𝑚 < 𝐴 ∧ 𝐴 < (𝑚 + ((𝑛 − 𝑚) + 1))))) |
38 | 37 | rspcev 2834 |
. . . . . 6
⊢ ((𝑚 ∈ ℤ ∧ (𝑚 < 𝐴 ∧ 𝐴 < (𝑚 + ((𝑛 − 𝑚) + 1)))) → ∃𝑦 ∈ ℤ (𝑦 < 𝐴 ∧ 𝐴 < (𝑦 + ((𝑛 − 𝑚) + 1)))) |
39 | 5, 9, 33, 38 | syl12anc 1231 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑚 < 𝐴 ∧ 𝐴 < 𝑛)) → ∃𝑦 ∈ ℤ (𝑦 < 𝐴 ∧ 𝐴 < (𝑦 + ((𝑛 − 𝑚) + 1)))) |
40 | | rebtwn2zlemshrink 10210 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ ((𝑛 − 𝑚) + 1) ∈
(ℤ≥‘2) ∧ ∃𝑦 ∈ ℤ (𝑦 < 𝐴 ∧ 𝐴 < (𝑦 + ((𝑛 − 𝑚) + 1)))) → ∃𝑥 ∈ ℤ (𝑥 < 𝐴 ∧ 𝐴 < (𝑥 + 2))) |
41 | 4, 21, 39, 40 | syl3anc 1233 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ (𝑚 < 𝐴 ∧ 𝐴 < 𝑛)) → ∃𝑥 ∈ ℤ (𝑥 < 𝐴 ∧ 𝐴 < (𝑥 + 2))) |
42 | 41 | ex 114 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) → ((𝑚 < 𝐴 ∧ 𝐴 < 𝑛) → ∃𝑥 ∈ ℤ (𝑥 < 𝐴 ∧ 𝐴 < (𝑥 + 2)))) |
43 | 42 | rexlimdvva 2595 |
. 2
⊢ (𝐴 ∈ ℝ →
(∃𝑚 ∈ ℤ
∃𝑛 ∈ ℤ
(𝑚 < 𝐴 ∧ 𝐴 < 𝑛) → ∃𝑥 ∈ ℤ (𝑥 < 𝐴 ∧ 𝐴 < (𝑥 + 2)))) |
44 | 3, 43 | mpd 13 |
1
⊢ (𝐴 ∈ ℝ →
∃𝑥 ∈ ℤ
(𝑥 < 𝐴 ∧ 𝐴 < (𝑥 + 2))) |