Metamath Proof Explorer

Theorem eluzadd

Description: Membership in a later upper set of integers. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by SN, 7-Feb-2025)

Ref Expression
Assertion eluzadd ⊢ N ∈ ℤ ≥ M ∧ K ∈ ℤ → N + K ∈ ℤ ≥ M + K

Proof

Step Hyp Ref Expression
1 eluzel2 ⊢ N ∈ ℤ ≥ M → M ∈ ℤ
2 zaddcl ⊢ M ∈ ℤ ∧ K ∈ ℤ → M + K ∈ ℤ
3 1 2 sylan ⊢ N ∈ ℤ ≥ M ∧ K ∈ ℤ → M + K ∈ ℤ
4 eluzelz ⊢ N ∈ ℤ ≥ M → N ∈ ℤ
5 zaddcl ⊢ N ∈ ℤ ∧ K ∈ ℤ → N + K ∈ ℤ
6 4 5 sylan ⊢ N ∈ ℤ ≥ M ∧ K ∈ ℤ → N + K ∈ ℤ
7 1 zred ⊢ N ∈ ℤ ≥ M → M ∈ ℝ
8 7 adantr ⊢ N ∈ ℤ ≥ M ∧ K ∈ ℤ → M ∈ ℝ
9 eluzelre ⊢ N ∈ ℤ ≥ M → N ∈ ℝ
10 9 adantr ⊢ N ∈ ℤ ≥ M ∧ K ∈ ℤ → N ∈ ℝ
11 zre ⊢ K ∈ ℤ → K ∈ ℝ
12 11 adantl ⊢ N ∈ ℤ ≥ M ∧ K ∈ ℤ → K ∈ ℝ
13 eluzle ⊢ N ∈ ℤ ≥ M → M ≤ N
14 13 adantr ⊢ N ∈ ℤ ≥ M ∧ K ∈ ℤ → M ≤ N
15 8 10 12 14 leadd1dd ⊢ N ∈ ℤ ≥ M ∧ K ∈ ℤ → M + K ≤ N + K
16 eluz2 ⊢ N + K ∈ ℤ ≥ M + K ↔ M + K ∈ ℤ ∧ N + K ∈ ℤ ∧ M + K ≤ N + K
17 3 6 15 16 syl3anbrc ⊢ N ∈ ℤ ≥ M ∧ K ∈ ℤ → N + K ∈ ℤ ≥ M + K