Metamath Proof Explorer

Theorem supfz

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

Ref Expression
Assertion supfz 
|- ( N e. ( ZZ>= ` M ) -> sup ( ( M ... N ) , ZZ , < ) = N )

Proof

Step Hyp Ref Expression
1 zssre 
 |-  ZZ C_ RR
2 ltso 
 |-  < Or RR
3 soss 
 |-  ( ZZ C_ RR -> ( < Or RR -> < Or ZZ ) )
4 1 2 3 mp2 
 |-  < Or ZZ
5 4 a1i 
 |-  ( N e. ( ZZ>= ` M ) -> < Or ZZ )
6 eluzelz 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ZZ )
7 eluzfz2 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ( M ... N ) )
8 elfzle2 
 |-  ( x e. ( M ... N ) -> x <_ N )
9 8 adantl 
 |-  ( ( N e. ( ZZ>= ` M ) /\ x e. ( M ... N ) ) -> x <_ N )
10 elfzelz 
 |-  ( x e. ( M ... N ) -> x e. ZZ )
11 10 zred 
 |-  ( x e. ( M ... N ) -> x e. RR )
12 eluzelre 
 |-  ( N e. ( ZZ>= ` M ) -> N e. RR )
13 lenlt 
 |-  ( ( x e. RR /\ N e. RR ) -> ( x <_ N <-> -. N < x ) )
14 11 12 13 syl2anr 
 |-  ( ( N e. ( ZZ>= ` M ) /\ x e. ( M ... N ) ) -> ( x <_ N <-> -. N < x ) )
15 9 14 mpbid 
 |-  ( ( N e. ( ZZ>= ` M ) /\ x e. ( M ... N ) ) -> -. N < x )
16 5 6 7 15 supmax 
 |-  ( N e. ( ZZ>= ` M ) -> sup ( ( M ... N ) , ZZ , < ) = N )