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