This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∈ ℤ
eluzsubi.2 ⊢ K ∈ ℤ
Assertion eluzsubi ⊢ N ∈ ℤ ≥ M + K → N − K ∈ ℤ ≥ M

Proof

Step Hyp Ref Expression
1 eluzsubi.1 ⊢ M ∈ ℤ
2 eluzsubi.2 ⊢ K ∈ ℤ
3 eluzsub ⊢ M ∈ ℤ ∧ K ∈ ℤ ∧ N ∈ ℤ ≥ M + K → N − K ∈ ℤ ≥ M
4 1 2 3 mp3an12 ⊢ N ∈ ℤ ≥ M + K → N − K ∈ ℤ ≥ M