fzval3

Description: Expressing a closed integer range as a half-open integer range. (Contributed by Stefan O'Rear, 15-Aug-2015)

		Ref	Expression
	Assertion	fzval3	$⊢ N \in ℤ \to (M \dots N) = (M ..^N + 1)$

Step	Hyp	Ref	Expression
1		peano2z	$⊢ N \in ℤ \to N + 1 \in ℤ$
2		fzoval	$⊢ N + 1 \in ℤ \to (M ..^N + 1) = (M \dots N + 1 - 1)$
3	1 2	syl	$⊢ N \in ℤ \to (M ..^N + 1) = (M \dots N + 1 - 1)$
4		zcn	$⊢ N \in ℤ \to N \in ℂ$
5		ax-1cn	$⊢ 1 \in ℂ$
6		pncan	$⊢ (N \in ℂ \land 1 \in ℂ) \to N + 1 - 1 = N$
7	4 5 6	sylancl	$⊢ N \in ℤ \to N + 1 - 1 = N$
8	7	oveq2d	$⊢ N \in ℤ \to (M \dots N + 1 - 1) = (M \dots N)$
9	3 8	eqtr2d	$⊢ N \in ℤ \to (M \dots N) = (M ..^N + 1)$

Metamath Proof Explorer