Metamath Proof Explorer
Description: Membership in an earlier upper set of integers. (Contributed by Paul
Chapman, 22-Nov-2007) (Proof shortened by SN, 7-Feb-2025)
|
|
Ref |
Expression |
|
Hypotheses |
eluzsubi.1 |
⊢ 𝑀 ∈ ℤ |
|
|
eluzsubi.2 |
⊢ 𝐾 ∈ ℤ |
|
Assertion |
eluzsubi |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) → ( 𝑁 − 𝐾 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
eluzsubi.1 |
⊢ 𝑀 ∈ ℤ |
2 |
|
eluzsubi.2 |
⊢ 𝐾 ∈ ℤ |
3 |
|
eluzsub |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) ) → ( 𝑁 − 𝐾 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) |
4 |
1 2 3
|
mp3an12 |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) → ( 𝑁 − 𝐾 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) |