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	⊢ ( 𝑁 ∈ ℤ → ( 𝑀 ... 𝑁 ) = ( 𝑀 ..^ ( 𝑁 + 1 ) ) )

Proof

Step	Hyp	Ref	Expression
1		peano2z	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 + 1 ) ∈ ℤ )
2		fzoval	⊢ ( ( 𝑁 + 1 ) ∈ ℤ → ( 𝑀 ..^ ( 𝑁 + 1 ) ) = ( 𝑀 ... ( ( 𝑁 + 1 ) − 1 ) ) )
3	1 2	syl	⊢ ( 𝑁 ∈ ℤ → ( 𝑀 ..^ ( 𝑁 + 1 ) ) = ( 𝑀 ... ( ( 𝑁 + 1 ) − 1 ) ) )
4		zcn	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
5		ax-1cn	⊢ 1 ∈ ℂ
6		pncan	⊢ ( ( 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
7	4 5 6	sylancl	⊢ ( 𝑁 ∈ ℤ → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
8	7	oveq2d	⊢ ( 𝑁 ∈ ℤ → ( 𝑀 ... ( ( 𝑁 + 1 ) − 1 ) ) = ( 𝑀 ... 𝑁 ) )
9	3 8	eqtr2d	⊢ ( 𝑁 ∈ ℤ → ( 𝑀 ... 𝑁 ) = ( 𝑀 ..^ ( 𝑁 + 1 ) ) )