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 

ax1cn 
 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 ) ) ) 