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	$⊢ \neg N \in ℤ \to W cyclShift N = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		df-csh	$⊢ cyclShift = (w \in \{f \| \exists l \in ℕ_{0} f Fn (0 ..^l)\}, n \in ℤ ⟼ if (w = \emptyset, \emptyset, (w substr ⟨n \mod \|w\|, \|w\|⟩) ++ (w prefix (n \mod \|w\|))))$
2		0ex	$⊢ \emptyset \in V$
3		ovex	$⊢ (w substr ⟨n \mod \|w\|, \|w\|⟩) ++ (w prefix (n \mod \|w\|)) \in V$
4	2 3	ifex	$⊢ if (w = \emptyset, \emptyset, (w substr ⟨n \mod \|w\|, \|w\|⟩) ++ (w prefix (n \mod \|w\|))) \in V$
5	1 4	dmmpo	$⊢ dom cyclShift = \{f \| \exists l \in ℕ_{0} f Fn (0 ..^l)\} \times ℤ$
6		id	$⊢ \neg N \in ℤ \to \neg N \in ℤ$
7	6	intnand	$⊢ \neg N \in ℤ \to \neg (W \in \{f \| \exists l \in ℕ_{0} f Fn (0 ..^l)\} \land N \in ℤ)$
8		ndmovg	$⊢ (dom cyclShift = \{f \| \exists l \in ℕ_{0} f Fn (0 ..^l)\} \times ℤ \land \neg (W \in \{f \| \exists l \in ℕ_{0} f Fn (0 ..^l)\} \land N \in ℤ)) \to W cyclShift N = \emptyset$
9	5 7 8	sylancr	$⊢ \neg N \in ℤ \to W cyclShift N = \emptyset$