Metamath Proof Explorer

Theorem eluzsubi

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

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

Proof

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