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	$$⊢K\in \mathbb{Z}$$
Assertion	eluzaddi	$$⊢N\in {\mathbb{Z}}_{\ge M}\to N+K\in {\mathbb{Z}}_{\ge \left(M+K\right)}$$

Proof

Step	Hyp	Ref	Expression
1		eluzaddi.1	$$⊢K\in \mathbb{Z}$$
2		eluzadd	$$⊢\left(N\in {\mathbb{Z}}_{\ge M}\wedge K\in \mathbb{Z}\right)\to N+K\in {\mathbb{Z}}_{\ge \left(M+K\right)}$$
3	1 2	mpan2	$$⊢N\in {\mathbb{Z}}_{\ge M}\to N+K\in {\mathbb{Z}}_{\ge \left(M+K\right)}$$