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

Metamath Proof Explorer

Theorem uzss

Description: Subset relationship for two sets of upper integers. (Contributed by NM, 5-Sep-2005)

Ref Expression
Assertion uzss ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ℤ≥ ‘ 𝑁 ) ⊆ ( ℤ≥ ‘ 𝑀 ) )

Proof

Step Hyp Ref Expression
1 eluzle ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ≤ 𝑁 )
2 1 adantr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑘 ∈ ℤ ) → 𝑀 ≤ 𝑁 )
3 eluzel2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
4 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ℤ )
5 3 4 jca ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
6 zletr ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( ( 𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑘 ) → 𝑀 ≤ 𝑘 ) )
7 6 3expa ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑘 ∈ ℤ ) → ( ( 𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑘 ) → 𝑀 ≤ 𝑘 ) )
8 5 7 sylan ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑘 ∈ ℤ ) → ( ( 𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑘 ) → 𝑀 ≤ 𝑘 ) )
9 2 8 mpand ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑘 ∈ ℤ ) → ( 𝑁 ≤ 𝑘 → 𝑀 ≤ 𝑘 ) )
10 9 imdistanda ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑘 ∈ ℤ ∧ 𝑁 ≤ 𝑘 ) → ( 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ) ) )
11 eluz1 ⊢ ( 𝑁 ∈ ℤ → ( 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ↔ ( 𝑘 ∈ ℤ ∧ 𝑁 ≤ 𝑘 ) ) )
12 4 11 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ↔ ( 𝑘 ∈ ℤ ∧ 𝑁 ≤ 𝑘 ) ) )
13 eluz1 ⊢ ( 𝑀 ∈ ℤ → ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ) ) )
14 3 13 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ) ) )
15 10 12 14 3imtr4d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) )
16 15 ssrdv ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ℤ≥ ‘ 𝑁 ) ⊆ ( ℤ≥ ‘ 𝑀 ) )