repswcshw

Description: A cyclically shifted "repeated symbol word". (Contributed by Alexander van der Vekens, 7-Nov-2018) (Proof shortened by AV, 16-Oct-2022)

		Ref	Expression
	Assertion	repswcshw	$⊢ (S \in V \land N \in ℕ_{0} \land I \in ℤ) \to (S repeatS N) cyclShift I = S repeatS N$

Proof

Step	Hyp	Ref	Expression
1		0csh0	$⊢ \emptyset cyclShift I = \emptyset$
2		repsw0	$⊢ S \in V \to S repeatS 0 = \emptyset$
3	2	oveq1d	$⊢ S \in V \to (S repeatS 0) cyclShift I = \emptyset cyclShift I$
4	1 3 2	3eqtr4a	$⊢ S \in V \to (S repeatS 0) cyclShift I = S repeatS 0$
5	4	3ad2ant1	$⊢ (S \in V \land N \in ℕ_{0} \land I \in ℤ) \to (S repeatS 0) cyclShift I = S repeatS 0$
6		oveq2	$⊢ N = 0 \to S repeatS N = S repeatS 0$
7	6	oveq1d	$⊢ N = 0 \to (S repeatS N) cyclShift I = (S repeatS 0) cyclShift I$
8	7 6	eqeq12d	$⊢ N = 0 \to ((S repeatS N) cyclShift I = S repeatS N \leftrightarrow (S repeatS 0) cyclShift I = S repeatS 0)$
9	5 8	imbitrrid	$⊢ N = 0 \to ((S \in V \land N \in ℕ_{0} \land I \in ℤ) \to (S repeatS N) cyclShift I = S repeatS N)$
10		idd	$⊢ \neg N = 0 \to (S \in V \to S \in V)$
11		df-ne	$⊢ N \neq 0 \leftrightarrow \neg N = 0$
12		elnnne0	$⊢ N \in ℕ \leftrightarrow (N \in ℕ_{0} \land N \neq 0)$
13	12	simplbi2com	$⊢ N \neq 0 \to (N \in ℕ_{0} \to N \in ℕ)$
14	11 13	sylbir	$⊢ \neg N = 0 \to (N \in ℕ_{0} \to N \in ℕ)$
15		idd	$⊢ \neg N = 0 \to (I \in ℤ \to I \in ℤ)$
16	10 14 15	3anim123d	$⊢ \neg N = 0 \to ((S \in V \land N \in ℕ_{0} \land I \in ℤ) \to (S \in V \land N \in ℕ \land I \in ℤ))$
17		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
18	17	anim2i	$⊢ (S \in V \land N \in ℕ) \to (S \in V \land N \in ℕ_{0})$
19		repsw	$⊢ (S \in V \land N \in ℕ_{0}) \to S repeatS N \in Word V$
20	18 19	syl	$⊢ (S \in V \land N \in ℕ) \to S repeatS N \in Word V$
21		cshword	$⊢ (S repeatS N \in Word V \land I \in ℤ) \to (S repeatS N) cyclShift I = ((S repeatS N) substr ⟨I \mod \|S repeatS N\|, \|S repeatS N\|⟩) ++ ((S repeatS N) prefix (I \mod \|S repeatS N\|))$
22	20 21	stoic3	$⊢ (S \in V \land N \in ℕ \land I \in ℤ) \to (S repeatS N) cyclShift I = ((S repeatS N) substr ⟨I \mod \|S repeatS N\|, \|S repeatS N\|⟩) ++ ((S repeatS N) prefix (I \mod \|S repeatS N\|))$
23		repswlen	$⊢ (S \in V \land N \in ℕ_{0}) \to \|S repeatS N\| = N$
24	18 23	syl	$⊢ (S \in V \land N \in ℕ) \to \|S repeatS N\| = N$
25	24	oveq2d	$⊢ (S \in V \land N \in ℕ) \to I \mod \|S repeatS N\| = I \mod N$
26	25 24	opeq12d	$⊢ (S \in V \land N \in ℕ) \to ⟨I \mod \|S repeatS N\|, \|S repeatS N\|⟩ = ⟨I \mod N, N⟩$
27	26	oveq2d	$⊢ (S \in V \land N \in ℕ) \to (S repeatS N) substr ⟨I \mod \|S repeatS N\|, \|S repeatS N\|⟩ = (S repeatS N) substr ⟨I \mod N, N⟩$
28	25	oveq2d	$⊢ (S \in V \land N \in ℕ) \to (S repeatS N) prefix (I \mod \|S repeatS N\|) = (S repeatS N) prefix (I \mod N)$
29	27 28	oveq12d	$⊢ (S \in V \land N \in ℕ) \to ((S repeatS N) substr ⟨I \mod \|S repeatS N\|, \|S repeatS N\|⟩) ++ ((S repeatS N) prefix (I \mod \|S repeatS N\|)) = ((S repeatS N) substr ⟨I \mod N, N⟩) ++ ((S repeatS N) prefix (I \mod N))$
30	29	3adant3	$⊢ (S \in V \land N \in ℕ \land I \in ℤ) \to ((S repeatS N) substr ⟨I \mod \|S repeatS N\|, \|S repeatS N\|⟩) ++ ((S repeatS N) prefix (I \mod \|S repeatS N\|)) = ((S repeatS N) substr ⟨I \mod N, N⟩) ++ ((S repeatS N) prefix (I \mod N))$
31	18	3adant3	$⊢ (S \in V \land N \in ℕ \land I \in ℤ) \to (S \in V \land N \in ℕ_{0})$
32		zmodcl	$⊢ (I \in ℤ \land N \in ℕ) \to I \mod N \in ℕ_{0}$
33	32	ancoms	$⊢ (N \in ℕ \land I \in ℤ) \to I \mod N \in ℕ_{0}$
34	17	adantr	$⊢ (N \in ℕ \land I \in ℤ) \to N \in ℕ_{0}$
35	33 34	jca	$⊢ (N \in ℕ \land I \in ℤ) \to (I \mod N \in ℕ_{0} \land N \in ℕ_{0})$
36	35	3adant1	$⊢ (S \in V \land N \in ℕ \land I \in ℤ) \to (I \mod N \in ℕ_{0} \land N \in ℕ_{0})$
37		nnre	$⊢ N \in ℕ \to N \in ℝ$
38	37	leidd	$⊢ N \in ℕ \to N \leq N$
39	38	3ad2ant2	$⊢ (S \in V \land N \in ℕ \land I \in ℤ) \to N \leq N$
40		repswswrd	$⊢ ((S \in V \land N \in ℕ_{0}) \land (I \mod N \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq N) \to (S repeatS N) substr ⟨I \mod N, N⟩ = S repeatS (N - (I \mod N))$
41	31 36 39 40	syl3anc	$⊢ (S \in V \land N \in ℕ \land I \in ℤ) \to (S repeatS N) substr ⟨I \mod N, N⟩ = S repeatS (N - (I \mod N))$
42		simp1	$⊢ (S \in V \land N \in ℕ \land I \in ℤ) \to S \in V$
43	17	3ad2ant2	$⊢ (S \in V \land N \in ℕ \land I \in ℤ) \to N \in ℕ_{0}$
44		zmodfzp1	$⊢ (I \in ℤ \land N \in ℕ) \to I \mod N \in (0 \dots N)$
45	44	ancoms	$⊢ (N \in ℕ \land I \in ℤ) \to I \mod N \in (0 \dots N)$
46	45	3adant1	$⊢ (S \in V \land N \in ℕ \land I \in ℤ) \to I \mod N \in (0 \dots N)$
47		repswpfx	$⊢ (S \in V \land N \in ℕ_{0} \land I \mod N \in (0 \dots N)) \to (S repeatS N) prefix (I \mod N) = S repeatS (I \mod N)$
48	42 43 46 47	syl3anc	$⊢ (S \in V \land N \in ℕ \land I \in ℤ) \to (S repeatS N) prefix (I \mod N) = S repeatS (I \mod N)$
49	41 48	oveq12d	$⊢ (S \in V \land N \in ℕ \land I \in ℤ) \to ((S repeatS N) substr ⟨I \mod N, N⟩) ++ ((S repeatS N) prefix (I \mod N)) = (S repeatS (N - (I \mod N))) ++ (S repeatS (I \mod N))$
50	32	nn0red	$⊢ (I \in ℤ \land N \in ℕ) \to I \mod N \in ℝ$
51	50	ancoms	$⊢ (N \in ℕ \land I \in ℤ) \to I \mod N \in ℝ$
52	37	adantr	$⊢ (N \in ℕ \land I \in ℤ) \to N \in ℝ$
53		zre	$⊢ I \in ℤ \to I \in ℝ$
54		nnrp	$⊢ N \in ℕ \to N \in ℝ^{+}$
55		modlt	$⊢ (I \in ℝ \land N \in ℝ^{+}) \to I \mod N < N$
56	53 54 55	syl2anr	$⊢ (N \in ℕ \land I \in ℤ) \to I \mod N < N$
57	51 52 56	ltled	$⊢ (N \in ℕ \land I \in ℤ) \to I \mod N \leq N$
58	57	3adant1	$⊢ (S \in V \land N \in ℕ \land I \in ℤ) \to I \mod N \leq N$
59	33	3adant1	$⊢ (S \in V \land N \in ℕ \land I \in ℤ) \to I \mod N \in ℕ_{0}$
60		nn0sub	$⊢ (I \mod N \in ℕ_{0} \land N \in ℕ_{0}) \to (I \mod N \leq N \leftrightarrow N - (I \mod N) \in ℕ_{0})$
61	59 43 60	syl2anc	$⊢ (S \in V \land N \in ℕ \land I \in ℤ) \to (I \mod N \leq N \leftrightarrow N - (I \mod N) \in ℕ_{0})$
62	58 61	mpbid	$⊢ (S \in V \land N \in ℕ \land I \in ℤ) \to N - (I \mod N) \in ℕ_{0}$
63		repswccat	$⊢ (S \in V \land N - (I \mod N) \in ℕ_{0} \land I \mod N \in ℕ_{0}) \to (S repeatS (N - (I \mod N))) ++ (S repeatS (I \mod N)) = S repeatS (N - (I \mod N) + (I \mod N))$
64	42 62 59 63	syl3anc	$⊢ (S \in V \land N \in ℕ \land I \in ℤ) \to (S repeatS (N - (I \mod N))) ++ (S repeatS (I \mod N)) = S repeatS (N - (I \mod N) + (I \mod N))$
65		nncn	$⊢ N \in ℕ \to N \in ℂ$
66	65	adantl	$⊢ (I \in ℤ \land N \in ℕ) \to N \in ℂ$
67	32	nn0cnd	$⊢ (I \in ℤ \land N \in ℕ) \to I \mod N \in ℂ$
68	66 67	npcand	$⊢ (I \in ℤ \land N \in ℕ) \to N - (I \mod N) + (I \mod N) = N$
69	68	ancoms	$⊢ (N \in ℕ \land I \in ℤ) \to N - (I \mod N) + (I \mod N) = N$
70	69	3adant1	$⊢ (S \in V \land N \in ℕ \land I \in ℤ) \to N - (I \mod N) + (I \mod N) = N$
71	70	oveq2d	$⊢ (S \in V \land N \in ℕ \land I \in ℤ) \to S repeatS (N - (I \mod N) + (I \mod N)) = S repeatS N$
72	49 64 71	3eqtrd	$⊢ (S \in V \land N \in ℕ \land I \in ℤ) \to ((S repeatS N) substr ⟨I \mod N, N⟩) ++ ((S repeatS N) prefix (I \mod N)) = S repeatS N$
73	22 30 72	3eqtrd	$⊢ (S \in V \land N \in ℕ \land I \in ℤ) \to (S repeatS N) cyclShift I = S repeatS N$
74	16 73	syl6	$⊢ \neg N = 0 \to ((S \in V \land N \in ℕ_{0} \land I \in ℤ) \to (S repeatS N) cyclShift I = S repeatS N)$
75	9 74	pm2.61i	$⊢ (S \in V \land N \in ℕ_{0} \land I \in ℤ) \to (S repeatS N) cyclShift I = S repeatS N$

Metamath Proof Explorer

Theorem repswcshw

Proof