# Metamath Proof Explorer

## Theorem crctcshwlkn0lem6

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)$
crctcshwlkn0lem.e ${⊢}{\phi }\to {P}\left({N}\right)={P}\left(0\right)$
Assertion crctcshwlkn0lem6 ${⊢}\left({\phi }\wedge {J}={N}-{S}\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)$

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