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