Metamath Proof Explorer

Theorem crctcshwlkn0lem4

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

Ref Expression
Hypotheses crctcshwlkn0lem.s 
|- ( ph -> S e. ( 1 ..^ N ) )
crctcshwlkn0lem.q 
|- Q = ( x e. ( 0 ... N ) |-> if ( x <_ ( N - S ) , ( P ` ( x + S ) ) , ( P ` ( ( x + S ) - N ) ) ) )
crctcshwlkn0lem.h 
|- H = ( F cyclShift S )
crctcshwlkn0lem.n 
|- N = ( # ` F )
crctcshwlkn0lem.f 
|- ( ph -> F e. Word A )
crctcshwlkn0lem.p 
|- ( ph -> A. i e. ( 0 ..^ N ) if- ( ( P ` i ) = ( P ` ( i + 1 ) ) , ( I ` ( F ` i ) ) = { ( P ` i ) } , { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) ) )
Assertion crctcshwlkn0lem4 
|- ( ph -> A. j e. ( 0 ..^ ( N - S ) ) if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) )

Proof

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