Metamath Proof Explorer

Theorem eluzaddi

Description: Membership in a later upper set of integers. (Contributed by Paul Chapman, 22-Nov-2007)

Ref Expression
Hypotheses eluzaddi.1 ⊢ M ∈ ℤ
eluzaddi.2 ⊢ K ∈ ℤ
Assertion eluzaddi ⊢ N ∈ ℤ ≥ M → N + K ∈ ℤ ≥ M + K

Proof

Step Hyp Ref Expression
1 eluzaddi.1 ⊢ M ∈ ℤ
2 eluzaddi.2 ⊢ K ∈ ℤ
3 eluzelz ⊢ N ∈ ℤ ≥ M → N ∈ ℤ
4 zaddcl ⊢ N ∈ ℤ ∧ K ∈ ℤ → N + K ∈ ℤ
5 3 2 4 sylancl ⊢ N ∈ ℤ ≥ M → N + K ∈ ℤ
6 1 eluz1i ⊢ N ∈ ℤ ≥ M ↔ N ∈ ℤ ∧ M ≤ N
7 zre ⊢ N ∈ ℤ → N ∈ ℝ
8 1 zrei ⊢ M ∈ ℝ
9 2 zrei ⊢ K ∈ ℝ
10 leadd1 ⊢ M ∈ ℝ ∧ N ∈ ℝ ∧ K ∈ ℝ → M ≤ N ↔ M + K ≤ N + K
11 8 9 10 mp3an13 ⊢ N ∈ ℝ → M ≤ N ↔ M + K ≤ N + K
12 7 11 syl ⊢ N ∈ ℤ → M ≤ N ↔ M + K ≤ N + K
13 12 biimpa ⊢ N ∈ ℤ ∧ M ≤ N → M + K ≤ N + K
14 6 13 sylbi ⊢ N ∈ ℤ ≥ M → M + K ≤ N + K
15 zaddcl ⊢ M ∈ ℤ ∧ K ∈ ℤ → M + K ∈ ℤ
16 1 2 15 mp2an ⊢ M + K ∈ ℤ
17 16 eluz1i ⊢ N + K ∈ ℤ ≥ M + K ↔ N + K ∈ ℤ ∧ M + K ≤ N + K
18 5 14 17 sylanbrc ⊢ N ∈ ℤ ≥ M → N + K ∈ ℤ ≥ M + K