Metamath Proof Explorer

Theorem eluzaddiOLD

Description: Obsolete version of eluzaddi as of 7-Feb-2025. (Contributed by Paul Chapman, 22-Nov-2007) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	eluzsubi.1	$⊢ M \in ℤ$
		eluzsubi.2	$⊢ K \in ℤ$
	Assertion	eluzaddiOLD	$⊢ N \in ℤ_{\geq M} \to N + K \in ℤ_{\geq (M + K)}$

Proof

Step	Hyp	Ref	Expression
1		eluzsubi.1	$⊢ M \in ℤ$
2		eluzsubi.2	$⊢ K \in ℤ$
3		eluzelz	$⊢ N \in ℤ_{\geq M} \to N \in ℤ$
4		zaddcl	$⊢ (N \in ℤ \land K \in ℤ) \to N + K \in ℤ$
5	3 2 4	sylancl	$⊢ N \in ℤ_{\geq M} \to N + K \in ℤ$
6	1	eluz1i	$⊢ N \in ℤ_{\geq M} \leftrightarrow (N \in ℤ \land M \leq N)$
7		zre	$⊢ N \in ℤ \to N \in ℝ$
8	1	zrei	$⊢ M \in ℝ$
9	2	zrei	$⊢ K \in ℝ$
10		leadd1	$⊢ (M \in ℝ \land N \in ℝ \land K \in ℝ) \to (M \leq N \leftrightarrow M + K \leq N + K)$
11	8 9 10	mp3an13	$⊢ N \in ℝ \to (M \leq N \leftrightarrow M + K \leq N + K)$
12	7 11	syl	$⊢ N \in ℤ \to (M \leq N \leftrightarrow M + K \leq N + K)$
13	12	biimpa	$⊢ (N \in ℤ \land M \leq N) \to M + K \leq N + K$
14	6 13	sylbi	$⊢ N \in ℤ_{\geq M} \to M + K \leq N + K$
15		zaddcl	$⊢ (M \in ℤ \land K \in ℤ) \to M + K \in ℤ$
16	1 2 15	mp2an	$⊢ M + K \in ℤ$
17	16	eluz1i	$⊢ N + K \in ℤ_{\geq (M + K)} \leftrightarrow (N + K \in ℤ \land M + K \leq N + K)$
18	5 14 17	sylanbrc	$⊢ N \in ℤ_{\geq M} \to N + K \in ℤ_{\geq (M + K)}$