Step |
Hyp |
Ref |
Expression |
1 |
|
uzinfi.1 |
⊢ 𝑀 ∈ ℤ |
2 |
|
ltso |
⊢ < Or ℝ |
3 |
2
|
a1i |
⊢ ( 𝑀 ∈ ℤ → < Or ℝ ) |
4 |
|
zre |
⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ ) |
5 |
|
uzid |
⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) ) |
6 |
|
eluz2 |
⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ) ) |
7 |
4
|
adantr |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → 𝑀 ∈ ℝ ) |
8 |
|
zre |
⊢ ( 𝑘 ∈ ℤ → 𝑘 ∈ ℝ ) |
9 |
8
|
adantl |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → 𝑘 ∈ ℝ ) |
10 |
7 9
|
lenltd |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( 𝑀 ≤ 𝑘 ↔ ¬ 𝑘 < 𝑀 ) ) |
11 |
10
|
biimp3a |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ) → ¬ 𝑘 < 𝑀 ) |
12 |
11
|
a1d |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ) → ( 𝑀 ∈ ℤ → ¬ 𝑘 < 𝑀 ) ) |
13 |
6 12
|
sylbi |
⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑀 ∈ ℤ → ¬ 𝑘 < 𝑀 ) ) |
14 |
13
|
impcom |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ¬ 𝑘 < 𝑀 ) |
15 |
3 4 5 14
|
infmin |
⊢ ( 𝑀 ∈ ℤ → inf ( ( ℤ≥ ‘ 𝑀 ) , ℝ , < ) = 𝑀 ) |
16 |
1 15
|
ax-mp |
⊢ inf ( ( ℤ≥ ‘ 𝑀 ) , ℝ , < ) = 𝑀 |