Metamath Proof Explorer

Theorem elfzom1b

Description: An integer is a member of a 1-based finite set of sequential integers iff its predecessor is a member of the corresponding 0-based set. (Contributed by Mario Carneiro, 27-Sep-2015)

		Ref	Expression
	Assertion	elfzom1b	$⊢ (K \in ℤ \land N \in ℤ) \to (K \in (1 ..^N) \leftrightarrow K - 1 \in (0 ..^N - 1))$

Proof

Step	Hyp	Ref	Expression
1		peano2zm	$⊢ N \in ℤ \to N - 1 \in ℤ$
2		elfzm1b	$⊢ (K \in ℤ \land N - 1 \in ℤ) \to (K \in (1 \dots N - 1) \leftrightarrow K - 1 \in (0 \dots N - 1 - 1))$
3	1 2	sylan2	$⊢ (K \in ℤ \land N \in ℤ) \to (K \in (1 \dots N - 1) \leftrightarrow K - 1 \in (0 \dots N - 1 - 1))$
4		fzoval	$⊢ N \in ℤ \to (1 ..^N) = (1 \dots N - 1)$
5	4	adantl	$⊢ (K \in ℤ \land N \in ℤ) \to (1 ..^N) = (1 \dots N - 1)$
6	5	eleq2d	$⊢ (K \in ℤ \land N \in ℤ) \to (K \in (1 ..^N) \leftrightarrow K \in (1 \dots N - 1))$
7	1	adantl	$⊢ (K \in ℤ \land N \in ℤ) \to N - 1 \in ℤ$
8		fzoval	$⊢ N - 1 \in ℤ \to (0 ..^N - 1) = (0 \dots N - 1 - 1)$
9	7 8	syl	$⊢ (K \in ℤ \land N \in ℤ) \to (0 ..^N - 1) = (0 \dots N - 1 - 1)$
10	9	eleq2d	$⊢ (K \in ℤ \land N \in ℤ) \to (K - 1 \in (0 ..^N - 1) \leftrightarrow K - 1 \in (0 \dots N - 1 - 1))$
11	3 6 10	3bitr4d	$⊢ (K \in ℤ \land N \in ℤ) \to (K \in (1 ..^N) \leftrightarrow K - 1 \in (0 ..^N - 1))$