Theorem eluzaddi

Description: Membership in a later upper set of integers. (Contributed by Paul Chapman, 22-Nov-2007)

	Ref	Expression
Hypotheses	eluzaddi.1	⊢ 𝑀 ∈ ℤ
	eluzaddi.2	⊢ 𝐾 ∈ ℤ
Assertion	eluzaddi	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 + 𝐾 ) ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eluzaddi.1	⊢ 𝑀 ∈ ℤ
2		eluzaddi.2	⊢ 𝐾 ∈ ℤ
3		eluzelz	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ℤ )
4		zaddcl	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑁 + 𝐾 ) ∈ ℤ )
5	3 2 4	sylancl	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 + 𝐾 ) ∈ ℤ )
6	1	eluz1i	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) )
7		zre	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
8	1	zrei	⊢ 𝑀 ∈ ℝ
9	2	zrei	⊢ 𝐾 ∈ ℝ
10		leadd1	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐾 ∈ ℝ ) → ( 𝑀 ≤ 𝑁 ↔ ( 𝑀 + 𝐾 ) ≤ ( 𝑁 + 𝐾 ) ) )
11	8 9 10	mp3an13	⊢ ( 𝑁 ∈ ℝ → ( 𝑀 ≤ 𝑁 ↔ ( 𝑀 + 𝐾 ) ≤ ( 𝑁 + 𝐾 ) ) )
12	7 11	syl	⊢ ( 𝑁 ∈ ℤ → ( 𝑀 ≤ 𝑁 ↔ ( 𝑀 + 𝐾 ) ≤ ( 𝑁 + 𝐾 ) ) )
13	12	biimpa	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) → ( 𝑀 + 𝐾 ) ≤ ( 𝑁 + 𝐾 ) )
14	6 13	sylbi	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑀 + 𝐾 ) ≤ ( 𝑁 + 𝐾 ) )
15		zaddcl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑀 + 𝐾 ) ∈ ℤ )
16	1 2 15	mp2an	⊢ ( 𝑀 + 𝐾 ) ∈ ℤ
17	16	eluz1i	⊢ ( ( 𝑁 + 𝐾 ) ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) ↔ ( ( 𝑁 + 𝐾 ) ∈ ℤ ∧ ( 𝑀 + 𝐾 ) ≤ ( 𝑁 + 𝐾 ) ) )
18	5 14 17	sylanbrc	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 + 𝐾 ) ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) )