Metamath Proof Explorer

Theorem eluzaddiOLD

Description: Obsolete version of eluzaddi as of 7-Feb-2025. (Contributed by Paul Chapman, 22-Nov-2007) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 eluzsubi.1 ⊢ M ∈ ℤ
2 eluzsubi.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