Metamath Proof Explorer

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 e. ZZ -> ( M ... N ) = ( M ..^ ( N + 1 ) ) )

Proof

Step Hyp Ref Expression
1 peano2z 
 |-  ( N e. ZZ -> ( N + 1 ) e. ZZ )
2 fzoval 
 |-  ( ( N + 1 ) e. ZZ -> ( M ..^ ( N + 1 ) ) = ( M ... ( ( N + 1 ) - 1 ) ) )
3 1 2 syl 
 |-  ( N e. ZZ -> ( M ..^ ( N + 1 ) ) = ( M ... ( ( N + 1 ) - 1 ) ) )
4 zcn 
 |-  ( N e. ZZ -> N e. CC )
5 ax-1cn 
 |-  1 e. CC
6 pncan 
 |-  ( ( N e. CC /\ 1 e. CC ) -> ( ( N + 1 ) - 1 ) = N )
7 4 5 6 sylancl 
 |-  ( N e. ZZ -> ( ( N + 1 ) - 1 ) = N )
8 7 oveq2d 
 |-  ( N e. ZZ -> ( M ... ( ( N + 1 ) - 1 ) ) = ( M ... N ) )
9 3 8 eqtr2d 
 |-  ( N e. ZZ -> ( M ... N ) = ( M ..^ ( N + 1 ) ) )