Theorem uztrn

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

	Ref	Expression
Assertion	uztrn	⊢ ( ( 𝑀 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		eluzel2	⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) → 𝑁 ∈ ℤ )
2	1	adantl	⊢ ( ( 𝑀 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑁 ∈ ℤ )
3		eluzelz	⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝐾 ) → 𝑀 ∈ ℤ )
4	3	adantr	⊢ ( ( 𝑀 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑀 ∈ ℤ )
5		eluzle	⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) → 𝑁 ≤ 𝐾 )
6	5	adantl	⊢ ( ( 𝑀 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑁 ≤ 𝐾 )
7		eluzle	⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝐾 ) → 𝐾 ≤ 𝑀 )
8	7	adantr	⊢ ( ( 𝑀 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝐾 ≤ 𝑀 )
9		eluzelz	⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) → 𝐾 ∈ ℤ )
10		zletr	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( 𝑁 ≤ 𝐾 ∧ 𝐾 ≤ 𝑀 ) → 𝑁 ≤ 𝑀 ) )
11	1 9 4 10	syl2an23an	⊢ ( ( 𝑀 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝑁 ≤ 𝐾 ∧ 𝐾 ≤ 𝑀 ) → 𝑁 ≤ 𝑀 ) )
12	6 8 11	mp2and	⊢ ( ( 𝑀 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑁 ≤ 𝑀 )
13		eluz2	⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ↔ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ≤ 𝑀 ) )
14	2 4 12 13	syl3anbrc	⊢ ( ( 𝑀 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) )