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 )