# Metamath Proof Explorer

## Theorem crctcshwlkn0lem4

Description: Lemma for crctcshwlkn0 . (Contributed by AV, 12-Mar-2021)

Ref Expression
Hypotheses crctcshwlkn0lem.s ${⊢}{\phi }\to {S}\in \left(1..^{N}\right)$
crctcshwlkn0lem.q ${⊢}{Q}=\left({x}\in \left(0\dots {N}\right)⟼if\left({x}\le {N}-{S},{P}\left({x}+{S}\right),{P}\left({x}+{S}-{N}\right)\right)\right)$
crctcshwlkn0lem.h ${⊢}{H}={F}\mathrm{cyclShift}{S}$
crctcshwlkn0lem.n ${⊢}{N}=\left|{F}\right|$
crctcshwlkn0lem.f ${⊢}{\phi }\to {F}\in \mathrm{Word}{A}$
crctcshwlkn0lem.p ${⊢}{\phi }\to \forall {i}\in \left(0..^{N}\right)\phantom{\rule{.4em}{0ex}}if-\left({P}\left({i}\right)={P}\left({i}+1\right),{I}\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right)\right\},\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\subseteq {I}\left({F}\left({i}\right)\right)\right)$
Assertion crctcshwlkn0lem4 ${⊢}{\phi }\to \forall {j}\in \left(0..^{N}-{S}\right)\phantom{\rule{.4em}{0ex}}if-\left({Q}\left({j}\right)={Q}\left({j}+1\right),{I}\left({H}\left({j}\right)\right)=\left\{{Q}\left({j}\right)\right\},\left\{{Q}\left({j}\right),{Q}\left({j}+1\right)\right\}\subseteq {I}\left({H}\left({j}\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 crctcshwlkn0lem.s ${⊢}{\phi }\to {S}\in \left(1..^{N}\right)$
2 crctcshwlkn0lem.q ${⊢}{Q}=\left({x}\in \left(0\dots {N}\right)⟼if\left({x}\le {N}-{S},{P}\left({x}+{S}\right),{P}\left({x}+{S}-{N}\right)\right)\right)$
3 crctcshwlkn0lem.h ${⊢}{H}={F}\mathrm{cyclShift}{S}$
4 crctcshwlkn0lem.n ${⊢}{N}=\left|{F}\right|$
5 crctcshwlkn0lem.f ${⊢}{\phi }\to {F}\in \mathrm{Word}{A}$
6 crctcshwlkn0lem.p ${⊢}{\phi }\to \forall {i}\in \left(0..^{N}\right)\phantom{\rule{.4em}{0ex}}if-\left({P}\left({i}\right)={P}\left({i}+1\right),{I}\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right)\right\},\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\subseteq {I}\left({F}\left({i}\right)\right)\right)$
7 elfzoelz ${⊢}{j}\in \left(0..^{N}-{S}\right)\to {j}\in ℤ$
8 7 zcnd ${⊢}{j}\in \left(0..^{N}-{S}\right)\to {j}\in ℂ$
9 8 adantl ${⊢}\left({S}\in \left(1..^{N}\right)\wedge {j}\in \left(0..^{N}-{S}\right)\right)\to {j}\in ℂ$
10 elfzoelz ${⊢}{S}\in \left(1..^{N}\right)\to {S}\in ℤ$
11 10 zcnd ${⊢}{S}\in \left(1..^{N}\right)\to {S}\in ℂ$
12 11 adantr ${⊢}\left({S}\in \left(1..^{N}\right)\wedge {j}\in \left(0..^{N}-{S}\right)\right)\to {S}\in ℂ$
13 1cnd ${⊢}\left({S}\in \left(1..^{N}\right)\wedge {j}\in \left(0..^{N}-{S}\right)\right)\to 1\in ℂ$
14 9 12 13 add32d ${⊢}\left({S}\in \left(1..^{N}\right)\wedge {j}\in \left(0..^{N}-{S}\right)\right)\to {j}+{S}+1={j}+1+{S}$
15 elfzo1 ${⊢}{S}\in \left(1..^{N}\right)↔\left({S}\in ℕ\wedge {N}\in ℕ\wedge {S}<{N}\right)$
16 elfzonn0 ${⊢}{j}\in \left(0..^{N}-{S}\right)\to {j}\in {ℕ}_{0}$
17 nnnn0 ${⊢}{S}\in ℕ\to {S}\in {ℕ}_{0}$
18 nn0addcl ${⊢}\left({j}\in {ℕ}_{0}\wedge {S}\in {ℕ}_{0}\right)\to {j}+{S}\in {ℕ}_{0}$
19 18 ex ${⊢}{j}\in {ℕ}_{0}\to \left({S}\in {ℕ}_{0}\to {j}+{S}\in {ℕ}_{0}\right)$
20 16 17 19 syl2imc ${⊢}{S}\in ℕ\to \left({j}\in \left(0..^{N}-{S}\right)\to {j}+{S}\in {ℕ}_{0}\right)$
21 20 3ad2ant1 ${⊢}\left({S}\in ℕ\wedge {N}\in ℕ\wedge {S}<{N}\right)\to \left({j}\in \left(0..^{N}-{S}\right)\to {j}+{S}\in {ℕ}_{0}\right)$
22 15 21 sylbi ${⊢}{S}\in \left(1..^{N}\right)\to \left({j}\in \left(0..^{N}-{S}\right)\to {j}+{S}\in {ℕ}_{0}\right)$
23 22 imp ${⊢}\left({S}\in \left(1..^{N}\right)\wedge {j}\in \left(0..^{N}-{S}\right)\right)\to {j}+{S}\in {ℕ}_{0}$
24 fzo0ss1 ${⊢}\left(1..^{N}\right)\subseteq \left(0..^{N}\right)$
25 24 sseli ${⊢}{S}\in \left(1..^{N}\right)\to {S}\in \left(0..^{N}\right)$
26 elfzo0 ${⊢}{S}\in \left(0..^{N}\right)↔\left({S}\in {ℕ}_{0}\wedge {N}\in ℕ\wedge {S}<{N}\right)$
27 26 simp2bi ${⊢}{S}\in \left(0..^{N}\right)\to {N}\in ℕ$
28 25 27 syl ${⊢}{S}\in \left(1..^{N}\right)\to {N}\in ℕ$
29 28 adantr ${⊢}\left({S}\in \left(1..^{N}\right)\wedge {j}\in \left(0..^{N}-{S}\right)\right)\to {N}\in ℕ$
30 elfzo0 ${⊢}{j}\in \left(0..^{N}-{S}\right)↔\left({j}\in {ℕ}_{0}\wedge {N}-{S}\in ℕ\wedge {j}<{N}-{S}\right)$
31 nn0re ${⊢}{j}\in {ℕ}_{0}\to {j}\in ℝ$
32 nnre ${⊢}{S}\in ℕ\to {S}\in ℝ$
33 nnre ${⊢}{N}\in ℕ\to {N}\in ℝ$
34 32 33 anim12i ${⊢}\left({S}\in ℕ\wedge {N}\in ℕ\right)\to \left({S}\in ℝ\wedge {N}\in ℝ\right)$
35 34 3adant3 ${⊢}\left({S}\in ℕ\wedge {N}\in ℕ\wedge {S}<{N}\right)\to \left({S}\in ℝ\wedge {N}\in ℝ\right)$
36 15 35 sylbi ${⊢}{S}\in \left(1..^{N}\right)\to \left({S}\in ℝ\wedge {N}\in ℝ\right)$
37 31 36 anim12i ${⊢}\left({j}\in {ℕ}_{0}\wedge {S}\in \left(1..^{N}\right)\right)\to \left({j}\in ℝ\wedge \left({S}\in ℝ\wedge {N}\in ℝ\right)\right)$
38 3anass ${⊢}\left({j}\in ℝ\wedge {S}\in ℝ\wedge {N}\in ℝ\right)↔\left({j}\in ℝ\wedge \left({S}\in ℝ\wedge {N}\in ℝ\right)\right)$
39 37 38 sylibr ${⊢}\left({j}\in {ℕ}_{0}\wedge {S}\in \left(1..^{N}\right)\right)\to \left({j}\in ℝ\wedge {S}\in ℝ\wedge {N}\in ℝ\right)$
40 ltaddsub ${⊢}\left({j}\in ℝ\wedge {S}\in ℝ\wedge {N}\in ℝ\right)\to \left({j}+{S}<{N}↔{j}<{N}-{S}\right)$
41 40 bicomd ${⊢}\left({j}\in ℝ\wedge {S}\in ℝ\wedge {N}\in ℝ\right)\to \left({j}<{N}-{S}↔{j}+{S}<{N}\right)$
42 39 41 syl ${⊢}\left({j}\in {ℕ}_{0}\wedge {S}\in \left(1..^{N}\right)\right)\to \left({j}<{N}-{S}↔{j}+{S}<{N}\right)$
43 42 biimpd ${⊢}\left({j}\in {ℕ}_{0}\wedge {S}\in \left(1..^{N}\right)\right)\to \left({j}<{N}-{S}\to {j}+{S}<{N}\right)$
44 43 ex ${⊢}{j}\in {ℕ}_{0}\to \left({S}\in \left(1..^{N}\right)\to \left({j}<{N}-{S}\to {j}+{S}<{N}\right)\right)$
45 44 com23 ${⊢}{j}\in {ℕ}_{0}\to \left({j}<{N}-{S}\to \left({S}\in \left(1..^{N}\right)\to {j}+{S}<{N}\right)\right)$
46 45 a1d ${⊢}{j}\in {ℕ}_{0}\to \left({N}-{S}\in ℕ\to \left({j}<{N}-{S}\to \left({S}\in \left(1..^{N}\right)\to {j}+{S}<{N}\right)\right)\right)$
47 46 3imp ${⊢}\left({j}\in {ℕ}_{0}\wedge {N}-{S}\in ℕ\wedge {j}<{N}-{S}\right)\to \left({S}\in \left(1..^{N}\right)\to {j}+{S}<{N}\right)$
48 30 47 sylbi ${⊢}{j}\in \left(0..^{N}-{S}\right)\to \left({S}\in \left(1..^{N}\right)\to {j}+{S}<{N}\right)$
49 48 impcom ${⊢}\left({S}\in \left(1..^{N}\right)\wedge {j}\in \left(0..^{N}-{S}\right)\right)\to {j}+{S}<{N}$
50 elfzo0 ${⊢}{j}+{S}\in \left(0..^{N}\right)↔\left({j}+{S}\in {ℕ}_{0}\wedge {N}\in ℕ\wedge {j}+{S}<{N}\right)$
51 23 29 49 50 syl3anbrc ${⊢}\left({S}\in \left(1..^{N}\right)\wedge {j}\in \left(0..^{N}-{S}\right)\right)\to {j}+{S}\in \left(0..^{N}\right)$
52 51 adantr ${⊢}\left(\left({S}\in \left(1..^{N}\right)\wedge {j}\in \left(0..^{N}-{S}\right)\right)\wedge {j}+{S}+1={j}+1+{S}\right)\to {j}+{S}\in \left(0..^{N}\right)$
53 fveq2 ${⊢}{i}={j}+{S}\to {P}\left({i}\right)={P}\left({j}+{S}\right)$
54 53 adantl ${⊢}\left(\left(\left({S}\in \left(1..^{N}\right)\wedge {j}\in \left(0..^{N}-{S}\right)\right)\wedge {j}+{S}+1={j}+1+{S}\right)\wedge {i}={j}+{S}\right)\to {P}\left({i}\right)={P}\left({j}+{S}\right)$
55 fvoveq1 ${⊢}{i}={j}+{S}\to {P}\left({i}+1\right)={P}\left({j}+{S}+1\right)$
56 simpr ${⊢}\left(\left({S}\in \left(1..^{N}\right)\wedge {j}\in \left(0..^{N}-{S}\right)\right)\wedge {j}+{S}+1={j}+1+{S}\right)\to {j}+{S}+1={j}+1+{S}$
57 56 fveq2d ${⊢}\left(\left({S}\in \left(1..^{N}\right)\wedge {j}\in \left(0..^{N}-{S}\right)\right)\wedge {j}+{S}+1={j}+1+{S}\right)\to {P}\left({j}+{S}+1\right)={P}\left({j}+1+{S}\right)$
58 55 57 sylan9eqr ${⊢}\left(\left(\left({S}\in \left(1..^{N}\right)\wedge {j}\in \left(0..^{N}-{S}\right)\right)\wedge {j}+{S}+1={j}+1+{S}\right)\wedge {i}={j}+{S}\right)\to {P}\left({i}+1\right)={P}\left({j}+1+{S}\right)$
59 54 58 eqeq12d ${⊢}\left(\left(\left({S}\in \left(1..^{N}\right)\wedge {j}\in \left(0..^{N}-{S}\right)\right)\wedge {j}+{S}+1={j}+1+{S}\right)\wedge {i}={j}+{S}\right)\to \left({P}\left({i}\right)={P}\left({i}+1\right)↔{P}\left({j}+{S}\right)={P}\left({j}+1+{S}\right)\right)$
60 2fveq3 ${⊢}{i}={j}+{S}\to {I}\left({F}\left({i}\right)\right)={I}\left({F}\left({j}+{S}\right)\right)$
61 53 sneqd ${⊢}{i}={j}+{S}\to \left\{{P}\left({i}\right)\right\}=\left\{{P}\left({j}+{S}\right)\right\}$
62 60 61 eqeq12d ${⊢}{i}={j}+{S}\to \left({I}\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right)\right\}↔{I}\left({F}\left({j}+{S}\right)\right)=\left\{{P}\left({j}+{S}\right)\right\}\right)$
63 62 adantl ${⊢}\left(\left(\left({S}\in \left(1..^{N}\right)\wedge {j}\in \left(0..^{N}-{S}\right)\right)\wedge {j}+{S}+1={j}+1+{S}\right)\wedge {i}={j}+{S}\right)\to \left({I}\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right)\right\}↔{I}\left({F}\left({j}+{S}\right)\right)=\left\{{P}\left({j}+{S}\right)\right\}\right)$
64 54 58 preq12d ${⊢}\left(\left(\left({S}\in \left(1..^{N}\right)\wedge {j}\in \left(0..^{N}-{S}\right)\right)\wedge {j}+{S}+1={j}+1+{S}\right)\wedge {i}={j}+{S}\right)\to \left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}=\left\{{P}\left({j}+{S}\right),{P}\left({j}+1+{S}\right)\right\}$
65 60 adantl ${⊢}\left(\left(\left({S}\in \left(1..^{N}\right)\wedge {j}\in \left(0..^{N}-{S}\right)\right)\wedge {j}+{S}+1={j}+1+{S}\right)\wedge {i}={j}+{S}\right)\to {I}\left({F}\left({i}\right)\right)={I}\left({F}\left({j}+{S}\right)\right)$
66 64 65 sseq12d ${⊢}\left(\left(\left({S}\in \left(1..^{N}\right)\wedge {j}\in \left(0..^{N}-{S}\right)\right)\wedge {j}+{S}+1={j}+1+{S}\right)\wedge {i}={j}+{S}\right)\to \left(\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\subseteq {I}\left({F}\left({i}\right)\right)↔\left\{{P}\left({j}+{S}\right),{P}\left({j}+1+{S}\right)\right\}\subseteq {I}\left({F}\left({j}+{S}\right)\right)\right)$
67 59 63 66 ifpbi123d ${⊢}\left(\left(\left({S}\in \left(1..^{N}\right)\wedge {j}\in \left(0..^{N}-{S}\right)\right)\wedge {j}+{S}+1={j}+1+{S}\right)\wedge {i}={j}+{S}\right)\to \left(if-\left({P}\left({i}\right)={P}\left({i}+1\right),{I}\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right)\right\},\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\subseteq {I}\left({F}\left({i}\right)\right)\right)↔if-\left({P}\left({j}+{S}\right)={P}\left({j}+1+{S}\right),{I}\left({F}\left({j}+{S}\right)\right)=\left\{{P}\left({j}+{S}\right)\right\},\left\{{P}\left({j}+{S}\right),{P}\left({j}+1+{S}\right)\right\}\subseteq {I}\left({F}\left({j}+{S}\right)\right)\right)\right)$
68 52 67 rspcdv ${⊢}\left(\left({S}\in \left(1..^{N}\right)\wedge {j}\in \left(0..^{N}-{S}\right)\right)\wedge {j}+{S}+1={j}+1+{S}\right)\to \left(\forall {i}\in \left(0..^{N}\right)\phantom{\rule{.4em}{0ex}}if-\left({P}\left({i}\right)={P}\left({i}+1\right),{I}\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right)\right\},\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\subseteq {I}\left({F}\left({i}\right)\right)\right)\to if-\left({P}\left({j}+{S}\right)={P}\left({j}+1+{S}\right),{I}\left({F}\left({j}+{S}\right)\right)=\left\{{P}\left({j}+{S}\right)\right\},\left\{{P}\left({j}+{S}\right),{P}\left({j}+1+{S}\right)\right\}\subseteq {I}\left({F}\left({j}+{S}\right)\right)\right)\right)$
69 14 68 mpdan ${⊢}\left({S}\in \left(1..^{N}\right)\wedge {j}\in \left(0..^{N}-{S}\right)\right)\to \left(\forall {i}\in \left(0..^{N}\right)\phantom{\rule{.4em}{0ex}}if-\left({P}\left({i}\right)={P}\left({i}+1\right),{I}\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right)\right\},\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\subseteq {I}\left({F}\left({i}\right)\right)\right)\to if-\left({P}\left({j}+{S}\right)={P}\left({j}+1+{S}\right),{I}\left({F}\left({j}+{S}\right)\right)=\left\{{P}\left({j}+{S}\right)\right\},\left\{{P}\left({j}+{S}\right),{P}\left({j}+1+{S}\right)\right\}\subseteq {I}\left({F}\left({j}+{S}\right)\right)\right)\right)$
70 1 69 sylan ${⊢}\left({\phi }\wedge {j}\in \left(0..^{N}-{S}\right)\right)\to \left(\forall {i}\in \left(0..^{N}\right)\phantom{\rule{.4em}{0ex}}if-\left({P}\left({i}\right)={P}\left({i}+1\right),{I}\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right)\right\},\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\subseteq {I}\left({F}\left({i}\right)\right)\right)\to if-\left({P}\left({j}+{S}\right)={P}\left({j}+1+{S}\right),{I}\left({F}\left({j}+{S}\right)\right)=\left\{{P}\left({j}+{S}\right)\right\},\left\{{P}\left({j}+{S}\right),{P}\left({j}+1+{S}\right)\right\}\subseteq {I}\left({F}\left({j}+{S}\right)\right)\right)\right)$
71 70 ex ${⊢}{\phi }\to \left({j}\in \left(0..^{N}-{S}\right)\to \left(\forall {i}\in \left(0..^{N}\right)\phantom{\rule{.4em}{0ex}}if-\left({P}\left({i}\right)={P}\left({i}+1\right),{I}\left({F}\left({i}\right)\right)=\left\{{P}\left({i}\right)\right\},\left\{{P}\left({i}\right),{P}\left({i}+1\right)\right\}\subseteq {I}\left({F}\left({i}\right)\right)\right)\to if-\left({P}\left({j}+{S}\right)={P}\left({j}+1+{S}\right),{I}\left({F}\left({j}+{S}\right)\right)=\left\{{P}\left({j}+{S}\right)\right\},\left\{{P}\left({j}+{S}\right),{P}\left({j}+1+{S}\right)\right\}\subseteq {I}\left({F}\left({j}+{S}\right)\right)\right)\right)\right)$
72 6 71 mpid ${⊢}{\phi }\to \left({j}\in \left(0..^{N}-{S}\right)\to if-\left({P}\left({j}+{S}\right)={P}\left({j}+1+{S}\right),{I}\left({F}\left({j}+{S}\right)\right)=\left\{{P}\left({j}+{S}\right)\right\},\left\{{P}\left({j}+{S}\right),{P}\left({j}+1+{S}\right)\right\}\subseteq {I}\left({F}\left({j}+{S}\right)\right)\right)\right)$
73 72 imp ${⊢}\left({\phi }\wedge {j}\in \left(0..^{N}-{S}\right)\right)\to if-\left({P}\left({j}+{S}\right)={P}\left({j}+1+{S}\right),{I}\left({F}\left({j}+{S}\right)\right)=\left\{{P}\left({j}+{S}\right)\right\},\left\{{P}\left({j}+{S}\right),{P}\left({j}+1+{S}\right)\right\}\subseteq {I}\left({F}\left({j}+{S}\right)\right)\right)$
74 elfzofz ${⊢}{j}\in \left(0..^{N}-{S}\right)\to {j}\in \left(0\dots {N}-{S}\right)$
75 1 2 crctcshwlkn0lem2 ${⊢}\left({\phi }\wedge {j}\in \left(0\dots {N}-{S}\right)\right)\to {Q}\left({j}\right)={P}\left({j}+{S}\right)$
76 74 75 sylan2 ${⊢}\left({\phi }\wedge {j}\in \left(0..^{N}-{S}\right)\right)\to {Q}\left({j}\right)={P}\left({j}+{S}\right)$
77 fzofzp1 ${⊢}{j}\in \left(0..^{N}-{S}\right)\to {j}+1\in \left(0\dots {N}-{S}\right)$
78 1 2 crctcshwlkn0lem2 ${⊢}\left({\phi }\wedge {j}+1\in \left(0\dots {N}-{S}\right)\right)\to {Q}\left({j}+1\right)={P}\left({j}+1+{S}\right)$
79 77 78 sylan2 ${⊢}\left({\phi }\wedge {j}\in \left(0..^{N}-{S}\right)\right)\to {Q}\left({j}+1\right)={P}\left({j}+1+{S}\right)$
80 3 fveq1i ${⊢}{H}\left({j}\right)=\left({F}\mathrm{cyclShift}{S}\right)\left({j}\right)$
81 5 adantr ${⊢}\left({\phi }\wedge {j}\in \left(0..^{N}-{S}\right)\right)\to {F}\in \mathrm{Word}{A}$
82 1 10 syl ${⊢}{\phi }\to {S}\in ℤ$
83 82 adantr ${⊢}\left({\phi }\wedge {j}\in \left(0..^{N}-{S}\right)\right)\to {S}\in ℤ$
84 nnz ${⊢}{N}\in ℕ\to {N}\in ℤ$
85 84 adantl ${⊢}\left({S}\in ℕ\wedge {N}\in ℕ\right)\to {N}\in ℤ$
86 nnz ${⊢}{S}\in ℕ\to {S}\in ℤ$
87 86 adantr ${⊢}\left({S}\in ℕ\wedge {N}\in ℕ\right)\to {S}\in ℤ$
88 85 87 zsubcld ${⊢}\left({S}\in ℕ\wedge {N}\in ℕ\right)\to {N}-{S}\in ℤ$
89 17 nn0ge0d ${⊢}{S}\in ℕ\to 0\le {S}$
90 89 adantr ${⊢}\left({S}\in ℕ\wedge {N}\in ℕ\right)\to 0\le {S}$
91 subge02 ${⊢}\left({N}\in ℝ\wedge {S}\in ℝ\right)\to \left(0\le {S}↔{N}-{S}\le {N}\right)$
92 33 32 91 syl2anr ${⊢}\left({S}\in ℕ\wedge {N}\in ℕ\right)\to \left(0\le {S}↔{N}-{S}\le {N}\right)$
93 90 92 mpbid ${⊢}\left({S}\in ℕ\wedge {N}\in ℕ\right)\to {N}-{S}\le {N}$
94 88 85 93 3jca ${⊢}\left({S}\in ℕ\wedge {N}\in ℕ\right)\to \left({N}-{S}\in ℤ\wedge {N}\in ℤ\wedge {N}-{S}\le {N}\right)$
95 94 3adant3 ${⊢}\left({S}\in ℕ\wedge {N}\in ℕ\wedge {S}<{N}\right)\to \left({N}-{S}\in ℤ\wedge {N}\in ℤ\wedge {N}-{S}\le {N}\right)$
96 15 95 sylbi ${⊢}{S}\in \left(1..^{N}\right)\to \left({N}-{S}\in ℤ\wedge {N}\in ℤ\wedge {N}-{S}\le {N}\right)$
97 eluz2 ${⊢}{N}\in {ℤ}_{\ge \left({N}-{S}\right)}↔\left({N}-{S}\in ℤ\wedge {N}\in ℤ\wedge {N}-{S}\le {N}\right)$
98 96 97 sylibr ${⊢}{S}\in \left(1..^{N}\right)\to {N}\in {ℤ}_{\ge \left({N}-{S}\right)}$
99 fzoss2 ${⊢}{N}\in {ℤ}_{\ge \left({N}-{S}\right)}\to \left(0..^{N}-{S}\right)\subseteq \left(0..^{N}\right)$
100 1 98 99 3syl ${⊢}{\phi }\to \left(0..^{N}-{S}\right)\subseteq \left(0..^{N}\right)$
101 100 sselda ${⊢}\left({\phi }\wedge {j}\in \left(0..^{N}-{S}\right)\right)\to {j}\in \left(0..^{N}\right)$
102 4 oveq2i ${⊢}\left(0..^{N}\right)=\left(0..^\left|{F}\right|\right)$
103 101 102 eleqtrdi ${⊢}\left({\phi }\wedge {j}\in \left(0..^{N}-{S}\right)\right)\to {j}\in \left(0..^\left|{F}\right|\right)$
104 cshwidxmod ${⊢}\left({F}\in \mathrm{Word}{A}\wedge {S}\in ℤ\wedge {j}\in \left(0..^\left|{F}\right|\right)\right)\to \left({F}\mathrm{cyclShift}{S}\right)\left({j}\right)={F}\left(\left({j}+{S}\right)\mathrm{mod}\left|{F}\right|\right)$
105 81 83 103 104 syl3anc ${⊢}\left({\phi }\wedge {j}\in \left(0..^{N}-{S}\right)\right)\to \left({F}\mathrm{cyclShift}{S}\right)\left({j}\right)={F}\left(\left({j}+{S}\right)\mathrm{mod}\left|{F}\right|\right)$
106 4 eqcomi ${⊢}\left|{F}\right|={N}$
107 106 oveq2i ${⊢}\left({j}+{S}\right)\mathrm{mod}\left|{F}\right|=\left({j}+{S}\right)\mathrm{mod}{N}$
108 21 imp ${⊢}\left(\left({S}\in ℕ\wedge {N}\in ℕ\wedge {S}<{N}\right)\wedge {j}\in \left(0..^{N}-{S}\right)\right)\to {j}+{S}\in {ℕ}_{0}$
109 nnm1nn0 ${⊢}{N}\in ℕ\to {N}-1\in {ℕ}_{0}$
110 109 3ad2ant2 ${⊢}\left({S}\in ℕ\wedge {N}\in ℕ\wedge {S}<{N}\right)\to {N}-1\in {ℕ}_{0}$
111 110 adantr ${⊢}\left(\left({S}\in ℕ\wedge {N}\in ℕ\wedge {S}<{N}\right)\wedge {j}\in \left(0..^{N}-{S}\right)\right)\to {N}-1\in {ℕ}_{0}$
112 31 35 anim12i ${⊢}\left({j}\in {ℕ}_{0}\wedge \left({S}\in ℕ\wedge {N}\in ℕ\wedge {S}<{N}\right)\right)\to \left({j}\in ℝ\wedge \left({S}\in ℝ\wedge {N}\in ℝ\right)\right)$
113 112 38 sylibr ${⊢}\left({j}\in {ℕ}_{0}\wedge \left({S}\in ℕ\wedge {N}\in ℕ\wedge {S}<{N}\right)\right)\to \left({j}\in ℝ\wedge {S}\in ℝ\wedge {N}\in ℝ\right)$
114 113 41 syl ${⊢}\left({j}\in {ℕ}_{0}\wedge \left({S}\in ℕ\wedge {N}\in ℕ\wedge {S}<{N}\right)\right)\to \left({j}<{N}-{S}↔{j}+{S}<{N}\right)$
115 17 3ad2ant1 ${⊢}\left({S}\in ℕ\wedge {N}\in ℕ\wedge {S}<{N}\right)\to {S}\in {ℕ}_{0}$
116 115 18 sylan2 ${⊢}\left({j}\in {ℕ}_{0}\wedge \left({S}\in ℕ\wedge {N}\in ℕ\wedge {S}<{N}\right)\right)\to {j}+{S}\in {ℕ}_{0}$
117 116 nn0zd ${⊢}\left({j}\in {ℕ}_{0}\wedge \left({S}\in ℕ\wedge {N}\in ℕ\wedge {S}<{N}\right)\right)\to {j}+{S}\in ℤ$
118 84 3ad2ant2 ${⊢}\left({S}\in ℕ\wedge {N}\in ℕ\wedge {S}<{N}\right)\to {N}\in ℤ$
119 118 adantl ${⊢}\left({j}\in {ℕ}_{0}\wedge \left({S}\in ℕ\wedge {N}\in ℕ\wedge {S}<{N}\right)\right)\to {N}\in ℤ$
120 zltlem1 ${⊢}\left({j}+{S}\in ℤ\wedge {N}\in ℤ\right)\to \left({j}+{S}<{N}↔{j}+{S}\le {N}-1\right)$
121 117 119 120 syl2anc ${⊢}\left({j}\in {ℕ}_{0}\wedge \left({S}\in ℕ\wedge {N}\in ℕ\wedge {S}<{N}\right)\right)\to \left({j}+{S}<{N}↔{j}+{S}\le {N}-1\right)$
122 121 biimpd ${⊢}\left({j}\in {ℕ}_{0}\wedge \left({S}\in ℕ\wedge {N}\in ℕ\wedge {S}<{N}\right)\right)\to \left({j}+{S}<{N}\to {j}+{S}\le {N}-1\right)$
123 114 122 sylbid ${⊢}\left({j}\in {ℕ}_{0}\wedge \left({S}\in ℕ\wedge {N}\in ℕ\wedge {S}<{N}\right)\right)\to \left({j}<{N}-{S}\to {j}+{S}\le {N}-1\right)$
124 123 impancom ${⊢}\left({j}\in {ℕ}_{0}\wedge {j}<{N}-{S}\right)\to \left(\left({S}\in ℕ\wedge {N}\in ℕ\wedge {S}<{N}\right)\to {j}+{S}\le {N}-1\right)$
125 124 3adant2 ${⊢}\left({j}\in {ℕ}_{0}\wedge {N}-{S}\in ℕ\wedge {j}<{N}-{S}\right)\to \left(\left({S}\in ℕ\wedge {N}\in ℕ\wedge {S}<{N}\right)\to {j}+{S}\le {N}-1\right)$
126 30 125 sylbi ${⊢}{j}\in \left(0..^{N}-{S}\right)\to \left(\left({S}\in ℕ\wedge {N}\in ℕ\wedge {S}<{N}\right)\to {j}+{S}\le {N}-1\right)$
127 126 impcom ${⊢}\left(\left({S}\in ℕ\wedge {N}\in ℕ\wedge {S}<{N}\right)\wedge {j}\in \left(0..^{N}-{S}\right)\right)\to {j}+{S}\le {N}-1$
128 108 111 127 3jca ${⊢}\left(\left({S}\in ℕ\wedge {N}\in ℕ\wedge {S}<{N}\right)\wedge {j}\in \left(0..^{N}-{S}\right)\right)\to \left({j}+{S}\in {ℕ}_{0}\wedge {N}-1\in {ℕ}_{0}\wedge {j}+{S}\le {N}-1\right)$
129 15 128 sylanb ${⊢}\left({S}\in \left(1..^{N}\right)\wedge {j}\in \left(0..^{N}-{S}\right)\right)\to \left({j}+{S}\in {ℕ}_{0}\wedge {N}-1\in {ℕ}_{0}\wedge {j}+{S}\le {N}-1\right)$
130 elfz2nn0 ${⊢}{j}+{S}\in \left(0\dots {N}-1\right)↔\left({j}+{S}\in {ℕ}_{0}\wedge {N}-1\in {ℕ}_{0}\wedge {j}+{S}\le {N}-1\right)$
131 129 130 sylibr ${⊢}\left({S}\in \left(1..^{N}\right)\wedge {j}\in \left(0..^{N}-{S}\right)\right)\to {j}+{S}\in \left(0\dots {N}-1\right)$
132 zaddcl ${⊢}\left({j}\in ℤ\wedge {S}\in ℤ\right)\to {j}+{S}\in ℤ$
133 7 10 132 syl2anr ${⊢}\left({S}\in \left(1..^{N}\right)\wedge {j}\in \left(0..^{N}-{S}\right)\right)\to {j}+{S}\in ℤ$
134 zmodid2 ${⊢}\left({j}+{S}\in ℤ\wedge {N}\in ℕ\right)\to \left(\left({j}+{S}\right)\mathrm{mod}{N}={j}+{S}↔{j}+{S}\in \left(0\dots {N}-1\right)\right)$
135 133 29 134 syl2anc ${⊢}\left({S}\in \left(1..^{N}\right)\wedge {j}\in \left(0..^{N}-{S}\right)\right)\to \left(\left({j}+{S}\right)\mathrm{mod}{N}={j}+{S}↔{j}+{S}\in \left(0\dots {N}-1\right)\right)$
136 131 135 mpbird ${⊢}\left({S}\in \left(1..^{N}\right)\wedge {j}\in \left(0..^{N}-{S}\right)\right)\to \left({j}+{S}\right)\mathrm{mod}{N}={j}+{S}$
137 1 136 sylan ${⊢}\left({\phi }\wedge {j}\in \left(0..^{N}-{S}\right)\right)\to \left({j}+{S}\right)\mathrm{mod}{N}={j}+{S}$
138 107 137 syl5eq ${⊢}\left({\phi }\wedge {j}\in \left(0..^{N}-{S}\right)\right)\to \left({j}+{S}\right)\mathrm{mod}\left|{F}\right|={j}+{S}$
139 138 fveq2d ${⊢}\left({\phi }\wedge {j}\in \left(0..^{N}-{S}\right)\right)\to {F}\left(\left({j}+{S}\right)\mathrm{mod}\left|{F}\right|\right)={F}\left({j}+{S}\right)$
140 105 139 eqtrd ${⊢}\left({\phi }\wedge {j}\in \left(0..^{N}-{S}\right)\right)\to \left({F}\mathrm{cyclShift}{S}\right)\left({j}\right)={F}\left({j}+{S}\right)$
141 80 140 syl5eq ${⊢}\left({\phi }\wedge {j}\in \left(0..^{N}-{S}\right)\right)\to {H}\left({j}\right)={F}\left({j}+{S}\right)$
142 141 fveq2d ${⊢}\left({\phi }\wedge {j}\in \left(0..^{N}-{S}\right)\right)\to {I}\left({H}\left({j}\right)\right)={I}\left({F}\left({j}+{S}\right)\right)$
143 simp1 ${⊢}\left({Q}\left({j}\right)={P}\left({j}+{S}\right)\wedge {Q}\left({j}+1\right)={P}\left({j}+1+{S}\right)\wedge {I}\left({H}\left({j}\right)\right)={I}\left({F}\left({j}+{S}\right)\right)\right)\to {Q}\left({j}\right)={P}\left({j}+{S}\right)$
144 simp2 ${⊢}\left({Q}\left({j}\right)={P}\left({j}+{S}\right)\wedge {Q}\left({j}+1\right)={P}\left({j}+1+{S}\right)\wedge {I}\left({H}\left({j}\right)\right)={I}\left({F}\left({j}+{S}\right)\right)\right)\to {Q}\left({j}+1\right)={P}\left({j}+1+{S}\right)$
145 143 144 eqeq12d ${⊢}\left({Q}\left({j}\right)={P}\left({j}+{S}\right)\wedge {Q}\left({j}+1\right)={P}\left({j}+1+{S}\right)\wedge {I}\left({H}\left({j}\right)\right)={I}\left({F}\left({j}+{S}\right)\right)\right)\to \left({Q}\left({j}\right)={Q}\left({j}+1\right)↔{P}\left({j}+{S}\right)={P}\left({j}+1+{S}\right)\right)$
146 simp3 ${⊢}\left({Q}\left({j}\right)={P}\left({j}+{S}\right)\wedge {Q}\left({j}+1\right)={P}\left({j}+1+{S}\right)\wedge {I}\left({H}\left({j}\right)\right)={I}\left({F}\left({j}+{S}\right)\right)\right)\to {I}\left({H}\left({j}\right)\right)={I}\left({F}\left({j}+{S}\right)\right)$
147 143 sneqd ${⊢}\left({Q}\left({j}\right)={P}\left({j}+{S}\right)\wedge {Q}\left({j}+1\right)={P}\left({j}+1+{S}\right)\wedge {I}\left({H}\left({j}\right)\right)={I}\left({F}\left({j}+{S}\right)\right)\right)\to \left\{{Q}\left({j}\right)\right\}=\left\{{P}\left({j}+{S}\right)\right\}$
148 146 147 eqeq12d ${⊢}\left({Q}\left({j}\right)={P}\left({j}+{S}\right)\wedge {Q}\left({j}+1\right)={P}\left({j}+1+{S}\right)\wedge {I}\left({H}\left({j}\right)\right)={I}\left({F}\left({j}+{S}\right)\right)\right)\to \left({I}\left({H}\left({j}\right)\right)=\left\{{Q}\left({j}\right)\right\}↔{I}\left({F}\left({j}+{S}\right)\right)=\left\{{P}\left({j}+{S}\right)\right\}\right)$
149 143 144 preq12d ${⊢}\left({Q}\left({j}\right)={P}\left({j}+{S}\right)\wedge {Q}\left({j}+1\right)={P}\left({j}+1+{S}\right)\wedge {I}\left({H}\left({j}\right)\right)={I}\left({F}\left({j}+{S}\right)\right)\right)\to \left\{{Q}\left({j}\right),{Q}\left({j}+1\right)\right\}=\left\{{P}\left({j}+{S}\right),{P}\left({j}+1+{S}\right)\right\}$
150 149 146 sseq12d ${⊢}\left({Q}\left({j}\right)={P}\left({j}+{S}\right)\wedge {Q}\left({j}+1\right)={P}\left({j}+1+{S}\right)\wedge {I}\left({H}\left({j}\right)\right)={I}\left({F}\left({j}+{S}\right)\right)\right)\to \left(\left\{{Q}\left({j}\right),{Q}\left({j}+1\right)\right\}\subseteq {I}\left({H}\left({j}\right)\right)↔\left\{{P}\left({j}+{S}\right),{P}\left({j}+1+{S}\right)\right\}\subseteq {I}\left({F}\left({j}+{S}\right)\right)\right)$
151 145 148 150 ifpbi123d ${⊢}\left({Q}\left({j}\right)={P}\left({j}+{S}\right)\wedge {Q}\left({j}+1\right)={P}\left({j}+1+{S}\right)\wedge {I}\left({H}\left({j}\right)\right)={I}\left({F}\left({j}+{S}\right)\right)\right)\to \left(if-\left({Q}\left({j}\right)={Q}\left({j}+1\right),{I}\left({H}\left({j}\right)\right)=\left\{{Q}\left({j}\right)\right\},\left\{{Q}\left({j}\right),{Q}\left({j}+1\right)\right\}\subseteq {I}\left({H}\left({j}\right)\right)\right)↔if-\left({P}\left({j}+{S}\right)={P}\left({j}+1+{S}\right),{I}\left({F}\left({j}+{S}\right)\right)=\left\{{P}\left({j}+{S}\right)\right\},\left\{{P}\left({j}+{S}\right),{P}\left({j}+1+{S}\right)\right\}\subseteq {I}\left({F}\left({j}+{S}\right)\right)\right)\right)$
152 76 79 142 151 syl3anc ${⊢}\left({\phi }\wedge {j}\in \left(0..^{N}-{S}\right)\right)\to \left(if-\left({Q}\left({j}\right)={Q}\left({j}+1\right),{I}\left({H}\left({j}\right)\right)=\left\{{Q}\left({j}\right)\right\},\left\{{Q}\left({j}\right),{Q}\left({j}+1\right)\right\}\subseteq {I}\left({H}\left({j}\right)\right)\right)↔if-\left({P}\left({j}+{S}\right)={P}\left({j}+1+{S}\right),{I}\left({F}\left({j}+{S}\right)\right)=\left\{{P}\left({j}+{S}\right)\right\},\left\{{P}\left({j}+{S}\right),{P}\left({j}+1+{S}\right)\right\}\subseteq {I}\left({F}\left({j}+{S}\right)\right)\right)\right)$
153 73 152 mpbird ${⊢}\left({\phi }\wedge {j}\in \left(0..^{N}-{S}\right)\right)\to if-\left({Q}\left({j}\right)={Q}\left({j}+1\right),{I}\left({H}\left({j}\right)\right)=\left\{{Q}\left({j}\right)\right\},\left\{{Q}\left({j}\right),{Q}\left({j}+1\right)\right\}\subseteq {I}\left({H}\left({j}\right)\right)\right)$
154 153 ralrimiva ${⊢}{\phi }\to \forall {j}\in \left(0..^{N}-{S}\right)\phantom{\rule{.4em}{0ex}}if-\left({Q}\left({j}\right)={Q}\left({j}+1\right),{I}\left({H}\left({j}\right)\right)=\left\{{Q}\left({j}\right)\right\},\left\{{Q}\left({j}\right),{Q}\left({j}+1\right)\right\}\subseteq {I}\left({H}\left({j}\right)\right)\right)$