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	$$⊢N\in {\mathbb{Z}}_{\ge M}\to sup\left(\left(M\dots N\right),\mathbb{Z},<\right)=M$$

Proof

Step	Hyp	Ref	Expression
1		zssre	$$⊢\mathbb{Z}\subseteq ℝ$$
2		ltso	$$⊢<\mathrm{Or}ℝ$$
3		soss	$$⊢\mathbb{Z}\subseteq ℝ\to \left(<\mathrm{Or}ℝ\to <\mathrm{Or}\mathbb{Z}\right)$$
4	1 2 3	mp2	$$⊢<\mathrm{Or}\mathbb{Z}$$
5	4	a1i	$$⊢N\in {\mathbb{Z}}_{\ge M}\to <\mathrm{Or}\mathbb{Z}$$
6		eluzel2	$$⊢N\in {\mathbb{Z}}_{\ge M}\to M\in \mathbb{Z}$$
7		eluzfz1	$$⊢N\in {\mathbb{Z}}_{\ge M}\to M\in \left(M\dots N\right)$$
8		elfzle1	$$⊢x\in \left(M\dots N\right)\to M\le x$$
9	8	adantl	$$⊢\left(N\in {\mathbb{Z}}_{\ge M}\wedge x\in \left(M\dots N\right)\right)\to M\le x$$
10	6	zred	$$⊢N\in {\mathbb{Z}}_{\ge M}\to M\in ℝ$$
11		elfzelz	$$⊢x\in \left(M\dots N\right)\to x\in \mathbb{Z}$$
12	11	zred	$$⊢x\in \left(M\dots N\right)\to x\in ℝ$$
13		lenlt	$$⊢\left(M\in ℝ\wedge x\in ℝ\right)\to \left(M\le x\leftrightarrow \neg x<M\right)$$
14	10 12 13	syl2an	$$⊢\left(N\in {\mathbb{Z}}_{\ge M}\wedge x\in \left(M\dots N\right)\right)\to \left(M\le x\leftrightarrow \neg x<M\right)$$
15	9 14	mpbid	$$⊢\left(N\in {\mathbb{Z}}_{\ge M}\wedge x\in \left(M\dots N\right)\right)\to \neg x<M$$
16	5 6 7 15	infmin	$$⊢N\in {\mathbb{Z}}_{\ge M}\to sup\left(\left(M\dots N\right),\mathbb{Z},<\right)=M$$