Metamath Proof Explorer

Theorem subeluzsub

Description: Membership of a difference in an earlier upper set of integers. (Contributed by AV, 10-May-2022)

Ref Expression
Assertion subeluzsub ⊢ M ∈ ℤ ∧ N ∈ ℤ ≥ K → M − K ∈ ℤ ≥ M − N

Proof

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