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 ⊢ ( 𝜑 → 𝑆 ∈ ( 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 biimtrid ⊢ ( ( 𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁 ) → ( 𝑗 ∈ ( ( ( 𝑁 − 𝑆 ) + 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 biimtrid ⊢ ( ( 𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁 ) → ( 𝑗 ∈ ( ( ( 𝑁 − 𝑆 ) + 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 eqtrid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( ( 𝑁 − 𝑆 ) + 1 ) ..^ 𝑁 ) ) → ( ( 𝑗 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) = ( ( 𝑗 + 𝑆 ) − 𝑁 ) )
173 172 fveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( ( 𝑁 − 𝑆 ) + 1 ) ..^ 𝑁 ) ) → ( 𝐹 ‘ ( ( 𝑗 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) = ( 𝐹 ‘ ( ( 𝑗 + 𝑆 ) − 𝑁 ) ) )
174 146 173 eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( ( 𝑁 − 𝑆 ) + 1 ) ..^ 𝑁 ) ) → ( ( 𝐹 cyclShift 𝑆 ) ‘ 𝑗 ) = ( 𝐹 ‘ ( ( 𝑗 + 𝑆 ) − 𝑁 ) ) )
175 120 174 eqtrid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( ( 𝑁 − 𝑆 ) + 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 ) ) } ⊆ ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) ) )