Theorem inffz

Description: The infimum of a finite sequence of integers. (Contributed by Scott Fenton, 8-Aug-2013) (Revised by AV, 10-Oct-2021)

	Ref	Expression
Assertion	inffz	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → inf ( ( 𝑀 ... 𝑁 ) , ℤ , < ) = 𝑀 )

Proof

Step	Hyp	Ref	Expression
1		zssre	⊢ ℤ ⊆ ℝ
2		ltso	⊢ < Or ℝ
3		soss	⊢ ( ℤ ⊆ ℝ → ( < Or ℝ → < Or ℤ ) )
4	1 2 3	mp2	⊢ < Or ℤ
5	4	a1i	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → < Or ℤ )
6		eluzel2	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
7		eluzfz1	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ( 𝑀 ... 𝑁 ) )
8		elfzle1	⊢ ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → 𝑀 ≤ 𝑥 )
9	8	adantl	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑀 ≤ 𝑥 )
10	6	zred	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℝ )
11		elfzelz	⊢ ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → 𝑥 ∈ ℤ )
12	11	zred	⊢ ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → 𝑥 ∈ ℝ )
13		lenlt	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝑀 ≤ 𝑥 ↔ ¬ 𝑥 < 𝑀 ) )
14	10 12 13	syl2an	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑀 ≤ 𝑥 ↔ ¬ 𝑥 < 𝑀 ) )
15	9 14	mpbid	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ¬ 𝑥 < 𝑀 )
16	5 6 7 15	infmin	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → inf ( ( 𝑀 ... 𝑁 ) , ℤ , < ) = 𝑀 )