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

Metamath Proof Explorer

Theorem subeluzsub

Description: Membership of a difference in an earlier upper set of integers. (Contributed by AV, 10-May-2022)

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

Proof

Step Hyp Ref Expression
1 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) → 𝑁 ∈ ℤ )
2 zsubcl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 − 𝑁 ) ∈ ℤ )
3 1 2 sylan2 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝑀 − 𝑁 ) ∈ ℤ )
4 eluzel2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) → 𝐾 ∈ ℤ )
5 zsubcl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑀 − 𝐾 ) ∈ ℤ )
6 4 5 sylan2 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝑀 − 𝐾 ) ∈ ℤ )
7 4 zred ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) → 𝐾 ∈ ℝ )
8 7 adantl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝐾 ∈ ℝ )
9 1 zred ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) → 𝑁 ∈ ℝ )
10 9 adantl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝑁 ∈ ℝ )
11 zre ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
12 11 adantr ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝑀 ∈ ℝ )
13 eluzle ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) → 𝐾 ≤ 𝑁 )
14 13 adantl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝐾 ≤ 𝑁 )
15 8 10 12 14 lesub2dd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝑀 − 𝑁 ) ≤ ( 𝑀 − 𝐾 ) )
16 eluz2 ⊢ ( ( 𝑀 − 𝐾 ) ∈ ( ℤ≥ ‘ ( 𝑀 − 𝑁 ) ) ↔ ( ( 𝑀 − 𝑁 ) ∈ ℤ ∧ ( 𝑀 − 𝐾 ) ∈ ℤ ∧ ( 𝑀 − 𝑁 ) ≤ ( 𝑀 − 𝐾 ) ) )
17 3 6 15 16 syl3anbrc ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝑀 − 𝐾 ) ∈ ( ℤ≥ ‘ ( 𝑀 − 𝑁 ) ) )