Metamath Proof Explorer

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 e. ( ZZ>= ` M ) -> inf ( ( M ... N ) , ZZ , < ) = M )

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 eluzel2 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ZZ )
7 eluzfz1 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ( M ... N ) )
8 elfzle1 
 |-  ( x e. ( M ... N ) -> M <_ x )
9 8 adantl 
 |-  ( ( N e. ( ZZ>= ` M ) /\ x e. ( M ... N ) ) -> M <_ x )
10 6 zred 
 |-  ( N e. ( ZZ>= ` M ) -> M e. RR )
11 elfzelz 
 |-  ( x e. ( M ... N ) -> x e. ZZ )
12 11 zred 
 |-  ( x e. ( M ... N ) -> x e. RR )
13 lenlt 
 |-  ( ( M e. RR /\ x e. RR ) -> ( M <_ x <-> -. x < M ) )
14 10 12 13 syl2an 
 |-  ( ( N e. ( ZZ>= ` M ) /\ x e. ( M ... N ) ) -> ( M <_ x <-> -. x < M ) )
15 9 14 mpbid 
 |-  ( ( N e. ( ZZ>= ` M ) /\ x e. ( M ... N ) ) -> -. x < M )
16 5 6 7 15 infmin 
 |-  ( N e. ( ZZ>= ` M ) -> inf ( ( M ... N ) , ZZ , < ) = M )