uztrn

Description: Transitive law for sets of upper integers. (Contributed by NM, 20-Sep-2005)

		Ref	Expression
	Assertion	uztrn	$⊢ (M \in ℤ_{\geq K} \land K \in ℤ_{\geq N}) \to M \in ℤ_{\geq N}$

Step	Hyp	Ref	Expression
1		eluzel2	$⊢ K \in ℤ_{\geq N} \to N \in ℤ$
2	1	adantl	$⊢ (M \in ℤ_{\geq K} \land K \in ℤ_{\geq N}) \to N \in ℤ$
3		eluzelz	$⊢ M \in ℤ_{\geq K} \to M \in ℤ$
4	3	adantr	$⊢ (M \in ℤ_{\geq K} \land K \in ℤ_{\geq N}) \to M \in ℤ$
5		eluzle	$⊢ K \in ℤ_{\geq N} \to N \leq K$
6	5	adantl	$⊢ (M \in ℤ_{\geq K} \land K \in ℤ_{\geq N}) \to N \leq K$
7		eluzle	$⊢ M \in ℤ_{\geq K} \to K \leq M$
8	7	adantr	$⊢ (M \in ℤ_{\geq K} \land K \in ℤ_{\geq N}) \to K \leq M$
9		eluzelz	$⊢ K \in ℤ_{\geq N} \to K \in ℤ$
10		zletr	$⊢ (N \in ℤ \land K \in ℤ \land M \in ℤ) \to ((N \leq K \land K \leq M) \to N \leq M)$
11	1 9 4 10	syl2an23an	$⊢ (M \in ℤ_{\geq K} \land K \in ℤ_{\geq N}) \to ((N \leq K \land K \leq M) \to N \leq M)$
12	6 8 11	mp2and	$⊢ (M \in ℤ_{\geq K} \land K \in ℤ_{\geq N}) \to N \leq M$
13		eluz2	$⊢ M \in ℤ_{\geq N} \leftrightarrow (N \in ℤ \land M \in ℤ \land N \leq M)$
14	2 4 12 13	syl3anbrc	$⊢ (M \in ℤ_{\geq K} \land K \in ℤ_{\geq N}) \to M \in ℤ_{\geq N}$

Metamath Proof Explorer