Step | Hyp | Ref
| Expression |
1 | | zmin 12338 |
. 2
⊢ (𝐴 ∈ ℝ →
∃!𝑥 ∈ ℤ
(𝐴 ≤ 𝑥 ∧ ∀𝑦 ∈ ℤ (𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦))) |
2 | | zre 11979 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℤ → 𝑦 ∈
ℝ) |
3 | | zre 11979 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℤ → 𝑥 ∈
ℝ) |
4 | | peano2rem 10947 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ → (𝑥 − 1) ∈
ℝ) |
5 | 3, 4 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℤ → (𝑥 − 1) ∈
ℝ) |
6 | | ltletr 10726 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 − 1) ∈ ℝ ∧
𝐴 ∈ ℝ ∧
𝑦 ∈ ℝ) →
(((𝑥 − 1) < 𝐴 ∧ 𝐴 ≤ 𝑦) → (𝑥 − 1) < 𝑦)) |
7 | 5, 6 | syl3an1 1159 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℤ ∧ 𝐴 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (((𝑥 − 1) < 𝐴 ∧ 𝐴 ≤ 𝑦) → (𝑥 − 1) < 𝑦)) |
8 | 7 | 3expa 1114 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℤ ∧ 𝐴 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → (((𝑥 − 1) < 𝐴 ∧ 𝐴 ≤ 𝑦) → (𝑥 − 1) < 𝑦)) |
9 | 2, 8 | sylan2 594 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℤ ∧ 𝐴 ∈ ℝ) ∧ 𝑦 ∈ ℤ) → (((𝑥 − 1) < 𝐴 ∧ 𝐴 ≤ 𝑦) → (𝑥 − 1) < 𝑦)) |
10 | | zlem1lt 12028 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝑥 ≤ 𝑦 ↔ (𝑥 − 1) < 𝑦)) |
11 | 10 | adantlr 713 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℤ ∧ 𝐴 ∈ ℝ) ∧ 𝑦 ∈ ℤ) → (𝑥 ≤ 𝑦 ↔ (𝑥 − 1) < 𝑦)) |
12 | 9, 11 | sylibrd 261 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℤ ∧ 𝐴 ∈ ℝ) ∧ 𝑦 ∈ ℤ) → (((𝑥 − 1) < 𝐴 ∧ 𝐴 ≤ 𝑦) → 𝑥 ≤ 𝑦)) |
13 | 12 | exp4b 433 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℤ ∧ 𝐴 ∈ ℝ) → (𝑦 ∈ ℤ → ((𝑥 − 1) < 𝐴 → (𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦)))) |
14 | 13 | com23 86 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℤ ∧ 𝐴 ∈ ℝ) → ((𝑥 − 1) < 𝐴 → (𝑦 ∈ ℤ → (𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦)))) |
15 | 14 | ralrimdv 3188 |
. . . . . . 7
⊢ ((𝑥 ∈ ℤ ∧ 𝐴 ∈ ℝ) → ((𝑥 − 1) < 𝐴 → ∀𝑦 ∈ ℤ (𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦))) |
16 | 5 | ltnrd 10768 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℤ → ¬
(𝑥 − 1) < (𝑥 − 1)) |
17 | | peano2zm 12019 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℤ → (𝑥 − 1) ∈
ℤ) |
18 | | zlem1lt 12028 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℤ ∧ (𝑥 − 1) ∈ ℤ)
→ (𝑥 ≤ (𝑥 − 1) ↔ (𝑥 − 1) < (𝑥 − 1))) |
19 | 17, 18 | mpdan 685 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℤ → (𝑥 ≤ (𝑥 − 1) ↔ (𝑥 − 1) < (𝑥 − 1))) |
20 | 16, 19 | mtbird 327 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℤ → ¬
𝑥 ≤ (𝑥 − 1)) |
21 | 20 | ad2antrr 724 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ℤ ∧ 𝐴 ∈ ℝ) ∧
∀𝑦 ∈ ℤ
(𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦)) → ¬ 𝑥 ≤ (𝑥 − 1)) |
22 | | lenlt 10713 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ (𝑥 − 1) ∈ ℝ)
→ (𝐴 ≤ (𝑥 − 1) ↔ ¬ (𝑥 − 1) < 𝐴)) |
23 | 5, 22 | sylan2 594 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ ℤ) → (𝐴 ≤ (𝑥 − 1) ↔ ¬ (𝑥 − 1) < 𝐴)) |
24 | 23 | ancoms 461 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℤ ∧ 𝐴 ∈ ℝ) → (𝐴 ≤ (𝑥 − 1) ↔ ¬ (𝑥 − 1) < 𝐴)) |
25 | 24 | adantr 483 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℤ ∧ 𝐴 ∈ ℝ) ∧
∀𝑦 ∈ ℤ
(𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦)) → (𝐴 ≤ (𝑥 − 1) ↔ ¬ (𝑥 − 1) < 𝐴)) |
26 | | breq2 5062 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝑥 − 1) → (𝐴 ≤ 𝑦 ↔ 𝐴 ≤ (𝑥 − 1))) |
27 | | breq2 5062 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝑥 − 1) → (𝑥 ≤ 𝑦 ↔ 𝑥 ≤ (𝑥 − 1))) |
28 | 26, 27 | imbi12d 347 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (𝑥 − 1) → ((𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦) ↔ (𝐴 ≤ (𝑥 − 1) → 𝑥 ≤ (𝑥 − 1)))) |
29 | 28 | rspcv 3617 |
. . . . . . . . . . . . 13
⊢ ((𝑥 − 1) ∈ ℤ
→ (∀𝑦 ∈
ℤ (𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦) → (𝐴 ≤ (𝑥 − 1) → 𝑥 ≤ (𝑥 − 1)))) |
30 | 17, 29 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℤ →
(∀𝑦 ∈ ℤ
(𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦) → (𝐴 ≤ (𝑥 − 1) → 𝑥 ≤ (𝑥 − 1)))) |
31 | 30 | imp 409 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℤ ∧
∀𝑦 ∈ ℤ
(𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦)) → (𝐴 ≤ (𝑥 − 1) → 𝑥 ≤ (𝑥 − 1))) |
32 | 31 | adantlr 713 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℤ ∧ 𝐴 ∈ ℝ) ∧
∀𝑦 ∈ ℤ
(𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦)) → (𝐴 ≤ (𝑥 − 1) → 𝑥 ≤ (𝑥 − 1))) |
33 | 25, 32 | sylbird 262 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ℤ ∧ 𝐴 ∈ ℝ) ∧
∀𝑦 ∈ ℤ
(𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦)) → (¬ (𝑥 − 1) < 𝐴 → 𝑥 ≤ (𝑥 − 1))) |
34 | 21, 33 | mt3d 150 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℤ ∧ 𝐴 ∈ ℝ) ∧
∀𝑦 ∈ ℤ
(𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦)) → (𝑥 − 1) < 𝐴) |
35 | 34 | ex 415 |
. . . . . . 7
⊢ ((𝑥 ∈ ℤ ∧ 𝐴 ∈ ℝ) →
(∀𝑦 ∈ ℤ
(𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦) → (𝑥 − 1) < 𝐴)) |
36 | 15, 35 | impbid 214 |
. . . . . 6
⊢ ((𝑥 ∈ ℤ ∧ 𝐴 ∈ ℝ) → ((𝑥 − 1) < 𝐴 ↔ ∀𝑦 ∈ ℤ (𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦))) |
37 | | 1re 10635 |
. . . . . . . 8
⊢ 1 ∈
ℝ |
38 | | ltsubadd 11104 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ ∧ 1 ∈
ℝ ∧ 𝐴 ∈
ℝ) → ((𝑥 −
1) < 𝐴 ↔ 𝑥 < (𝐴 + 1))) |
39 | 37, 38 | mp3an2 1445 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ ∧ 𝐴 ∈ ℝ) → ((𝑥 − 1) < 𝐴 ↔ 𝑥 < (𝐴 + 1))) |
40 | 3, 39 | sylan 582 |
. . . . . 6
⊢ ((𝑥 ∈ ℤ ∧ 𝐴 ∈ ℝ) → ((𝑥 − 1) < 𝐴 ↔ 𝑥 < (𝐴 + 1))) |
41 | 36, 40 | bitr3d 283 |
. . . . 5
⊢ ((𝑥 ∈ ℤ ∧ 𝐴 ∈ ℝ) →
(∀𝑦 ∈ ℤ
(𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦) ↔ 𝑥 < (𝐴 + 1))) |
42 | 41 | ancoms 461 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ ℤ) →
(∀𝑦 ∈ ℤ
(𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦) ↔ 𝑥 < (𝐴 + 1))) |
43 | 42 | anbi2d 630 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ ℤ) → ((𝐴 ≤ 𝑥 ∧ ∀𝑦 ∈ ℤ (𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦)) ↔ (𝐴 ≤ 𝑥 ∧ 𝑥 < (𝐴 + 1)))) |
44 | 43 | reubidva 3388 |
. 2
⊢ (𝐴 ∈ ℝ →
(∃!𝑥 ∈ ℤ
(𝐴 ≤ 𝑥 ∧ ∀𝑦 ∈ ℤ (𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦)) ↔ ∃!𝑥 ∈ ℤ (𝐴 ≤ 𝑥 ∧ 𝑥 < (𝐴 + 1)))) |
45 | 1, 44 | mpbid 234 |
1
⊢ (𝐴 ∈ ℝ →
∃!𝑥 ∈ ℤ
(𝐴 ≤ 𝑥 ∧ 𝑥 < (𝐴 + 1))) |