Step | Hyp | Ref
| Expression |
1 | | simp2 905 |
. 2
⊢ ((𝐴 ∈ ℚ ∧ 𝐽 ∈ ℕ ∧
∃𝑚 ∈ ℤ
(𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + 𝐽))) → 𝐽 ∈ ℕ) |
2 | | 3simpb 902 |
. 2
⊢ ((𝐴 ∈ ℚ ∧ 𝐽 ∈ ℕ ∧
∃𝑚 ∈ ℤ
(𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + 𝐽))) → (𝐴 ∈ ℚ ∧ ∃𝑚 ∈ ℤ (𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + 𝐽)))) |
3 | | oveq2 5520 |
. . . . . . . 8
⊢ (𝑤 = 1 → (𝑚 + 𝑤) = (𝑚 + 1)) |
4 | 3 | breq2d 3776 |
. . . . . . 7
⊢ (𝑤 = 1 → (𝐴 < (𝑚 + 𝑤) ↔ 𝐴 < (𝑚 + 1))) |
5 | 4 | anbi2d 437 |
. . . . . 6
⊢ (𝑤 = 1 → ((𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + 𝑤)) ↔ (𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + 1)))) |
6 | 5 | rexbidv 2327 |
. . . . 5
⊢ (𝑤 = 1 → (∃𝑚 ∈ ℤ (𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + 𝑤)) ↔ ∃𝑚 ∈ ℤ (𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + 1)))) |
7 | 6 | anbi2d 437 |
. . . 4
⊢ (𝑤 = 1 → ((𝐴 ∈ ℚ ∧ ∃𝑚 ∈ ℤ (𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + 𝑤))) ↔ (𝐴 ∈ ℚ ∧ ∃𝑚 ∈ ℤ (𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + 1))))) |
8 | 7 | imbi1d 220 |
. . 3
⊢ (𝑤 = 1 → (((𝐴 ∈ ℚ ∧ ∃𝑚 ∈ ℤ (𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + 𝑤))) → ∃𝑥 ∈ ℤ (𝑥 ≤ 𝐴 ∧ 𝐴 < (𝑥 + 1))) ↔ ((𝐴 ∈ ℚ ∧ ∃𝑚 ∈ ℤ (𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + 1))) → ∃𝑥 ∈ ℤ (𝑥 ≤ 𝐴 ∧ 𝐴 < (𝑥 + 1))))) |
9 | | oveq2 5520 |
. . . . . . . 8
⊢ (𝑤 = 𝑘 → (𝑚 + 𝑤) = (𝑚 + 𝑘)) |
10 | 9 | breq2d 3776 |
. . . . . . 7
⊢ (𝑤 = 𝑘 → (𝐴 < (𝑚 + 𝑤) ↔ 𝐴 < (𝑚 + 𝑘))) |
11 | 10 | anbi2d 437 |
. . . . . 6
⊢ (𝑤 = 𝑘 → ((𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + 𝑤)) ↔ (𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + 𝑘)))) |
12 | 11 | rexbidv 2327 |
. . . . 5
⊢ (𝑤 = 𝑘 → (∃𝑚 ∈ ℤ (𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + 𝑤)) ↔ ∃𝑚 ∈ ℤ (𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + 𝑘)))) |
13 | 12 | anbi2d 437 |
. . . 4
⊢ (𝑤 = 𝑘 → ((𝐴 ∈ ℚ ∧ ∃𝑚 ∈ ℤ (𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + 𝑤))) ↔ (𝐴 ∈ ℚ ∧ ∃𝑚 ∈ ℤ (𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + 𝑘))))) |
14 | 13 | imbi1d 220 |
. . 3
⊢ (𝑤 = 𝑘 → (((𝐴 ∈ ℚ ∧ ∃𝑚 ∈ ℤ (𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + 𝑤))) → ∃𝑥 ∈ ℤ (𝑥 ≤ 𝐴 ∧ 𝐴 < (𝑥 + 1))) ↔ ((𝐴 ∈ ℚ ∧ ∃𝑚 ∈ ℤ (𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + 𝑘))) → ∃𝑥 ∈ ℤ (𝑥 ≤ 𝐴 ∧ 𝐴 < (𝑥 + 1))))) |
15 | | oveq2 5520 |
. . . . . . . 8
⊢ (𝑤 = (𝑘 + 1) → (𝑚 + 𝑤) = (𝑚 + (𝑘 + 1))) |
16 | 15 | breq2d 3776 |
. . . . . . 7
⊢ (𝑤 = (𝑘 + 1) → (𝐴 < (𝑚 + 𝑤) ↔ 𝐴 < (𝑚 + (𝑘 + 1)))) |
17 | 16 | anbi2d 437 |
. . . . . 6
⊢ (𝑤 = (𝑘 + 1) → ((𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + 𝑤)) ↔ (𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + (𝑘 + 1))))) |
18 | 17 | rexbidv 2327 |
. . . . 5
⊢ (𝑤 = (𝑘 + 1) → (∃𝑚 ∈ ℤ (𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + 𝑤)) ↔ ∃𝑚 ∈ ℤ (𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + (𝑘 + 1))))) |
19 | 18 | anbi2d 437 |
. . . 4
⊢ (𝑤 = (𝑘 + 1) → ((𝐴 ∈ ℚ ∧ ∃𝑚 ∈ ℤ (𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + 𝑤))) ↔ (𝐴 ∈ ℚ ∧ ∃𝑚 ∈ ℤ (𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + (𝑘 + 1)))))) |
20 | 19 | imbi1d 220 |
. . 3
⊢ (𝑤 = (𝑘 + 1) → (((𝐴 ∈ ℚ ∧ ∃𝑚 ∈ ℤ (𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + 𝑤))) → ∃𝑥 ∈ ℤ (𝑥 ≤ 𝐴 ∧ 𝐴 < (𝑥 + 1))) ↔ ((𝐴 ∈ ℚ ∧ ∃𝑚 ∈ ℤ (𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + (𝑘 + 1)))) → ∃𝑥 ∈ ℤ (𝑥 ≤ 𝐴 ∧ 𝐴 < (𝑥 + 1))))) |
21 | | oveq2 5520 |
. . . . . . . 8
⊢ (𝑤 = 𝐽 → (𝑚 + 𝑤) = (𝑚 + 𝐽)) |
22 | 21 | breq2d 3776 |
. . . . . . 7
⊢ (𝑤 = 𝐽 → (𝐴 < (𝑚 + 𝑤) ↔ 𝐴 < (𝑚 + 𝐽))) |
23 | 22 | anbi2d 437 |
. . . . . 6
⊢ (𝑤 = 𝐽 → ((𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + 𝑤)) ↔ (𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + 𝐽)))) |
24 | 23 | rexbidv 2327 |
. . . . 5
⊢ (𝑤 = 𝐽 → (∃𝑚 ∈ ℤ (𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + 𝑤)) ↔ ∃𝑚 ∈ ℤ (𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + 𝐽)))) |
25 | 24 | anbi2d 437 |
. . . 4
⊢ (𝑤 = 𝐽 → ((𝐴 ∈ ℚ ∧ ∃𝑚 ∈ ℤ (𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + 𝑤))) ↔ (𝐴 ∈ ℚ ∧ ∃𝑚 ∈ ℤ (𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + 𝐽))))) |
26 | 25 | imbi1d 220 |
. . 3
⊢ (𝑤 = 𝐽 → (((𝐴 ∈ ℚ ∧ ∃𝑚 ∈ ℤ (𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + 𝑤))) → ∃𝑥 ∈ ℤ (𝑥 ≤ 𝐴 ∧ 𝐴 < (𝑥 + 1))) ↔ ((𝐴 ∈ ℚ ∧ ∃𝑚 ∈ ℤ (𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + 𝐽))) → ∃𝑥 ∈ ℤ (𝑥 ≤ 𝐴 ∧ 𝐴 < (𝑥 + 1))))) |
27 | | breq1 3767 |
. . . . . . 7
⊢ (𝑚 = 𝑥 → (𝑚 ≤ 𝐴 ↔ 𝑥 ≤ 𝐴)) |
28 | | oveq1 5519 |
. . . . . . . 8
⊢ (𝑚 = 𝑥 → (𝑚 + 1) = (𝑥 + 1)) |
29 | 28 | breq2d 3776 |
. . . . . . 7
⊢ (𝑚 = 𝑥 → (𝐴 < (𝑚 + 1) ↔ 𝐴 < (𝑥 + 1))) |
30 | 27, 29 | anbi12d 442 |
. . . . . 6
⊢ (𝑚 = 𝑥 → ((𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + 1)) ↔ (𝑥 ≤ 𝐴 ∧ 𝐴 < (𝑥 + 1)))) |
31 | 30 | cbvrexv 2534 |
. . . . 5
⊢
(∃𝑚 ∈
ℤ (𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + 1)) ↔ ∃𝑥 ∈ ℤ (𝑥 ≤ 𝐴 ∧ 𝐴 < (𝑥 + 1))) |
32 | 31 | biimpi 113 |
. . . 4
⊢
(∃𝑚 ∈
ℤ (𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + 1)) → ∃𝑥 ∈ ℤ (𝑥 ≤ 𝐴 ∧ 𝐴 < (𝑥 + 1))) |
33 | 32 | adantl 262 |
. . 3
⊢ ((𝐴 ∈ ℚ ∧
∃𝑚 ∈ ℤ
(𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + 1))) → ∃𝑥 ∈ ℤ (𝑥 ≤ 𝐴 ∧ 𝐴 < (𝑥 + 1))) |
34 | | qbtwnzlemstep 9103 |
. . . . . 6
⊢ ((𝑘 ∈ ℕ ∧ 𝐴 ∈ ℚ ∧
∃𝑚 ∈ ℤ
(𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + (𝑘 + 1)))) → ∃𝑚 ∈ ℤ (𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + 𝑘))) |
35 | 34 | 3expia 1106 |
. . . . 5
⊢ ((𝑘 ∈ ℕ ∧ 𝐴 ∈ ℚ) →
(∃𝑚 ∈ ℤ
(𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + (𝑘 + 1))) → ∃𝑚 ∈ ℤ (𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + 𝑘)))) |
36 | 35 | imdistanda 422 |
. . . 4
⊢ (𝑘 ∈ ℕ → ((𝐴 ∈ ℚ ∧
∃𝑚 ∈ ℤ
(𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + (𝑘 + 1)))) → (𝐴 ∈ ℚ ∧ ∃𝑚 ∈ ℤ (𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + 𝑘))))) |
37 | 36 | imim1d 69 |
. . 3
⊢ (𝑘 ∈ ℕ → (((𝐴 ∈ ℚ ∧
∃𝑚 ∈ ℤ
(𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + 𝑘))) → ∃𝑥 ∈ ℤ (𝑥 ≤ 𝐴 ∧ 𝐴 < (𝑥 + 1))) → ((𝐴 ∈ ℚ ∧ ∃𝑚 ∈ ℤ (𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + (𝑘 + 1)))) → ∃𝑥 ∈ ℤ (𝑥 ≤ 𝐴 ∧ 𝐴 < (𝑥 + 1))))) |
38 | 8, 14, 20, 26, 33, 37 | nnind 7930 |
. 2
⊢ (𝐽 ∈ ℕ → ((𝐴 ∈ ℚ ∧
∃𝑚 ∈ ℤ
(𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + 𝐽))) → ∃𝑥 ∈ ℤ (𝑥 ≤ 𝐴 ∧ 𝐴 < (𝑥 + 1)))) |
39 | 1, 2, 38 | sylc 56 |
1
⊢ ((𝐴 ∈ ℚ ∧ 𝐽 ∈ ℕ ∧
∃𝑚 ∈ ℤ
(𝑚 ≤ 𝐴 ∧ 𝐴 < (𝑚 + 𝐽))) → ∃𝑥 ∈ ℤ (𝑥 ≤ 𝐴 ∧ 𝐴 < (𝑥 + 1))) |