preduz

Description: The value of the predecessor class over an upper integer set. (Contributed by Scott Fenton, 16-May-2014)

		Ref	Expression
	Assertion	preduz	$⊢ N \in ℤ_{\geq M} \to Pred (< ℤ_{\geq M} N) = (M \dots N - 1)$

Proof

Step	Hyp	Ref	Expression
1		vex	$⊢ x \in V$
2	1	elpred	$⊢ N \in ℤ_{\geq M} \to (x \in Pred (< ℤ_{\geq M} N) \leftrightarrow (x \in ℤ_{\geq M} \land x < N))$
3		eluzelz	$⊢ x \in ℤ_{\geq M} \to x \in ℤ$
4		eluzelz	$⊢ N \in ℤ_{\geq M} \to N \in ℤ$
5		zltlem1	$⊢ (x \in ℤ \land N \in ℤ) \to (x < N \leftrightarrow x \leq N - 1)$
6	3 4 5	syl2anr	$⊢ (N \in ℤ_{\geq M} \land x \in ℤ_{\geq M}) \to (x < N \leftrightarrow x \leq N - 1)$
7	6	pm5.32da	$⊢ N \in ℤ_{\geq M} \to ((x \in ℤ_{\geq M} \land x < N) \leftrightarrow (x \in ℤ_{\geq M} \land x \leq N - 1))$
8		eluzel2	$⊢ N \in ℤ_{\geq M} \to M \in ℤ$
9		eluz1	$⊢ M \in ℤ \to (x \in ℤ_{\geq M} \leftrightarrow (x \in ℤ \land M \leq x))$
10	8 9	syl	$⊢ N \in ℤ_{\geq M} \to (x \in ℤ_{\geq M} \leftrightarrow (x \in ℤ \land M \leq x))$
11	10	anbi1d	$⊢ N \in ℤ_{\geq M} \to ((x \in ℤ_{\geq M} \land x \leq N - 1) \leftrightarrow ((x \in ℤ \land M \leq x) \land x \leq N - 1))$
12	7 11	bitrd	$⊢ N \in ℤ_{\geq M} \to ((x \in ℤ_{\geq M} \land x < N) \leftrightarrow ((x \in ℤ \land M \leq x) \land x \leq N - 1))$
13	2 12	bitrd	$⊢ N \in ℤ_{\geq M} \to (x \in Pred (< ℤ_{\geq M} N) \leftrightarrow ((x \in ℤ \land M \leq x) \land x \leq N - 1))$
14		peano2zm	$⊢ N \in ℤ \to N - 1 \in ℤ$
15	4 14	syl	$⊢ N \in ℤ_{\geq M} \to N - 1 \in ℤ$
16	8 15	jca	$⊢ N \in ℤ_{\geq M} \to (M \in ℤ \land N - 1 \in ℤ)$
17	16	biantrurd	$⊢ N \in ℤ_{\geq M} \to (((x \in ℤ \land M \leq x) \land x \leq N - 1) \leftrightarrow ((M \in ℤ \land N - 1 \in ℤ) \land ((x \in ℤ \land M \leq x) \land x \leq N - 1)))$
18	13 17	bitrd	$⊢ N \in ℤ_{\geq M} \to (x \in Pred (< ℤ_{\geq M} N) \leftrightarrow ((M \in ℤ \land N - 1 \in ℤ) \land ((x \in ℤ \land M \leq x) \land x \leq N - 1)))$
19		elfz2	$⊢ x \in (M \dots N - 1) \leftrightarrow ((M \in ℤ \land N - 1 \in ℤ \land x \in ℤ) \land (M \leq x \land x \leq N - 1))$
20		df-3an	$⊢ (M \in ℤ \land N - 1 \in ℤ \land x \in ℤ) \leftrightarrow ((M \in ℤ \land N - 1 \in ℤ) \land x \in ℤ)$
21	20	anbi1i	$⊢ ((M \in ℤ \land N - 1 \in ℤ \land x \in ℤ) \land (M \leq x \land x \leq N - 1)) \leftrightarrow (((M \in ℤ \land N - 1 \in ℤ) \land x \in ℤ) \land (M \leq x \land x \leq N - 1))$
22		anass	$⊢ (((M \in ℤ \land N - 1 \in ℤ) \land x \in ℤ) \land (M \leq x \land x \leq N - 1)) \leftrightarrow ((M \in ℤ \land N - 1 \in ℤ) \land (x \in ℤ \land (M \leq x \land x \leq N - 1)))$
23		anass	$⊢ ((x \in ℤ \land M \leq x) \land x \leq N - 1) \leftrightarrow (x \in ℤ \land (M \leq x \land x \leq N - 1))$
24	23	anbi2i	$⊢ ((M \in ℤ \land N - 1 \in ℤ) \land ((x \in ℤ \land M \leq x) \land x \leq N - 1)) \leftrightarrow ((M \in ℤ \land N - 1 \in ℤ) \land (x \in ℤ \land (M \leq x \land x \leq N - 1)))$
25	22 24	bitr4i	$⊢ (((M \in ℤ \land N - 1 \in ℤ) \land x \in ℤ) \land (M \leq x \land x \leq N - 1)) \leftrightarrow ((M \in ℤ \land N - 1 \in ℤ) \land ((x \in ℤ \land M \leq x) \land x \leq N - 1))$
26	19 21 25	3bitri	$⊢ x \in (M \dots N - 1) \leftrightarrow ((M \in ℤ \land N - 1 \in ℤ) \land ((x \in ℤ \land M \leq x) \land x \leq N - 1))$
27	18 26	bitr4di	$⊢ N \in ℤ_{\geq M} \to (x \in Pred (< ℤ_{\geq M} N) \leftrightarrow x \in (M \dots N - 1))$
28	27	eqrdv	$⊢ N \in ℤ_{\geq M} \to Pred (< ℤ_{\geq M} N) = (M \dots N - 1)$

Metamath Proof Explorer

Theorem preduz

Proof