Theorem eluzsubi

Description: Membership in an earlier upper set of integers. (Contributed by Paul Chapman, 22-Nov-2007) (Proof shortened by SN, 7-Feb-2025)

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

Proof

Step	Hyp	Ref	Expression
1		eluzsubi.1	⊢ 𝑀 ∈ ℤ
2		eluzsubi.2	⊢ 𝐾 ∈ ℤ
3		eluzsub	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) ) → ( 𝑁 − 𝐾 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
4	1 2 3	mp3an12	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) → ( 𝑁 − 𝐾 ) ∈ ( ℤ≥ ‘ 𝑀 ) )