Theorem uztrn2

Description: Transitive law for sets of upper integers. (Contributed by Mario Carneiro, 26-Dec-2013)

	Ref	Expression
Hypothesis	uztrn2.1	$$⊢Z={\mathbb{Z}}_{\ge K}$$
Assertion	uztrn2	$$⊢\left(N\in Z\wedge M\in {\mathbb{Z}}_{\ge N}\right)\to M\in Z$$

Proof

Step	Hyp	Ref	Expression
1		uztrn2.1	$$⊢Z={\mathbb{Z}}_{\ge K}$$
2	1	eleq2i	$$⊢N\in Z\leftrightarrow N\in {\mathbb{Z}}_{\ge K}$$
3		uztrn	$$⊢\left(M\in {\mathbb{Z}}_{\ge N}\wedge N\in {\mathbb{Z}}_{\ge K}\right)\to M\in {\mathbb{Z}}_{\ge K}$$
4	3	ancoms	$$⊢\left(N\in {\mathbb{Z}}_{\ge K}\wedge M\in {\mathbb{Z}}_{\ge N}\right)\to M\in {\mathbb{Z}}_{\ge K}$$
5	2 4	sylanb	$$⊢\left(N\in Z\wedge M\in {\mathbb{Z}}_{\ge N}\right)\to M\in {\mathbb{Z}}_{\ge K}$$
6	5 1	eleqtrrdi	$$⊢\left(N\in Z\wedge M\in {\mathbb{Z}}_{\ge N}\right)\to M\in Z$$