Theorem eluzsubi

Description: Membership in an earlier upper set of integers. (Contributed by Paul Chapman, 22-Nov-2007)

	Ref	Expression
Hypotheses	eluzaddi.1	⊢ 𝑀 ∈ ℤ
	eluzaddi.2	⊢ 𝐾 ∈ ℤ
Assertion	eluzsubi	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) → ( 𝑁 − 𝐾 ) ∈ ( ℤ≥ ‘ 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		eluzaddi.1	⊢ 𝑀 ∈ ℤ
2		eluzaddi.2	⊢ 𝐾 ∈ ℤ
3		eluzelz	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) → 𝑁 ∈ ℤ )
4		zsubcl	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑁 − 𝐾 ) ∈ ℤ )
5	3 2 4	sylancl	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) → ( 𝑁 − 𝐾 ) ∈ ℤ )
6		zaddcl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑀 + 𝐾 ) ∈ ℤ )
7	1 2 6	mp2an	⊢ ( 𝑀 + 𝐾 ) ∈ ℤ
8	7	eluz1i	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) ↔ ( 𝑁 ∈ ℤ ∧ ( 𝑀 + 𝐾 ) ≤ 𝑁 ) )
9	1	zrei	⊢ 𝑀 ∈ ℝ
10	2	zrei	⊢ 𝐾 ∈ ℝ
11		zre	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
12		leaddsub	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 𝑀 + 𝐾 ) ≤ 𝑁 ↔ 𝑀 ≤ ( 𝑁 − 𝐾 ) ) )
13	9 10 11 12	mp3an12i	⊢ ( 𝑁 ∈ ℤ → ( ( 𝑀 + 𝐾 ) ≤ 𝑁 ↔ 𝑀 ≤ ( 𝑁 − 𝐾 ) ) )
14	13	biimpa	⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝑀 + 𝐾 ) ≤ 𝑁 ) → 𝑀 ≤ ( 𝑁 − 𝐾 ) )
15	8 14	sylbi	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) → 𝑀 ≤ ( 𝑁 − 𝐾 ) )
16	1	eluz1i	⊢ ( ( 𝑁 − 𝐾 ) ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( ( 𝑁 − 𝐾 ) ∈ ℤ ∧ 𝑀 ≤ ( 𝑁 − 𝐾 ) ) )
17	5 15 16	sylanbrc	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) → ( 𝑁 − 𝐾 ) ∈ ( ℤ≥ ‘ 𝑀 ) )