Metamath Proof Explorer

Theorem fz0add1fz1

Description: Translate membership in a 0-based half-open integer range into membership in a 1-based finite sequence of integers. (Contributed by Alexander van der Vekens, 23-Nov-2017)

		Ref	Expression
	Assertion	fz0add1fz1	$⊢ (N \in ℕ_{0} \land X \in (0 ..^N)) \to X + 1 \in (1 \dots N)$

Proof

Step	Hyp	Ref	Expression
1		1z	$⊢ 1 \in ℤ$
2		fzoaddel	$⊢ (X \in (0 ..^N) \land 1 \in ℤ) \to X + 1 \in (0 + 1 ..^N + 1)$
3	1 2	mpan2	$⊢ X \in (0 ..^N) \to X + 1 \in (0 + 1 ..^N + 1)$
4	3	adantl	$⊢ (N \in ℕ_{0} \land X \in (0 ..^N)) \to X + 1 \in (0 + 1 ..^N + 1)$
5		0p1e1	$⊢ 0 + 1 = 1$
6	5	oveq1i	$⊢ (0 + 1 ..^N + 1) = (1 ..^N + 1)$
7		nn0z	$⊢ N \in ℕ_{0} \to N \in ℤ$
8		fzval3	$⊢ N \in ℤ \to (1 \dots N) = (1 ..^N + 1)$
9	8	eqcomd	$⊢ N \in ℤ \to (1 ..^N + 1) = (1 \dots N)$
10	7 9	syl	$⊢ N \in ℕ_{0} \to (1 ..^N + 1) = (1 \dots N)$
11	6 10	eqtrid	$⊢ N \in ℕ_{0} \to (0 + 1 ..^N + 1) = (1 \dots N)$
12	11	eleq2d	$⊢ N \in ℕ_{0} \to (X + 1 \in (0 + 1 ..^N + 1) \leftrightarrow X + 1 \in (1 \dots N))$
13	12	adantr	$⊢ (N \in ℕ_{0} \land X \in (0 ..^N)) \to (X + 1 \in (0 + 1 ..^N + 1) \leftrightarrow X + 1 \in (1 \dots N))$
14	4 13	mpbid	$⊢ (N \in ℕ_{0} \land X \in (0 ..^N)) \to X + 1 \in (1 \dots N)$