| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > zsubcl | Structured version Visualization version GIF version | ||
| Description: Closure of subtraction of integers. (Contributed by NM, 11-May-2004.) |
| Ref | Expression |
|---|---|
| zsubcl | ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 − 𝑁) ∈ ℤ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | zcn 12618 | . . 3 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℂ) | |
| 2 | zcn 12618 | . . 3 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℂ) | |
| 3 | negsub 11557 | . . 3 ⊢ ((𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (𝑀 + -𝑁) = (𝑀 − 𝑁)) | |
| 4 | 1, 2, 3 | syl2an 596 | . 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 + -𝑁) = (𝑀 − 𝑁)) |
| 5 | znegcl 12652 | . . 3 ⊢ (𝑁 ∈ ℤ → -𝑁 ∈ ℤ) | |
| 6 | zaddcl 12657 | . . 3 ⊢ ((𝑀 ∈ ℤ ∧ -𝑁 ∈ ℤ) → (𝑀 + -𝑁) ∈ ℤ) | |
| 7 | 5, 6 | sylan2 593 | . 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 + -𝑁) ∈ ℤ) |
| 8 | 4, 7 | eqeltrrd 2842 | 1 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 − 𝑁) ∈ ℤ) |
| Copyright terms: Public domain | W3C validator |