crctcshwlkn0lem6

	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)))$
	crctcshwlkn0lem.e	$⊢ φ \to P (N) = P (0)$
Assertion	crctcshwlkn0lem6	$⊢ (φ \land J = N - S) \to 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		crctcshwlkn0lem.e	$⊢ φ \to P (N) = P (0)$
8		oveq1	$⊢ i = 0 \to i + 1 = 0 + 1$
9		0p1e1	$⊢ 0 + 1 = 1$
10	8 9	eqtrdi	$⊢ i = 0 \to i + 1 = 1$
11		wkslem2	$⊢ (i = 0 \land i + 1 = 1) \to (if- (P (i) = P (i + 1), I (F (i)) = \{P (i)\}, \{P (i), P (i + 1)\} \subseteq I (F (i))) \leftrightarrow if- (P (0) = P (1), I (F (0)) = \{P (0)\}, \{P (0), P (1)\} \subseteq I (F (0))))$
12	10 11	mpdan	$⊢ i = 0 \to (if- (P (i) = P (i + 1), I (F (i)) = \{P (i)\}, \{P (i), P (i + 1)\} \subseteq I (F (i))) \leftrightarrow if- (P (0) = P (1), I (F (0)) = \{P (0)\}, \{P (0), P (1)\} \subseteq I (F (0))))$
13		elfzo1	$⊢ S \in (1 ..^N) \leftrightarrow (S \in ℕ \land N \in ℕ \land S < N)$
14		simp2	$⊢ (S \in ℕ \land N \in ℕ \land S < N) \to N \in ℕ$
15	13 14	sylbi	$⊢ S \in (1 ..^N) \to N \in ℕ$
16	1 15	syl	$⊢ φ \to N \in ℕ$
17		lbfzo0	$⊢ 0 \in (0 ..^N) \leftrightarrow N \in ℕ$
18	16 17	sylibr	$⊢ φ \to 0 \in (0 ..^N)$
19	12 6 18	rspcdva	$⊢ φ \to if- (P (0) = P (1), I (F (0)) = \{P (0)\}, \{P (0), P (1)\} \subseteq I (F (0)))$
20		eqeq1	$⊢ P (N) = P (0) \to (P (N) = P (1) \leftrightarrow P (0) = P (1))$
21		sneq	$⊢ P (N) = P (0) \to \{P (N)\} = \{P (0)\}$
22	21	eqeq2d	$⊢ P (N) = P (0) \to (I (F (0)) = \{P (N)\} \leftrightarrow I (F (0)) = \{P (0)\})$
23		preq1	$⊢ P (N) = P (0) \to \{P (N), P (1)\} = \{P (0), P (1)\}$
24	23	sseq1d	$⊢ P (N) = P (0) \to (\{P (N), P (1)\} \subseteq I (F (0)) \leftrightarrow \{P (0), P (1)\} \subseteq I (F (0)))$
25	20 22 24	ifpbi123d	$⊢ P (N) = P (0) \to (if- (P (N) = P (1), I (F (0)) = \{P (N)\}, \{P (N), P (1)\} \subseteq I (F (0))) \leftrightarrow if- (P (0) = P (1), I (F (0)) = \{P (0)\}, \{P (0), P (1)\} \subseteq I (F (0))))$
26	7 25	syl	$⊢ φ \to (if- (P (N) = P (1), I (F (0)) = \{P (N)\}, \{P (N), P (1)\} \subseteq I (F (0))) \leftrightarrow if- (P (0) = P (1), I (F (0)) = \{P (0)\}, \{P (0), P (1)\} \subseteq I (F (0))))$
27	19 26	mpbird	$⊢ φ \to if- (P (N) = P (1), I (F (0)) = \{P (N)\}, \{P (N), P (1)\} \subseteq I (F (0)))$
28		nncn	$⊢ N \in ℕ \to N \in ℂ$
29		nncn	$⊢ S \in ℕ \to S \in ℂ$
30		npcan	$⊢ (N \in ℂ \land S \in ℂ) \to N - S + S = N$
31	28 29 30	syl2anr	$⊢ (S \in ℕ \land N \in ℕ) \to N - S + S = N$
32		simpr	$⊢ ((S \in ℕ \land N \in ℕ) \land N - S + S = N) \to N - S + S = N$
33		oveq1	$⊢ N - S + S = N \to (N - S + S) \mod \|F\| = N \mod \|F\|$
34	4	eqcomi	$⊢ \|F\| = N$
35	34	a1i	$⊢ (S \in ℕ \land N \in ℕ) \to \|F\| = N$
36	35	oveq2d	$⊢ (S \in ℕ \land N \in ℕ) \to N \mod \|F\| = N \mod N$
37		nnrp	$⊢ N \in ℕ \to N \in ℝ^{+}$
38		modid0	$⊢ N \in ℝ^{+} \to N \mod N = 0$
39	37 38	syl	$⊢ N \in ℕ \to N \mod N = 0$
40	39	adantl	$⊢ (S \in ℕ \land N \in ℕ) \to N \mod N = 0$
41	36 40	eqtrd	$⊢ (S \in ℕ \land N \in ℕ) \to N \mod \|F\| = 0$
42	33 41	sylan9eqr	$⊢ ((S \in ℕ \land N \in ℕ) \land N - S + S = N) \to (N - S + S) \mod \|F\| = 0$
43		simpl	$⊢ ((S \in ℕ \land N \in ℕ) \land N - S + S = N) \to (S \in ℕ \land N \in ℕ)$
44	32 42 43	3jca	$⊢ ((S \in ℕ \land N \in ℕ) \land N - S + S = N) \to (N - S + S = N \land (N - S + S) \mod \|F\| = 0 \land (S \in ℕ \land N \in ℕ))$
45	31 44	mpdan	$⊢ (S \in ℕ \land N \in ℕ) \to (N - S + S = N \land (N - S + S) \mod \|F\| = 0 \land (S \in ℕ \land N \in ℕ))$
46	45	3adant3	$⊢ (S \in ℕ \land N \in ℕ \land S < N) \to (N - S + S = N \land (N - S + S) \mod \|F\| = 0 \land (S \in ℕ \land N \in ℕ))$
47	13 46	sylbi	$⊢ S \in (1 ..^N) \to (N - S + S = N \land (N - S + S) \mod \|F\| = 0 \land (S \in ℕ \land N \in ℕ))$
48		simp1	$⊢ (N - S + S = N \land (N - S + S) \mod \|F\| = 0 \land (S \in ℕ \land N \in ℕ)) \to N - S + S = N$
49	48	fveq2d	$⊢ (N - S + S = N \land (N - S + S) \mod \|F\| = 0 \land (S \in ℕ \land N \in ℕ)) \to P (N - S + S) = P (N)$
50	49	eqeq1d	$⊢ (N - S + S = N \land (N - S + S) \mod \|F\| = 0 \land (S \in ℕ \land N \in ℕ)) \to (P (N - S + S) = P (1) \leftrightarrow P (N) = P (1))$
51		simp2	$⊢ (N - S + S = N \land (N - S + S) \mod \|F\| = 0 \land (S \in ℕ \land N \in ℕ)) \to (N - S + S) \mod \|F\| = 0$
52	51	fveq2d	$⊢ (N - S + S = N \land (N - S + S) \mod \|F\| = 0 \land (S \in ℕ \land N \in ℕ)) \to F ((N - S + S) \mod \|F\|) = F (0)$
53	52	fveq2d	$⊢ (N - S + S = N \land (N - S + S) \mod \|F\| = 0 \land (S \in ℕ \land N \in ℕ)) \to I (F ((N - S + S) \mod \|F\|)) = I (F (0))$
54	49	sneqd	$⊢ (N - S + S = N \land (N - S + S) \mod \|F\| = 0 \land (S \in ℕ \land N \in ℕ)) \to \{P (N - S + S)\} = \{P (N)\}$
55	53 54	eqeq12d	$⊢ (N - S + S = N \land (N - S + S) \mod \|F\| = 0 \land (S \in ℕ \land N \in ℕ)) \to (I (F ((N - S + S) \mod \|F\|)) = \{P (N - S + S)\} \leftrightarrow I (F (0)) = \{P (N)\})$
56	49	preq1d	$⊢ (N - S + S = N \land (N - S + S) \mod \|F\| = 0 \land (S \in ℕ \land N \in ℕ)) \to \{P (N - S + S), P (1)\} = \{P (N), P (1)\}$
57	56 53	sseq12d	$⊢ (N - S + S = N \land (N - S + S) \mod \|F\| = 0 \land (S \in ℕ \land N \in ℕ)) \to (\{P (N - S + S), P (1)\} \subseteq I (F ((N - S + S) \mod \|F\|)) \leftrightarrow \{P (N), P (1)\} \subseteq I (F (0)))$
58	50 55 57	ifpbi123d	$⊢ (N - S + S = N \land (N - S + S) \mod \|F\| = 0 \land (S \in ℕ \land N \in ℕ)) \to (if- (P (N - S + S) = P (1), I (F ((N - S + S) \mod \|F\|)) = \{P (N - S + S)\}, \{P (N - S + S), P (1)\} \subseteq I (F ((N - S + S) \mod \|F\|))) \leftrightarrow if- (P (N) = P (1), I (F (0)) = \{P (N)\}, \{P (N), P (1)\} \subseteq I (F (0))))$
59	1 47 58	3syl	$⊢ φ \to (if- (P (N - S + S) = P (1), I (F ((N - S + S) \mod \|F\|)) = \{P (N - S + S)\}, \{P (N - S + S), P (1)\} \subseteq I (F ((N - S + S) \mod \|F\|))) \leftrightarrow if- (P (N) = P (1), I (F (0)) = \{P (N)\}, \{P (N), P (1)\} \subseteq I (F (0))))$
60	27 59	mpbird	$⊢ φ \to if- (P (N - S + S) = P (1), I (F ((N - S + S) \mod \|F\|)) = \{P (N - S + S)\}, \{P (N - S + S), P (1)\} \subseteq I (F ((N - S + S) \mod \|F\|)))$
61		nnsub	$⊢ (S \in ℕ \land N \in ℕ) \to (S < N \leftrightarrow N - S \in ℕ)$
62	61	biimp3a	$⊢ (S \in ℕ \land N \in ℕ \land S < N) \to N - S \in ℕ$
63	62	nnnn0d	$⊢ (S \in ℕ \land N \in ℕ \land S < N) \to N - S \in ℕ_{0}$
64	13 63	sylbi	$⊢ S \in (1 ..^N) \to N - S \in ℕ_{0}$
65	1 64	syl	$⊢ φ \to N - S \in ℕ_{0}$
66		nn0fz0	$⊢ N - S \in ℕ_{0} \leftrightarrow N - S \in (0 \dots N - S)$
67	65 66	sylib	$⊢ φ \to N - S \in (0 \dots N - S)$
68	1 2	crctcshwlkn0lem2	$⊢ (φ \land N - S \in (0 \dots N - S)) \to Q (N - S) = P (N - S + S)$
69	67 68	mpdan	$⊢ φ \to Q (N - S) = P (N - S + S)$
70		elfzoel2	$⊢ S \in (1 ..^N) \to N \in ℤ$
71		elfzoelz	$⊢ S \in (1 ..^N) \to S \in ℤ$
72	70 71	zsubcld	$⊢ S \in (1 ..^N) \to N - S \in ℤ$
73	72	peano2zd	$⊢ S \in (1 ..^N) \to N - S + 1 \in ℤ$
74		nnre	$⊢ N \in ℕ \to N \in ℝ$
75	74	anim1i	$⊢ (N \in ℕ \land S \in ℕ) \to (N \in ℝ \land S \in ℕ)$
76	75	ancoms	$⊢ (S \in ℕ \land N \in ℕ) \to (N \in ℝ \land S \in ℕ)$
77		crctcshwlkn0lem1	$⊢ (N \in ℝ \land S \in ℕ) \to N - S + 1 \leq N$
78	76 77	syl	$⊢ (S \in ℕ \land N \in ℕ) \to N - S + 1 \leq N$
79	78	3adant3	$⊢ (S \in ℕ \land N \in ℕ \land S < N) \to N - S + 1 \leq N$
80	13 79	sylbi	$⊢ S \in (1 ..^N) \to N - S + 1 \leq N$
81	73 70 80	3jca	$⊢ S \in (1 ..^N) \to (N - S + 1 \in ℤ \land N \in ℤ \land N - S + 1 \leq N)$
82	1 81	syl	$⊢ φ \to (N - S + 1 \in ℤ \land N \in ℤ \land N - S + 1 \leq N)$
83		eluz2	$⊢ N \in ℤ_{\geq (N - S + 1)} \leftrightarrow (N - S + 1 \in ℤ \land N \in ℤ \land N - S + 1 \leq N)$
84	82 83	sylibr	$⊢ φ \to N \in ℤ_{\geq (N - S + 1)}$
85		eluzfz1	$⊢ N \in ℤ_{\geq (N - S + 1)} \to N - S + 1 \in (N - S + 1 \dots N)$
86	84 85	syl	$⊢ φ \to N - S + 1 \in (N - S + 1 \dots N)$
87	1 2	crctcshwlkn0lem3	$⊢ (φ \land N - S + 1 \in (N - S + 1 \dots N)) \to Q (N - S + 1) = P ((N - S + 1) + S - N)$
88	86 87	mpdan	$⊢ φ \to Q (N - S + 1) = P ((N - S + 1) + S - N)$
89		subcl	$⊢ (N \in ℂ \land S \in ℂ) \to N - S \in ℂ$
90	89	ancoms	$⊢ (S \in ℂ \land N \in ℂ) \to N - S \in ℂ$
91		ax-1cn	$⊢ 1 \in ℂ$
92		pncan2	$⊢ (N - S \in ℂ \land 1 \in ℂ) \to (N - S) + 1 - (N - S) = 1$
93	92	eqcomd	$⊢ (N - S \in ℂ \land 1 \in ℂ) \to 1 = (N - S) + 1 - (N - S)$
94	90 91 93	sylancl	$⊢ (S \in ℂ \land N \in ℂ) \to 1 = (N - S) + 1 - (N - S)$
95		peano2cn	$⊢ N - S \in ℂ \to N - S + 1 \in ℂ$
96	90 95	syl	$⊢ (S \in ℂ \land N \in ℂ) \to N - S + 1 \in ℂ$
97		simpr	$⊢ (S \in ℂ \land N \in ℂ) \to N \in ℂ$
98		simpl	$⊢ (S \in ℂ \land N \in ℂ) \to S \in ℂ$
99	96 97 98	subsub3d	$⊢ (S \in ℂ \land N \in ℂ) \to (N - S) + 1 - (N - S) = (N - S + 1) + S - N$
100	94 99	eqtr2d	$⊢ (S \in ℂ \land N \in ℂ) \to (N - S + 1) + S - N = 1$
101	29 28 100	syl2an	$⊢ (S \in ℕ \land N \in ℕ) \to (N - S + 1) + S - N = 1$
102	101	3adant3	$⊢ (S \in ℕ \land N \in ℕ \land S < N) \to (N - S + 1) + S - N = 1$
103	13 102	sylbi	$⊢ S \in (1 ..^N) \to (N - S + 1) + S - N = 1$
104	1 103	syl	$⊢ φ \to (N - S + 1) + S - N = 1$
105	104	fveq2d	$⊢ φ \to P ((N - S + 1) + S - N) = P (1)$
106	88 105	eqtrd	$⊢ φ \to Q (N - S + 1) = P (1)$
107	3	fveq1i	$⊢ H (N - S) = (F cyclShift S) (N - S)$
108	5	adantr	$⊢ (φ \land S \in (1 ..^N)) \to F \in Word A$
109	71	adantl	$⊢ (φ \land S \in (1 ..^N)) \to S \in ℤ$
110		elfzofz	$⊢ S \in (1 ..^N) \to S \in (1 \dots N)$
111		ubmelfzo	$⊢ S \in (1 \dots N) \to N - S \in (0 ..^N)$
112	110 111	syl	$⊢ S \in (1 ..^N) \to N - S \in (0 ..^N)$
113	112	adantl	$⊢ (φ \land S \in (1 ..^N)) \to N - S \in (0 ..^N)$
114	34	oveq2i	$⊢ (0 ..^\|F\|) = (0 ..^N)$
115	113 114	eleqtrrdi	$⊢ (φ \land S \in (1 ..^N)) \to N - S \in (0 ..^\|F\|)$
116		cshwidxmod	$⊢ (F \in Word A \land S \in ℤ \land N - S \in (0 ..^\|F\|)) \to (F cyclShift S) (N - S) = F ((N - S + S) \mod \|F\|)$
117	108 109 115 116	syl3anc	$⊢ (φ \land S \in (1 ..^N)) \to (F cyclShift S) (N - S) = F ((N - S + S) \mod \|F\|)$
118	1 117	mpdan	$⊢ φ \to (F cyclShift S) (N - S) = F ((N - S + S) \mod \|F\|)$
119	107 118	eqtrid	$⊢ φ \to H (N - S) = F ((N - S + S) \mod \|F\|)$
120		simp1	$⊢ (Q (N - S) = P (N - S + S) \land Q (N - S + 1) = P (1) \land H (N - S) = F ((N - S + S) \mod \|F\|)) \to Q (N - S) = P (N - S + S)$
121		simp2	$⊢ (Q (N - S) = P (N - S + S) \land Q (N - S + 1) = P (1) \land H (N - S) = F ((N - S + S) \mod \|F\|)) \to Q (N - S + 1) = P (1)$
122	120 121	eqeq12d	$⊢ (Q (N - S) = P (N - S + S) \land Q (N - S + 1) = P (1) \land H (N - S) = F ((N - S + S) \mod \|F\|)) \to (Q (N - S) = Q (N - S + 1) \leftrightarrow P (N - S + S) = P (1))$
123		simp3	$⊢ (Q (N - S) = P (N - S + S) \land Q (N - S + 1) = P (1) \land H (N - S) = F ((N - S + S) \mod \|F\|)) \to H (N - S) = F ((N - S + S) \mod \|F\|)$
124	123	fveq2d	$⊢ (Q (N - S) = P (N - S + S) \land Q (N - S + 1) = P (1) \land H (N - S) = F ((N - S + S) \mod \|F\|)) \to I (H (N - S)) = I (F ((N - S + S) \mod \|F\|))$
125	120	sneqd	$⊢ (Q (N - S) = P (N - S + S) \land Q (N - S + 1) = P (1) \land H (N - S) = F ((N - S + S) \mod \|F\|)) \to \{Q (N - S)\} = \{P (N - S + S)\}$
126	124 125	eqeq12d	$⊢ (Q (N - S) = P (N - S + S) \land Q (N - S + 1) = P (1) \land H (N - S) = F ((N - S + S) \mod \|F\|)) \to (I (H (N - S)) = \{Q (N - S)\} \leftrightarrow I (F ((N - S + S) \mod \|F\|)) = \{P (N - S + S)\})$
127	120 121	preq12d	$⊢ (Q (N - S) = P (N - S + S) \land Q (N - S + 1) = P (1) \land H (N - S) = F ((N - S + S) \mod \|F\|)) \to \{Q (N - S), Q (N - S + 1)\} = \{P (N - S + S), P (1)\}$
128	127 124	sseq12d	$⊢ (Q (N - S) = P (N - S + S) \land Q (N - S + 1) = P (1) \land H (N - S) = F ((N - S + S) \mod \|F\|)) \to (\{Q (N - S), Q (N - S + 1)\} \subseteq I (H (N - S)) \leftrightarrow \{P (N - S + S), P (1)\} \subseteq I (F ((N - S + S) \mod \|F\|)))$
129	122 126 128	ifpbi123d	$⊢ (Q (N - S) = P (N - S + S) \land Q (N - S + 1) = P (1) \land H (N - S) = F ((N - S + S) \mod \|F\|)) \to (if- (Q (N - S) = Q (N - S + 1), I (H (N - S)) = \{Q (N - S)\}, \{Q (N - S), Q (N - S + 1)\} \subseteq I (H (N - S))) \leftrightarrow if- (P (N - S + S) = P (1), I (F ((N - S + S) \mod \|F\|)) = \{P (N - S + S)\}, \{P (N - S + S), P (1)\} \subseteq I (F ((N - S + S) \mod \|F\|))))$
130	69 106 119 129	syl3anc	$⊢ φ \to (if- (Q (N - S) = Q (N - S + 1), I (H (N - S)) = \{Q (N - S)\}, \{Q (N - S), Q (N - S + 1)\} \subseteq I (H (N - S))) \leftrightarrow if- (P (N - S + S) = P (1), I (F ((N - S + S) \mod \|F\|)) = \{P (N - S + S)\}, \{P (N - S + S), P (1)\} \subseteq I (F ((N - S + S) \mod \|F\|))))$
131	60 130	mpbird	$⊢ φ \to if- (Q (N - S) = Q (N - S + 1), I (H (N - S)) = \{Q (N - S)\}, \{Q (N - S), Q (N - S + 1)\} \subseteq I (H (N - S)))$
132	131	adantr	$⊢ (φ \land J = N - S) \to if- (Q (N - S) = Q (N - S + 1), I (H (N - S)) = \{Q (N - S)\}, \{Q (N - S), Q (N - S + 1)\} \subseteq I (H (N - S)))$
133		wkslem1	$⊢ J = N - S \to (if- (Q (J) = Q (J + 1), I (H (J)) = \{Q (J)\}, \{Q (J), Q (J + 1)\} \subseteq I (H (J))) \leftrightarrow if- (Q (N - S) = Q (N - S + 1), I (H (N - S)) = \{Q (N - S)\}, \{Q (N - S), Q (N - S + 1)\} \subseteq I (H (N - S))))$
134	133	adantl	$⊢ (φ \land J = N - S) \to (if- (Q (J) = Q (J + 1), I (H (J)) = \{Q (J)\}, \{Q (J), Q (J + 1)\} \subseteq I (H (J))) \leftrightarrow if- (Q (N - S) = Q (N - S + 1), I (H (N - S)) = \{Q (N - S)\}, \{Q (N - S), Q (N - S + 1)\} \subseteq I (H (N - S))))$
135	132 134	mpbird	$⊢ (φ \land J = N - S) \to if- (Q (J) = Q (J + 1), I (H (J)) = \{Q (J)\}, \{Q (J), Q (J + 1)\} \subseteq I (H (J)))$

Metamath Proof Explorer

Theorem crctcshwlkn0lem6

Proof