Metamath Proof Explorer

Theorem crctcshwlkn0lem7

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 crctcshwlkn0lem7 ${⊢}{\phi }\to \forall {j}\in \left(0..^{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 crctcshwlkn0lem.e ${⊢}{\phi }\to {P}\left({N}\right)={P}\left(0\right)$
8 1 2 3 4 5 6 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)$
9 eqidd ${⊢}{\phi }\to {N}-{S}={N}-{S}$
10 1 2 3 4 5 6 7 crctcshwlkn0lem6 ${⊢}\left({\phi }\wedge {N}-{S}={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)$
11 9 10 mpdan ${⊢}{\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)$
12 ovex ${⊢}{N}-{S}\in \mathrm{V}$
13 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)$
14 12 13 ralsn ${⊢}\forall {j}\in \left\{{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)↔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)$
15 11 14 sylibr ${⊢}{\phi }\to \forall {j}\in \left\{{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)$
16 ralunb ${⊢}\forall {j}\in \left(\left(0..^{N}-{S}\right)\cup \left\{{N}-{S}\right\}\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)↔\left(\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)\wedge \forall {j}\in \left\{{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)\right)$
17 8 15 16 sylanbrc ${⊢}{\phi }\to \forall {j}\in \left(\left(0..^{N}-{S}\right)\cup \left\{{N}-{S}\right\}\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)$
18 elfzo1 ${⊢}{S}\in \left(1..^{N}\right)↔\left({S}\in ℕ\wedge {N}\in ℕ\wedge {S}<{N}\right)$
19 nnz ${⊢}{N}\in ℕ\to {N}\in ℤ$
20 nnz ${⊢}{S}\in ℕ\to {S}\in ℤ$
21 zsubcl ${⊢}\left({N}\in ℤ\wedge {S}\in ℤ\right)\to {N}-{S}\in ℤ$
22 19 20 21 syl2anr ${⊢}\left({S}\in ℕ\wedge {N}\in ℕ\right)\to {N}-{S}\in ℤ$
23 22 3adant3 ${⊢}\left({S}\in ℕ\wedge {N}\in ℕ\wedge {S}<{N}\right)\to {N}-{S}\in ℤ$
24 nnre ${⊢}{S}\in ℕ\to {S}\in ℝ$
25 nnre ${⊢}{N}\in ℕ\to {N}\in ℝ$
26 posdif ${⊢}\left({S}\in ℝ\wedge {N}\in ℝ\right)\to \left({S}<{N}↔0<{N}-{S}\right)$
27 0re ${⊢}0\in ℝ$
28 resubcl ${⊢}\left({N}\in ℝ\wedge {S}\in ℝ\right)\to {N}-{S}\in ℝ$
29 28 ancoms ${⊢}\left({S}\in ℝ\wedge {N}\in ℝ\right)\to {N}-{S}\in ℝ$
30 ltle ${⊢}\left(0\in ℝ\wedge {N}-{S}\in ℝ\right)\to \left(0<{N}-{S}\to 0\le {N}-{S}\right)$
31 27 29 30 sylancr ${⊢}\left({S}\in ℝ\wedge {N}\in ℝ\right)\to \left(0<{N}-{S}\to 0\le {N}-{S}\right)$
32 26 31 sylbid ${⊢}\left({S}\in ℝ\wedge {N}\in ℝ\right)\to \left({S}<{N}\to 0\le {N}-{S}\right)$
33 24 25 32 syl2an ${⊢}\left({S}\in ℕ\wedge {N}\in ℕ\right)\to \left({S}<{N}\to 0\le {N}-{S}\right)$
34 33 3impia ${⊢}\left({S}\in ℕ\wedge {N}\in ℕ\wedge {S}<{N}\right)\to 0\le {N}-{S}$
35 elnn0z ${⊢}{N}-{S}\in {ℕ}_{0}↔\left({N}-{S}\in ℤ\wedge 0\le {N}-{S}\right)$
36 23 34 35 sylanbrc ${⊢}\left({S}\in ℕ\wedge {N}\in ℕ\wedge {S}<{N}\right)\to {N}-{S}\in {ℕ}_{0}$
37 elnn0uz ${⊢}{N}-{S}\in {ℕ}_{0}↔{N}-{S}\in {ℤ}_{\ge 0}$
38 36 37 sylib ${⊢}\left({S}\in ℕ\wedge {N}\in ℕ\wedge {S}<{N}\right)\to {N}-{S}\in {ℤ}_{\ge 0}$
39 fzosplitsn ${⊢}{N}-{S}\in {ℤ}_{\ge 0}\to \left(0..^{N}-{S}+1\right)=\left(0..^{N}-{S}\right)\cup \left\{{N}-{S}\right\}$
40 38 39 syl ${⊢}\left({S}\in ℕ\wedge {N}\in ℕ\wedge {S}<{N}\right)\to \left(0..^{N}-{S}+1\right)=\left(0..^{N}-{S}\right)\cup \left\{{N}-{S}\right\}$
41 18 40 sylbi ${⊢}{S}\in \left(1..^{N}\right)\to \left(0..^{N}-{S}+1\right)=\left(0..^{N}-{S}\right)\cup \left\{{N}-{S}\right\}$
42 1 41 syl ${⊢}{\phi }\to \left(0..^{N}-{S}+1\right)=\left(0..^{N}-{S}\right)\cup \left\{{N}-{S}\right\}$
43 42 raleqdv ${⊢}{\phi }\to \left(\forall {j}\in \left(0..^{N}-{S}+1\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)↔\forall {j}\in \left(\left(0..^{N}-{S}\right)\cup \left\{{N}-{S}\right\}\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)\right)$
44 17 43 mpbird ${⊢}{\phi }\to \forall {j}\in \left(0..^{N}-{S}+1\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)$
45 1 2 3 4 5 6 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)$
46 ralunb ${⊢}\forall {j}\in \left(\left(0..^{N}-{S}+1\right)\cup \left({N}-{S}+1..^{N}\right)\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)↔\left(\forall {j}\in \left(0..^{N}-{S}+1\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)\wedge \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)\right)$
47 44 45 46 sylanbrc ${⊢}{\phi }\to \forall {j}\in \left(\left(0..^{N}-{S}+1\right)\cup \left({N}-{S}+1..^{N}\right)\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)$
48 nnsub ${⊢}\left({S}\in ℕ\wedge {N}\in ℕ\right)\to \left({S}<{N}↔{N}-{S}\in ℕ\right)$
49 48 biimp3a ${⊢}\left({S}\in ℕ\wedge {N}\in ℕ\wedge {S}<{N}\right)\to {N}-{S}\in ℕ$
50 nnnn0 ${⊢}{N}-{S}\in ℕ\to {N}-{S}\in {ℕ}_{0}$
51 peano2nn0 ${⊢}{N}-{S}\in {ℕ}_{0}\to {N}-{S}+1\in {ℕ}_{0}$
52 49 50 51 3syl ${⊢}\left({S}\in ℕ\wedge {N}\in ℕ\wedge {S}<{N}\right)\to {N}-{S}+1\in {ℕ}_{0}$
53 nnnn0 ${⊢}{N}\in ℕ\to {N}\in {ℕ}_{0}$
54 53 3ad2ant2 ${⊢}\left({S}\in ℕ\wedge {N}\in ℕ\wedge {S}<{N}\right)\to {N}\in {ℕ}_{0}$
55 25 anim1i ${⊢}\left({N}\in ℕ\wedge {S}\in ℕ\right)\to \left({N}\in ℝ\wedge {S}\in ℕ\right)$
56 55 ancoms ${⊢}\left({S}\in ℕ\wedge {N}\in ℕ\right)\to \left({N}\in ℝ\wedge {S}\in ℕ\right)$
57 crctcshwlkn0lem1 ${⊢}\left({N}\in ℝ\wedge {S}\in ℕ\right)\to {N}-{S}+1\le {N}$
58 56 57 syl ${⊢}\left({S}\in ℕ\wedge {N}\in ℕ\right)\to {N}-{S}+1\le {N}$
59 58 3adant3 ${⊢}\left({S}\in ℕ\wedge {N}\in ℕ\wedge {S}<{N}\right)\to {N}-{S}+1\le {N}$
60 elfz2nn0 ${⊢}{N}-{S}+1\in \left(0\dots {N}\right)↔\left({N}-{S}+1\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\wedge {N}-{S}+1\le {N}\right)$
61 52 54 59 60 syl3anbrc ${⊢}\left({S}\in ℕ\wedge {N}\in ℕ\wedge {S}<{N}\right)\to {N}-{S}+1\in \left(0\dots {N}\right)$
62 18 61 sylbi ${⊢}{S}\in \left(1..^{N}\right)\to {N}-{S}+1\in \left(0\dots {N}\right)$
63 fzosplit ${⊢}{N}-{S}+1\in \left(0\dots {N}\right)\to \left(0..^{N}\right)=\left(0..^{N}-{S}+1\right)\cup \left({N}-{S}+1..^{N}\right)$
64 1 62 63 3syl ${⊢}{\phi }\to \left(0..^{N}\right)=\left(0..^{N}-{S}+1\right)\cup \left({N}-{S}+1..^{N}\right)$
65 64 raleqdv ${⊢}{\phi }\to \left(\forall {j}\in \left(0..^{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)↔\forall {j}\in \left(\left(0..^{N}-{S}+1\right)\cup \left({N}-{S}+1..^{N}\right)\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)\right)$
66 47 65 mpbird ${⊢}{\phi }\to \forall {j}\in \left(0..^{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)$