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	$⊢ (N \in ℤ_{\geq M} \land K \in ℤ) \to N + K \in ℤ_{\geq (M + K)}$

Step	Hyp	Ref	Expression
1		eluzel2	$⊢ N \in ℤ_{\geq M} \to M \in ℤ$
2		zaddcl	$⊢ (M \in ℤ \land K \in ℤ) \to M + K \in ℤ$
3	1 2	sylan	$⊢ (N \in ℤ_{\geq M} \land K \in ℤ) \to M + K \in ℤ$
4		eluzelz	$⊢ N \in ℤ_{\geq M} \to N \in ℤ$
5		zaddcl	$⊢ (N \in ℤ \land K \in ℤ) \to N + K \in ℤ$
6	4 5	sylan	$⊢ (N \in ℤ_{\geq M} \land K \in ℤ) \to N + K \in ℤ$
7	1	zred	$⊢ N \in ℤ_{\geq M} \to M \in ℝ$
8	7	adantr	$⊢ (N \in ℤ_{\geq M} \land K \in ℤ) \to M \in ℝ$
9		eluzelre	$⊢ N \in ℤ_{\geq M} \to N \in ℝ$
10	9	adantr	$⊢ (N \in ℤ_{\geq M} \land K \in ℤ) \to N \in ℝ$
11		zre	$⊢ K \in ℤ \to K \in ℝ$
12	11	adantl	$⊢ (N \in ℤ_{\geq M} \land K \in ℤ) \to K \in ℝ$
13		eluzle	$⊢ N \in ℤ_{\geq M} \to M \leq N$
14	13	adantr	$⊢ (N \in ℤ_{\geq M} \land K \in ℤ) \to M \leq N$
15	8 10 12 14	leadd1dd	$⊢ (N \in ℤ_{\geq M} \land K \in ℤ) \to M + K \leq N + K$
16		eluz2	$⊢ N + K \in ℤ_{\geq (M + K)} \leftrightarrow (M + K \in ℤ \land N + K \in ℤ \land M + K \leq N + K)$
17	3 6 15 16	syl3anbrc	$⊢ (N \in ℤ_{\geq M} \land K \in ℤ) \to N + K \in ℤ_{\geq (M + K)}$

Metamath Proof Explorer