Metamath Proof Explorer


Theorem crctcshwlkn0lem5

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

Ref Expression
Hypotheses crctcshwlkn0lem.s ( 𝜑𝑆 ∈ ( 1 ..^ 𝑁 ) )
crctcshwlkn0lem.q 𝑄 = ( 𝑥 ∈ ( 0 ... 𝑁 ) ↦ if ( 𝑥 ≤ ( 𝑁𝑆 ) , ( 𝑃 ‘ ( 𝑥 + 𝑆 ) ) , ( 𝑃 ‘ ( ( 𝑥 + 𝑆 ) − 𝑁 ) ) ) )
crctcshwlkn0lem.h 𝐻 = ( 𝐹 cyclShift 𝑆 )
crctcshwlkn0lem.n 𝑁 = ( ♯ ‘ 𝐹 )
crctcshwlkn0lem.f ( 𝜑𝐹 ∈ Word 𝐴 )
crctcshwlkn0lem.p ( 𝜑 → ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) if- ( ( 𝑃𝑖 ) = ( 𝑃 ‘ ( 𝑖 + 1 ) ) , ( 𝐼 ‘ ( 𝐹𝑖 ) ) = { ( 𝑃𝑖 ) } , { ( 𝑃𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹𝑖 ) ) ) )
Assertion crctcshwlkn0lem5 ( 𝜑 → ∀ 𝑗 ∈ ( ( ( 𝑁𝑆 ) + 1 ) ..^ 𝑁 ) if- ( ( 𝑄𝑗 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) , ( 𝐼 ‘ ( 𝐻𝑗 ) ) = { ( 𝑄𝑗 ) } , { ( 𝑄𝑗 ) , ( 𝑄 ‘ ( 𝑗 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐻𝑗 ) ) ) )

Proof

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