# Metamath Proof Explorer

## Theorem crctcshwlkn0lem5

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