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

Proof

Step	Hyp	Ref	Expression
1		eluzsubi.1	$$⊢M\in \mathbb{Z}$$
2		eluzsubi.2	$$⊢K\in \mathbb{Z}$$
3		eluzsub	$$⊢\left(M\in \mathbb{Z}\wedge K\in \mathbb{Z}\wedge N\in {\mathbb{Z}}_{\ge \left(M+K\right)}\right)\to N-K\in {\mathbb{Z}}_{\ge M}$$
4	1 2 3	mp3an12	$$⊢N\in {\mathbb{Z}}_{\ge \left(M+K\right)}\to N-K\in {\mathbb{Z}}_{\ge M}$$