# 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 ( ¬ 𝑁 ∈ ℤ → ( 𝑊 cyclShift 𝑁 ) = ∅ )

### Proof

Step Hyp Ref Expression
1 df-csh cyclShift = ( 𝑤 ∈ { 𝑓 ∣ ∃ 𝑙 ∈ ℕ0 𝑓 Fn ( 0 ..^ 𝑙 ) } , 𝑛 ∈ ℤ ↦ if ( 𝑤 = ∅ , ∅ , ( ( 𝑤 substr ⟨ ( 𝑛 mod ( ♯ ‘ 𝑤 ) ) , ( ♯ ‘ 𝑤 ) ⟩ ) ++ ( 𝑤 prefix ( 𝑛 mod ( ♯ ‘ 𝑤 ) ) ) ) ) )
2 0ex ∅ ∈ V
3 ovex ( ( 𝑤 substr ⟨ ( 𝑛 mod ( ♯ ‘ 𝑤 ) ) , ( ♯ ‘ 𝑤 ) ⟩ ) ++ ( 𝑤 prefix ( 𝑛 mod ( ♯ ‘ 𝑤 ) ) ) ) ∈ V
4 2 3 ifex if ( 𝑤 = ∅ , ∅ , ( ( 𝑤 substr ⟨ ( 𝑛 mod ( ♯ ‘ 𝑤 ) ) , ( ♯ ‘ 𝑤 ) ⟩ ) ++ ( 𝑤 prefix ( 𝑛 mod ( ♯ ‘ 𝑤 ) ) ) ) ) ∈ V
5 1 4 dmmpo dom cyclShift = ( { 𝑓 ∣ ∃ 𝑙 ∈ ℕ0 𝑓 Fn ( 0 ..^ 𝑙 ) } × ℤ )
6 id ( ¬ 𝑁 ∈ ℤ → ¬ 𝑁 ∈ ℤ )
7 6 intnand ( ¬ 𝑁 ∈ ℤ → ¬ ( 𝑊 ∈ { 𝑓 ∣ ∃ 𝑙 ∈ ℕ0 𝑓 Fn ( 0 ..^ 𝑙 ) } ∧ 𝑁 ∈ ℤ ) )
8 ndmovg ( ( dom cyclShift = ( { 𝑓 ∣ ∃ 𝑙 ∈ ℕ0 𝑓 Fn ( 0 ..^ 𝑙 ) } × ℤ ) ∧ ¬ ( 𝑊 ∈ { 𝑓 ∣ ∃ 𝑙 ∈ ℕ0 𝑓 Fn ( 0 ..^ 𝑙 ) } ∧ 𝑁 ∈ ℤ ) ) → ( 𝑊 cyclShift 𝑁 ) = ∅ )
9 5 7 8 sylancr ( ¬ 𝑁 ∈ ℤ → ( 𝑊 cyclShift 𝑁 ) = ∅ )