Theorem uztrn

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

	Ref	Expression
Assertion	uztrn	$$⊢\left(M\in {\mathbb{Z}}_{\ge K}\wedge K\in {\mathbb{Z}}_{\ge N}\right)\to M\in {\mathbb{Z}}_{\ge N}$$

Proof

Step	Hyp	Ref	Expression
1		eluzel2	$$⊢K\in {\mathbb{Z}}_{\ge N}\to N\in \mathbb{Z}$$
2	1	adantl	$$⊢\left(M\in {\mathbb{Z}}_{\ge K}\wedge K\in {\mathbb{Z}}_{\ge N}\right)\to N\in \mathbb{Z}$$
3		eluzelz	$$⊢M\in {\mathbb{Z}}_{\ge K}\to M\in \mathbb{Z}$$
4	3	adantr	$$⊢\left(M\in {\mathbb{Z}}_{\ge K}\wedge K\in {\mathbb{Z}}_{\ge N}\right)\to M\in \mathbb{Z}$$
5		eluzle	$$⊢K\in {\mathbb{Z}}_{\ge N}\to N\le K$$
6	5	adantl	$$⊢\left(M\in {\mathbb{Z}}_{\ge K}\wedge K\in {\mathbb{Z}}_{\ge N}\right)\to N\le K$$
7		eluzle	$$⊢M\in {\mathbb{Z}}_{\ge K}\to K\le M$$
8	7	adantr	$$⊢\left(M\in {\mathbb{Z}}_{\ge K}\wedge K\in {\mathbb{Z}}_{\ge N}\right)\to K\le M$$
9		eluzelz	$$⊢K\in {\mathbb{Z}}_{\ge N}\to K\in \mathbb{Z}$$
10		zletr	$$⊢\left(N\in \mathbb{Z}\wedge K\in \mathbb{Z}\wedge M\in \mathbb{Z}\right)\to \left(\left(N\le K\wedge K\le M\right)\to N\le M\right)$$
11	1 9 4 10	syl2an23an	$$⊢\left(M\in {\mathbb{Z}}_{\ge K}\wedge K\in {\mathbb{Z}}_{\ge N}\right)\to \left(\left(N\le K\wedge K\le M\right)\to N\le M\right)$$
12	6 8 11	mp2and	$$⊢\left(M\in {\mathbb{Z}}_{\ge K}\wedge K\in {\mathbb{Z}}_{\ge N}\right)\to N\le M$$
13		eluz2	$$⊢M\in {\mathbb{Z}}_{\ge N}\leftrightarrow \left(N\in \mathbb{Z}\wedge M\in \mathbb{Z}\wedge N\le M\right)$$
14	2 4 12 13	syl3anbrc	$$⊢\left(M\in {\mathbb{Z}}_{\ge K}\wedge K\in {\mathbb{Z}}_{\ge N}\right)\to M\in {\mathbb{Z}}_{\ge N}$$