Metamath Proof Explorer


Theorem eluzsubi

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 ( 𝑁 ∈ ( ℤ ‘ ( 𝑀 + 𝐾 ) ) → ( 𝑁𝐾 ) ∈ ( ℤ𝑀 ) )