Theorem supfz

Description: The supremum of a finite sequence of integers. (Contributed by Scott Fenton, 8-Aug-2013)

	Ref	Expression
Assertion	supfz	$$⊢N\in {\mathbb{Z}}_{\ge M}\to sup\left(\left(M\dots N\right),\mathbb{Z},<\right)=N$$

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		eluzelz	$$⊢N\in {\mathbb{Z}}_{\ge M}\to N\in \mathbb{Z}$$
7		eluzfz2	$$⊢N\in {\mathbb{Z}}_{\ge M}\to N\in \left(M\dots N\right)$$
8		elfzle2	$$⊢x\in \left(M\dots N\right)\to x\le N$$
9	8	adantl	$$⊢\left(N\in {\mathbb{Z}}_{\ge M}\wedge x\in \left(M\dots N\right)\right)\to x\le N$$
10		elfzelz	$$⊢x\in \left(M\dots N\right)\to x\in \mathbb{Z}$$
11	10	zred	$$⊢x\in \left(M\dots N\right)\to x\in ℝ$$
12		eluzelre	$$⊢N\in {\mathbb{Z}}_{\ge M}\to N\in ℝ$$
13		lenlt	$$⊢\left(x\in ℝ\wedge N\in ℝ\right)\to \left(x\le N\leftrightarrow \neg N<x\right)$$
14	11 12 13	syl2anr	$$⊢\left(N\in {\mathbb{Z}}_{\ge M}\wedge x\in \left(M\dots N\right)\right)\to \left(x\le N\leftrightarrow \neg N<x\right)$$
15	9 14	mpbid	$$⊢\left(N\in {\mathbb{Z}}_{\ge M}\wedge x\in \left(M\dots N\right)\right)\to \neg N<x$$
16	5 6 7 15	supmax	$$⊢N\in {\mathbb{Z}}_{\ge M}\to sup\left(\left(M\dots N\right),\mathbb{Z},<\right)=N$$