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

Metamath Proof Explorer

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 ∈ ℤ
Assertion eluzaddi ⊢ N ∈ ℤ ≥ M → N + K ∈ ℤ ≥ M + K

Proof

Step Hyp Ref Expression
1 eluzaddi.1 ⊢ K ∈ ℤ
2 eluzadd ⊢ N ∈ ℤ ≥ M ∧ K ∈ ℤ → N + K ∈ ℤ ≥ M + K
3 1 2 mpan2 ⊢ N ∈ ℤ ≥ M → N + K ∈ ℤ ≥ M + K