| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | zmin 12987 | . 2
⊢ (𝐴 ∈ ℝ →
∃!𝑥 ∈ ℤ
(𝐴 ≤ 𝑥 ∧ ∀𝑦 ∈ ℤ (𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦))) | 
| 2 |  | zre 12619 | . . . . . . . . . . . 12
⊢ (𝑦 ∈ ℤ → 𝑦 ∈
ℝ) | 
| 3 |  | zre 12619 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℤ → 𝑥 ∈
ℝ) | 
| 4 |  | peano2rem 11577 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ → (𝑥 − 1) ∈
ℝ) | 
| 5 | 3, 4 | syl 17 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℤ → (𝑥 − 1) ∈
ℝ) | 
| 6 |  | ltletr 11354 | . . . . . . . . . . . . . 14
⊢ (((𝑥 − 1) ∈ ℝ ∧
𝐴 ∈ ℝ ∧
𝑦 ∈ ℝ) →
(((𝑥 − 1) < 𝐴 ∧ 𝐴 ≤ 𝑦) → (𝑥 − 1) < 𝑦)) | 
| 7 | 5, 6 | syl3an1 1163 | . . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℤ ∧ 𝐴 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (((𝑥 − 1) < 𝐴 ∧ 𝐴 ≤ 𝑦) → (𝑥 − 1) < 𝑦)) | 
| 8 | 7 | 3expa 1118 | . . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℤ ∧ 𝐴 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → (((𝑥 − 1) < 𝐴 ∧ 𝐴 ≤ 𝑦) → (𝑥 − 1) < 𝑦)) | 
| 9 | 2, 8 | sylan2 593 | . . . . . . . . . . 11
⊢ (((𝑥 ∈ ℤ ∧ 𝐴 ∈ ℝ) ∧ 𝑦 ∈ ℤ) → (((𝑥 − 1) < 𝐴 ∧ 𝐴 ≤ 𝑦) → (𝑥 − 1) < 𝑦)) | 
| 10 |  | zlem1lt 12671 | . . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝑥 ≤ 𝑦 ↔ (𝑥 − 1) < 𝑦)) | 
| 11 | 10 | adantlr 715 | . . . . . . . . . . 11
⊢ (((𝑥 ∈ ℤ ∧ 𝐴 ∈ ℝ) ∧ 𝑦 ∈ ℤ) → (𝑥 ≤ 𝑦 ↔ (𝑥 − 1) < 𝑦)) | 
| 12 | 9, 11 | sylibrd 259 | . . . . . . . . . 10
⊢ (((𝑥 ∈ ℤ ∧ 𝐴 ∈ ℝ) ∧ 𝑦 ∈ ℤ) → (((𝑥 − 1) < 𝐴 ∧ 𝐴 ≤ 𝑦) → 𝑥 ≤ 𝑦)) | 
| 13 | 12 | exp4b 430 | . . . . . . . . 9
⊢ ((𝑥 ∈ ℤ ∧ 𝐴 ∈ ℝ) → (𝑦 ∈ ℤ → ((𝑥 − 1) < 𝐴 → (𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦)))) | 
| 14 | 13 | com23 86 | . . . . . . . 8
⊢ ((𝑥 ∈ ℤ ∧ 𝐴 ∈ ℝ) → ((𝑥 − 1) < 𝐴 → (𝑦 ∈ ℤ → (𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦)))) | 
| 15 | 14 | ralrimdv 3151 | . . . . . . 7
⊢ ((𝑥 ∈ ℤ ∧ 𝐴 ∈ ℝ) → ((𝑥 − 1) < 𝐴 → ∀𝑦 ∈ ℤ (𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦))) | 
| 16 | 5 | ltnrd 11396 | . . . . . . . . . . 11
⊢ (𝑥 ∈ ℤ → ¬
(𝑥 − 1) < (𝑥 − 1)) | 
| 17 |  | peano2zm 12662 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ ℤ → (𝑥 − 1) ∈
ℤ) | 
| 18 |  | zlem1lt 12671 | . . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℤ ∧ (𝑥 − 1) ∈ ℤ)
→ (𝑥 ≤ (𝑥 − 1) ↔ (𝑥 − 1) < (𝑥 − 1))) | 
| 19 | 17, 18 | mpdan 687 | . . . . . . . . . . 11
⊢ (𝑥 ∈ ℤ → (𝑥 ≤ (𝑥 − 1) ↔ (𝑥 − 1) < (𝑥 − 1))) | 
| 20 | 16, 19 | mtbird 325 | . . . . . . . . . 10
⊢ (𝑥 ∈ ℤ → ¬
𝑥 ≤ (𝑥 − 1)) | 
| 21 | 20 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝑥 ∈ ℤ ∧ 𝐴 ∈ ℝ) ∧
∀𝑦 ∈ ℤ
(𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦)) → ¬ 𝑥 ≤ (𝑥 − 1)) | 
| 22 |  | lenlt 11340 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ (𝑥 − 1) ∈ ℝ)
→ (𝐴 ≤ (𝑥 − 1) ↔ ¬ (𝑥 − 1) < 𝐴)) | 
| 23 | 5, 22 | sylan2 593 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ ℤ) → (𝐴 ≤ (𝑥 − 1) ↔ ¬ (𝑥 − 1) < 𝐴)) | 
| 24 | 23 | ancoms 458 | . . . . . . . . . . 11
⊢ ((𝑥 ∈ ℤ ∧ 𝐴 ∈ ℝ) → (𝐴 ≤ (𝑥 − 1) ↔ ¬ (𝑥 − 1) < 𝐴)) | 
| 25 | 24 | adantr 480 | . . . . . . . . . 10
⊢ (((𝑥 ∈ ℤ ∧ 𝐴 ∈ ℝ) ∧
∀𝑦 ∈ ℤ
(𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦)) → (𝐴 ≤ (𝑥 − 1) ↔ ¬ (𝑥 − 1) < 𝐴)) | 
| 26 |  | breq2 5146 | . . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝑥 − 1) → (𝐴 ≤ 𝑦 ↔ 𝐴 ≤ (𝑥 − 1))) | 
| 27 |  | breq2 5146 | . . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝑥 − 1) → (𝑥 ≤ 𝑦 ↔ 𝑥 ≤ (𝑥 − 1))) | 
| 28 | 26, 27 | imbi12d 344 | . . . . . . . . . . . . . 14
⊢ (𝑦 = (𝑥 − 1) → ((𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦) ↔ (𝐴 ≤ (𝑥 − 1) → 𝑥 ≤ (𝑥 − 1)))) | 
| 29 | 28 | rspcv 3617 | . . . . . . . . . . . . 13
⊢ ((𝑥 − 1) ∈ ℤ
→ (∀𝑦 ∈
ℤ (𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦) → (𝐴 ≤ (𝑥 − 1) → 𝑥 ≤ (𝑥 − 1)))) | 
| 30 | 17, 29 | syl 17 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ ℤ →
(∀𝑦 ∈ ℤ
(𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦) → (𝐴 ≤ (𝑥 − 1) → 𝑥 ≤ (𝑥 − 1)))) | 
| 31 | 30 | imp 406 | . . . . . . . . . . 11
⊢ ((𝑥 ∈ ℤ ∧
∀𝑦 ∈ ℤ
(𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦)) → (𝐴 ≤ (𝑥 − 1) → 𝑥 ≤ (𝑥 − 1))) | 
| 32 | 31 | adantlr 715 | . . . . . . . . . 10
⊢ (((𝑥 ∈ ℤ ∧ 𝐴 ∈ ℝ) ∧
∀𝑦 ∈ ℤ
(𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦)) → (𝐴 ≤ (𝑥 − 1) → 𝑥 ≤ (𝑥 − 1))) | 
| 33 | 25, 32 | sylbird 260 | . . . . . . . . 9
⊢ (((𝑥 ∈ ℤ ∧ 𝐴 ∈ ℝ) ∧
∀𝑦 ∈ ℤ
(𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦)) → (¬ (𝑥 − 1) < 𝐴 → 𝑥 ≤ (𝑥 − 1))) | 
| 34 | 21, 33 | mt3d 148 | . . . . . . . 8
⊢ (((𝑥 ∈ ℤ ∧ 𝐴 ∈ ℝ) ∧
∀𝑦 ∈ ℤ
(𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦)) → (𝑥 − 1) < 𝐴) | 
| 35 | 34 | ex 412 | . . . . . . 7
⊢ ((𝑥 ∈ ℤ ∧ 𝐴 ∈ ℝ) →
(∀𝑦 ∈ ℤ
(𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦) → (𝑥 − 1) < 𝐴)) | 
| 36 | 15, 35 | impbid 212 | . . . . . 6
⊢ ((𝑥 ∈ ℤ ∧ 𝐴 ∈ ℝ) → ((𝑥 − 1) < 𝐴 ↔ ∀𝑦 ∈ ℤ (𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦))) | 
| 37 |  | 1re 11262 | . . . . . . . 8
⊢ 1 ∈
ℝ | 
| 38 |  | ltsubadd 11734 | . . . . . . . 8
⊢ ((𝑥 ∈ ℝ ∧ 1 ∈
ℝ ∧ 𝐴 ∈
ℝ) → ((𝑥 −
1) < 𝐴 ↔ 𝑥 < (𝐴 + 1))) | 
| 39 | 37, 38 | mp3an2 1450 | . . . . . . 7
⊢ ((𝑥 ∈ ℝ ∧ 𝐴 ∈ ℝ) → ((𝑥 − 1) < 𝐴 ↔ 𝑥 < (𝐴 + 1))) | 
| 40 | 3, 39 | sylan 580 | . . . . . 6
⊢ ((𝑥 ∈ ℤ ∧ 𝐴 ∈ ℝ) → ((𝑥 − 1) < 𝐴 ↔ 𝑥 < (𝐴 + 1))) | 
| 41 | 36, 40 | bitr3d 281 | . . . . 5
⊢ ((𝑥 ∈ ℤ ∧ 𝐴 ∈ ℝ) →
(∀𝑦 ∈ ℤ
(𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦) ↔ 𝑥 < (𝐴 + 1))) | 
| 42 | 41 | ancoms 458 | . . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ ℤ) →
(∀𝑦 ∈ ℤ
(𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦) ↔ 𝑥 < (𝐴 + 1))) | 
| 43 | 42 | anbi2d 630 | . . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ ℤ) → ((𝐴 ≤ 𝑥 ∧ ∀𝑦 ∈ ℤ (𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦)) ↔ (𝐴 ≤ 𝑥 ∧ 𝑥 < (𝐴 + 1)))) | 
| 44 | 43 | reubidva 3395 | . 2
⊢ (𝐴 ∈ ℝ →
(∃!𝑥 ∈ ℤ
(𝐴 ≤ 𝑥 ∧ ∀𝑦 ∈ ℤ (𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦)) ↔ ∃!𝑥 ∈ ℤ (𝐴 ≤ 𝑥 ∧ 𝑥 < (𝐴 + 1)))) | 
| 45 | 1, 44 | mpbid 232 | 1
⊢ (𝐴 ∈ ℝ →
∃!𝑥 ∈ ℤ
(𝐴 ≤ 𝑥 ∧ 𝑥 < (𝐴 + 1))) |