This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem uzinfi

Description: Extract the lower bound of an upper set of integers as its infimum. (Contributed by NM, 7-Oct-2005) (Revised by AV, 4-Sep-2020)

Ref Expression
Hypothesis uzinfi.1 ⊢ 𝑀 ∈ ℤ
Assertion uzinfi inf ( ( ℤ≥ ‘ 𝑀 ) , ℝ , < ) = 𝑀

Proof

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 ( ( ℤ≥ ‘ 𝑀 ) , ℝ , < ) = 𝑀