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