cshwidxmodr

Description: The symbol at a given index of a cyclically shifted nonempty word is the symbol at the shifted index of the original word. (Contributed by AV, 17-Mar-2021)

		Ref	Expression
	Assertion	cshwidxmodr	$⊢ (W \in Word V \land N \in ℤ \land I \in (0 ..^\|W\|)) \to (W cyclShift N) ((I - N) \mod \|W\|) = W (I)$

Proof

Step	Hyp	Ref	Expression
1		elfzo0	$⊢ I \in (0 ..^\|W\|) \leftrightarrow (I \in ℕ_{0} \land \|W\| \in ℕ \land I < \|W\|)$
2		nn0z	$⊢ I \in ℕ_{0} \to I \in ℤ$
3	2	3ad2ant1	$⊢ (I \in ℕ_{0} \land \|W\| \in ℕ \land I < \|W\|) \to I \in ℤ$
4		zsubcl	$⊢ (I \in ℤ \land N \in ℤ) \to I - N \in ℤ$
5	3 4	sylan	$⊢ ((I \in ℕ_{0} \land \|W\| \in ℕ \land I < \|W\|) \land N \in ℤ) \to I - N \in ℤ$
6		simpl2	$⊢ ((I \in ℕ_{0} \land \|W\| \in ℕ \land I < \|W\|) \land N \in ℤ) \to \|W\| \in ℕ$
7	5 6	jca	$⊢ ((I \in ℕ_{0} \land \|W\| \in ℕ \land I < \|W\|) \land N \in ℤ) \to (I - N \in ℤ \land \|W\| \in ℕ)$
8	7	ex	$⊢ (I \in ℕ_{0} \land \|W\| \in ℕ \land I < \|W\|) \to (N \in ℤ \to (I - N \in ℤ \land \|W\| \in ℕ))$
9	1 8	sylbi	$⊢ I \in (0 ..^\|W\|) \to (N \in ℤ \to (I - N \in ℤ \land \|W\| \in ℕ))$
10	9	impcom	$⊢ (N \in ℤ \land I \in (0 ..^\|W\|)) \to (I - N \in ℤ \land \|W\| \in ℕ)$
11	10	3adant1	$⊢ (W \in Word V \land N \in ℤ \land I \in (0 ..^\|W\|)) \to (I - N \in ℤ \land \|W\| \in ℕ)$
12		zmodfzo	$⊢ (I - N \in ℤ \land \|W\| \in ℕ) \to (I - N) \mod \|W\| \in (0 ..^\|W\|)$
13	11 12	syl	$⊢ (W \in Word V \land N \in ℤ \land I \in (0 ..^\|W\|)) \to (I - N) \mod \|W\| \in (0 ..^\|W\|)$
14		cshwidxmod	$⊢ (W \in Word V \land N \in ℤ \land (I - N) \mod \|W\| \in (0 ..^\|W\|)) \to (W cyclShift N) ((I - N) \mod \|W\|) = W ((((I - N) \mod \|W\|) + N) \mod \|W\|)$
15	13 14	syld3an3	$⊢ (W \in Word V \land N \in ℤ \land I \in (0 ..^\|W\|)) \to (W cyclShift N) ((I - N) \mod \|W\|) = W ((((I - N) \mod \|W\|) + N) \mod \|W\|)$
16		elfzoelz	$⊢ I \in (0 ..^\|W\|) \to I \in ℤ$
17	16	adantl	$⊢ ((I \in ℕ_{0} \land \|W\| \in ℕ) \land I \in (0 ..^\|W\|)) \to I \in ℤ$
18	17 4	sylan	$⊢ (((I \in ℕ_{0} \land \|W\| \in ℕ) \land I \in (0 ..^\|W\|)) \land N \in ℤ) \to I - N \in ℤ$
19	18	zred	$⊢ (((I \in ℕ_{0} \land \|W\| \in ℕ) \land I \in (0 ..^\|W\|)) \land N \in ℤ) \to I - N \in ℝ$
20		zre	$⊢ N \in ℤ \to N \in ℝ$
21	20	adantl	$⊢ (((I \in ℕ_{0} \land \|W\| \in ℕ) \land I \in (0 ..^\|W\|)) \land N \in ℤ) \to N \in ℝ$
22		nnrp	$⊢ \|W\| \in ℕ \to \|W\| \in ℝ^{+}$
23	22	ad3antlr	$⊢ (((I \in ℕ_{0} \land \|W\| \in ℕ) \land I \in (0 ..^\|W\|)) \land N \in ℤ) \to \|W\| \in ℝ^{+}$
24		modaddmod	$⊢ (I - N \in ℝ \land N \in ℝ \land \|W\| \in ℝ^{+}) \to (((I - N) \mod \|W\|) + N) \mod \|W\| = (I - N + N) \mod \|W\|$
25	19 21 23 24	syl3anc	$⊢ (((I \in ℕ_{0} \land \|W\| \in ℕ) \land I \in (0 ..^\|W\|)) \land N \in ℤ) \to (((I - N) \mod \|W\|) + N) \mod \|W\| = (I - N + N) \mod \|W\|$
26		nn0cn	$⊢ I \in ℕ_{0} \to I \in ℂ$
27	26	ad2antrr	$⊢ ((I \in ℕ_{0} \land \|W\| \in ℕ) \land I \in (0 ..^\|W\|)) \to I \in ℂ$
28		zcn	$⊢ N \in ℤ \to N \in ℂ$
29		npcan	$⊢ (I \in ℂ \land N \in ℂ) \to I - N + N = I$
30	27 28 29	syl2an	$⊢ (((I \in ℕ_{0} \land \|W\| \in ℕ) \land I \in (0 ..^\|W\|)) \land N \in ℤ) \to I - N + N = I$
31	30	oveq1d	$⊢ (((I \in ℕ_{0} \land \|W\| \in ℕ) \land I \in (0 ..^\|W\|)) \land N \in ℤ) \to (I - N + N) \mod \|W\| = I \mod \|W\|$
32		zmodidfzoimp	$⊢ I \in (0 ..^\|W\|) \to I \mod \|W\| = I$
33	32	ad2antlr	$⊢ (((I \in ℕ_{0} \land \|W\| \in ℕ) \land I \in (0 ..^\|W\|)) \land N \in ℤ) \to I \mod \|W\| = I$
34	25 31 33	3eqtrd	$⊢ (((I \in ℕ_{0} \land \|W\| \in ℕ) \land I \in (0 ..^\|W\|)) \land N \in ℤ) \to (((I - N) \mod \|W\|) + N) \mod \|W\| = I$
35	34	fveq2d	$⊢ (((I \in ℕ_{0} \land \|W\| \in ℕ) \land I \in (0 ..^\|W\|)) \land N \in ℤ) \to W ((((I - N) \mod \|W\|) + N) \mod \|W\|) = W (I)$
36	35	ex	$⊢ ((I \in ℕ_{0} \land \|W\| \in ℕ) \land I \in (0 ..^\|W\|)) \to (N \in ℤ \to W ((((I - N) \mod \|W\|) + N) \mod \|W\|) = W (I))$
37	36	ex	$⊢ (I \in ℕ_{0} \land \|W\| \in ℕ) \to (I \in (0 ..^\|W\|) \to (N \in ℤ \to W ((((I - N) \mod \|W\|) + N) \mod \|W\|) = W (I)))$
38	37	3adant3	$⊢ (I \in ℕ_{0} \land \|W\| \in ℕ \land I < \|W\|) \to (I \in (0 ..^\|W\|) \to (N \in ℤ \to W ((((I - N) \mod \|W\|) + N) \mod \|W\|) = W (I)))$
39	1 38	sylbi	$⊢ I \in (0 ..^\|W\|) \to (I \in (0 ..^\|W\|) \to (N \in ℤ \to W ((((I - N) \mod \|W\|) + N) \mod \|W\|) = W (I)))$
40	39	pm2.43i	$⊢ I \in (0 ..^\|W\|) \to (N \in ℤ \to W ((((I - N) \mod \|W\|) + N) \mod \|W\|) = W (I))$
41	40	impcom	$⊢ (N \in ℤ \land I \in (0 ..^\|W\|)) \to W ((((I - N) \mod \|W\|) + N) \mod \|W\|) = W (I)$
42	41	3adant1	$⊢ (W \in Word V \land N \in ℤ \land I \in (0 ..^\|W\|)) \to W ((((I - N) \mod \|W\|) + N) \mod \|W\|) = W (I)$
43	15 42	eqtrd	$⊢ (W \in Word V \land N \in ℤ \land I \in (0 ..^\|W\|)) \to (W cyclShift N) ((I - N) \mod \|W\|) = W (I)$

Metamath Proof Explorer

Theorem cshwidxmodr

Proof