This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem crctcshwlkn0lem5

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