crctcshwlkn0lem5

	Ref	Expression
Hypotheses	crctcshwlkn0lem.s	$⊢ φ \to S \in (1 ..^N)$
	crctcshwlkn0lem.q	$⊢ Q = (x \in (0 \dots N) ⟼ if (x \leq N - S, P (x + S), P (x + S - N)))$
	crctcshwlkn0lem.h	$⊢ H = F cyclShift S$
	crctcshwlkn0lem.n	$⊢ N = \|F\|$
	crctcshwlkn0lem.f	$⊢ φ \to F \in Word A$
	crctcshwlkn0lem.p	$⊢ φ \to \forall i \in (0 ..^N) if- (P (i) = P (i + 1), I (F (i)) = \{P (i)\}, \{P (i), P (i + 1)\} \subseteq I (F (i)))$
Assertion	crctcshwlkn0lem5	$⊢ φ \to \forall j \in (N - S + 1 ..^N) if- (Q (j) = Q (j + 1), I (H (j)) = \{Q (j)\}, \{Q (j), Q (j + 1)\} \subseteq I (H (j)))$

Proof

Step	Hyp	Ref	Expression
1		crctcshwlkn0lem.s	$⊢ φ \to S \in (1 ..^N)$
2		crctcshwlkn0lem.q	$⊢ Q = (x \in (0 \dots N) ⟼ if (x \leq N - S, P (x + S), P (x + S - N)))$
3		crctcshwlkn0lem.h	$⊢ H = F cyclShift S$
4		crctcshwlkn0lem.n	$⊢ N = \|F\|$
5		crctcshwlkn0lem.f	$⊢ φ \to F \in Word A$
6		crctcshwlkn0lem.p	$⊢ φ \to \forall i \in (0 ..^N) if- (P (i) = P (i + 1), I (F (i)) = \{P (i)\}, \{P (i), P (i + 1)\} \subseteq I (F (i)))$
7		elfzoelz	$⊢ j \in (N - S + 1 ..^N) \to j \in ℤ$
8	7	zcnd	$⊢ j \in (N - S + 1 ..^N) \to j \in ℂ$
9	8	adantl	$⊢ (S \in (1 ..^N) \land j \in (N - S + 1 ..^N)) \to j \in ℂ$
10		1cnd	$⊢ (S \in (1 ..^N) \land j \in (N - S + 1 ..^N)) \to 1 \in ℂ$
11		elfzoelz	$⊢ S \in (1 ..^N) \to S \in ℤ$
12	11	zcnd	$⊢ S \in (1 ..^N) \to S \in ℂ$
13	12	adantr	$⊢ (S \in (1 ..^N) \land j \in (N - S + 1 ..^N)) \to S \in ℂ$
14		elfzoel2	$⊢ S \in (1 ..^N) \to N \in ℤ$
15	14	zcnd	$⊢ S \in (1 ..^N) \to N \in ℂ$
16	15	adantr	$⊢ (S \in (1 ..^N) \land j \in (N - S + 1 ..^N)) \to N \in ℂ$
17	9 10 13 16	2addsubd	$⊢ (S \in (1 ..^N) \land j \in (N - S + 1 ..^N)) \to (j + 1) + S - N = (j + S) - N + 1$
18	17	eqcomd	$⊢ (S \in (1 ..^N) \land j \in (N - S + 1 ..^N)) \to (j + S) - N + 1 = (j + 1) + S - N$
19		elfzo1	$⊢ S \in (1 ..^N) \leftrightarrow (S \in ℕ \land N \in ℕ \land S < N)$
20		nnz	$⊢ N \in ℕ \to N \in ℤ$
21	20	3ad2ant2	$⊢ (S \in ℕ \land N \in ℕ \land S < N) \to N \in ℤ$
22	21	adantr	$⊢ ((S \in ℕ \land N \in ℕ \land S < N) \land j \in (N - S + 1 ..^N)) \to N \in ℤ$
23	7	adantl	$⊢ ((S \in ℕ \land N \in ℕ \land S < N) \land j \in (N - S + 1 ..^N)) \to j \in ℤ$
24		nnz	$⊢ S \in ℕ \to S \in ℤ$
25	24	3ad2ant1	$⊢ (S \in ℕ \land N \in ℕ \land S < N) \to S \in ℤ$
26	25	adantr	$⊢ ((S \in ℕ \land N \in ℕ \land S < N) \land j \in (N - S + 1 ..^N)) \to S \in ℤ$
27	23 26	zaddcld	$⊢ ((S \in ℕ \land N \in ℕ \land S < N) \land j \in (N - S + 1 ..^N)) \to j + S \in ℤ$
28		elfzo2	$⊢ j \in (N - S + 1 ..^N) \leftrightarrow (j \in ℤ_{\geq (N - S + 1)} \land N \in ℤ \land j < N)$
29		eluz2	$⊢ j \in ℤ_{\geq (N - S + 1)} \leftrightarrow (N - S + 1 \in ℤ \land j \in ℤ \land N - S + 1 \leq j)$
30		zre	$⊢ j \in ℤ \to j \in ℝ$
31		nnre	$⊢ S \in ℕ \to S \in ℝ$
32		nnre	$⊢ N \in ℕ \to N \in ℝ$
33	31 32	anim12i	$⊢ (S \in ℕ \land N \in ℕ) \to (S \in ℝ \land N \in ℝ)$
34		simplr	$⊢ ((S \in ℝ \land N \in ℝ) \land j \in ℝ) \to N \in ℝ$
35		simpll	$⊢ ((S \in ℝ \land N \in ℝ) \land j \in ℝ) \to S \in ℝ$
36	34 35	resubcld	$⊢ ((S \in ℝ \land N \in ℝ) \land j \in ℝ) \to N - S \in ℝ$
37	36	lep1d	$⊢ ((S \in ℝ \land N \in ℝ) \land j \in ℝ) \to N - S \leq N - S + 1$
38		1red	$⊢ ((S \in ℝ \land N \in ℝ) \land j \in ℝ) \to 1 \in ℝ$
39	36 38	readdcld	$⊢ ((S \in ℝ \land N \in ℝ) \land j \in ℝ) \to N - S + 1 \in ℝ$
40		simpr	$⊢ ((S \in ℝ \land N \in ℝ) \land j \in ℝ) \to j \in ℝ$
41		letr	$⊢ (N - S \in ℝ \land N - S + 1 \in ℝ \land j \in ℝ) \to ((N - S \leq N - S + 1 \land N - S + 1 \leq j) \to N - S \leq j)$
42	36 39 40 41	syl3anc	$⊢ ((S \in ℝ \land N \in ℝ) \land j \in ℝ) \to ((N - S \leq N - S + 1 \land N - S + 1 \leq j) \to N - S \leq j)$
43	37 42	mpand	$⊢ ((S \in ℝ \land N \in ℝ) \land j \in ℝ) \to (N - S + 1 \leq j \to N - S \leq j)$
44	34 35 40	lesubaddd	$⊢ ((S \in ℝ \land N \in ℝ) \land j \in ℝ) \to (N - S \leq j \leftrightarrow N \leq j + S)$
45	43 44	sylibd	$⊢ ((S \in ℝ \land N \in ℝ) \land j \in ℝ) \to (N - S + 1 \leq j \to N \leq j + S)$
46	45	ex	$⊢ (S \in ℝ \land N \in ℝ) \to (j \in ℝ \to (N - S + 1 \leq j \to N \leq j + S))$
47	33 46	syl	$⊢ (S \in ℕ \land N \in ℕ) \to (j \in ℝ \to (N - S + 1 \leq j \to N \leq j + S))$
48	47	3adant3	$⊢ (S \in ℕ \land N \in ℕ \land S < N) \to (j \in ℝ \to (N - S + 1 \leq j \to N \leq j + S))$
49	30 48	syl5com	$⊢ j \in ℤ \to ((S \in ℕ \land N \in ℕ \land S < N) \to (N - S + 1 \leq j \to N \leq j + S))$
50	49	com23	$⊢ j \in ℤ \to (N - S + 1 \leq j \to ((S \in ℕ \land N \in ℕ \land S < N) \to N \leq j + S))$
51	50	imp	$⊢ (j \in ℤ \land N - S + 1 \leq j) \to ((S \in ℕ \land N \in ℕ \land S < N) \to N \leq j + S)$
52	51	3adant1	$⊢ (N - S + 1 \in ℤ \land j \in ℤ \land N - S + 1 \leq j) \to ((S \in ℕ \land N \in ℕ \land S < N) \to N \leq j + S)$
53	29 52	sylbi	$⊢ j \in ℤ_{\geq (N - S + 1)} \to ((S \in ℕ \land N \in ℕ \land S < N) \to N \leq j + S)$
54	53	3ad2ant1	$⊢ (j \in ℤ_{\geq (N - S + 1)} \land N \in ℤ \land j < N) \to ((S \in ℕ \land N \in ℕ \land S < N) \to N \leq j + S)$
55	54	com12	$⊢ (S \in ℕ \land N \in ℕ \land S < N) \to ((j \in ℤ_{\geq (N - S + 1)} \land N \in ℤ \land j < N) \to N \leq j + S)$
56	28 55	syl5bi	$⊢ (S \in ℕ \land N \in ℕ \land S < N) \to (j \in (N - S + 1 ..^N) \to N \leq j + S)$
57	56	imp	$⊢ ((S \in ℕ \land N \in ℕ \land S < N) \land j \in (N - S + 1 ..^N)) \to N \leq j + S$
58		eluz2	$⊢ j + S \in ℤ_{\geq N} \leftrightarrow (N \in ℤ \land j + S \in ℤ \land N \leq j + S)$
59	22 27 57 58	syl3anbrc	$⊢ ((S \in ℕ \land N \in ℕ \land S < N) \land j \in (N - S + 1 ..^N)) \to j + S \in ℤ_{\geq N}$
60		uznn0sub	$⊢ j + S \in ℤ_{\geq N} \to j + S - N \in ℕ_{0}$
61	59 60	syl	$⊢ ((S \in ℕ \land N \in ℕ \land S < N) \land j \in (N - S + 1 ..^N)) \to j + S - N \in ℕ_{0}$
62		simpl2	$⊢ ((S \in ℕ \land N \in ℕ \land S < N) \land j \in (N - S + 1 ..^N)) \to N \in ℕ$
63	30	adantl	$⊢ ((S \in ℝ \land N \in ℝ) \land j \in ℤ) \to j \in ℝ$
64		simpll	$⊢ ((S \in ℝ \land N \in ℝ) \land j \in ℤ) \to S \in ℝ$
65		ax-1	$⊢ N \in ℝ \to (S \in ℝ \to N \in ℝ)$
66	65	imdistanri	$⊢ (S \in ℝ \land N \in ℝ) \to (N \in ℝ \land N \in ℝ)$
67	66	adantr	$⊢ ((S \in ℝ \land N \in ℝ) \land j \in ℤ) \to (N \in ℝ \land N \in ℝ)$
68		lt2add	$⊢ ((j \in ℝ \land S \in ℝ) \land (N \in ℝ \land N \in ℝ)) \to ((j < N \land S < N) \to j + S < N + N)$
69	63 64 67 68	syl21anc	$⊢ ((S \in ℝ \land N \in ℝ) \land j \in ℤ) \to ((j < N \land S < N) \to j + S < N + N)$
70	63 64	readdcld	$⊢ ((S \in ℝ \land N \in ℝ) \land j \in ℤ) \to j + S \in ℝ$
71		simplr	$⊢ ((S \in ℝ \land N \in ℝ) \land j \in ℤ) \to N \in ℝ$
72	70 71 71	ltsubaddd	$⊢ ((S \in ℝ \land N \in ℝ) \land j \in ℤ) \to (j + S - N < N \leftrightarrow j + S < N + N)$
73	69 72	sylibrd	$⊢ ((S \in ℝ \land N \in ℝ) \land j \in ℤ) \to ((j < N \land S < N) \to j + S - N < N)$
74	73	ex	$⊢ (S \in ℝ \land N \in ℝ) \to (j \in ℤ \to ((j < N \land S < N) \to j + S - N < N))$
75	74	com23	$⊢ (S \in ℝ \land N \in ℝ) \to ((j < N \land S < N) \to (j \in ℤ \to j + S - N < N))$
76	75	expcomd	$⊢ (S \in ℝ \land N \in ℝ) \to (S < N \to (j < N \to (j \in ℤ \to j + S - N < N)))$
77	33 76	syl	$⊢ (S \in ℕ \land N \in ℕ) \to (S < N \to (j < N \to (j \in ℤ \to j + S - N < N)))$
78	77	3impia	$⊢ (S \in ℕ \land N \in ℕ \land S < N) \to (j < N \to (j \in ℤ \to j + S - N < N))$
79	78	com13	$⊢ j \in ℤ \to (j < N \to ((S \in ℕ \land N \in ℕ \land S < N) \to j + S - N < N))$
80	79	3ad2ant2	$⊢ (N - S + 1 \in ℤ \land j \in ℤ \land N - S + 1 \leq j) \to (j < N \to ((S \in ℕ \land N \in ℕ \land S < N) \to j + S - N < N))$
81	29 80	sylbi	$⊢ j \in ℤ_{\geq (N - S + 1)} \to (j < N \to ((S \in ℕ \land N \in ℕ \land S < N) \to j + S - N < N))$
82	81	imp	$⊢ (j \in ℤ_{\geq (N - S + 1)} \land j < N) \to ((S \in ℕ \land N \in ℕ \land S < N) \to j + S - N < N)$
83	82	3adant2	$⊢ (j \in ℤ_{\geq (N - S + 1)} \land N \in ℤ \land j < N) \to ((S \in ℕ \land N \in ℕ \land S < N) \to j + S - N < N)$
84	28 83	sylbi	$⊢ j \in (N - S + 1 ..^N) \to ((S \in ℕ \land N \in ℕ \land S < N) \to j + S - N < N)$
85	84	impcom	$⊢ ((S \in ℕ \land N \in ℕ \land S < N) \land j \in (N - S + 1 ..^N)) \to j + S - N < N$
86	61 62 85	3jca	$⊢ ((S \in ℕ \land N \in ℕ \land S < N) \land j \in (N - S + 1 ..^N)) \to (j + S - N \in ℕ_{0} \land N \in ℕ \land j + S - N < N)$
87	19 86	sylanb	$⊢ (S \in (1 ..^N) \land j \in (N - S + 1 ..^N)) \to (j + S - N \in ℕ_{0} \land N \in ℕ \land j + S - N < N)$
88		elfzo0	$⊢ j + S - N \in (0 ..^N) \leftrightarrow (j + S - N \in ℕ_{0} \land N \in ℕ \land j + S - N < N)$
89	87 88	sylibr	$⊢ (S \in (1 ..^N) \land j \in (N - S + 1 ..^N)) \to j + S - N \in (0 ..^N)$
90	89	adantr	$⊢ ((S \in (1 ..^N) \land j \in (N - S + 1 ..^N)) \land (j + S) - N + 1 = (j + 1) + S - N) \to j + S - N \in (0 ..^N)$
91		fveq2	$⊢ i = j + S - N \to P (i) = P (j + S - N)$
92	91	adantl	$⊢ (((S \in (1 ..^N) \land j \in (N - S + 1 ..^N)) \land (j + S) - N + 1 = (j + 1) + S - N) \land i = j + S - N) \to P (i) = P (j + S - N)$
93		fvoveq1	$⊢ i = j + S - N \to P (i + 1) = P ((j + S) - N + 1)$
94		simpr	$⊢ ((S \in (1 ..^N) \land j \in (N - S + 1 ..^N)) \land (j + S) - N + 1 = (j + 1) + S - N) \to (j + S) - N + 1 = (j + 1) + S - N$
95	94	fveq2d	$⊢ ((S \in (1 ..^N) \land j \in (N - S + 1 ..^N)) \land (j + S) - N + 1 = (j + 1) + S - N) \to P ((j + S) - N + 1) = P ((j + 1) + S - N)$
96	93 95	sylan9eqr	$⊢ (((S \in (1 ..^N) \land j \in (N - S + 1 ..^N)) \land (j + S) - N + 1 = (j + 1) + S - N) \land i = j + S - N) \to P (i + 1) = P ((j + 1) + S - N)$
97	92 96	eqeq12d	$⊢ (((S \in (1 ..^N) \land j \in (N - S + 1 ..^N)) \land (j + S) - N + 1 = (j + 1) + S - N) \land i = j + S - N) \to (P (i) = P (i + 1) \leftrightarrow P (j + S - N) = P ((j + 1) + S - N))$
98		2fveq3	$⊢ i = j + S - N \to I (F (i)) = I (F (j + S - N))$
99	91	sneqd	$⊢ i = j + S - N \to \{P (i)\} = \{P (j + S - N)\}$
100	98 99	eqeq12d	$⊢ i = j + S - N \to (I (F (i)) = \{P (i)\} \leftrightarrow I (F (j + S - N)) = \{P (j + S - N)\})$
101	100	adantl	$⊢ (((S \in (1 ..^N) \land j \in (N - S + 1 ..^N)) \land (j + S) - N + 1 = (j + 1) + S - N) \land i = j + S - N) \to (I (F (i)) = \{P (i)\} \leftrightarrow I (F (j + S - N)) = \{P (j + S - N)\})$
102	92 96	preq12d	$⊢ (((S \in (1 ..^N) \land j \in (N - S + 1 ..^N)) \land (j + S) - N + 1 = (j + 1) + S - N) \land i = j + S - N) \to \{P (i), P (i + 1)\} = \{P (j + S - N), P ((j + 1) + S - N)\}$
103		simpr	$⊢ (((S \in (1 ..^N) \land j \in (N - S + 1 ..^N)) \land (j + S) - N + 1 = (j + 1) + S - N) \land i = j + S - N) \to i = j + S - N$
104	103	fveq2d	$⊢ (((S \in (1 ..^N) \land j \in (N - S + 1 ..^N)) \land (j + S) - N + 1 = (j + 1) + S - N) \land i = j + S - N) \to F (i) = F (j + S - N)$
105	104	fveq2d	$⊢ (((S \in (1 ..^N) \land j \in (N - S + 1 ..^N)) \land (j + S) - N + 1 = (j + 1) + S - N) \land i = j + S - N) \to I (F (i)) = I (F (j + S - N))$
106	102 105	sseq12d	$⊢ (((S \in (1 ..^N) \land j \in (N - S + 1 ..^N)) \land (j + S) - N + 1 = (j + 1) + S - N) \land i = j + S - N) \to (\{P (i), P (i + 1)\} \subseteq I (F (i)) \leftrightarrow \{P (j + S - N), P ((j + 1) + S - N)\} \subseteq I (F (j + S - N)))$
107	97 101 106	ifpbi123d	$⊢ (((S \in (1 ..^N) \land j \in (N - S + 1 ..^N)) \land (j + S) - N + 1 = (j + 1) + S - N) \land i = j + S - N) \to (if- (P (i) = P (i + 1), I (F (i)) = \{P (i)\}, \{P (i), P (i + 1)\} \subseteq I (F (i))) \leftrightarrow if- (P (j + S - N) = P ((j + 1) + S - N), I (F (j + S - N)) = \{P (j + S - N)\}, \{P (j + S - N), P ((j + 1) + S - N)\} \subseteq I (F (j + S - N))))$
108	90 107	rspcdv	$⊢ ((S \in (1 ..^N) \land j \in (N - S + 1 ..^N)) \land (j + S) - N + 1 = (j + 1) + S - N) \to (\forall i \in (0 ..^N) if- (P (i) = P (i + 1), I (F (i)) = \{P (i)\}, \{P (i), P (i + 1)\} \subseteq I (F (i))) \to if- (P (j + S - N) = P ((j + 1) + S - N), I (F (j + S - N)) = \{P (j + S - N)\}, \{P (j + S - N), P ((j + 1) + S - N)\} \subseteq I (F (j + S - N))))$
109	18 108	mpdan	$⊢ (S \in (1 ..^N) \land j \in (N - S + 1 ..^N)) \to (\forall i \in (0 ..^N) if- (P (i) = P (i + 1), I (F (i)) = \{P (i)\}, \{P (i), P (i + 1)\} \subseteq I (F (i))) \to if- (P (j + S - N) = P ((j + 1) + S - N), I (F (j + S - N)) = \{P (j + S - N)\}, \{P (j + S - N), P ((j + 1) + S - N)\} \subseteq I (F (j + S - N))))$
110	1 109	sylan	$⊢ (φ \land j \in (N - S + 1 ..^N)) \to (\forall i \in (0 ..^N) if- (P (i) = P (i + 1), I (F (i)) = \{P (i)\}, \{P (i), P (i + 1)\} \subseteq I (F (i))) \to if- (P (j + S - N) = P ((j + 1) + S - N), I (F (j + S - N)) = \{P (j + S - N)\}, \{P (j + S - N), P ((j + 1) + S - N)\} \subseteq I (F (j + S - N))))$
111	110	ex	$⊢ φ \to (j \in (N - S + 1 ..^N) \to (\forall i \in (0 ..^N) if- (P (i) = P (i + 1), I (F (i)) = \{P (i)\}, \{P (i), P (i + 1)\} \subseteq I (F (i))) \to if- (P (j + S - N) = P ((j + 1) + S - N), I (F (j + S - N)) = \{P (j + S - N)\}, \{P (j + S - N), P ((j + 1) + S - N)\} \subseteq I (F (j + S - N)))))$
112	6 111	mpid	$⊢ φ \to (j \in (N - S + 1 ..^N) \to if- (P (j + S - N) = P ((j + 1) + S - N), I (F (j + S - N)) = \{P (j + S - N)\}, \{P (j + S - N), P ((j + 1) + S - N)\} \subseteq I (F (j + S - N))))$
113	112	imp	$⊢ (φ \land j \in (N - S + 1 ..^N)) \to if- (P (j + S - N) = P ((j + 1) + S - N), I (F (j + S - N)) = \{P (j + S - N)\}, \{P (j + S - N), P ((j + 1) + S - N)\} \subseteq I (F (j + S - N)))$
114		elfzofz	$⊢ j \in (N - S + 1 ..^N) \to j \in (N - S + 1 \dots N)$
115	1 2	crctcshwlkn0lem3	$⊢ (φ \land j \in (N - S + 1 \dots N)) \to Q (j) = P (j + S - N)$
116	114 115	sylan2	$⊢ (φ \land j \in (N - S + 1 ..^N)) \to Q (j) = P (j + S - N)$
117		fzofzp1	$⊢ j \in (N - S + 1 ..^N) \to j + 1 \in (N - S + 1 \dots N)$
118	1 2	crctcshwlkn0lem3	$⊢ (φ \land j + 1 \in (N - S + 1 \dots N)) \to Q (j + 1) = P ((j + 1) + S - N)$
119	117 118	sylan2	$⊢ (φ \land j \in (N - S + 1 ..^N)) \to Q (j + 1) = P ((j + 1) + S - N)$
120	3	fveq1i	$⊢ H (j) = (F cyclShift S) (j)$
121	5	adantr	$⊢ (φ \land j \in (N - S + 1 ..^N)) \to F \in Word A$
122	1 11	syl	$⊢ φ \to S \in ℤ$
123	122	adantr	$⊢ (φ \land j \in (N - S + 1 ..^N)) \to S \in ℤ$
124		ltle	$⊢ (S \in ℝ \land N \in ℝ) \to (S < N \to S \leq N)$
125	33 124	syl	$⊢ (S \in ℕ \land N \in ℕ) \to (S < N \to S \leq N)$
126	125	3impia	$⊢ (S \in ℕ \land N \in ℕ \land S < N) \to S \leq N$
127		nnnn0	$⊢ S \in ℕ \to S \in ℕ_{0}$
128		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
129	127 128	anim12i	$⊢ (S \in ℕ \land N \in ℕ) \to (S \in ℕ_{0} \land N \in ℕ_{0})$
130	129	3adant3	$⊢ (S \in ℕ \land N \in ℕ \land S < N) \to (S \in ℕ_{0} \land N \in ℕ_{0})$
131		nn0sub	$⊢ (S \in ℕ_{0} \land N \in ℕ_{0}) \to (S \leq N \leftrightarrow N - S \in ℕ_{0})$
132	130 131	syl	$⊢ (S \in ℕ \land N \in ℕ \land S < N) \to (S \leq N \leftrightarrow N - S \in ℕ_{0})$
133	126 132	mpbid	$⊢ (S \in ℕ \land N \in ℕ \land S < N) \to N - S \in ℕ_{0}$
134	19 133	sylbi	$⊢ S \in (1 ..^N) \to N - S \in ℕ_{0}$
135		1nn0	$⊢ 1 \in ℕ_{0}$
136	135	a1i	$⊢ S \in (1 ..^N) \to 1 \in ℕ_{0}$
137	134 136	nn0addcld	$⊢ S \in (1 ..^N) \to N - S + 1 \in ℕ_{0}$
138		elnn0uz	$⊢ N - S + 1 \in ℕ_{0} \leftrightarrow N - S + 1 \in ℤ_{\geq 0}$
139	137 138	sylib	$⊢ S \in (1 ..^N) \to N - S + 1 \in ℤ_{\geq 0}$
140		fzoss1	$⊢ N - S + 1 \in ℤ_{\geq 0} \to (N - S + 1 ..^N) \subseteq (0 ..^N)$
141	1 139 140	3syl	$⊢ φ \to (N - S + 1 ..^N) \subseteq (0 ..^N)$
142	141	sselda	$⊢ (φ \land j \in (N - S + 1 ..^N)) \to j \in (0 ..^N)$
143	4	oveq2i	$⊢ (0 ..^N) = (0 ..^\|F\|)$
144	142 143	eleqtrdi	$⊢ (φ \land j \in (N - S + 1 ..^N)) \to j \in (0 ..^\|F\|)$
145		cshwidxmod	$⊢ (F \in Word A \land S \in ℤ \land j \in (0 ..^\|F\|)) \to (F cyclShift S) (j) = F ((j + S) \mod \|F\|)$
146	121 123 144 145	syl3anc	$⊢ (φ \land j \in (N - S + 1 ..^N)) \to (F cyclShift S) (j) = F ((j + S) \mod \|F\|)$
147	4	eqcomi	$⊢ \|F\| = N$
148	147	oveq2i	$⊢ (j + S) \mod \|F\| = (j + S) \mod N$
149		eluzelre	$⊢ j \in ℤ_{\geq (N - S + 1)} \to j \in ℝ$
150	149	3ad2ant1	$⊢ (j \in ℤ_{\geq (N - S + 1)} \land N \in ℤ \land j < N) \to j \in ℝ$
151	150	adantl	$⊢ ((S \in ℕ \land N \in ℕ \land S < N) \land (j \in ℤ_{\geq (N - S + 1)} \land N \in ℤ \land j < N)) \to j \in ℝ$
152	31	3ad2ant1	$⊢ (S \in ℕ \land N \in ℕ \land S < N) \to S \in ℝ$
153	152	adantr	$⊢ ((S \in ℕ \land N \in ℕ \land S < N) \land (j \in ℤ_{\geq (N - S + 1)} \land N \in ℤ \land j < N)) \to S \in ℝ$
154	151 153	readdcld	$⊢ ((S \in ℕ \land N \in ℕ \land S < N) \land (j \in ℤ_{\geq (N - S + 1)} \land N \in ℤ \land j < N)) \to j + S \in ℝ$
155		nnrp	$⊢ N \in ℕ \to N \in ℝ^{+}$
156	155	3ad2ant2	$⊢ (S \in ℕ \land N \in ℕ \land S < N) \to N \in ℝ^{+}$
157	156	adantr	$⊢ ((S \in ℕ \land N \in ℕ \land S < N) \land (j \in ℤ_{\geq (N - S + 1)} \land N \in ℤ \land j < N)) \to N \in ℝ^{+}$
158	54	impcom	$⊢ ((S \in ℕ \land N \in ℕ \land S < N) \land (j \in ℤ_{\geq (N - S + 1)} \land N \in ℤ \land j < N)) \to N \leq j + S$
159	157	rpred	$⊢ ((S \in ℕ \land N \in ℕ \land S < N) \land (j \in ℤ_{\geq (N - S + 1)} \land N \in ℤ \land j < N)) \to N \in ℝ$
160		simpr3	$⊢ ((S \in ℕ \land N \in ℕ \land S < N) \land (j \in ℤ_{\geq (N - S + 1)} \land N \in ℤ \land j < N)) \to j < N$
161		simpl3	$⊢ ((S \in ℕ \land N \in ℕ \land S < N) \land (j \in ℤ_{\geq (N - S + 1)} \land N \in ℤ \land j < N)) \to S < N$
162	151 153 159 160 161	lt2addmuld	$⊢ ((S \in ℕ \land N \in ℕ \land S < N) \land (j \in ℤ_{\geq (N - S + 1)} \land N \in ℤ \land j < N)) \to j + S < 2 \cdot N$
163	158 162	jca	$⊢ ((S \in ℕ \land N \in ℕ \land S < N) \land (j \in ℤ_{\geq (N - S + 1)} \land N \in ℤ \land j < N)) \to (N \leq j + S \land j + S < 2 \cdot N)$
164	154 157 163	jca31	$⊢ ((S \in ℕ \land N \in ℕ \land S < N) \land (j \in ℤ_{\geq (N - S + 1)} \land N \in ℤ \land j < N)) \to ((j + S \in ℝ \land N \in ℝ^{+}) \land (N \leq j + S \land j + S < 2 \cdot N))$
165	164	ex	$⊢ (S \in ℕ \land N \in ℕ \land S < N) \to ((j \in ℤ_{\geq (N - S + 1)} \land N \in ℤ \land j < N) \to ((j + S \in ℝ \land N \in ℝ^{+}) \land (N \leq j + S \land j + S < 2 \cdot N)))$
166	28 165	syl5bi	$⊢ (S \in ℕ \land N \in ℕ \land S < N) \to (j \in (N - S + 1 ..^N) \to ((j + S \in ℝ \land N \in ℝ^{+}) \land (N \leq j + S \land j + S < 2 \cdot N)))$
167	19 166	sylbi	$⊢ S \in (1 ..^N) \to (j \in (N - S + 1 ..^N) \to ((j + S \in ℝ \land N \in ℝ^{+}) \land (N \leq j + S \land j + S < 2 \cdot N)))$
168	1 167	syl	$⊢ φ \to (j \in (N - S + 1 ..^N) \to ((j + S \in ℝ \land N \in ℝ^{+}) \land (N \leq j + S \land j + S < 2 \cdot N)))$
169	168	imp	$⊢ (φ \land j \in (N - S + 1 ..^N)) \to ((j + S \in ℝ \land N \in ℝ^{+}) \land (N \leq j + S \land j + S < 2 \cdot N))$
170		2submod	$⊢ ((j + S \in ℝ \land N \in ℝ^{+}) \land (N \leq j + S \land j + S < 2 \cdot N)) \to (j + S) \mod N = j + S - N$
171	169 170	syl	$⊢ (φ \land j \in (N - S + 1 ..^N)) \to (j + S) \mod N = j + S - N$
172	148 171	eqtrid	$⊢ (φ \land j \in (N - S + 1 ..^N)) \to (j + S) \mod \|F\| = j + S - N$
173	172	fveq2d	$⊢ (φ \land j \in (N - S + 1 ..^N)) \to F ((j + S) \mod \|F\|) = F (j + S - N)$
174	146 173	eqtrd	$⊢ (φ \land j \in (N - S + 1 ..^N)) \to (F cyclShift S) (j) = F (j + S - N)$
175	120 174	eqtrid	$⊢ (φ \land j \in (N - S + 1 ..^N)) \to H (j) = F (j + S - N)$
176	175	fveq2d	$⊢ (φ \land j \in (N - S + 1 ..^N)) \to I (H (j)) = I (F (j + S - N))$
177		simp1	$⊢ (Q (j) = P (j + S - N) \land Q (j + 1) = P ((j + 1) + S - N) \land I (H (j)) = I (F (j + S - N))) \to Q (j) = P (j + S - N)$
178		simp2	$⊢ (Q (j) = P (j + S - N) \land Q (j + 1) = P ((j + 1) + S - N) \land I (H (j)) = I (F (j + S - N))) \to Q (j + 1) = P ((j + 1) + S - N)$
179	177 178	eqeq12d	$⊢ (Q (j) = P (j + S - N) \land Q (j + 1) = P ((j + 1) + S - N) \land I (H (j)) = I (F (j + S - N))) \to (Q (j) = Q (j + 1) \leftrightarrow P (j + S - N) = P ((j + 1) + S - N))$
180		simp3	$⊢ (Q (j) = P (j + S - N) \land Q (j + 1) = P ((j + 1) + S - N) \land I (H (j)) = I (F (j + S - N))) \to I (H (j)) = I (F (j + S - N))$
181	177	sneqd	$⊢ (Q (j) = P (j + S - N) \land Q (j + 1) = P ((j + 1) + S - N) \land I (H (j)) = I (F (j + S - N))) \to \{Q (j)\} = \{P (j + S - N)\}$
182	180 181	eqeq12d	$⊢ (Q (j) = P (j + S - N) \land Q (j + 1) = P ((j + 1) + S - N) \land I (H (j)) = I (F (j + S - N))) \to (I (H (j)) = \{Q (j)\} \leftrightarrow I (F (j + S - N)) = \{P (j + S - N)\})$
183	177 178	preq12d	$⊢ (Q (j) = P (j + S - N) \land Q (j + 1) = P ((j + 1) + S - N) \land I (H (j)) = I (F (j + S - N))) \to \{Q (j), Q (j + 1)\} = \{P (j + S - N), P ((j + 1) + S - N)\}$
184	183 180	sseq12d	$⊢ (Q (j) = P (j + S - N) \land Q (j + 1) = P ((j + 1) + S - N) \land I (H (j)) = I (F (j + S - N))) \to (\{Q (j), Q (j + 1)\} \subseteq I (H (j)) \leftrightarrow \{P (j + S - N), P ((j + 1) + S - N)\} \subseteq I (F (j + S - N)))$
185	179 182 184	ifpbi123d	$⊢ (Q (j) = P (j + S - N) \land Q (j + 1) = P ((j + 1) + S - N) \land I (H (j)) = I (F (j + S - N))) \to (if- (Q (j) = Q (j + 1), I (H (j)) = \{Q (j)\}, \{Q (j), Q (j + 1)\} \subseteq I (H (j))) \leftrightarrow if- (P (j + S - N) = P ((j + 1) + S - N), I (F (j + S - N)) = \{P (j + S - N)\}, \{P (j + S - N), P ((j + 1) + S - N)\} \subseteq I (F (j + S - N))))$
186	116 119 176 185	syl3anc	$⊢ (φ \land j \in (N - S + 1 ..^N)) \to (if- (Q (j) = Q (j + 1), I (H (j)) = \{Q (j)\}, \{Q (j), Q (j + 1)\} \subseteq I (H (j))) \leftrightarrow if- (P (j + S - N) = P ((j + 1) + S - N), I (F (j + S - N)) = \{P (j + S - N)\}, \{P (j + S - N), P ((j + 1) + S - N)\} \subseteq I (F (j + S - N))))$
187	113 186	mpbird	$⊢ (φ \land j \in (N - S + 1 ..^N)) \to if- (Q (j) = Q (j + 1), I (H (j)) = \{Q (j)\}, \{Q (j), Q (j + 1)\} \subseteq I (H (j)))$
188	187	ralrimiva	$⊢ φ \to \forall j \in (N - S + 1 ..^N) if- (Q (j) = Q (j + 1), I (H (j)) = \{Q (j)\}, \{Q (j), Q (j + 1)\} \subseteq I (H (j)))$

Metamath Proof Explorer

Theorem crctcshwlkn0lem5

Proof