| Step | Hyp | Ref
| Expression |
| 1 | | uzinico.2 |
. . . . . . . 8
⊢ 𝑍 =
(ℤ≥‘𝑀) |
| 2 | 1 | eluzelz2 45414 |
. . . . . . 7
⊢ (𝑘 ∈ 𝑍 → 𝑘 ∈ ℤ) |
| 3 | 2 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ ℤ) |
| 4 | | uzinico.1 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 5 | 4 | zred 12722 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℝ) |
| 6 | 5 | rexrd 11311 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈
ℝ*) |
| 7 | 6 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑀 ∈
ℝ*) |
| 8 | | pnfxr 11315 |
. . . . . . . 8
⊢ +∞
∈ ℝ* |
| 9 | 8 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → +∞ ∈
ℝ*) |
| 10 | | zssre 12620 |
. . . . . . . . . 10
⊢ ℤ
⊆ ℝ |
| 11 | | ressxr 11305 |
. . . . . . . . . 10
⊢ ℝ
⊆ ℝ* |
| 12 | 10, 11 | sstri 3993 |
. . . . . . . . 9
⊢ ℤ
⊆ ℝ* |
| 13 | 12, 2 | sselid 3981 |
. . . . . . . 8
⊢ (𝑘 ∈ 𝑍 → 𝑘 ∈ ℝ*) |
| 14 | 13 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ ℝ*) |
| 15 | 1 | eleq2i 2833 |
. . . . . . . . . 10
⊢ (𝑘 ∈ 𝑍 ↔ 𝑘 ∈ (ℤ≥‘𝑀)) |
| 16 | 15 | biimpi 216 |
. . . . . . . . 9
⊢ (𝑘 ∈ 𝑍 → 𝑘 ∈ (ℤ≥‘𝑀)) |
| 17 | | eluzle 12891 |
. . . . . . . . 9
⊢ (𝑘 ∈
(ℤ≥‘𝑀) → 𝑀 ≤ 𝑘) |
| 18 | 16, 17 | syl 17 |
. . . . . . . 8
⊢ (𝑘 ∈ 𝑍 → 𝑀 ≤ 𝑘) |
| 19 | 18 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑀 ≤ 𝑘) |
| 20 | 10, 2 | sselid 3981 |
. . . . . . . . 9
⊢ (𝑘 ∈ 𝑍 → 𝑘 ∈ ℝ) |
| 21 | 20 | ltpnfd 13163 |
. . . . . . . 8
⊢ (𝑘 ∈ 𝑍 → 𝑘 < +∞) |
| 22 | 21 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑘 < +∞) |
| 23 | 7, 9, 14, 19, 22 | elicod 13437 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ (𝑀[,)+∞)) |
| 24 | 3, 23 | elind 4200 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ (ℤ ∩ (𝑀[,)+∞))) |
| 25 | 24 | ex 412 |
. . . 4
⊢ (𝜑 → (𝑘 ∈ 𝑍 → 𝑘 ∈ (ℤ ∩ (𝑀[,)+∞)))) |
| 26 | 4 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ ∩ (𝑀[,)+∞))) → 𝑀 ∈ ℤ) |
| 27 | | elinel1 4201 |
. . . . . . 7
⊢ (𝑘 ∈ (ℤ ∩ (𝑀[,)+∞)) → 𝑘 ∈
ℤ) |
| 28 | 27 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ ∩ (𝑀[,)+∞))) → 𝑘 ∈ ℤ) |
| 29 | | elinel2 4202 |
. . . . . . . 8
⊢ (𝑘 ∈ (ℤ ∩ (𝑀[,)+∞)) → 𝑘 ∈ (𝑀[,)+∞)) |
| 30 | 29 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ ∩ (𝑀[,)+∞))) → 𝑘 ∈ (𝑀[,)+∞)) |
| 31 | 6 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀[,)+∞)) → 𝑀 ∈
ℝ*) |
| 32 | 8 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀[,)+∞)) → +∞ ∈
ℝ*) |
| 33 | | simpr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀[,)+∞)) → 𝑘 ∈ (𝑀[,)+∞)) |
| 34 | 31, 32, 33 | icogelbd 45571 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀[,)+∞)) → 𝑀 ≤ 𝑘) |
| 35 | 30, 34 | syldan 591 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ ∩ (𝑀[,)+∞))) → 𝑀 ≤ 𝑘) |
| 36 | 1, 26, 28, 35 | eluzd 45420 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ ∩ (𝑀[,)+∞))) → 𝑘 ∈ 𝑍) |
| 37 | 36 | ex 412 |
. . . 4
⊢ (𝜑 → (𝑘 ∈ (ℤ ∩ (𝑀[,)+∞)) → 𝑘 ∈ 𝑍)) |
| 38 | 25, 37 | impbid 212 |
. . 3
⊢ (𝜑 → (𝑘 ∈ 𝑍 ↔ 𝑘 ∈ (ℤ ∩ (𝑀[,)+∞)))) |
| 39 | 38 | alrimiv 1927 |
. 2
⊢ (𝜑 → ∀𝑘(𝑘 ∈ 𝑍 ↔ 𝑘 ∈ (ℤ ∩ (𝑀[,)+∞)))) |
| 40 | | dfcleq 2730 |
. 2
⊢ (𝑍 = (ℤ ∩ (𝑀[,)+∞)) ↔
∀𝑘(𝑘 ∈ 𝑍 ↔ 𝑘 ∈ (ℤ ∩ (𝑀[,)+∞)))) |
| 41 | 39, 40 | sylibr 234 |
1
⊢ (𝜑 → 𝑍 = (ℤ ∩ (𝑀[,)+∞))) |