Theorem 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 \mathbb{Z}\to \left(M\dots N\right)=\left(M..^N+1\right)$$

Proof

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