Theorem supfz

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

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

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		eluzelz	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ℤ )
7		eluzfz2	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ( 𝑀 ... 𝑁 ) )
8		elfzle2	⊢ ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → 𝑥 ≤ 𝑁 )
9	8	adantl	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑥 ≤ 𝑁 )
10		elfzelz	⊢ ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → 𝑥 ∈ ℤ )
11	10	zred	⊢ ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → 𝑥 ∈ ℝ )
12		eluzelre	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ℝ )
13		lenlt	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝑥 ≤ 𝑁 ↔ ¬ 𝑁 < 𝑥 ) )
14	11 12 13	syl2anr	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑥 ≤ 𝑁 ↔ ¬ 𝑁 < 𝑥 ) )
15	9 14	mpbid	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ¬ 𝑁 < 𝑥 )
16	5 6 7 15	supmax	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → sup ( ( 𝑀 ... 𝑁 ) , ℤ , < ) = 𝑁 )