eluzp1p1

Description: Membership in the next upper set of integers. (Contributed by NM, 5-Oct-2005)

		Ref	Expression
	Assertion	eluzp1p1	$⊢ N \in ℤ_{\geq M} \to N + 1 \in ℤ_{\geq (M + 1)}$

Step	Hyp	Ref	Expression
1		peano2z	$⊢ M \in ℤ \to M + 1 \in ℤ$
2	1	3ad2ant1	$⊢ (M \in ℤ \land N \in ℤ \land M \leq N) \to M + 1 \in ℤ$
3		peano2z	$⊢ N \in ℤ \to N + 1 \in ℤ$
4	3	3ad2ant2	$⊢ (M \in ℤ \land N \in ℤ \land M \leq N) \to N + 1 \in ℤ$
5		zre	$⊢ M \in ℤ \to M \in ℝ$
6		zre	$⊢ N \in ℤ \to N \in ℝ$
7		1re	$⊢ 1 \in ℝ$
8		leadd1	$⊢ (M \in ℝ \land N \in ℝ \land 1 \in ℝ) \to (M \leq N \leftrightarrow M + 1 \leq N + 1)$
9	7 8	mp3an3	$⊢ (M \in ℝ \land N \in ℝ) \to (M \leq N \leftrightarrow M + 1 \leq N + 1)$
10	5 6 9	syl2an	$⊢ (M \in ℤ \land N \in ℤ) \to (M \leq N \leftrightarrow M + 1 \leq N + 1)$
11	10	biimp3a	$⊢ (M \in ℤ \land N \in ℤ \land M \leq N) \to M + 1 \leq N + 1$
12	2 4 11	3jca	$⊢ (M \in ℤ \land N \in ℤ \land M \leq N) \to (M + 1 \in ℤ \land N + 1 \in ℤ \land M + 1 \leq N + 1)$
13		eluz2	$⊢ N \in ℤ_{\geq M} \leftrightarrow (M \in ℤ \land N \in ℤ \land M \leq N)$
14		eluz2	$⊢ N + 1 \in ℤ_{\geq (M + 1)} \leftrightarrow (M + 1 \in ℤ \land N + 1 \in ℤ \land M + 1 \leq N + 1)$
15	12 13 14	3imtr4i	$⊢ N \in ℤ_{\geq M} \to N + 1 \in ℤ_{\geq (M + 1)}$

Metamath Proof Explorer