Step | Hyp | Ref
| Expression |
1 | | simpllr 486 |
. . . . . . . 8
⊢
(((((𝐾 ∈
ℕ ∧ 𝐴 ∈
ℚ) ∧ 𝑚 ∈
ℤ) ∧ (𝑚 ≤
𝐴 ∧ 𝐴 < (𝑚 + (𝐾 + 1)))) ∧ (𝑚 + 𝐾) ≤ 𝐴) → 𝑚 ∈ ℤ) |
2 | | simpll 481 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ ℕ ∧ 𝐴 ∈ ℚ) ∧ 𝑚 ∈ ℤ) → 𝐾 ∈
ℕ) |
3 | 2 | ad2antrr 457 |
. . . . . . . . 9
⊢
(((((𝐾 ∈
ℕ ∧ 𝐴 ∈
ℚ) ∧ 𝑚 ∈
ℤ) ∧ (𝑚 ≤
𝐴 ∧ 𝐴 < (𝑚 + (𝐾 + 1)))) ∧ (𝑚 + 𝐾) ≤ 𝐴) → 𝐾 ∈ ℕ) |
4 | 3 | nnzd 8359 |
. . . . . . . 8
⊢
(((((𝐾 ∈
ℕ ∧ 𝐴 ∈
ℚ) ∧ 𝑚 ∈
ℤ) ∧ (𝑚 ≤
𝐴 ∧ 𝐴 < (𝑚 + (𝐾 + 1)))) ∧ (𝑚 + 𝐾) ≤ 𝐴) → 𝐾 ∈ ℤ) |
5 | 1, 4 | zaddcld 8364 |
. . . . . . 7
⊢
(((((𝐾 ∈
ℕ ∧ 𝐴 ∈
ℚ) ∧ 𝑚 ∈
ℤ) ∧ (𝑚 ≤
𝐴 ∧ 𝐴 < (𝑚 + (𝐾 + 1)))) ∧ (𝑚 + 𝐾) ≤ 𝐴) → (𝑚 + 𝐾) ∈ ℤ) |
6 | | simpr 103 |
. . . . . . 7
⊢
(((((𝐾 ∈
ℕ ∧ 𝐴 ∈
ℚ) ∧ 𝑚 ∈
ℤ) ∧ (𝑚 ≤
𝐴 ∧ 𝐴 < (𝑚 + (𝐾 + 1)))) ∧ (𝑚 + 𝐾) ≤ 𝐴) → (𝑚 + 𝐾) ≤ 𝐴) |
7 | | qre 8560 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℚ → 𝐴 ∈
ℝ) |
8 | 7 | ad4antlr 464 |
. . . . . . . 8
⊢
(((((𝐾 ∈
ℕ ∧ 𝐴 ∈
ℚ) ∧ 𝑚 ∈
ℤ) ∧ (𝑚 ≤
𝐴 ∧ 𝐴 < (𝑚 + (𝐾 + 1)))) ∧ (𝑚 + 𝐾) ≤ 𝐴) → 𝐴 ∈ ℝ) |
9 | 5 | zred 8360 |
. . . . . . . . 9
⊢
(((((𝐾 ∈
ℕ ∧ 𝐴 ∈
ℚ) ∧ 𝑚 ∈
ℤ) ∧ (𝑚 ≤
𝐴 ∧ 𝐴 < (𝑚 + (𝐾 + 1)))) ∧ (𝑚 + 𝐾) ≤ 𝐴) → (𝑚 + 𝐾) ∈ ℝ) |
10 | | 1red 7042 |
. . . . . . . . 9
⊢
(((((𝐾 ∈
ℕ ∧ 𝐴 ∈
ℚ) ∧ 𝑚 ∈
ℤ) ∧ (𝑚 ≤
𝐴 ∧ 𝐴 < (𝑚 + (𝐾 + 1)))) ∧ (𝑚 + 𝐾) ≤ 𝐴) → 1 ∈ ℝ) |
11 | 9, 10 | readdcld 7055 |
. . . . . . . 8
⊢
(((((𝐾 ∈
ℕ ∧ 𝐴 ∈
ℚ) ∧ 𝑚 ∈
ℤ) ∧ (𝑚 ≤
𝐴 ∧ 𝐴 < (𝑚 + (𝐾 + 1)))) ∧ (𝑚 + 𝐾) ≤ 𝐴) → ((𝑚 + 𝐾) + 1) ∈ ℝ) |
12 | 3 | nnred 7927 |
. . . . . . . . 9
⊢
(((((𝐾 ∈
ℕ ∧ 𝐴 ∈
ℚ) ∧ 𝑚 ∈
ℤ) ∧ (𝑚 ≤
𝐴 ∧ 𝐴 < (𝑚 + (𝐾 + 1)))) ∧ (𝑚 + 𝐾) ≤ 𝐴) → 𝐾 ∈ ℝ) |
13 | 9, 12 | readdcld 7055 |
. . . . . . . 8
⊢
(((((𝐾 ∈
ℕ ∧ 𝐴 ∈
ℚ) ∧ 𝑚 ∈
ℤ) ∧ (𝑚 ≤
𝐴 ∧ 𝐴 < (𝑚 + (𝐾 + 1)))) ∧ (𝑚 + 𝐾) ≤ 𝐴) → ((𝑚 + 𝐾) + 𝐾) ∈ ℝ) |
14 | | simplrr 488 |
. . . . . . . . 9
⊢
(((((𝐾 ∈
ℕ ∧ 𝐴 ∈
ℚ) ∧ 𝑚 ∈
ℤ) ∧ (𝑚 ≤
𝐴 ∧ 𝐴 < (𝑚 + (𝐾 + 1)))) ∧ (𝑚 + 𝐾) ≤ 𝐴) → 𝐴 < (𝑚 + (𝐾 + 1))) |
15 | 1 | zcnd 8361 |
. . . . . . . . . 10
⊢
(((((𝐾 ∈
ℕ ∧ 𝐴 ∈
ℚ) ∧ 𝑚 ∈
ℤ) ∧ (𝑚 ≤
𝐴 ∧ 𝐴 < (𝑚 + (𝐾 + 1)))) ∧ (𝑚 + 𝐾) ≤ 𝐴) → 𝑚 ∈ ℂ) |
16 | 3 | nncnd 7928 |
. . . . . . . . . 10
⊢
(((((𝐾 ∈
ℕ ∧ 𝐴 ∈
ℚ) ∧ 𝑚 ∈
ℤ) ∧ (𝑚 ≤
𝐴 ∧ 𝐴 < (𝑚 + (𝐾 + 1)))) ∧ (𝑚 + 𝐾) ≤ 𝐴) → 𝐾 ∈ ℂ) |
17 | | 1cnd 7043 |
. . . . . . . . . 10
⊢
(((((𝐾 ∈
ℕ ∧ 𝐴 ∈
ℚ) ∧ 𝑚 ∈
ℤ) ∧ (𝑚 ≤
𝐴 ∧ 𝐴 < (𝑚 + (𝐾 + 1)))) ∧ (𝑚 + 𝐾) ≤ 𝐴) → 1 ∈ ℂ) |
18 | 15, 16, 17 | addassd 7049 |
. . . . . . . . 9
⊢
(((((𝐾 ∈
ℕ ∧ 𝐴 ∈
ℚ) ∧ 𝑚 ∈
ℤ) ∧ (𝑚 ≤
𝐴 ∧ 𝐴 < (𝑚 + (𝐾 + 1)))) ∧ (𝑚 + 𝐾) ≤ 𝐴) → ((𝑚 + 𝐾) + 1) = (𝑚 + (𝐾 + 1))) |
19 | 14, 18 | breqtrrd 3790 |
. . . . . . . 8
⊢
(((((𝐾 ∈
ℕ ∧ 𝐴 ∈
ℚ) ∧ 𝑚 ∈
ℤ) ∧ (𝑚 ≤
𝐴 ∧ 𝐴 < (𝑚 + (𝐾 + 1)))) ∧ (𝑚 + 𝐾) ≤ 𝐴) → 𝐴 < ((𝑚 + 𝐾) + 1)) |
20 | 3 | nnge1d 7956 |
. . . . . . . . 9
⊢
(((((𝐾 ∈
ℕ ∧ 𝐴 ∈
ℚ) ∧ 𝑚 ∈
ℤ) ∧ (𝑚 ≤
𝐴 ∧ 𝐴 < (𝑚 + (𝐾 + 1)))) ∧ (𝑚 + 𝐾) ≤ 𝐴) → 1 ≤ 𝐾) |
21 | 10, 12, 9, 20 | leadd2dd 7551 |
. . . . . . . 8
⊢
(((((𝐾 ∈
ℕ ∧ 𝐴 ∈
ℚ) ∧ 𝑚 ∈
ℤ) ∧ (𝑚 ≤
𝐴 ∧ 𝐴 < (𝑚 + (𝐾 + 1)))) ∧ (𝑚 + 𝐾) ≤ 𝐴) → ((𝑚 + 𝐾) + 1) ≤ ((𝑚 + 𝐾) + 𝐾)) |
22 | 8, 11, 13, 19, 21 | ltletrd 7420 |
. . . . . . 7
⊢
(((((𝐾 ∈
ℕ ∧ 𝐴 ∈
ℚ) ∧ 𝑚 ∈
ℤ) ∧ (𝑚 ≤
𝐴 ∧ 𝐴 < (𝑚 + (𝐾 + 1)))) ∧ (𝑚 + 𝐾) ≤ 𝐴) → 𝐴 < ((𝑚 + 𝐾) + 𝐾)) |
23 | | breq1 3767 |
. . . . . . . . 9
⊢ (𝑗 = (𝑚 + 𝐾) → (𝑗 ≤ 𝐴 ↔ (𝑚 + 𝐾) ≤ 𝐴)) |
24 | | oveq1 5519 |
. . . . . . . . . 10
⊢ (𝑗 = (𝑚 + 𝐾) → (𝑗 + 𝐾) = ((𝑚 + 𝐾) + 𝐾)) |
25 | 24 | breq2d 3776 |
. . . . . . . . 9
⊢ (𝑗 = (𝑚 + 𝐾) → (𝐴 < (𝑗 + 𝐾) ↔ 𝐴 < ((𝑚 + 𝐾) + 𝐾))) |
26 | 23, 25 | anbi12d 442 |
. . . . . . . 8
⊢ (𝑗 = (𝑚 + 𝐾) → ((𝑗 ≤ 𝐴 ∧ 𝐴 < (𝑗 + 𝐾)) ↔ ((𝑚 + 𝐾) ≤ 𝐴 ∧ 𝐴 < ((𝑚 + 𝐾) + 𝐾)))) |
27 | 26 | rspcev 2656 |
. . . . . . 7
⊢ (((𝑚 + 𝐾) ∈ ℤ ∧ ((𝑚 + 𝐾) ≤ 𝐴 ∧ 𝐴 < ((𝑚 + 𝐾) + 𝐾))) → ∃𝑗 ∈ ℤ (𝑗 ≤ 𝐴 ∧ 𝐴 < (𝑗 + 𝐾))) |
28 | 5, 6, 22, 27 | syl12anc 1133 |
. . . . . 6
⊢
(((((𝐾 ∈
ℕ ∧ 𝐴 ∈
ℚ) ∧ 𝑚 ∈
ℤ) ∧ (𝑚 ≤
𝐴 ∧ 𝐴 < (𝑚 + (𝐾 + 1)))) ∧ (𝑚 + 𝐾) ≤ 𝐴) → ∃𝑗 ∈ ℤ (𝑗 ≤ 𝐴 ∧ 𝐴 < (𝑗 + 𝐾))) |
29 | | simpllr 486 |
. . . . . . 7
⊢
(((((𝐾 ∈
ℕ ∧ 𝐴 ∈
ℚ) ∧ 𝑚 ∈
ℤ) ∧ (𝑚 ≤
𝐴 ∧ 𝐴 < (𝑚 + (𝐾 + 1)))) ∧ 𝐴 < (𝑚 + 𝐾)) → 𝑚 ∈ ℤ) |
30 | | simplrl 487 |
. . . . . . 7
⊢
(((((𝐾 ∈
ℕ ∧ 𝐴 ∈
ℚ) ∧ 𝑚 ∈
ℤ) ∧ (𝑚 ≤
𝐴 ∧ 𝐴 < (𝑚 + (𝐾 + 1)))) ∧ 𝐴 < (𝑚 + 𝐾)) → 𝑚 ≤ 𝐴) |
31 | | simpr 103 |
. . . . . . 7
⊢
(((((𝐾 ∈
ℕ ∧ 𝐴 ∈
ℚ) ∧ 𝑚 ∈
ℤ) ∧ (𝑚 ≤
𝐴 ∧ 𝐴 < (𝑚 + (𝐾 + 1)))) ∧ 𝐴 < (𝑚 + 𝐾)) → 𝐴 < (𝑚 + 𝐾)) |
32 | | breq1 3767 |
. . . . . . . . 9
⊢ (𝑗 = 𝑚 → (𝑗 ≤ 𝐴 ↔ 𝑚 ≤ 𝐴)) |
33 | | oveq1 5519 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑚 → (𝑗 + 𝐾) = (𝑚 + 𝐾)) |
34 | 33 | breq2d 3776 |
. . . . . . . . 9
⊢ (𝑗 = 𝑚 → (𝐴 < (𝑗 + 𝐾) ↔ 𝐴 < (𝑚 + 𝐾))) |
35 | 32, 34 | anbi12d 442 |
. . . . . . . 8
⊢ (𝑗 = 𝑚 → ((𝑗 ≤ 𝐴 ∧ 𝐴 < (𝑗 + 𝐾)) ↔ (𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + 𝐾)))) |
36 | 35 | rspcev 2656 |
. . . . . . 7
⊢ ((𝑚 ∈ ℤ ∧ (𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + 𝐾))) → ∃𝑗 ∈ ℤ (𝑗 ≤ 𝐴 ∧ 𝐴 < (𝑗 + 𝐾))) |
37 | 29, 30, 31, 36 | syl12anc 1133 |
. . . . . 6
⊢
(((((𝐾 ∈
ℕ ∧ 𝐴 ∈
ℚ) ∧ 𝑚 ∈
ℤ) ∧ (𝑚 ≤
𝐴 ∧ 𝐴 < (𝑚 + (𝐾 + 1)))) ∧ 𝐴 < (𝑚 + 𝐾)) → ∃𝑗 ∈ ℤ (𝑗 ≤ 𝐴 ∧ 𝐴 < (𝑗 + 𝐾))) |
38 | | zq 8561 |
. . . . . . . . 9
⊢ (𝑚 ∈ ℤ → 𝑚 ∈
ℚ) |
39 | 38 | ad2antlr 458 |
. . . . . . . 8
⊢ ((((𝐾 ∈ ℕ ∧ 𝐴 ∈ ℚ) ∧ 𝑚 ∈ ℤ) ∧ (𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + (𝐾 + 1)))) → 𝑚 ∈ ℚ) |
40 | | nnq 8568 |
. . . . . . . . 9
⊢ (𝐾 ∈ ℕ → 𝐾 ∈
ℚ) |
41 | 40 | ad3antrrr 461 |
. . . . . . . 8
⊢ ((((𝐾 ∈ ℕ ∧ 𝐴 ∈ ℚ) ∧ 𝑚 ∈ ℤ) ∧ (𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + (𝐾 + 1)))) → 𝐾 ∈ ℚ) |
42 | | qaddcl 8570 |
. . . . . . . 8
⊢ ((𝑚 ∈ ℚ ∧ 𝐾 ∈ ℚ) → (𝑚 + 𝐾) ∈ ℚ) |
43 | 39, 41, 42 | syl2anc 391 |
. . . . . . 7
⊢ ((((𝐾 ∈ ℕ ∧ 𝐴 ∈ ℚ) ∧ 𝑚 ∈ ℤ) ∧ (𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + (𝐾 + 1)))) → (𝑚 + 𝐾) ∈ ℚ) |
44 | | simpllr 486 |
. . . . . . 7
⊢ ((((𝐾 ∈ ℕ ∧ 𝐴 ∈ ℚ) ∧ 𝑚 ∈ ℤ) ∧ (𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + (𝐾 + 1)))) → 𝐴 ∈ ℚ) |
45 | | qlelttric 9100 |
. . . . . . 7
⊢ (((𝑚 + 𝐾) ∈ ℚ ∧ 𝐴 ∈ ℚ) → ((𝑚 + 𝐾) ≤ 𝐴 ∨ 𝐴 < (𝑚 + 𝐾))) |
46 | 43, 44, 45 | syl2anc 391 |
. . . . . 6
⊢ ((((𝐾 ∈ ℕ ∧ 𝐴 ∈ ℚ) ∧ 𝑚 ∈ ℤ) ∧ (𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + (𝐾 + 1)))) → ((𝑚 + 𝐾) ≤ 𝐴 ∨ 𝐴 < (𝑚 + 𝐾))) |
47 | 28, 37, 46 | mpjaodan 711 |
. . . . 5
⊢ ((((𝐾 ∈ ℕ ∧ 𝐴 ∈ ℚ) ∧ 𝑚 ∈ ℤ) ∧ (𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + (𝐾 + 1)))) → ∃𝑗 ∈ ℤ (𝑗 ≤ 𝐴 ∧ 𝐴 < (𝑗 + 𝐾))) |
48 | 47 | ex 108 |
. . . 4
⊢ (((𝐾 ∈ ℕ ∧ 𝐴 ∈ ℚ) ∧ 𝑚 ∈ ℤ) → ((𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + (𝐾 + 1))) → ∃𝑗 ∈ ℤ (𝑗 ≤ 𝐴 ∧ 𝐴 < (𝑗 + 𝐾)))) |
49 | 48 | rexlimdva 2433 |
. . 3
⊢ ((𝐾 ∈ ℕ ∧ 𝐴 ∈ ℚ) →
(∃𝑚 ∈ ℤ
(𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + (𝐾 + 1))) → ∃𝑗 ∈ ℤ (𝑗 ≤ 𝐴 ∧ 𝐴 < (𝑗 + 𝐾)))) |
50 | 49 | 3impia 1101 |
. 2
⊢ ((𝐾 ∈ ℕ ∧ 𝐴 ∈ ℚ ∧
∃𝑚 ∈ ℤ
(𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + (𝐾 + 1)))) → ∃𝑗 ∈ ℤ (𝑗 ≤ 𝐴 ∧ 𝐴 < (𝑗 + 𝐾))) |
51 | | breq1 3767 |
. . . 4
⊢ (𝑚 = 𝑗 → (𝑚 ≤ 𝐴 ↔ 𝑗 ≤ 𝐴)) |
52 | | oveq1 5519 |
. . . . 5
⊢ (𝑚 = 𝑗 → (𝑚 + 𝐾) = (𝑗 + 𝐾)) |
53 | 52 | breq2d 3776 |
. . . 4
⊢ (𝑚 = 𝑗 → (𝐴 < (𝑚 + 𝐾) ↔ 𝐴 < (𝑗 + 𝐾))) |
54 | 51, 53 | anbi12d 442 |
. . 3
⊢ (𝑚 = 𝑗 → ((𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + 𝐾)) ↔ (𝑗 ≤ 𝐴 ∧ 𝐴 < (𝑗 + 𝐾)))) |
55 | 54 | cbvrexv 2534 |
. 2
⊢
(∃𝑚 ∈
ℤ (𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + 𝐾)) ↔ ∃𝑗 ∈ ℤ (𝑗 ≤ 𝐴 ∧ 𝐴 < (𝑗 + 𝐾))) |
56 | 50, 55 | sylibr 137 |
1
⊢ ((𝐾 ∈ ℕ ∧ 𝐴 ∈ ℚ ∧
∃𝑚 ∈ ℤ
(𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + (𝐾 + 1)))) → ∃𝑚 ∈ ℤ (𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + 𝐾))) |