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

Metamath Proof Explorer

Theorem eluzadd

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

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

Proof

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