This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem eluzsub

Description: Membership in an earlier upper set of integers. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by SN, 7-Feb-2025)

Ref Expression
Assertion eluzsub ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) ) → ( 𝑁 − 𝐾 ) ∈ ( ℤ≥ ‘ 𝑀 ) )

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) ) → 𝑀 ∈ ℤ )
2 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) → 𝑁 ∈ ℤ )
3 2 3ad2ant3 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) ) → 𝑁 ∈ ℤ )
4 simp2 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) ) → 𝐾 ∈ ℤ )
5 3 4 zsubcld ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) ) → ( 𝑁 − 𝐾 ) ∈ ℤ )
6 eluzle ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) → ( 𝑀 + 𝐾 ) ≤ 𝑁 )
7 6 3ad2ant3 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) ) → ( 𝑀 + 𝐾 ) ≤ 𝑁 )
8 zre ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
9 zre ⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℝ )
10 eluzelre ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) → 𝑁 ∈ ℝ )
11 leaddsub ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 𝑀 + 𝐾 ) ≤ 𝑁 ↔ 𝑀 ≤ ( 𝑁 − 𝐾 ) ) )
12 8 9 10 11 syl3an ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) ) → ( ( 𝑀 + 𝐾 ) ≤ 𝑁 ↔ 𝑀 ≤ ( 𝑁 − 𝐾 ) ) )
13 7 12 mpbid ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) ) → 𝑀 ≤ ( 𝑁 − 𝐾 ) )
14 eluz2 ⊢ ( ( 𝑁 − 𝐾 ) ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ ( 𝑁 − 𝐾 ) ∈ ℤ ∧ 𝑀 ≤ ( 𝑁 − 𝐾 ) ) )
15 1 5 13 14 syl3anbrc ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) ) → ( 𝑁 − 𝐾 ) ∈ ( ℤ≥ ‘ 𝑀 ) )