This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cshnz

Description: A cyclical shift is the empty set if the number of shifts is not an integer. (Contributed by Alexander van der Vekens, 21-May-2018) (Revised by AV, 17-Nov-2018)

Ref Expression
Assertion cshnz 
|- ( -. N e. ZZ -> ( W cyclShift N ) = (/) )

Proof

Step Hyp Ref Expression
1 df-csh 
 |-  cyclShift = ( w e. { f | E. l e. NN0 f Fn ( 0 ..^ l ) } , n e. ZZ |-> if ( w = (/) , (/) , ( ( w substr <. ( n mod ( # ` w ) ) , ( # ` w ) >. ) ++ ( w prefix ( n mod ( # ` w ) ) ) ) ) )
2 0ex 
 |-  (/) e. _V
3 ovex 
 |-  ( ( w substr <. ( n mod ( # ` w ) ) , ( # ` w ) >. ) ++ ( w prefix ( n mod ( # ` w ) ) ) ) e. _V
4 2 3 ifex 
 |-  if ( w = (/) , (/) , ( ( w substr <. ( n mod ( # ` w ) ) , ( # ` w ) >. ) ++ ( w prefix ( n mod ( # ` w ) ) ) ) ) e. _V
5 1 4 dmmpo 
 |-  dom cyclShift = ( { f | E. l e. NN0 f Fn ( 0 ..^ l ) } X. ZZ )
6 id 
 |-  ( -. N e. ZZ -> -. N e. ZZ )
7 6 intnand 
 |-  ( -. N e. ZZ -> -. ( W e. { f | E. l e. NN0 f Fn ( 0 ..^ l ) } /\ N e. ZZ ) )
8 ndmovg 
 |-  ( ( dom cyclShift = ( { f | E. l e. NN0 f Fn ( 0 ..^ l ) } X. ZZ ) /\ -. ( W e. { f | E. l e. NN0 f Fn ( 0 ..^ l ) } /\ N e. ZZ ) ) -> ( W cyclShift N ) = (/) )
9 5 7 8 sylancr 
 |-  ( -. N e. ZZ -> ( W cyclShift N ) = (/) )