eluzp1m1

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

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

Step	Hyp	Ref	Expression
1		peano2zm	$⊢ N \in ℤ \to N - 1 \in ℤ$
2	1	ad2antrl	$⊢ (M \in ℤ \land (N \in ℤ \land M + 1 \leq N)) \to N - 1 \in ℤ$
3		zre	$⊢ M \in ℤ \to M \in ℝ$
4		zre	$⊢ N \in ℤ \to N \in ℝ$
5		1re	$⊢ 1 \in ℝ$
6		leaddsub	$⊢ (M \in ℝ \land 1 \in ℝ \land N \in ℝ) \to (M + 1 \leq N \leftrightarrow M \leq N - 1)$
7	5 6	mp3an2	$⊢ (M \in ℝ \land N \in ℝ) \to (M + 1 \leq N \leftrightarrow M \leq N - 1)$
8	3 4 7	syl2an	$⊢ (M \in ℤ \land N \in ℤ) \to (M + 1 \leq N \leftrightarrow M \leq N - 1)$
9	8	biimpa	$⊢ ((M \in ℤ \land N \in ℤ) \land M + 1 \leq N) \to M \leq N - 1$
10	9	anasss	$⊢ (M \in ℤ \land (N \in ℤ \land M + 1 \leq N)) \to M \leq N - 1$
11	2 10	jca	$⊢ (M \in ℤ \land (N \in ℤ \land M + 1 \leq N)) \to (N - 1 \in ℤ \land M \leq N - 1)$
12	11	ex	$⊢ M \in ℤ \to ((N \in ℤ \land M + 1 \leq N) \to (N - 1 \in ℤ \land M \leq N - 1))$
13		peano2z	$⊢ M \in ℤ \to M + 1 \in ℤ$
14		eluz1	$⊢ M + 1 \in ℤ \to (N \in ℤ_{\geq (M + 1)} \leftrightarrow (N \in ℤ \land M + 1 \leq N))$
15	13 14	syl	$⊢ M \in ℤ \to (N \in ℤ_{\geq (M + 1)} \leftrightarrow (N \in ℤ \land M + 1 \leq N))$
16		eluz1	$⊢ M \in ℤ \to (N - 1 \in ℤ_{\geq M} \leftrightarrow (N - 1 \in ℤ \land M \leq N - 1))$
17	12 15 16	3imtr4d	$⊢ M \in ℤ \to (N \in ℤ_{\geq (M + 1)} \to N - 1 \in ℤ_{\geq M})$
18	17	imp	$⊢ (M \in ℤ \land N \in ℤ_{\geq (M + 1)}) \to N - 1 \in ℤ_{\geq M}$

Metamath Proof Explorer