Step | Hyp | Ref
| Expression |
1 | | simp2 993 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐽 ∈
(ℤ≥‘2) ∧ ∃𝑚 ∈ ℤ (𝑚 < 𝐴 ∧ 𝐴 < (𝑚 + 𝐽))) → 𝐽 ∈
(ℤ≥‘2)) |
2 | | 3simpb 990 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐽 ∈
(ℤ≥‘2) ∧ ∃𝑚 ∈ ℤ (𝑚 < 𝐴 ∧ 𝐴 < (𝑚 + 𝐽))) → (𝐴 ∈ ℝ ∧ ∃𝑚 ∈ ℤ (𝑚 < 𝐴 ∧ 𝐴 < (𝑚 + 𝐽)))) |
3 | | oveq2 5858 |
. . . . . . . 8
⊢ (𝑤 = 2 → (𝑚 + 𝑤) = (𝑚 + 2)) |
4 | 3 | breq2d 3999 |
. . . . . . 7
⊢ (𝑤 = 2 → (𝐴 < (𝑚 + 𝑤) ↔ 𝐴 < (𝑚 + 2))) |
5 | 4 | anbi2d 461 |
. . . . . 6
⊢ (𝑤 = 2 → ((𝑚 < 𝐴 ∧ 𝐴 < (𝑚 + 𝑤)) ↔ (𝑚 < 𝐴 ∧ 𝐴 < (𝑚 + 2)))) |
6 | 5 | rexbidv 2471 |
. . . . 5
⊢ (𝑤 = 2 → (∃𝑚 ∈ ℤ (𝑚 < 𝐴 ∧ 𝐴 < (𝑚 + 𝑤)) ↔ ∃𝑚 ∈ ℤ (𝑚 < 𝐴 ∧ 𝐴 < (𝑚 + 2)))) |
7 | 6 | anbi2d 461 |
. . . 4
⊢ (𝑤 = 2 → ((𝐴 ∈ ℝ ∧ ∃𝑚 ∈ ℤ (𝑚 < 𝐴 ∧ 𝐴 < (𝑚 + 𝑤))) ↔ (𝐴 ∈ ℝ ∧ ∃𝑚 ∈ ℤ (𝑚 < 𝐴 ∧ 𝐴 < (𝑚 + 2))))) |
8 | 7 | imbi1d 230 |
. . 3
⊢ (𝑤 = 2 → (((𝐴 ∈ ℝ ∧ ∃𝑚 ∈ ℤ (𝑚 < 𝐴 ∧ 𝐴 < (𝑚 + 𝑤))) → ∃𝑥 ∈ ℤ (𝑥 < 𝐴 ∧ 𝐴 < (𝑥 + 2))) ↔ ((𝐴 ∈ ℝ ∧ ∃𝑚 ∈ ℤ (𝑚 < 𝐴 ∧ 𝐴 < (𝑚 + 2))) → ∃𝑥 ∈ ℤ (𝑥 < 𝐴 ∧ 𝐴 < (𝑥 + 2))))) |
9 | | oveq2 5858 |
. . . . . . . 8
⊢ (𝑤 = 𝑘 → (𝑚 + 𝑤) = (𝑚 + 𝑘)) |
10 | 9 | breq2d 3999 |
. . . . . . 7
⊢ (𝑤 = 𝑘 → (𝐴 < (𝑚 + 𝑤) ↔ 𝐴 < (𝑚 + 𝑘))) |
11 | 10 | anbi2d 461 |
. . . . . 6
⊢ (𝑤 = 𝑘 → ((𝑚 < 𝐴 ∧ 𝐴 < (𝑚 + 𝑤)) ↔ (𝑚 < 𝐴 ∧ 𝐴 < (𝑚 + 𝑘)))) |
12 | 11 | rexbidv 2471 |
. . . . 5
⊢ (𝑤 = 𝑘 → (∃𝑚 ∈ ℤ (𝑚 < 𝐴 ∧ 𝐴 < (𝑚 + 𝑤)) ↔ ∃𝑚 ∈ ℤ (𝑚 < 𝐴 ∧ 𝐴 < (𝑚 + 𝑘)))) |
13 | 12 | anbi2d 461 |
. . . 4
⊢ (𝑤 = 𝑘 → ((𝐴 ∈ ℝ ∧ ∃𝑚 ∈ ℤ (𝑚 < 𝐴 ∧ 𝐴 < (𝑚 + 𝑤))) ↔ (𝐴 ∈ ℝ ∧ ∃𝑚 ∈ ℤ (𝑚 < 𝐴 ∧ 𝐴 < (𝑚 + 𝑘))))) |
14 | 13 | imbi1d 230 |
. . 3
⊢ (𝑤 = 𝑘 → (((𝐴 ∈ ℝ ∧ ∃𝑚 ∈ ℤ (𝑚 < 𝐴 ∧ 𝐴 < (𝑚 + 𝑤))) → ∃𝑥 ∈ ℤ (𝑥 < 𝐴 ∧ 𝐴 < (𝑥 + 2))) ↔ ((𝐴 ∈ ℝ ∧ ∃𝑚 ∈ ℤ (𝑚 < 𝐴 ∧ 𝐴 < (𝑚 + 𝑘))) → ∃𝑥 ∈ ℤ (𝑥 < 𝐴 ∧ 𝐴 < (𝑥 + 2))))) |
15 | | oveq2 5858 |
. . . . . . . 8
⊢ (𝑤 = (𝑘 + 1) → (𝑚 + 𝑤) = (𝑚 + (𝑘 + 1))) |
16 | 15 | breq2d 3999 |
. . . . . . 7
⊢ (𝑤 = (𝑘 + 1) → (𝐴 < (𝑚 + 𝑤) ↔ 𝐴 < (𝑚 + (𝑘 + 1)))) |
17 | 16 | anbi2d 461 |
. . . . . 6
⊢ (𝑤 = (𝑘 + 1) → ((𝑚 < 𝐴 ∧ 𝐴 < (𝑚 + 𝑤)) ↔ (𝑚 < 𝐴 ∧ 𝐴 < (𝑚 + (𝑘 + 1))))) |
18 | 17 | rexbidv 2471 |
. . . . 5
⊢ (𝑤 = (𝑘 + 1) → (∃𝑚 ∈ ℤ (𝑚 < 𝐴 ∧ 𝐴 < (𝑚 + 𝑤)) ↔ ∃𝑚 ∈ ℤ (𝑚 < 𝐴 ∧ 𝐴 < (𝑚 + (𝑘 + 1))))) |
19 | 18 | anbi2d 461 |
. . . 4
⊢ (𝑤 = (𝑘 + 1) → ((𝐴 ∈ ℝ ∧ ∃𝑚 ∈ ℤ (𝑚 < 𝐴 ∧ 𝐴 < (𝑚 + 𝑤))) ↔ (𝐴 ∈ ℝ ∧ ∃𝑚 ∈ ℤ (𝑚 < 𝐴 ∧ 𝐴 < (𝑚 + (𝑘 + 1)))))) |
20 | 19 | imbi1d 230 |
. . 3
⊢ (𝑤 = (𝑘 + 1) → (((𝐴 ∈ ℝ ∧ ∃𝑚 ∈ ℤ (𝑚 < 𝐴 ∧ 𝐴 < (𝑚 + 𝑤))) → ∃𝑥 ∈ ℤ (𝑥 < 𝐴 ∧ 𝐴 < (𝑥 + 2))) ↔ ((𝐴 ∈ ℝ ∧ ∃𝑚 ∈ ℤ (𝑚 < 𝐴 ∧ 𝐴 < (𝑚 + (𝑘 + 1)))) → ∃𝑥 ∈ ℤ (𝑥 < 𝐴 ∧ 𝐴 < (𝑥 + 2))))) |
21 | | oveq2 5858 |
. . . . . . . 8
⊢ (𝑤 = 𝐽 → (𝑚 + 𝑤) = (𝑚 + 𝐽)) |
22 | 21 | breq2d 3999 |
. . . . . . 7
⊢ (𝑤 = 𝐽 → (𝐴 < (𝑚 + 𝑤) ↔ 𝐴 < (𝑚 + 𝐽))) |
23 | 22 | anbi2d 461 |
. . . . . 6
⊢ (𝑤 = 𝐽 → ((𝑚 < 𝐴 ∧ 𝐴 < (𝑚 + 𝑤)) ↔ (𝑚 < 𝐴 ∧ 𝐴 < (𝑚 + 𝐽)))) |
24 | 23 | rexbidv 2471 |
. . . . 5
⊢ (𝑤 = 𝐽 → (∃𝑚 ∈ ℤ (𝑚 < 𝐴 ∧ 𝐴 < (𝑚 + 𝑤)) ↔ ∃𝑚 ∈ ℤ (𝑚 < 𝐴 ∧ 𝐴 < (𝑚 + 𝐽)))) |
25 | 24 | anbi2d 461 |
. . . 4
⊢ (𝑤 = 𝐽 → ((𝐴 ∈ ℝ ∧ ∃𝑚 ∈ ℤ (𝑚 < 𝐴 ∧ 𝐴 < (𝑚 + 𝑤))) ↔ (𝐴 ∈ ℝ ∧ ∃𝑚 ∈ ℤ (𝑚 < 𝐴 ∧ 𝐴 < (𝑚 + 𝐽))))) |
26 | 25 | imbi1d 230 |
. . 3
⊢ (𝑤 = 𝐽 → (((𝐴 ∈ ℝ ∧ ∃𝑚 ∈ ℤ (𝑚 < 𝐴 ∧ 𝐴 < (𝑚 + 𝑤))) → ∃𝑥 ∈ ℤ (𝑥 < 𝐴 ∧ 𝐴 < (𝑥 + 2))) ↔ ((𝐴 ∈ ℝ ∧ ∃𝑚 ∈ ℤ (𝑚 < 𝐴 ∧ 𝐴 < (𝑚 + 𝐽))) → ∃𝑥 ∈ ℤ (𝑥 < 𝐴 ∧ 𝐴 < (𝑥 + 2))))) |
27 | | breq1 3990 |
. . . . . . 7
⊢ (𝑚 = 𝑥 → (𝑚 < 𝐴 ↔ 𝑥 < 𝐴)) |
28 | | oveq1 5857 |
. . . . . . . 8
⊢ (𝑚 = 𝑥 → (𝑚 + 2) = (𝑥 + 2)) |
29 | 28 | breq2d 3999 |
. . . . . . 7
⊢ (𝑚 = 𝑥 → (𝐴 < (𝑚 + 2) ↔ 𝐴 < (𝑥 + 2))) |
30 | 27, 29 | anbi12d 470 |
. . . . . 6
⊢ (𝑚 = 𝑥 → ((𝑚 < 𝐴 ∧ 𝐴 < (𝑚 + 2)) ↔ (𝑥 < 𝐴 ∧ 𝐴 < (𝑥 + 2)))) |
31 | 30 | cbvrexv 2697 |
. . . . 5
⊢
(∃𝑚 ∈
ℤ (𝑚 < 𝐴 ∧ 𝐴 < (𝑚 + 2)) ↔ ∃𝑥 ∈ ℤ (𝑥 < 𝐴 ∧ 𝐴 < (𝑥 + 2))) |
32 | 31 | biimpi 119 |
. . . 4
⊢
(∃𝑚 ∈
ℤ (𝑚 < 𝐴 ∧ 𝐴 < (𝑚 + 2)) → ∃𝑥 ∈ ℤ (𝑥 < 𝐴 ∧ 𝐴 < (𝑥 + 2))) |
33 | 32 | adantl 275 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧
∃𝑚 ∈ ℤ
(𝑚 < 𝐴 ∧ 𝐴 < (𝑚 + 2))) → ∃𝑥 ∈ ℤ (𝑥 < 𝐴 ∧ 𝐴 < (𝑥 + 2))) |
34 | | rebtwn2zlemstep 10196 |
. . . . . 6
⊢ ((𝑘 ∈
(ℤ≥‘2) ∧ 𝐴 ∈ ℝ ∧ ∃𝑚 ∈ ℤ (𝑚 < 𝐴 ∧ 𝐴 < (𝑚 + (𝑘 + 1)))) → ∃𝑚 ∈ ℤ (𝑚 < 𝐴 ∧ 𝐴 < (𝑚 + 𝑘))) |
35 | 34 | 3expia 1200 |
. . . . 5
⊢ ((𝑘 ∈
(ℤ≥‘2) ∧ 𝐴 ∈ ℝ) → (∃𝑚 ∈ ℤ (𝑚 < 𝐴 ∧ 𝐴 < (𝑚 + (𝑘 + 1))) → ∃𝑚 ∈ ℤ (𝑚 < 𝐴 ∧ 𝐴 < (𝑚 + 𝑘)))) |
36 | 35 | imdistanda 446 |
. . . 4
⊢ (𝑘 ∈
(ℤ≥‘2) → ((𝐴 ∈ ℝ ∧ ∃𝑚 ∈ ℤ (𝑚 < 𝐴 ∧ 𝐴 < (𝑚 + (𝑘 + 1)))) → (𝐴 ∈ ℝ ∧ ∃𝑚 ∈ ℤ (𝑚 < 𝐴 ∧ 𝐴 < (𝑚 + 𝑘))))) |
37 | 36 | imim1d 75 |
. . 3
⊢ (𝑘 ∈
(ℤ≥‘2) → (((𝐴 ∈ ℝ ∧ ∃𝑚 ∈ ℤ (𝑚 < 𝐴 ∧ 𝐴 < (𝑚 + 𝑘))) → ∃𝑥 ∈ ℤ (𝑥 < 𝐴 ∧ 𝐴 < (𝑥 + 2))) → ((𝐴 ∈ ℝ ∧ ∃𝑚 ∈ ℤ (𝑚 < 𝐴 ∧ 𝐴 < (𝑚 + (𝑘 + 1)))) → ∃𝑥 ∈ ℤ (𝑥 < 𝐴 ∧ 𝐴 < (𝑥 + 2))))) |
38 | 8, 14, 20, 26, 33, 37 | uzind4i 9538 |
. 2
⊢ (𝐽 ∈
(ℤ≥‘2) → ((𝐴 ∈ ℝ ∧ ∃𝑚 ∈ ℤ (𝑚 < 𝐴 ∧ 𝐴 < (𝑚 + 𝐽))) → ∃𝑥 ∈ ℤ (𝑥 < 𝐴 ∧ 𝐴 < (𝑥 + 2)))) |
39 | 1, 2, 38 | sylc 62 |
1
⊢ ((𝐴 ∈ ℝ ∧ 𝐽 ∈
(ℤ≥‘2) ∧ ∃𝑚 ∈ ℤ (𝑚 < 𝐴 ∧ 𝐴 < (𝑚 + 𝐽))) → ∃𝑥 ∈ ℤ (𝑥 < 𝐴 ∧ 𝐴 < (𝑥 + 2))) |