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 ) = (/) )