Theorem eluzaddi

Description: Membership in a later upper set of integers. (Contributed by Paul Chapman, 22-Nov-2007) Shorten and remove M e. ZZ hypothesis. (Revised by SN, 7-Feb-2025)

	Ref	Expression
Hypothesis	eluzaddi.1	⊢ 𝐾 ∈ ℤ
Assertion	eluzaddi	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 + 𝐾 ) ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eluzaddi.1	⊢ 𝐾 ∈ ℤ
2		eluzadd	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐾 ∈ ℤ ) → ( 𝑁 + 𝐾 ) ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) )
3	1 2	mpan2	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 + 𝐾 ) ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) )