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 \in ℤ$
	Assertion	uzinfi	$⊢ inf (ℤ_{\geq M} ℝ <) = M$

Step	Hyp	Ref	Expression
1		uzinfi.1	$⊢ M \in ℤ$
2		ltso	$⊢ < Or ℝ$
3	2	a1i	$⊢ M \in ℤ \to < Or ℝ$
4		zre	$⊢ M \in ℤ \to M \in ℝ$
5		uzid	$⊢ M \in ℤ \to M \in ℤ_{\geq M}$
6		eluz2	$⊢ k \in ℤ_{\geq M} \leftrightarrow (M \in ℤ \land k \in ℤ \land M \leq k)$
7	4	adantr	$⊢ (M \in ℤ \land k \in ℤ) \to M \in ℝ$
8		zre	$⊢ k \in ℤ \to k \in ℝ$
9	8	adantl	$⊢ (M \in ℤ \land k \in ℤ) \to k \in ℝ$
10	7 9	lenltd	$⊢ (M \in ℤ \land k \in ℤ) \to (M \leq k \leftrightarrow \neg k < M)$
11	10	biimp3a	$⊢ (M \in ℤ \land k \in ℤ \land M \leq k) \to \neg k < M$
12	11	a1d	$⊢ (M \in ℤ \land k \in ℤ \land M \leq k) \to (M \in ℤ \to \neg k < M)$
13	6 12	sylbi	$⊢ k \in ℤ_{\geq M} \to (M \in ℤ \to \neg k < M)$
14	13	impcom	$⊢ (M \in ℤ \land k \in ℤ_{\geq M}) \to \neg k < M$
15	3 4 5 14	infmin	$⊢ M \in ℤ \to inf (ℤ_{\geq M} ℝ <) = M$
16	1 15	ax-mp	$⊢ inf (ℤ_{\geq M} ℝ <) = M$

Metamath Proof Explorer