Theorem subeluzsub

Description: Membership of a difference in an earlier upper set of integers. (Contributed by AV, 10-May-2022)

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

Proof

Step	Hyp	Ref	Expression
1		eluzelz	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) → 𝑁 ∈ ℤ )
2		zsubcl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 − 𝑁 ) ∈ ℤ )
3	1 2	sylan2	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝑀 − 𝑁 ) ∈ ℤ )
4		eluzel2	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) → 𝐾 ∈ ℤ )
5		zsubcl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑀 − 𝐾 ) ∈ ℤ )
6	4 5	sylan2	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝑀 − 𝐾 ) ∈ ℤ )
7	4	zred	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) → 𝐾 ∈ ℝ )
8	7	adantl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝐾 ∈ ℝ )
9	1	zred	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) → 𝑁 ∈ ℝ )
10	9	adantl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝑁 ∈ ℝ )
11		zre	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
12	11	adantr	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝑀 ∈ ℝ )
13		eluzle	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) → 𝐾 ≤ 𝑁 )
14	13	adantl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝐾 ≤ 𝑁 )
15	8 10 12 14	lesub2dd	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝑀 − 𝑁 ) ≤ ( 𝑀 − 𝐾 ) )
16		eluz2	⊢ ( ( 𝑀 − 𝐾 ) ∈ ( ℤ≥ ‘ ( 𝑀 − 𝑁 ) ) ↔ ( ( 𝑀 − 𝑁 ) ∈ ℤ ∧ ( 𝑀 − 𝐾 ) ∈ ℤ ∧ ( 𝑀 − 𝑁 ) ≤ ( 𝑀 − 𝐾 ) ) )
17	3 6 15 16	syl3anbrc	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝑀 − 𝐾 ) ∈ ( ℤ≥ ‘ ( 𝑀 − 𝑁 ) ) )