Metamath Proof Explorer

Theorem eluzmn

Description: Membership in an earlier upper set of integers. (Contributed by Thierry Arnoux, 8-Oct-2018)

Ref Expression
Assertion eluzmn ⊢ M ∈ ℤ ∧ N ∈ ℕ 0 → M ∈ ℤ ≥ M − N

Proof

Step Hyp Ref Expression
1 simpl ⊢ M ∈ ℤ ∧ N ∈ ℕ 0 → M ∈ ℤ
2 simpr ⊢ M ∈ ℤ ∧ N ∈ ℕ 0 → N ∈ ℕ 0
3 2 nn0zd ⊢ M ∈ ℤ ∧ N ∈ ℕ 0 → N ∈ ℤ
4 1 3 zsubcld ⊢ M ∈ ℤ ∧ N ∈ ℕ 0 → M − N ∈ ℤ
5 1 zred ⊢ M ∈ ℤ ∧ N ∈ ℕ 0 → M ∈ ℝ
6 2 nn0red ⊢ M ∈ ℤ ∧ N ∈ ℕ 0 → N ∈ ℝ
7 5 6 readdcld ⊢ M ∈ ℤ ∧ N ∈ ℕ 0 → M + N ∈ ℝ
8 nn0addge1 ⊢ M ∈ ℝ ∧ N ∈ ℕ 0 → M ≤ M + N
9 5 8 sylancom ⊢ M ∈ ℤ ∧ N ∈ ℕ 0 → M ≤ M + N
10 5 7 6 9 lesub1dd ⊢ M ∈ ℤ ∧ N ∈ ℕ 0 → M − N ≤ M + N - N
11 5 recnd ⊢ M ∈ ℤ ∧ N ∈ ℕ 0 → M ∈ ℂ
12 6 recnd ⊢ M ∈ ℤ ∧ N ∈ ℕ 0 → N ∈ ℂ
13 11 12 pncand ⊢ M ∈ ℤ ∧ N ∈ ℕ 0 → M + N - N = M
14 10 13 breqtrd ⊢ M ∈ ℤ ∧ N ∈ ℕ 0 → M − N ≤ M
15 eluz2 ⊢ M ∈ ℤ ≥ M − N ↔ M − N ∈ ℤ ∧ M ∈ ℤ ∧ M − N ≤ M
16 4 1 14 15 syl3anbrc ⊢ M ∈ ℤ ∧ N ∈ ℕ 0 → M ∈ ℤ ≥ M − N