# Metamath Proof Explorer

## Theorem 2cshwcshw

Description: If a word is a cyclically shifted word, and a second word is the result of cyclically shifting the same word, then the second word is the result of cyclically shifting the first word. (Contributed by AV, 11-May-2018) (Revised by AV, 12-Jun-2018) (Proof shortened by AV, 3-Nov-2018)

Ref Expression
Assertion 2cshwcshw ${⊢}\left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\to \left(\left({K}\in \left(0\dots {N}\right)\wedge {X}={Y}\mathrm{cyclShift}{K}\wedge \exists {m}\in \left(0\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Z}={Y}\mathrm{cyclShift}{m}\right)\to \exists {n}\in \left(0\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Z}={X}\mathrm{cyclShift}{n}\right)$

### Proof

Step Hyp Ref Expression
1 difelfznle ${⊢}\left({K}\in \left(0\dots {N}\right)\wedge {m}\in \left(0\dots {N}\right)\wedge ¬{K}\le {m}\right)\to {m}+{N}-{K}\in \left(0\dots {N}\right)$
2 1 3exp ${⊢}{K}\in \left(0\dots {N}\right)\to \left({m}\in \left(0\dots {N}\right)\to \left(¬{K}\le {m}\to {m}+{N}-{K}\in \left(0\dots {N}\right)\right)\right)$
3 2 ad2antrr ${⊢}\left(\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\wedge {X}={Y}\mathrm{cyclShift}{K}\right)\to \left({m}\in \left(0\dots {N}\right)\to \left(¬{K}\le {m}\to {m}+{N}-{K}\in \left(0\dots {N}\right)\right)\right)$
4 3 imp ${⊢}\left(\left(\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\wedge {X}={Y}\mathrm{cyclShift}{K}\right)\wedge {m}\in \left(0\dots {N}\right)\right)\to \left(¬{K}\le {m}\to {m}+{N}-{K}\in \left(0\dots {N}\right)\right)$
5 4 adantr ${⊢}\left(\left(\left(\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\wedge {X}={Y}\mathrm{cyclShift}{K}\right)\wedge {m}\in \left(0\dots {N}\right)\right)\wedge {Z}={Y}\mathrm{cyclShift}{m}\right)\to \left(¬{K}\le {m}\to {m}+{N}-{K}\in \left(0\dots {N}\right)\right)$
6 5 com12 ${⊢}¬{K}\le {m}\to \left(\left(\left(\left(\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\wedge {X}={Y}\mathrm{cyclShift}{K}\right)\wedge {m}\in \left(0\dots {N}\right)\right)\wedge {Z}={Y}\mathrm{cyclShift}{m}\right)\to {m}+{N}-{K}\in \left(0\dots {N}\right)\right)$
7 6 adantl ${⊢}\left(¬{m}=0\wedge ¬{K}\le {m}\right)\to \left(\left(\left(\left(\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\wedge {X}={Y}\mathrm{cyclShift}{K}\right)\wedge {m}\in \left(0\dots {N}\right)\right)\wedge {Z}={Y}\mathrm{cyclShift}{m}\right)\to {m}+{N}-{K}\in \left(0\dots {N}\right)\right)$
8 7 imp ${⊢}\left(\left(¬{m}=0\wedge ¬{K}\le {m}\right)\wedge \left(\left(\left(\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\wedge {X}={Y}\mathrm{cyclShift}{K}\right)\wedge {m}\in \left(0\dots {N}\right)\right)\wedge {Z}={Y}\mathrm{cyclShift}{m}\right)\right)\to {m}+{N}-{K}\in \left(0\dots {N}\right)$
9 simprl ${⊢}\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\to {Y}\in \mathrm{Word}{V}$
10 9 ad2antrr ${⊢}\left(\left(\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\wedge \left(¬{m}=0\wedge ¬{K}\le {m}\right)\right)\wedge {m}\in \left(0\dots {N}\right)\right)\to {Y}\in \mathrm{Word}{V}$
11 elfzelz ${⊢}{K}\in \left(0\dots {N}\right)\to {K}\in ℤ$
12 11 adantr ${⊢}\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\to {K}\in ℤ$
13 12 ad2antrr ${⊢}\left(\left(\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\wedge \left(¬{m}=0\wedge ¬{K}\le {m}\right)\right)\wedge {m}\in \left(0\dots {N}\right)\right)\to {K}\in ℤ$
14 elfz2 ${⊢}{K}\in \left(0\dots {N}\right)↔\left(\left(0\in ℤ\wedge {N}\in ℤ\wedge {K}\in ℤ\right)\wedge \left(0\le {K}\wedge {K}\le {N}\right)\right)$
15 zaddcl ${⊢}\left({m}\in ℤ\wedge {N}\in ℤ\right)\to {m}+{N}\in ℤ$
16 15 adantrr ${⊢}\left({m}\in ℤ\wedge \left({N}\in ℤ\wedge {K}\in ℤ\right)\right)\to {m}+{N}\in ℤ$
17 simprr ${⊢}\left({m}\in ℤ\wedge \left({N}\in ℤ\wedge {K}\in ℤ\right)\right)\to {K}\in ℤ$
18 16 17 zsubcld ${⊢}\left({m}\in ℤ\wedge \left({N}\in ℤ\wedge {K}\in ℤ\right)\right)\to {m}+{N}-{K}\in ℤ$
19 18 ex ${⊢}{m}\in ℤ\to \left(\left({N}\in ℤ\wedge {K}\in ℤ\right)\to {m}+{N}-{K}\in ℤ\right)$
20 elfzelz ${⊢}{m}\in \left(0\dots {N}\right)\to {m}\in ℤ$
21 19 20 syl11 ${⊢}\left({N}\in ℤ\wedge {K}\in ℤ\right)\to \left({m}\in \left(0\dots {N}\right)\to {m}+{N}-{K}\in ℤ\right)$
22 21 3adant1 ${⊢}\left(0\in ℤ\wedge {N}\in ℤ\wedge {K}\in ℤ\right)\to \left({m}\in \left(0\dots {N}\right)\to {m}+{N}-{K}\in ℤ\right)$
23 22 adantr ${⊢}\left(\left(0\in ℤ\wedge {N}\in ℤ\wedge {K}\in ℤ\right)\wedge \left(0\le {K}\wedge {K}\le {N}\right)\right)\to \left({m}\in \left(0\dots {N}\right)\to {m}+{N}-{K}\in ℤ\right)$
24 14 23 sylbi ${⊢}{K}\in \left(0\dots {N}\right)\to \left({m}\in \left(0\dots {N}\right)\to {m}+{N}-{K}\in ℤ\right)$
25 24 ad2antrr ${⊢}\left(\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\wedge \left(¬{m}=0\wedge ¬{K}\le {m}\right)\right)\to \left({m}\in \left(0\dots {N}\right)\to {m}+{N}-{K}\in ℤ\right)$
26 25 imp ${⊢}\left(\left(\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\wedge \left(¬{m}=0\wedge ¬{K}\le {m}\right)\right)\wedge {m}\in \left(0\dots {N}\right)\right)\to {m}+{N}-{K}\in ℤ$
27 2cshw ${⊢}\left({Y}\in \mathrm{Word}{V}\wedge {K}\in ℤ\wedge {m}+{N}-{K}\in ℤ\right)\to \left({Y}\mathrm{cyclShift}{K}\right)\mathrm{cyclShift}\left({m}+{N}-{K}\right)={Y}\mathrm{cyclShift}\left({K}+\left({m}+{N}\right)-{K}\right)$
28 10 13 26 27 syl3anc ${⊢}\left(\left(\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\wedge \left(¬{m}=0\wedge ¬{K}\le {m}\right)\right)\wedge {m}\in \left(0\dots {N}\right)\right)\to \left({Y}\mathrm{cyclShift}{K}\right)\mathrm{cyclShift}\left({m}+{N}-{K}\right)={Y}\mathrm{cyclShift}\left({K}+\left({m}+{N}\right)-{K}\right)$
29 17 18 zaddcld ${⊢}\left({m}\in ℤ\wedge \left({N}\in ℤ\wedge {K}\in ℤ\right)\right)\to {K}+\left({m}+{N}\right)-{K}\in ℤ$
30 29 ex ${⊢}{m}\in ℤ\to \left(\left({N}\in ℤ\wedge {K}\in ℤ\right)\to {K}+\left({m}+{N}\right)-{K}\in ℤ\right)$
31 30 20 syl11 ${⊢}\left({N}\in ℤ\wedge {K}\in ℤ\right)\to \left({m}\in \left(0\dots {N}\right)\to {K}+\left({m}+{N}\right)-{K}\in ℤ\right)$
32 31 3adant1 ${⊢}\left(0\in ℤ\wedge {N}\in ℤ\wedge {K}\in ℤ\right)\to \left({m}\in \left(0\dots {N}\right)\to {K}+\left({m}+{N}\right)-{K}\in ℤ\right)$
33 32 adantr ${⊢}\left(\left(0\in ℤ\wedge {N}\in ℤ\wedge {K}\in ℤ\right)\wedge \left(0\le {K}\wedge {K}\le {N}\right)\right)\to \left({m}\in \left(0\dots {N}\right)\to {K}+\left({m}+{N}\right)-{K}\in ℤ\right)$
34 14 33 sylbi ${⊢}{K}\in \left(0\dots {N}\right)\to \left({m}\in \left(0\dots {N}\right)\to {K}+\left({m}+{N}\right)-{K}\in ℤ\right)$
35 34 ad2antrr ${⊢}\left(\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\wedge \left(¬{m}=0\wedge ¬{K}\le {m}\right)\right)\to \left({m}\in \left(0\dots {N}\right)\to {K}+\left({m}+{N}\right)-{K}\in ℤ\right)$
36 35 imp ${⊢}\left(\left(\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\wedge \left(¬{m}=0\wedge ¬{K}\le {m}\right)\right)\wedge {m}\in \left(0\dots {N}\right)\right)\to {K}+\left({m}+{N}\right)-{K}\in ℤ$
37 cshwsublen ${⊢}\left({Y}\in \mathrm{Word}{V}\wedge {K}+\left({m}+{N}\right)-{K}\in ℤ\right)\to {Y}\mathrm{cyclShift}\left({K}+\left({m}+{N}\right)-{K}\right)={Y}\mathrm{cyclShift}\left({K}+\left({m}+{N}-{K}\right)-\left|{Y}\right|\right)$
38 10 36 37 syl2anc ${⊢}\left(\left(\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\wedge \left(¬{m}=0\wedge ¬{K}\le {m}\right)\right)\wedge {m}\in \left(0\dots {N}\right)\right)\to {Y}\mathrm{cyclShift}\left({K}+\left({m}+{N}\right)-{K}\right)={Y}\mathrm{cyclShift}\left({K}+\left({m}+{N}-{K}\right)-\left|{Y}\right|\right)$
39 28 38 eqtrd ${⊢}\left(\left(\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\wedge \left(¬{m}=0\wedge ¬{K}\le {m}\right)\right)\wedge {m}\in \left(0\dots {N}\right)\right)\to \left({Y}\mathrm{cyclShift}{K}\right)\mathrm{cyclShift}\left({m}+{N}-{K}\right)={Y}\mathrm{cyclShift}\left({K}+\left({m}+{N}-{K}\right)-\left|{Y}\right|\right)$
40 elfz2nn0 ${⊢}{K}\in \left(0\dots {N}\right)↔\left({K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\wedge {K}\le {N}\right)$
41 nn0cn ${⊢}{m}\in {ℕ}_{0}\to {m}\in ℂ$
42 nn0cn ${⊢}{K}\in {ℕ}_{0}\to {K}\in ℂ$
43 nn0cn ${⊢}{N}\in {ℕ}_{0}\to {N}\in ℂ$
44 42 43 anim12i ${⊢}\left({K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to \left({K}\in ℂ\wedge {N}\in ℂ\right)$
45 simprl ${⊢}\left({m}\in ℂ\wedge \left({K}\in ℂ\wedge {N}\in ℂ\right)\right)\to {K}\in ℂ$
46 addcl ${⊢}\left({m}\in ℂ\wedge {N}\in ℂ\right)\to {m}+{N}\in ℂ$
47 46 adantrl ${⊢}\left({m}\in ℂ\wedge \left({K}\in ℂ\wedge {N}\in ℂ\right)\right)\to {m}+{N}\in ℂ$
48 45 47 pncan3d ${⊢}\left({m}\in ℂ\wedge \left({K}\in ℂ\wedge {N}\in ℂ\right)\right)\to {K}+\left({m}+{N}\right)-{K}={m}+{N}$
49 48 oveq1d ${⊢}\left({m}\in ℂ\wedge \left({K}\in ℂ\wedge {N}\in ℂ\right)\right)\to {K}+\left({m}+{N}-{K}\right)-{N}={m}+{N}-{N}$
50 pncan ${⊢}\left({m}\in ℂ\wedge {N}\in ℂ\right)\to {m}+{N}-{N}={m}$
51 50 adantrl ${⊢}\left({m}\in ℂ\wedge \left({K}\in ℂ\wedge {N}\in ℂ\right)\right)\to {m}+{N}-{N}={m}$
52 49 51 eqtrd ${⊢}\left({m}\in ℂ\wedge \left({K}\in ℂ\wedge {N}\in ℂ\right)\right)\to {K}+\left({m}+{N}-{K}\right)-{N}={m}$
53 41 44 52 syl2an ${⊢}\left({m}\in {ℕ}_{0}\wedge \left({K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\right)\to {K}+\left({m}+{N}-{K}\right)-{N}={m}$
54 53 ex ${⊢}{m}\in {ℕ}_{0}\to \left(\left({K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to {K}+\left({m}+{N}-{K}\right)-{N}={m}\right)$
55 elfznn0 ${⊢}{m}\in \left(0\dots {N}\right)\to {m}\in {ℕ}_{0}$
56 54 55 syl11 ${⊢}\left({K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to \left({m}\in \left(0\dots {N}\right)\to {K}+\left({m}+{N}-{K}\right)-{N}={m}\right)$
57 56 3adant3 ${⊢}\left({K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\wedge {K}\le {N}\right)\to \left({m}\in \left(0\dots {N}\right)\to {K}+\left({m}+{N}-{K}\right)-{N}={m}\right)$
58 40 57 sylbi ${⊢}{K}\in \left(0\dots {N}\right)\to \left({m}\in \left(0\dots {N}\right)\to {K}+\left({m}+{N}-{K}\right)-{N}={m}\right)$
59 58 adantr ${⊢}\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\to \left({m}\in \left(0\dots {N}\right)\to {K}+\left({m}+{N}-{K}\right)-{N}={m}\right)$
60 oveq2 ${⊢}\left|{Y}\right|={N}\to {K}+\left({m}+{N}-{K}\right)-\left|{Y}\right|={K}+\left({m}+{N}-{K}\right)-{N}$
61 60 eqeq1d ${⊢}\left|{Y}\right|={N}\to \left({K}+\left({m}+{N}-{K}\right)-\left|{Y}\right|={m}↔{K}+\left({m}+{N}-{K}\right)-{N}={m}\right)$
62 61 imbi2d ${⊢}\left|{Y}\right|={N}\to \left(\left({m}\in \left(0\dots {N}\right)\to {K}+\left({m}+{N}-{K}\right)-\left|{Y}\right|={m}\right)↔\left({m}\in \left(0\dots {N}\right)\to {K}+\left({m}+{N}-{K}\right)-{N}={m}\right)\right)$
63 62 adantl ${⊢}\left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\to \left(\left({m}\in \left(0\dots {N}\right)\to {K}+\left({m}+{N}-{K}\right)-\left|{Y}\right|={m}\right)↔\left({m}\in \left(0\dots {N}\right)\to {K}+\left({m}+{N}-{K}\right)-{N}={m}\right)\right)$
64 63 adantl ${⊢}\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\to \left(\left({m}\in \left(0\dots {N}\right)\to {K}+\left({m}+{N}-{K}\right)-\left|{Y}\right|={m}\right)↔\left({m}\in \left(0\dots {N}\right)\to {K}+\left({m}+{N}-{K}\right)-{N}={m}\right)\right)$
65 59 64 mpbird ${⊢}\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\to \left({m}\in \left(0\dots {N}\right)\to {K}+\left({m}+{N}-{K}\right)-\left|{Y}\right|={m}\right)$
66 65 adantr ${⊢}\left(\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\wedge \left(¬{m}=0\wedge ¬{K}\le {m}\right)\right)\to \left({m}\in \left(0\dots {N}\right)\to {K}+\left({m}+{N}-{K}\right)-\left|{Y}\right|={m}\right)$
67 66 imp ${⊢}\left(\left(\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\wedge \left(¬{m}=0\wedge ¬{K}\le {m}\right)\right)\wedge {m}\in \left(0\dots {N}\right)\right)\to {K}+\left({m}+{N}-{K}\right)-\left|{Y}\right|={m}$
68 67 oveq2d ${⊢}\left(\left(\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\wedge \left(¬{m}=0\wedge ¬{K}\le {m}\right)\right)\wedge {m}\in \left(0\dots {N}\right)\right)\to {Y}\mathrm{cyclShift}\left({K}+\left({m}+{N}-{K}\right)-\left|{Y}\right|\right)={Y}\mathrm{cyclShift}{m}$
69 39 68 eqtr2d ${⊢}\left(\left(\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\wedge \left(¬{m}=0\wedge ¬{K}\le {m}\right)\right)\wedge {m}\in \left(0\dots {N}\right)\right)\to {Y}\mathrm{cyclShift}{m}=\left({Y}\mathrm{cyclShift}{K}\right)\mathrm{cyclShift}\left({m}+{N}-{K}\right)$
70 69 adantr ${⊢}\left(\left(\left(\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\wedge \left(¬{m}=0\wedge ¬{K}\le {m}\right)\right)\wedge {m}\in \left(0\dots {N}\right)\right)\wedge {X}={Y}\mathrm{cyclShift}{K}\right)\to {Y}\mathrm{cyclShift}{m}=\left({Y}\mathrm{cyclShift}{K}\right)\mathrm{cyclShift}\left({m}+{N}-{K}\right)$
71 oveq1 ${⊢}{X}={Y}\mathrm{cyclShift}{K}\to {X}\mathrm{cyclShift}\left({m}+{N}-{K}\right)=\left({Y}\mathrm{cyclShift}{K}\right)\mathrm{cyclShift}\left({m}+{N}-{K}\right)$
72 71 adantl ${⊢}\left(\left(\left(\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\wedge \left(¬{m}=0\wedge ¬{K}\le {m}\right)\right)\wedge {m}\in \left(0\dots {N}\right)\right)\wedge {X}={Y}\mathrm{cyclShift}{K}\right)\to {X}\mathrm{cyclShift}\left({m}+{N}-{K}\right)=\left({Y}\mathrm{cyclShift}{K}\right)\mathrm{cyclShift}\left({m}+{N}-{K}\right)$
73 70 72 eqtr4d ${⊢}\left(\left(\left(\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\wedge \left(¬{m}=0\wedge ¬{K}\le {m}\right)\right)\wedge {m}\in \left(0\dots {N}\right)\right)\wedge {X}={Y}\mathrm{cyclShift}{K}\right)\to {Y}\mathrm{cyclShift}{m}={X}\mathrm{cyclShift}\left({m}+{N}-{K}\right)$
74 73 exp41 ${⊢}\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\to \left(\left(¬{m}=0\wedge ¬{K}\le {m}\right)\to \left({m}\in \left(0\dots {N}\right)\to \left({X}={Y}\mathrm{cyclShift}{K}\to {Y}\mathrm{cyclShift}{m}={X}\mathrm{cyclShift}\left({m}+{N}-{K}\right)\right)\right)\right)$
75 74 com24 ${⊢}\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\to \left({X}={Y}\mathrm{cyclShift}{K}\to \left({m}\in \left(0\dots {N}\right)\to \left(\left(¬{m}=0\wedge ¬{K}\le {m}\right)\to {Y}\mathrm{cyclShift}{m}={X}\mathrm{cyclShift}\left({m}+{N}-{K}\right)\right)\right)\right)$
76 75 imp41 ${⊢}\left(\left(\left(\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\wedge {X}={Y}\mathrm{cyclShift}{K}\right)\wedge {m}\in \left(0\dots {N}\right)\right)\wedge \left(¬{m}=0\wedge ¬{K}\le {m}\right)\right)\to {Y}\mathrm{cyclShift}{m}={X}\mathrm{cyclShift}\left({m}+{N}-{K}\right)$
77 76 eqeq2d ${⊢}\left(\left(\left(\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\wedge {X}={Y}\mathrm{cyclShift}{K}\right)\wedge {m}\in \left(0\dots {N}\right)\right)\wedge \left(¬{m}=0\wedge ¬{K}\le {m}\right)\right)\to \left({Z}={Y}\mathrm{cyclShift}{m}↔{Z}={X}\mathrm{cyclShift}\left({m}+{N}-{K}\right)\right)$
78 77 biimpd ${⊢}\left(\left(\left(\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\wedge {X}={Y}\mathrm{cyclShift}{K}\right)\wedge {m}\in \left(0\dots {N}\right)\right)\wedge \left(¬{m}=0\wedge ¬{K}\le {m}\right)\right)\to \left({Z}={Y}\mathrm{cyclShift}{m}\to {Z}={X}\mathrm{cyclShift}\left({m}+{N}-{K}\right)\right)$
79 78 impancom ${⊢}\left(\left(\left(\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\wedge {X}={Y}\mathrm{cyclShift}{K}\right)\wedge {m}\in \left(0\dots {N}\right)\right)\wedge {Z}={Y}\mathrm{cyclShift}{m}\right)\to \left(\left(¬{m}=0\wedge ¬{K}\le {m}\right)\to {Z}={X}\mathrm{cyclShift}\left({m}+{N}-{K}\right)\right)$
80 79 impcom ${⊢}\left(\left(¬{m}=0\wedge ¬{K}\le {m}\right)\wedge \left(\left(\left(\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\wedge {X}={Y}\mathrm{cyclShift}{K}\right)\wedge {m}\in \left(0\dots {N}\right)\right)\wedge {Z}={Y}\mathrm{cyclShift}{m}\right)\right)\to {Z}={X}\mathrm{cyclShift}\left({m}+{N}-{K}\right)$
81 oveq2 ${⊢}{n}={m}+{N}-{K}\to {X}\mathrm{cyclShift}{n}={X}\mathrm{cyclShift}\left({m}+{N}-{K}\right)$
82 81 rspceeqv ${⊢}\left({m}+{N}-{K}\in \left(0\dots {N}\right)\wedge {Z}={X}\mathrm{cyclShift}\left({m}+{N}-{K}\right)\right)\to \exists {n}\in \left(0\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Z}={X}\mathrm{cyclShift}{n}$
83 8 80 82 syl2anc ${⊢}\left(\left(¬{m}=0\wedge ¬{K}\le {m}\right)\wedge \left(\left(\left(\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\wedge {X}={Y}\mathrm{cyclShift}{K}\right)\wedge {m}\in \left(0\dots {N}\right)\right)\wedge {Z}={Y}\mathrm{cyclShift}{m}\right)\right)\to \exists {n}\in \left(0\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Z}={X}\mathrm{cyclShift}{n}$
84 83 exp31 ${⊢}¬{m}=0\to \left(¬{K}\le {m}\to \left(\left(\left(\left(\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\wedge {X}={Y}\mathrm{cyclShift}{K}\right)\wedge {m}\in \left(0\dots {N}\right)\right)\wedge {Z}={Y}\mathrm{cyclShift}{m}\right)\to \exists {n}\in \left(0\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Z}={X}\mathrm{cyclShift}{n}\right)\right)$
85 oveq2 ${⊢}{m}=0\to {Y}\mathrm{cyclShift}{m}={Y}\mathrm{cyclShift}0$
86 85 eqeq2d ${⊢}{m}=0\to \left({Z}={Y}\mathrm{cyclShift}{m}↔{Z}={Y}\mathrm{cyclShift}0\right)$
87 cshw0 ${⊢}{Y}\in \mathrm{Word}{V}\to {Y}\mathrm{cyclShift}0={Y}$
88 87 adantr ${⊢}\left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\to {Y}\mathrm{cyclShift}0={Y}$
89 88 eqeq2d ${⊢}\left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\to \left({Z}={Y}\mathrm{cyclShift}0↔{Z}={Y}\right)$
90 fznn0sub2 ${⊢}{K}\in \left(0\dots {N}\right)\to {N}-{K}\in \left(0\dots {N}\right)$
91 90 adantl ${⊢}\left(\left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\wedge {K}\in \left(0\dots {N}\right)\right)\to {N}-{K}\in \left(0\dots {N}\right)$
92 oveq1 ${⊢}\left|{Y}\right|={N}\to \left|{Y}\right|-{K}={N}-{K}$
93 92 eleq1d ${⊢}\left|{Y}\right|={N}\to \left(\left|{Y}\right|-{K}\in \left(0\dots {N}\right)↔{N}-{K}\in \left(0\dots {N}\right)\right)$
94 93 ad2antlr ${⊢}\left(\left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\wedge {K}\in \left(0\dots {N}\right)\right)\to \left(\left|{Y}\right|-{K}\in \left(0\dots {N}\right)↔{N}-{K}\in \left(0\dots {N}\right)\right)$
95 91 94 mpbird ${⊢}\left(\left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\wedge {K}\in \left(0\dots {N}\right)\right)\to \left|{Y}\right|-{K}\in \left(0\dots {N}\right)$
96 95 adantr ${⊢}\left(\left(\left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\wedge {K}\in \left(0\dots {N}\right)\right)\wedge {X}={Y}\mathrm{cyclShift}{K}\right)\to \left|{Y}\right|-{K}\in \left(0\dots {N}\right)$
97 oveq1 ${⊢}{X}={Y}\mathrm{cyclShift}{K}\to {X}\mathrm{cyclShift}\left(\left|{Y}\right|-{K}\right)=\left({Y}\mathrm{cyclShift}{K}\right)\mathrm{cyclShift}\left(\left|{Y}\right|-{K}\right)$
98 simpl ${⊢}\left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\to {Y}\in \mathrm{Word}{V}$
99 2cshwid ${⊢}\left({Y}\in \mathrm{Word}{V}\wedge {K}\in ℤ\right)\to \left({Y}\mathrm{cyclShift}{K}\right)\mathrm{cyclShift}\left(\left|{Y}\right|-{K}\right)={Y}$
100 98 11 99 syl2an ${⊢}\left(\left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\wedge {K}\in \left(0\dots {N}\right)\right)\to \left({Y}\mathrm{cyclShift}{K}\right)\mathrm{cyclShift}\left(\left|{Y}\right|-{K}\right)={Y}$
101 97 100 sylan9eqr ${⊢}\left(\left(\left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\wedge {K}\in \left(0\dots {N}\right)\right)\wedge {X}={Y}\mathrm{cyclShift}{K}\right)\to {X}\mathrm{cyclShift}\left(\left|{Y}\right|-{K}\right)={Y}$
102 101 eqcomd ${⊢}\left(\left(\left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\wedge {K}\in \left(0\dots {N}\right)\right)\wedge {X}={Y}\mathrm{cyclShift}{K}\right)\to {Y}={X}\mathrm{cyclShift}\left(\left|{Y}\right|-{K}\right)$
103 oveq2 ${⊢}{n}=\left|{Y}\right|-{K}\to {X}\mathrm{cyclShift}{n}={X}\mathrm{cyclShift}\left(\left|{Y}\right|-{K}\right)$
104 103 rspceeqv ${⊢}\left(\left|{Y}\right|-{K}\in \left(0\dots {N}\right)\wedge {Y}={X}\mathrm{cyclShift}\left(\left|{Y}\right|-{K}\right)\right)\to \exists {n}\in \left(0\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Y}={X}\mathrm{cyclShift}{n}$
105 96 102 104 syl2anc ${⊢}\left(\left(\left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\wedge {K}\in \left(0\dots {N}\right)\right)\wedge {X}={Y}\mathrm{cyclShift}{K}\right)\to \exists {n}\in \left(0\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Y}={X}\mathrm{cyclShift}{n}$
106 105 adantr ${⊢}\left(\left(\left(\left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\wedge {K}\in \left(0\dots {N}\right)\right)\wedge {X}={Y}\mathrm{cyclShift}{K}\right)\wedge {Z}={Y}\right)\to \exists {n}\in \left(0\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Y}={X}\mathrm{cyclShift}{n}$
107 eqeq1 ${⊢}{Z}={Y}\to \left({Z}={X}\mathrm{cyclShift}{n}↔{Y}={X}\mathrm{cyclShift}{n}\right)$
108 107 rexbidv ${⊢}{Z}={Y}\to \left(\exists {n}\in \left(0\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Z}={X}\mathrm{cyclShift}{n}↔\exists {n}\in \left(0\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Y}={X}\mathrm{cyclShift}{n}\right)$
109 108 adantl ${⊢}\left(\left(\left(\left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\wedge {K}\in \left(0\dots {N}\right)\right)\wedge {X}={Y}\mathrm{cyclShift}{K}\right)\wedge {Z}={Y}\right)\to \left(\exists {n}\in \left(0\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Z}={X}\mathrm{cyclShift}{n}↔\exists {n}\in \left(0\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Y}={X}\mathrm{cyclShift}{n}\right)$
110 106 109 mpbird ${⊢}\left(\left(\left(\left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\wedge {K}\in \left(0\dots {N}\right)\right)\wedge {X}={Y}\mathrm{cyclShift}{K}\right)\wedge {Z}={Y}\right)\to \exists {n}\in \left(0\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Z}={X}\mathrm{cyclShift}{n}$
111 110 exp41 ${⊢}\left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\to \left({K}\in \left(0\dots {N}\right)\to \left({X}={Y}\mathrm{cyclShift}{K}\to \left({Z}={Y}\to \exists {n}\in \left(0\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Z}={X}\mathrm{cyclShift}{n}\right)\right)\right)$
112 111 com24 ${⊢}\left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\to \left({Z}={Y}\to \left({X}={Y}\mathrm{cyclShift}{K}\to \left({K}\in \left(0\dots {N}\right)\to \exists {n}\in \left(0\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Z}={X}\mathrm{cyclShift}{n}\right)\right)\right)$
113 89 112 sylbid ${⊢}\left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\to \left({Z}={Y}\mathrm{cyclShift}0\to \left({X}={Y}\mathrm{cyclShift}{K}\to \left({K}\in \left(0\dots {N}\right)\to \exists {n}\in \left(0\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Z}={X}\mathrm{cyclShift}{n}\right)\right)\right)$
114 113 com24 ${⊢}\left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\to \left({K}\in \left(0\dots {N}\right)\to \left({X}={Y}\mathrm{cyclShift}{K}\to \left({Z}={Y}\mathrm{cyclShift}0\to \exists {n}\in \left(0\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Z}={X}\mathrm{cyclShift}{n}\right)\right)\right)$
115 114 impcom ${⊢}\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\to \left({X}={Y}\mathrm{cyclShift}{K}\to \left({Z}={Y}\mathrm{cyclShift}0\to \exists {n}\in \left(0\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Z}={X}\mathrm{cyclShift}{n}\right)\right)$
116 115 com13 ${⊢}{Z}={Y}\mathrm{cyclShift}0\to \left({X}={Y}\mathrm{cyclShift}{K}\to \left(\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\to \exists {n}\in \left(0\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Z}={X}\mathrm{cyclShift}{n}\right)\right)$
117 116 a1d ${⊢}{Z}={Y}\mathrm{cyclShift}0\to \left({m}\in \left(0\dots {N}\right)\to \left({X}={Y}\mathrm{cyclShift}{K}\to \left(\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\to \exists {n}\in \left(0\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Z}={X}\mathrm{cyclShift}{n}\right)\right)\right)$
118 86 117 syl6bi ${⊢}{m}=0\to \left({Z}={Y}\mathrm{cyclShift}{m}\to \left({m}\in \left(0\dots {N}\right)\to \left({X}={Y}\mathrm{cyclShift}{K}\to \left(\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\to \exists {n}\in \left(0\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Z}={X}\mathrm{cyclShift}{n}\right)\right)\right)\right)$
119 118 com24 ${⊢}{m}=0\to \left({X}={Y}\mathrm{cyclShift}{K}\to \left({m}\in \left(0\dots {N}\right)\to \left({Z}={Y}\mathrm{cyclShift}{m}\to \left(\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\to \exists {n}\in \left(0\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Z}={X}\mathrm{cyclShift}{n}\right)\right)\right)\right)$
120 119 com15 ${⊢}\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\to \left({X}={Y}\mathrm{cyclShift}{K}\to \left({m}\in \left(0\dots {N}\right)\to \left({Z}={Y}\mathrm{cyclShift}{m}\to \left({m}=0\to \exists {n}\in \left(0\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Z}={X}\mathrm{cyclShift}{n}\right)\right)\right)\right)$
121 120 imp41 ${⊢}\left(\left(\left(\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\wedge {X}={Y}\mathrm{cyclShift}{K}\right)\wedge {m}\in \left(0\dots {N}\right)\right)\wedge {Z}={Y}\mathrm{cyclShift}{m}\right)\to \left({m}=0\to \exists {n}\in \left(0\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Z}={X}\mathrm{cyclShift}{n}\right)$
122 121 com12 ${⊢}{m}=0\to \left(\left(\left(\left(\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\wedge {X}={Y}\mathrm{cyclShift}{K}\right)\wedge {m}\in \left(0\dots {N}\right)\right)\wedge {Z}={Y}\mathrm{cyclShift}{m}\right)\to \exists {n}\in \left(0\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Z}={X}\mathrm{cyclShift}{n}\right)$
123 difelfzle ${⊢}\left({K}\in \left(0\dots {N}\right)\wedge {m}\in \left(0\dots {N}\right)\wedge {K}\le {m}\right)\to {m}-{K}\in \left(0\dots {N}\right)$
124 123 3exp ${⊢}{K}\in \left(0\dots {N}\right)\to \left({m}\in \left(0\dots {N}\right)\to \left({K}\le {m}\to {m}-{K}\in \left(0\dots {N}\right)\right)\right)$
125 124 ad2antrr ${⊢}\left(\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\wedge {X}={Y}\mathrm{cyclShift}{K}\right)\to \left({m}\in \left(0\dots {N}\right)\to \left({K}\le {m}\to {m}-{K}\in \left(0\dots {N}\right)\right)\right)$
126 125 imp ${⊢}\left(\left(\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\wedge {X}={Y}\mathrm{cyclShift}{K}\right)\wedge {m}\in \left(0\dots {N}\right)\right)\to \left({K}\le {m}\to {m}-{K}\in \left(0\dots {N}\right)\right)$
127 126 adantr ${⊢}\left(\left(\left(\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\wedge {X}={Y}\mathrm{cyclShift}{K}\right)\wedge {m}\in \left(0\dots {N}\right)\right)\wedge {Z}={Y}\mathrm{cyclShift}{m}\right)\to \left({K}\le {m}\to {m}-{K}\in \left(0\dots {N}\right)\right)$
128 127 impcom ${⊢}\left({K}\le {m}\wedge \left(\left(\left(\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\wedge {X}={Y}\mathrm{cyclShift}{K}\right)\wedge {m}\in \left(0\dots {N}\right)\right)\wedge {Z}={Y}\mathrm{cyclShift}{m}\right)\right)\to {m}-{K}\in \left(0\dots {N}\right)$
129 9 ad2antrr ${⊢}\left(\left(\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\wedge {K}\le {m}\right)\wedge {m}\in \left(0\dots {N}\right)\right)\to {Y}\in \mathrm{Word}{V}$
130 12 ad2antrr ${⊢}\left(\left(\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\wedge {K}\le {m}\right)\wedge {m}\in \left(0\dots {N}\right)\right)\to {K}\in ℤ$
131 zsubcl ${⊢}\left({m}\in ℤ\wedge {K}\in ℤ\right)\to {m}-{K}\in ℤ$
132 131 ex ${⊢}{m}\in ℤ\to \left({K}\in ℤ\to {m}-{K}\in ℤ\right)$
133 20 11 132 syl2imc ${⊢}{K}\in \left(0\dots {N}\right)\to \left({m}\in \left(0\dots {N}\right)\to {m}-{K}\in ℤ\right)$
134 133 ad2antrr ${⊢}\left(\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\wedge {K}\le {m}\right)\to \left({m}\in \left(0\dots {N}\right)\to {m}-{K}\in ℤ\right)$
135 134 imp ${⊢}\left(\left(\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\wedge {K}\le {m}\right)\wedge {m}\in \left(0\dots {N}\right)\right)\to {m}-{K}\in ℤ$
136 2cshw ${⊢}\left({Y}\in \mathrm{Word}{V}\wedge {K}\in ℤ\wedge {m}-{K}\in ℤ\right)\to \left({Y}\mathrm{cyclShift}{K}\right)\mathrm{cyclShift}\left({m}-{K}\right)={Y}\mathrm{cyclShift}\left({K}+{m}-{K}\right)$
137 129 130 135 136 syl3anc ${⊢}\left(\left(\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\wedge {K}\le {m}\right)\wedge {m}\in \left(0\dots {N}\right)\right)\to \left({Y}\mathrm{cyclShift}{K}\right)\mathrm{cyclShift}\left({m}-{K}\right)={Y}\mathrm{cyclShift}\left({K}+{m}-{K}\right)$
138 zcn ${⊢}{K}\in ℤ\to {K}\in ℂ$
139 20 zcnd ${⊢}{m}\in \left(0\dots {N}\right)\to {m}\in ℂ$
140 pncan3 ${⊢}\left({K}\in ℂ\wedge {m}\in ℂ\right)\to {K}+{m}-{K}={m}$
141 138 139 140 syl2anr ${⊢}\left({m}\in \left(0\dots {N}\right)\wedge {K}\in ℤ\right)\to {K}+{m}-{K}={m}$
142 141 ex ${⊢}{m}\in \left(0\dots {N}\right)\to \left({K}\in ℤ\to {K}+{m}-{K}={m}\right)$
143 11 142 syl5com ${⊢}{K}\in \left(0\dots {N}\right)\to \left({m}\in \left(0\dots {N}\right)\to {K}+{m}-{K}={m}\right)$
144 143 ad2antrr ${⊢}\left(\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\wedge {K}\le {m}\right)\to \left({m}\in \left(0\dots {N}\right)\to {K}+{m}-{K}={m}\right)$
145 144 imp ${⊢}\left(\left(\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\wedge {K}\le {m}\right)\wedge {m}\in \left(0\dots {N}\right)\right)\to {K}+{m}-{K}={m}$
146 145 oveq2d ${⊢}\left(\left(\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\wedge {K}\le {m}\right)\wedge {m}\in \left(0\dots {N}\right)\right)\to {Y}\mathrm{cyclShift}\left({K}+{m}-{K}\right)={Y}\mathrm{cyclShift}{m}$
147 137 146 eqtr2d ${⊢}\left(\left(\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\wedge {K}\le {m}\right)\wedge {m}\in \left(0\dots {N}\right)\right)\to {Y}\mathrm{cyclShift}{m}=\left({Y}\mathrm{cyclShift}{K}\right)\mathrm{cyclShift}\left({m}-{K}\right)$
148 147 adantr ${⊢}\left(\left(\left(\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\wedge {K}\le {m}\right)\wedge {m}\in \left(0\dots {N}\right)\right)\wedge {X}={Y}\mathrm{cyclShift}{K}\right)\to {Y}\mathrm{cyclShift}{m}=\left({Y}\mathrm{cyclShift}{K}\right)\mathrm{cyclShift}\left({m}-{K}\right)$
149 oveq1 ${⊢}{X}={Y}\mathrm{cyclShift}{K}\to {X}\mathrm{cyclShift}\left({m}-{K}\right)=\left({Y}\mathrm{cyclShift}{K}\right)\mathrm{cyclShift}\left({m}-{K}\right)$
150 149 eqeq2d ${⊢}{X}={Y}\mathrm{cyclShift}{K}\to \left({Y}\mathrm{cyclShift}{m}={X}\mathrm{cyclShift}\left({m}-{K}\right)↔{Y}\mathrm{cyclShift}{m}=\left({Y}\mathrm{cyclShift}{K}\right)\mathrm{cyclShift}\left({m}-{K}\right)\right)$
151 150 adantl ${⊢}\left(\left(\left(\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\wedge {K}\le {m}\right)\wedge {m}\in \left(0\dots {N}\right)\right)\wedge {X}={Y}\mathrm{cyclShift}{K}\right)\to \left({Y}\mathrm{cyclShift}{m}={X}\mathrm{cyclShift}\left({m}-{K}\right)↔{Y}\mathrm{cyclShift}{m}=\left({Y}\mathrm{cyclShift}{K}\right)\mathrm{cyclShift}\left({m}-{K}\right)\right)$
152 148 151 mpbird ${⊢}\left(\left(\left(\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\wedge {K}\le {m}\right)\wedge {m}\in \left(0\dots {N}\right)\right)\wedge {X}={Y}\mathrm{cyclShift}{K}\right)\to {Y}\mathrm{cyclShift}{m}={X}\mathrm{cyclShift}\left({m}-{K}\right)$
153 152 eqeq2d ${⊢}\left(\left(\left(\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\wedge {K}\le {m}\right)\wedge {m}\in \left(0\dots {N}\right)\right)\wedge {X}={Y}\mathrm{cyclShift}{K}\right)\to \left({Z}={Y}\mathrm{cyclShift}{m}↔{Z}={X}\mathrm{cyclShift}\left({m}-{K}\right)\right)$
154 153 biimpd ${⊢}\left(\left(\left(\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\wedge {K}\le {m}\right)\wedge {m}\in \left(0\dots {N}\right)\right)\wedge {X}={Y}\mathrm{cyclShift}{K}\right)\to \left({Z}={Y}\mathrm{cyclShift}{m}\to {Z}={X}\mathrm{cyclShift}\left({m}-{K}\right)\right)$
155 154 exp41 ${⊢}\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\to \left({K}\le {m}\to \left({m}\in \left(0\dots {N}\right)\to \left({X}={Y}\mathrm{cyclShift}{K}\to \left({Z}={Y}\mathrm{cyclShift}{m}\to {Z}={X}\mathrm{cyclShift}\left({m}-{K}\right)\right)\right)\right)\right)$
156 155 com24 ${⊢}\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\to \left({X}={Y}\mathrm{cyclShift}{K}\to \left({m}\in \left(0\dots {N}\right)\to \left({K}\le {m}\to \left({Z}={Y}\mathrm{cyclShift}{m}\to {Z}={X}\mathrm{cyclShift}\left({m}-{K}\right)\right)\right)\right)\right)$
157 156 imp31 ${⊢}\left(\left(\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\wedge {X}={Y}\mathrm{cyclShift}{K}\right)\wedge {m}\in \left(0\dots {N}\right)\right)\to \left({K}\le {m}\to \left({Z}={Y}\mathrm{cyclShift}{m}\to {Z}={X}\mathrm{cyclShift}\left({m}-{K}\right)\right)\right)$
158 157 com23 ${⊢}\left(\left(\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\wedge {X}={Y}\mathrm{cyclShift}{K}\right)\wedge {m}\in \left(0\dots {N}\right)\right)\to \left({Z}={Y}\mathrm{cyclShift}{m}\to \left({K}\le {m}\to {Z}={X}\mathrm{cyclShift}\left({m}-{K}\right)\right)\right)$
159 158 imp ${⊢}\left(\left(\left(\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\wedge {X}={Y}\mathrm{cyclShift}{K}\right)\wedge {m}\in \left(0\dots {N}\right)\right)\wedge {Z}={Y}\mathrm{cyclShift}{m}\right)\to \left({K}\le {m}\to {Z}={X}\mathrm{cyclShift}\left({m}-{K}\right)\right)$
160 159 impcom ${⊢}\left({K}\le {m}\wedge \left(\left(\left(\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\wedge {X}={Y}\mathrm{cyclShift}{K}\right)\wedge {m}\in \left(0\dots {N}\right)\right)\wedge {Z}={Y}\mathrm{cyclShift}{m}\right)\right)\to {Z}={X}\mathrm{cyclShift}\left({m}-{K}\right)$
161 oveq2 ${⊢}{n}={m}-{K}\to {X}\mathrm{cyclShift}{n}={X}\mathrm{cyclShift}\left({m}-{K}\right)$
162 161 rspceeqv ${⊢}\left({m}-{K}\in \left(0\dots {N}\right)\wedge {Z}={X}\mathrm{cyclShift}\left({m}-{K}\right)\right)\to \exists {n}\in \left(0\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Z}={X}\mathrm{cyclShift}{n}$
163 128 160 162 syl2anc ${⊢}\left({K}\le {m}\wedge \left(\left(\left(\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\wedge {X}={Y}\mathrm{cyclShift}{K}\right)\wedge {m}\in \left(0\dots {N}\right)\right)\wedge {Z}={Y}\mathrm{cyclShift}{m}\right)\right)\to \exists {n}\in \left(0\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Z}={X}\mathrm{cyclShift}{n}$
164 163 ex ${⊢}{K}\le {m}\to \left(\left(\left(\left(\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\wedge {X}={Y}\mathrm{cyclShift}{K}\right)\wedge {m}\in \left(0\dots {N}\right)\right)\wedge {Z}={Y}\mathrm{cyclShift}{m}\right)\to \exists {n}\in \left(0\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Z}={X}\mathrm{cyclShift}{n}\right)$
165 84 122 164 pm2.61ii ${⊢}\left(\left(\left(\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\wedge {X}={Y}\mathrm{cyclShift}{K}\right)\wedge {m}\in \left(0\dots {N}\right)\right)\wedge {Z}={Y}\mathrm{cyclShift}{m}\right)\to \exists {n}\in \left(0\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Z}={X}\mathrm{cyclShift}{n}$
166 165 rexlimdva2 ${⊢}\left(\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\wedge {X}={Y}\mathrm{cyclShift}{K}\right)\to \left(\exists {m}\in \left(0\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Z}={Y}\mathrm{cyclShift}{m}\to \exists {n}\in \left(0\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Z}={X}\mathrm{cyclShift}{n}\right)$
167 166 ex ${⊢}\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\to \left({X}={Y}\mathrm{cyclShift}{K}\to \left(\exists {m}\in \left(0\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Z}={Y}\mathrm{cyclShift}{m}\to \exists {n}\in \left(0\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Z}={X}\mathrm{cyclShift}{n}\right)\right)$
168 167 com23 ${⊢}\left({K}\in \left(0\dots {N}\right)\wedge \left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\right)\to \left(\exists {m}\in \left(0\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Z}={Y}\mathrm{cyclShift}{m}\to \left({X}={Y}\mathrm{cyclShift}{K}\to \exists {n}\in \left(0\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Z}={X}\mathrm{cyclShift}{n}\right)\right)$
169 168 ex ${⊢}{K}\in \left(0\dots {N}\right)\to \left(\left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\to \left(\exists {m}\in \left(0\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Z}={Y}\mathrm{cyclShift}{m}\to \left({X}={Y}\mathrm{cyclShift}{K}\to \exists {n}\in \left(0\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Z}={X}\mathrm{cyclShift}{n}\right)\right)\right)$
170 169 com24 ${⊢}{K}\in \left(0\dots {N}\right)\to \left({X}={Y}\mathrm{cyclShift}{K}\to \left(\exists {m}\in \left(0\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Z}={Y}\mathrm{cyclShift}{m}\to \left(\left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\to \exists {n}\in \left(0\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Z}={X}\mathrm{cyclShift}{n}\right)\right)\right)$
171 170 3imp ${⊢}\left({K}\in \left(0\dots {N}\right)\wedge {X}={Y}\mathrm{cyclShift}{K}\wedge \exists {m}\in \left(0\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Z}={Y}\mathrm{cyclShift}{m}\right)\to \left(\left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\to \exists {n}\in \left(0\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Z}={X}\mathrm{cyclShift}{n}\right)$
172 171 com12 ${⊢}\left({Y}\in \mathrm{Word}{V}\wedge \left|{Y}\right|={N}\right)\to \left(\left({K}\in \left(0\dots {N}\right)\wedge {X}={Y}\mathrm{cyclShift}{K}\wedge \exists {m}\in \left(0\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Z}={Y}\mathrm{cyclShift}{m}\right)\to \exists {n}\in \left(0\dots {N}\right)\phantom{\rule{.4em}{0ex}}{Z}={X}\mathrm{cyclShift}{n}\right)$