Step | Hyp | Ref
| Expression |
1 | | eluzelre 12581 |
. . . . . 6
⊢ (𝑗 ∈
(ℤ≥‘𝑀) → 𝑗 ∈ ℝ) |
2 | | rexuz3.1 |
. . . . . 6
⊢ 𝑍 =
(ℤ≥‘𝑀) |
3 | 1, 2 | eleq2s 2857 |
. . . . 5
⊢ (𝑗 ∈ 𝑍 → 𝑗 ∈ ℝ) |
4 | 3 | adantr 481 |
. . . 4
⊢ ((𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑) → 𝑗 ∈ ℝ) |
5 | | eluzelz 12580 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈
(ℤ≥‘𝑀) → 𝑗 ∈ ℤ) |
6 | 5, 2 | eleq2s 2857 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ 𝑍 → 𝑗 ∈ ℤ) |
7 | | eluzelz 12580 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈
(ℤ≥‘𝑀) → 𝑘 ∈ ℤ) |
8 | 7, 2 | eleq2s 2857 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ 𝑍 → 𝑘 ∈ ℤ) |
9 | | eluz 12584 |
. . . . . . . . . . 11
⊢ ((𝑗 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑘 ∈
(ℤ≥‘𝑗) ↔ 𝑗 ≤ 𝑘)) |
10 | 6, 8, 9 | syl2an 596 |
. . . . . . . . . 10
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍) → (𝑘 ∈ (ℤ≥‘𝑗) ↔ 𝑗 ≤ 𝑘)) |
11 | 10 | biimprd 247 |
. . . . . . . . 9
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍) → (𝑗 ≤ 𝑘 → 𝑘 ∈ (ℤ≥‘𝑗))) |
12 | 11 | expimpd 454 |
. . . . . . . 8
⊢ (𝑗 ∈ 𝑍 → ((𝑘 ∈ 𝑍 ∧ 𝑗 ≤ 𝑘) → 𝑘 ∈ (ℤ≥‘𝑗))) |
13 | 12 | imim1d 82 |
. . . . . . 7
⊢ (𝑗 ∈ 𝑍 → ((𝑘 ∈ (ℤ≥‘𝑗) → 𝜑) → ((𝑘 ∈ 𝑍 ∧ 𝑗 ≤ 𝑘) → 𝜑))) |
14 | 13 | exp4a 432 |
. . . . . 6
⊢ (𝑗 ∈ 𝑍 → ((𝑘 ∈ (ℤ≥‘𝑗) → 𝜑) → (𝑘 ∈ 𝑍 → (𝑗 ≤ 𝑘 → 𝜑)))) |
15 | 14 | ralimdv2 3102 |
. . . . 5
⊢ (𝑗 ∈ 𝑍 → (∀𝑘 ∈ (ℤ≥‘𝑗)𝜑 → ∀𝑘 ∈ 𝑍 (𝑗 ≤ 𝑘 → 𝜑))) |
16 | 15 | imp 407 |
. . . 4
⊢ ((𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑) → ∀𝑘 ∈ 𝑍 (𝑗 ≤ 𝑘 → 𝜑)) |
17 | 4, 16 | jca 512 |
. . 3
⊢ ((𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑) → (𝑗 ∈ ℝ ∧ ∀𝑘 ∈ 𝑍 (𝑗 ≤ 𝑘 → 𝜑))) |
18 | 17 | reximi2 3173 |
. 2
⊢
(∃𝑗 ∈
𝑍 ∀𝑘 ∈
(ℤ≥‘𝑗)𝜑 → ∃𝑗 ∈ ℝ ∀𝑘 ∈ 𝑍 (𝑗 ≤ 𝑘 → 𝜑)) |
19 | | simpl 483 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ) → 𝑀 ∈
ℤ) |
20 | | flcl 13503 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ℝ →
(⌊‘𝑗) ∈
ℤ) |
21 | 20 | adantl 482 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ) →
(⌊‘𝑗) ∈
ℤ) |
22 | 21 | peano2zd 12417 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ) →
((⌊‘𝑗) + 1)
∈ ℤ) |
23 | 22, 19 | ifcld 4506 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ) → if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀) ∈ ℤ) |
24 | | zre 12311 |
. . . . . . . 8
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℝ) |
25 | | reflcl 13504 |
. . . . . . . . 9
⊢ (𝑗 ∈ ℝ →
(⌊‘𝑗) ∈
ℝ) |
26 | | peano2re 11136 |
. . . . . . . . 9
⊢
((⌊‘𝑗)
∈ ℝ → ((⌊‘𝑗) + 1) ∈ ℝ) |
27 | 25, 26 | syl 17 |
. . . . . . . 8
⊢ (𝑗 ∈ ℝ →
((⌊‘𝑗) + 1)
∈ ℝ) |
28 | | max1 12907 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℝ ∧
((⌊‘𝑗) + 1)
∈ ℝ) → 𝑀
≤ if(𝑀 ≤
((⌊‘𝑗) + 1),
((⌊‘𝑗) + 1),
𝑀)) |
29 | 24, 27, 28 | syl2an 596 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ) → 𝑀 ≤ if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀)) |
30 | | eluz2 12576 |
. . . . . . 7
⊢ (if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀) ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀) ∈ ℤ ∧ 𝑀 ≤ if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀))) |
31 | 19, 23, 29, 30 | syl3anbrc 1342 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ) → if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀) ∈ (ℤ≥‘𝑀)) |
32 | 31, 2 | eleqtrrdi 2850 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ) → if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀) ∈ 𝑍) |
33 | | impexp 451 |
. . . . . . 7
⊢ (((𝑘 ∈ 𝑍 ∧ 𝑗 ≤ 𝑘) → 𝜑) ↔ (𝑘 ∈ 𝑍 → (𝑗 ≤ 𝑘 → 𝜑))) |
34 | | uzss 12593 |
. . . . . . . . . . . . 13
⊢ (if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀) ∈ (ℤ≥‘𝑀) →
(ℤ≥‘if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀)) ⊆
(ℤ≥‘𝑀)) |
35 | 31, 34 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ) →
(ℤ≥‘if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀)) ⊆
(ℤ≥‘𝑀)) |
36 | 35, 2 | sseqtrrdi 3972 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ) →
(ℤ≥‘if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀)) ⊆ 𝑍) |
37 | 36 | sselda 3921 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀))) → 𝑘 ∈ 𝑍) |
38 | | simplr 766 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀))) → 𝑗 ∈ ℝ) |
39 | 23 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀))) → if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀) ∈ ℤ) |
40 | 39 | zred 12414 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀))) → if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀) ∈ ℝ) |
41 | | eluzelre 12581 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈
(ℤ≥‘if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀)) → 𝑘 ∈ ℝ) |
42 | 41 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀))) → 𝑘 ∈ ℝ) |
43 | | simpr 485 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ) → 𝑗 ∈
ℝ) |
44 | 27 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ) →
((⌊‘𝑗) + 1)
∈ ℝ) |
45 | 23 | zred 12414 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ) → if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀) ∈ ℝ) |
46 | | fllep1 13509 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ℝ → 𝑗 ≤ ((⌊‘𝑗) + 1)) |
47 | 46 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ) → 𝑗 ≤ ((⌊‘𝑗) + 1)) |
48 | | max2 12909 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℝ ∧
((⌊‘𝑗) + 1)
∈ ℝ) → ((⌊‘𝑗) + 1) ≤ if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀)) |
49 | 24, 27, 48 | syl2an 596 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ) →
((⌊‘𝑗) + 1)
≤ if(𝑀 ≤
((⌊‘𝑗) + 1),
((⌊‘𝑗) + 1),
𝑀)) |
50 | 43, 44, 45, 47, 49 | letrd 11120 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ) → 𝑗 ≤ if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀)) |
51 | 50 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀))) → 𝑗 ≤ if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀)) |
52 | | eluzle 12583 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈
(ℤ≥‘if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀)) → if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀) ≤ 𝑘) |
53 | 52 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀))) → if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀) ≤ 𝑘) |
54 | 38, 40, 42, 51, 53 | letrd 11120 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀))) → 𝑗 ≤ 𝑘) |
55 | 37, 54 | jca 512 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ) ∧ 𝑘 ∈
(ℤ≥‘if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀))) → (𝑘 ∈ 𝑍 ∧ 𝑗 ≤ 𝑘)) |
56 | 55 | ex 413 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ) → (𝑘 ∈
(ℤ≥‘if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀)) → (𝑘 ∈ 𝑍 ∧ 𝑗 ≤ 𝑘))) |
57 | 56 | imim1d 82 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ) → (((𝑘 ∈ 𝑍 ∧ 𝑗 ≤ 𝑘) → 𝜑) → (𝑘 ∈
(ℤ≥‘if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀)) → 𝜑))) |
58 | 33, 57 | syl5bir 242 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ) → ((𝑘 ∈ 𝑍 → (𝑗 ≤ 𝑘 → 𝜑)) → (𝑘 ∈
(ℤ≥‘if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀)) → 𝜑))) |
59 | 58 | ralimdv2 3102 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ) →
(∀𝑘 ∈ 𝑍 (𝑗 ≤ 𝑘 → 𝜑) → ∀𝑘 ∈
(ℤ≥‘if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀))𝜑)) |
60 | | fveq2 6767 |
. . . . . . 7
⊢ (𝑚 = if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀) → (ℤ≥‘𝑚) =
(ℤ≥‘if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀))) |
61 | 60 | raleqdv 3346 |
. . . . . 6
⊢ (𝑚 = if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀) → (∀𝑘 ∈ (ℤ≥‘𝑚)𝜑 ↔ ∀𝑘 ∈
(ℤ≥‘if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀))𝜑)) |
62 | 61 | rspcev 3560 |
. . . . 5
⊢
((if(𝑀 ≤
((⌊‘𝑗) + 1),
((⌊‘𝑗) + 1),
𝑀) ∈ 𝑍 ∧ ∀𝑘 ∈
(ℤ≥‘if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀))𝜑) → ∃𝑚 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑚)𝜑) |
63 | 32, 59, 62 | syl6an 681 |
. . . 4
⊢ ((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ) →
(∀𝑘 ∈ 𝑍 (𝑗 ≤ 𝑘 → 𝜑) → ∃𝑚 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑚)𝜑)) |
64 | 63 | rexlimdva 3211 |
. . 3
⊢ (𝑀 ∈ ℤ →
(∃𝑗 ∈ ℝ
∀𝑘 ∈ 𝑍 (𝑗 ≤ 𝑘 → 𝜑) → ∃𝑚 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑚)𝜑)) |
65 | | fveq2 6767 |
. . . . 5
⊢ (𝑚 = 𝑗 → (ℤ≥‘𝑚) =
(ℤ≥‘𝑗)) |
66 | 65 | raleqdv 3346 |
. . . 4
⊢ (𝑚 = 𝑗 → (∀𝑘 ∈ (ℤ≥‘𝑚)𝜑 ↔ ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑)) |
67 | 66 | cbvrexvw 3382 |
. . 3
⊢
(∃𝑚 ∈
𝑍 ∀𝑘 ∈
(ℤ≥‘𝑚)𝜑 ↔ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑) |
68 | 64, 67 | syl6ib 250 |
. 2
⊢ (𝑀 ∈ ℤ →
(∃𝑗 ∈ ℝ
∀𝑘 ∈ 𝑍 (𝑗 ≤ 𝑘 → 𝜑) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑)) |
69 | 18, 68 | impbid2 225 |
1
⊢ (𝑀 ∈ ℤ →
(∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑 ↔ ∃𝑗 ∈ ℝ ∀𝑘 ∈ 𝑍 (𝑗 ≤ 𝑘 → 𝜑))) |