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 ∈ ℤ → W cyclShift N = ∅

Proof

Step Hyp Ref Expression
1 df-csh ⊢ cyclShift = w ∈ f | ∃ l ∈ ℕ 0 f Fn 0 ..^ l , n ∈ ℤ ⟼ if w = ∅ ∅ w substr n mod w w ++ w prefix n mod w
2 0ex ⊢ ∅ ∈ V
3 ovex ⊢ w substr n mod w w ++ w prefix n mod w ∈ V
4 2 3 ifex ⊢ if w = ∅ ∅ w substr n mod w w ++ w prefix n mod w ∈ V
5 1 4 dmmpo ⊢ dom ⁡ cyclShift = f | ∃ l ∈ ℕ 0 f Fn 0 ..^ l × ℤ
6 id ⊢ ¬ N ∈ ℤ → ¬ N ∈ ℤ
7 6 intnand ⊢ ¬ N ∈ ℤ → ¬ W ∈ f | ∃ l ∈ ℕ 0 f Fn 0 ..^ l ∧ N ∈ ℤ
8 ndmovg ⊢ dom ⁡ cyclShift = f | ∃ l ∈ ℕ 0 f Fn 0 ..^ l × ℤ ∧ ¬ W ∈ f | ∃ l ∈ ℕ 0 f Fn 0 ..^ l ∧ N ∈ ℤ → W cyclShift N = ∅
9 5 7 8 sylancr ⊢ ¬ N ∈ ℤ → W cyclShift N = ∅