This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem uzinfi

Description: Extract the lower bound of an upper set of integers as its infimum. (Contributed by NM, 7-Oct-2005) (Revised by AV, 4-Sep-2020)

Ref Expression
Hypothesis uzinfi.1 
|- M e. ZZ
Assertion uzinfi 
|- inf ( ( ZZ>= ` M ) , RR , < ) = M

Proof

Step Hyp Ref Expression
1 uzinfi.1 
 |-  M e. ZZ
2 ltso 
 |-  < Or RR
3 2 a1i 
 |-  ( M e. ZZ -> < Or RR )
4 zre 
 |-  ( M e. ZZ -> M e. RR )
5 uzid 
 |-  ( M e. ZZ -> M e. ( ZZ>= ` M ) )
6 eluz2 
 |-  ( k e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ k e. ZZ /\ M <_ k ) )
7 4 adantr 
 |-  ( ( M e. ZZ /\ k e. ZZ ) -> M e. RR )
8 zre 
 |-  ( k e. ZZ -> k e. RR )
9 8 adantl 
 |-  ( ( M e. ZZ /\ k e. ZZ ) -> k e. RR )
10 7 9 lenltd 
 |-  ( ( M e. ZZ /\ k e. ZZ ) -> ( M <_ k <-> -. k < M ) )
11 10 biimp3a 
 |-  ( ( M e. ZZ /\ k e. ZZ /\ M <_ k ) -> -. k < M )
12 11 a1d 
 |-  ( ( M e. ZZ /\ k e. ZZ /\ M <_ k ) -> ( M e. ZZ -> -. k < M ) )
13 6 12 sylbi 
 |-  ( k e. ( ZZ>= ` M ) -> ( M e. ZZ -> -. k < M ) )
14 13 impcom 
 |-  ( ( M e. ZZ /\ k e. ( ZZ>= ` M ) ) -> -. k < M )
15 3 4 5 14 infmin 
 |-  ( M e. ZZ -> inf ( ( ZZ>= ` M ) , RR , < ) = M )
16 1 15 ax-mp 
 |-  inf ( ( ZZ>= ` M ) , RR , < ) = M