This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( 𝑀 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) )