predfz

Description: Calculate the predecessor of an integer under a finite set of integers. (Contributed by Scott Fenton, 8-Aug-2013) (Proof shortened by Mario Carneiro, 3-May-2015)

		Ref	Expression
	Assertion	predfz	$⊢ K \in (M \dots N) \to Pred (< (M \dots N) K) = (M \dots K - 1)$

Proof

Step	Hyp	Ref	Expression
1		elfzelz	$⊢ x \in (M \dots N) \to x \in ℤ$
2		elfzelz	$⊢ K \in (M \dots N) \to K \in ℤ$
3		zltlem1	$⊢ (x \in ℤ \land K \in ℤ) \to (x < K \leftrightarrow x \leq K - 1)$
4	1 2 3	syl2anr	$⊢ (K \in (M \dots N) \land x \in (M \dots N)) \to (x < K \leftrightarrow x \leq K - 1)$
5		elfzuz	$⊢ x \in (M \dots N) \to x \in ℤ_{\geq M}$
6		peano2zm	$⊢ K \in ℤ \to K - 1 \in ℤ$
7	2 6	syl	$⊢ K \in (M \dots N) \to K - 1 \in ℤ$
8		elfz5	$⊢ (x \in ℤ_{\geq M} \land K - 1 \in ℤ) \to (x \in (M \dots K - 1) \leftrightarrow x \leq K - 1)$
9	5 7 8	syl2anr	$⊢ (K \in (M \dots N) \land x \in (M \dots N)) \to (x \in (M \dots K - 1) \leftrightarrow x \leq K - 1)$
10	4 9	bitr4d	$⊢ (K \in (M \dots N) \land x \in (M \dots N)) \to (x < K \leftrightarrow x \in (M \dots K - 1))$
11	10	pm5.32da	$⊢ K \in (M \dots N) \to ((x \in (M \dots N) \land x < K) \leftrightarrow (x \in (M \dots N) \land x \in (M \dots K - 1)))$
12		vex	$⊢ x \in V$
13	12	elpred	$⊢ K \in (M \dots N) \to (x \in Pred (< (M \dots N) K) \leftrightarrow (x \in (M \dots N) \land x < K))$
14		elfzuz3	$⊢ K \in (M \dots N) \to N \in ℤ_{\geq K}$
15	2	zcnd	$⊢ K \in (M \dots N) \to K \in ℂ$
16		ax-1cn	$⊢ 1 \in ℂ$
17		npcan	$⊢ (K \in ℂ \land 1 \in ℂ) \to K - 1 + 1 = K$
18	15 16 17	sylancl	$⊢ K \in (M \dots N) \to K - 1 + 1 = K$
19	18	fveq2d	$⊢ K \in (M \dots N) \to ℤ_{\geq (K - 1 + 1)} = ℤ_{\geq K}$
20	14 19	eleqtrrd	$⊢ K \in (M \dots N) \to N \in ℤ_{\geq (K - 1 + 1)}$
21		peano2uzr	$⊢ (K - 1 \in ℤ \land N \in ℤ_{\geq (K - 1 + 1)}) \to N \in ℤ_{\geq (K - 1)}$
22	7 20 21	syl2anc	$⊢ K \in (M \dots N) \to N \in ℤ_{\geq (K - 1)}$
23		fzss2	$⊢ N \in ℤ_{\geq (K - 1)} \to (M \dots K - 1) \subseteq (M \dots N)$
24	22 23	syl	$⊢ K \in (M \dots N) \to (M \dots K - 1) \subseteq (M \dots N)$
25	24	sseld	$⊢ K \in (M \dots N) \to (x \in (M \dots K - 1) \to x \in (M \dots N))$
26	25	pm4.71rd	$⊢ K \in (M \dots N) \to (x \in (M \dots K - 1) \leftrightarrow (x \in (M \dots N) \land x \in (M \dots K - 1)))$
27	11 13 26	3bitr4d	$⊢ K \in (M \dots N) \to (x \in Pred (< (M \dots N) K) \leftrightarrow x \in (M \dots K - 1))$
28	27	eqrdv	$⊢ K \in (M \dots N) \to Pred (< (M \dots N) K) = (M \dots K - 1)$

Metamath Proof Explorer

Theorem predfz

Proof