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