Metamath Proof Explorer

Theorem crctcshwlkn0lem6

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 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) )
crctcshwlkn0lem.e ⊢ ( 𝜑 → ( 𝑃 ‘ 𝑁 ) = ( 𝑃 ‘ 0 ) )
Assertion crctcshwlkn0lem6 ( ( 𝜑 ∧ 𝐽 = ( 𝑁 − 𝑆 ) ) → 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 crctcshwlkn0lem.e ⊢ ( 𝜑 → ( 𝑃 ‘ 𝑁 ) = ( 𝑃 ‘ 0 ) )
8 oveq1 ⊢ ( 𝑖 = 0 → ( 𝑖 + 1 ) = ( 0 + 1 ) )
9 0p1e1 ⊢ ( 0 + 1 ) = 1
10 8 9 eqtrdi ⊢ ( 𝑖 = 0 → ( 𝑖 + 1 ) = 1 )
11 wkslem2 ⊢ ( ( 𝑖 = 0 ∧ ( 𝑖 + 1 ) = 1 ) → ( if- ( ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ ( 𝑖 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) } , { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) ↔ if- ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 1 ) , ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) } , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) ) ) )
12 10 11 mpdan ⊢ ( 𝑖 = 0 → ( if- ( ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ ( 𝑖 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) } , { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) ↔ if- ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 1 ) , ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) } , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) ) ) )
13 elfzo1 ⊢ ( 𝑆 ∈ ( 1 ..^ 𝑁 ) ↔ ( 𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁 ) )
14 simp2 ⊢ ( ( 𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁 ) → 𝑁 ∈ ℕ )
15 13 14 sylbi ⊢ ( 𝑆 ∈ ( 1 ..^ 𝑁 ) → 𝑁 ∈ ℕ )
16 1 15 syl ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
17 lbfzo0 ⊢ ( 0 ∈ ( 0 ..^ 𝑁 ) ↔ 𝑁 ∈ ℕ )
18 16 17 sylibr ⊢ ( 𝜑 → 0 ∈ ( 0 ..^ 𝑁 ) )
19 12 6 18 rspcdva ⊢ ( 𝜑 → if- ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 1 ) , ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) } , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) ) )
20 eqeq1 ⊢ ( ( 𝑃 ‘ 𝑁 ) = ( 𝑃 ‘ 0 ) → ( ( 𝑃 ‘ 𝑁 ) = ( 𝑃 ‘ 1 ) ↔ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 1 ) ) )
21 sneq ⊢ ( ( 𝑃 ‘ 𝑁 ) = ( 𝑃 ‘ 0 ) → { ( 𝑃 ‘ 𝑁 ) } = { ( 𝑃 ‘ 0 ) } )
22 21 eqeq2d ⊢ ( ( 𝑃 ‘ 𝑁 ) = ( 𝑃 ‘ 0 ) → ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 𝑁 ) } ↔ ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) } ) )
23 preq1 ⊢ ( ( 𝑃 ‘ 𝑁 ) = ( 𝑃 ‘ 0 ) → { ( 𝑃 ‘ 𝑁 ) , ( 𝑃 ‘ 1 ) } = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } )
24 23 sseq1d ⊢ ( ( 𝑃 ‘ 𝑁 ) = ( 𝑃 ‘ 0 ) → ( { ( 𝑃 ‘ 𝑁 ) , ( 𝑃 ‘ 1 ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) ↔ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) ) )
25 20 22 24 ifpbi123d ⊢ ( ( 𝑃 ‘ 𝑁 ) = ( 𝑃 ‘ 0 ) → ( if- ( ( 𝑃 ‘ 𝑁 ) = ( 𝑃 ‘ 1 ) , ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 𝑁 ) } , { ( 𝑃 ‘ 𝑁 ) , ( 𝑃 ‘ 1 ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) ) ↔ if- ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 1 ) , ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) } , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) ) ) )
26 7 25 syl ⊢ ( 𝜑 → ( if- ( ( 𝑃 ‘ 𝑁 ) = ( 𝑃 ‘ 1 ) , ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 𝑁 ) } , { ( 𝑃 ‘ 𝑁 ) , ( 𝑃 ‘ 1 ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) ) ↔ if- ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 1 ) , ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) } , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) ) ) )
27 19 26 mpbird ⊢ ( 𝜑 → if- ( ( 𝑃 ‘ 𝑁 ) = ( 𝑃 ‘ 1 ) , ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 𝑁 ) } , { ( 𝑃 ‘ 𝑁 ) , ( 𝑃 ‘ 1 ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) ) )
28 nncn ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
29 nncn ⊢ ( 𝑆 ∈ ℕ → 𝑆 ∈ ℂ )
30 npcan ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑆 ∈ ℂ ) → ( ( 𝑁 − 𝑆 ) + 𝑆 ) = 𝑁 )
31 28 29 30 syl2anr ⊢ ( ( 𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑁 − 𝑆 ) + 𝑆 ) = 𝑁 )
32 simpr ⊢ ( ( ( 𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝑁 − 𝑆 ) + 𝑆 ) = 𝑁 ) → ( ( 𝑁 − 𝑆 ) + 𝑆 ) = 𝑁 )
33 oveq1 ⊢ ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) = 𝑁 → ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) = ( 𝑁 mod ( ♯ ‘ 𝐹 ) ) )
34 4 eqcomi ⊢ ( ♯ ‘ 𝐹 ) = 𝑁
35 34 a1i ⊢ ( ( 𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ♯ ‘ 𝐹 ) = 𝑁 )
36 35 oveq2d ⊢ ( ( 𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 mod ( ♯ ‘ 𝐹 ) ) = ( 𝑁 mod 𝑁 ) )
37 nnrp ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ+ )
38 modid0 ⊢ ( 𝑁 ∈ ℝ+ → ( 𝑁 mod 𝑁 ) = 0 )
39 37 38 syl ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 mod 𝑁 ) = 0 )
40 39 adantl ⊢ ( ( 𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 mod 𝑁 ) = 0 )
41 36 40 eqtrd ⊢ ( ( 𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 mod ( ♯ ‘ 𝐹 ) ) = 0 )
42 33 41 sylan9eqr ⊢ ( ( ( 𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝑁 − 𝑆 ) + 𝑆 ) = 𝑁 ) → ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) = 0 )
43 simpl ⊢ ( ( ( 𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝑁 − 𝑆 ) + 𝑆 ) = 𝑁 ) → ( 𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ) )
44 32 42 43 3jca ⊢ ( ( ( 𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 𝑁 − 𝑆 ) + 𝑆 ) = 𝑁 ) → ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) = 𝑁 ∧ ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) = 0 ∧ ( 𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ) )
45 31 44 mpdan ⊢ ( ( 𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) = 𝑁 ∧ ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) = 0 ∧ ( 𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ) )
46 45 3adant3 ⊢ ( ( 𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁 ) → ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) = 𝑁 ∧ ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) = 0 ∧ ( 𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ) )
47 13 46 sylbi ⊢ ( 𝑆 ∈ ( 1 ..^ 𝑁 ) → ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) = 𝑁 ∧ ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) = 0 ∧ ( 𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ) )
48 simp1 ⊢ ( ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) = 𝑁 ∧ ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) = 0 ∧ ( 𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ) → ( ( 𝑁 − 𝑆 ) + 𝑆 ) = 𝑁 )
49 48 fveq2d ⊢ ( ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) = 𝑁 ∧ ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) = 0 ∧ ( 𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ) → ( 𝑃 ‘ ( ( 𝑁 − 𝑆 ) + 𝑆 ) ) = ( 𝑃 ‘ 𝑁 ) )
50 49 eqeq1d ⊢ ( ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) = 𝑁 ∧ ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) = 0 ∧ ( 𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ) → ( ( 𝑃 ‘ ( ( 𝑁 − 𝑆 ) + 𝑆 ) ) = ( 𝑃 ‘ 1 ) ↔ ( 𝑃 ‘ 𝑁 ) = ( 𝑃 ‘ 1 ) ) )
51 simp2 ⊢ ( ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) = 𝑁 ∧ ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) = 0 ∧ ( 𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ) → ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) = 0 )
52 51 fveq2d ⊢ ( ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) = 𝑁 ∧ ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) = 0 ∧ ( 𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ) → ( 𝐹 ‘ ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) = ( 𝐹 ‘ 0 ) )
53 52 fveq2d ⊢ ( ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) = 𝑁 ∧ ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) = 0 ∧ ( 𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ) → ( 𝐼 ‘ ( 𝐹 ‘ ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) )
54 49 sneqd ⊢ ( ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) = 𝑁 ∧ ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) = 0 ∧ ( 𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ) → { ( 𝑃 ‘ ( ( 𝑁 − 𝑆 ) + 𝑆 ) ) } = { ( 𝑃 ‘ 𝑁 ) } )
55 53 54 eqeq12d ⊢ ( ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) = 𝑁 ∧ ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) = 0 ∧ ( 𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ) → ( ( 𝐼 ‘ ( 𝐹 ‘ ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) ) = { ( 𝑃 ‘ ( ( 𝑁 − 𝑆 ) + 𝑆 ) ) } ↔ ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 𝑁 ) } ) )
56 49 preq1d ⊢ ( ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) = 𝑁 ∧ ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) = 0 ∧ ( 𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ) → { ( 𝑃 ‘ ( ( 𝑁 − 𝑆 ) + 𝑆 ) ) , ( 𝑃 ‘ 1 ) } = { ( 𝑃 ‘ 𝑁 ) , ( 𝑃 ‘ 1 ) } )
57 56 53 sseq12d ⊢ ( ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) = 𝑁 ∧ ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) = 0 ∧ ( 𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ) → ( { ( 𝑃 ‘ ( ( 𝑁 − 𝑆 ) + 𝑆 ) ) , ( 𝑃 ‘ 1 ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) ) ↔ { ( 𝑃 ‘ 𝑁 ) , ( 𝑃 ‘ 1 ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) ) )
58 50 55 57 ifpbi123d ⊢ ( ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) = 𝑁 ∧ ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) = 0 ∧ ( 𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ) → ( if- ( ( 𝑃 ‘ ( ( 𝑁 − 𝑆 ) + 𝑆 ) ) = ( 𝑃 ‘ 1 ) , ( 𝐼 ‘ ( 𝐹 ‘ ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) ) = { ( 𝑃 ‘ ( ( 𝑁 − 𝑆 ) + 𝑆 ) ) } , { ( 𝑃 ‘ ( ( 𝑁 − 𝑆 ) + 𝑆 ) ) , ( 𝑃 ‘ 1 ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) ) ) ↔ if- ( ( 𝑃 ‘ 𝑁 ) = ( 𝑃 ‘ 1 ) , ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 𝑁 ) } , { ( 𝑃 ‘ 𝑁 ) , ( 𝑃 ‘ 1 ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) ) ) )
59 1 47 58 3syl ⊢ ( 𝜑 → ( if- ( ( 𝑃 ‘ ( ( 𝑁 − 𝑆 ) + 𝑆 ) ) = ( 𝑃 ‘ 1 ) , ( 𝐼 ‘ ( 𝐹 ‘ ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) ) = { ( 𝑃 ‘ ( ( 𝑁 − 𝑆 ) + 𝑆 ) ) } , { ( 𝑃 ‘ ( ( 𝑁 − 𝑆 ) + 𝑆 ) ) , ( 𝑃 ‘ 1 ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) ) ) ↔ if- ( ( 𝑃 ‘ 𝑁 ) = ( 𝑃 ‘ 1 ) , ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 𝑁 ) } , { ( 𝑃 ‘ 𝑁 ) , ( 𝑃 ‘ 1 ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) ) ) )
60 27 59 mpbird ⊢ ( 𝜑 → if- ( ( 𝑃 ‘ ( ( 𝑁 − 𝑆 ) + 𝑆 ) ) = ( 𝑃 ‘ 1 ) , ( 𝐼 ‘ ( 𝐹 ‘ ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) ) = { ( 𝑃 ‘ ( ( 𝑁 − 𝑆 ) + 𝑆 ) ) } , { ( 𝑃 ‘ ( ( 𝑁 − 𝑆 ) + 𝑆 ) ) , ( 𝑃 ‘ 1 ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) ) ) )
61 nnsub ⊢ ( ( 𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑆 < 𝑁 ↔ ( 𝑁 − 𝑆 ) ∈ ℕ ) )
62 61 biimp3a ⊢ ( ( 𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁 ) → ( 𝑁 − 𝑆 ) ∈ ℕ )
63 62 nnnn0d ⊢ ( ( 𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁 ) → ( 𝑁 − 𝑆 ) ∈ ℕ0 )
64 13 63 sylbi ⊢ ( 𝑆 ∈ ( 1 ..^ 𝑁 ) → ( 𝑁 − 𝑆 ) ∈ ℕ0 )
65 1 64 syl ⊢ ( 𝜑 → ( 𝑁 − 𝑆 ) ∈ ℕ0 )
66 nn0fz0 ⊢ ( ( 𝑁 − 𝑆 ) ∈ ℕ0 ↔ ( 𝑁 − 𝑆 ) ∈ ( 0 ... ( 𝑁 − 𝑆 ) ) )
67 65 66 sylib ⊢ ( 𝜑 → ( 𝑁 − 𝑆 ) ∈ ( 0 ... ( 𝑁 − 𝑆 ) ) )
68 1 2 crctcshwlkn0lem2 ⊢ ( ( 𝜑 ∧ ( 𝑁 − 𝑆 ) ∈ ( 0 ... ( 𝑁 − 𝑆 ) ) ) → ( 𝑄 ‘ ( 𝑁 − 𝑆 ) ) = ( 𝑃 ‘ ( ( 𝑁 − 𝑆 ) + 𝑆 ) ) )
69 67 68 mpdan ⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝑁 − 𝑆 ) ) = ( 𝑃 ‘ ( ( 𝑁 − 𝑆 ) + 𝑆 ) ) )
70 elfzoel2 ⊢ ( 𝑆 ∈ ( 1 ..^ 𝑁 ) → 𝑁 ∈ ℤ )
71 elfzoelz ⊢ ( 𝑆 ∈ ( 1 ..^ 𝑁 ) → 𝑆 ∈ ℤ )
72 70 71 zsubcld ⊢ ( 𝑆 ∈ ( 1 ..^ 𝑁 ) → ( 𝑁 − 𝑆 ) ∈ ℤ )
73 72 peano2zd ⊢ ( 𝑆 ∈ ( 1 ..^ 𝑁 ) → ( ( 𝑁 − 𝑆 ) + 1 ) ∈ ℤ )
74 nnre ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
75 74 anim1i ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ℕ ) → ( 𝑁 ∈ ℝ ∧ 𝑆 ∈ ℕ ) )
76 75 ancoms ⊢ ( ( 𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 ∈ ℝ ∧ 𝑆 ∈ ℕ ) )
77 crctcshwlkn0lem1 ⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑆 ∈ ℕ ) → ( ( 𝑁 − 𝑆 ) + 1 ) ≤ 𝑁 )
78 76 77 syl ⊢ ( ( 𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑁 − 𝑆 ) + 1 ) ≤ 𝑁 )
79 78 3adant3 ⊢ ( ( 𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁 ) → ( ( 𝑁 − 𝑆 ) + 1 ) ≤ 𝑁 )
80 13 79 sylbi ⊢ ( 𝑆 ∈ ( 1 ..^ 𝑁 ) → ( ( 𝑁 − 𝑆 ) + 1 ) ≤ 𝑁 )
81 73 70 80 3jca ⊢ ( 𝑆 ∈ ( 1 ..^ 𝑁 ) → ( ( ( 𝑁 − 𝑆 ) + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( ( 𝑁 − 𝑆 ) + 1 ) ≤ 𝑁 ) )
82 1 81 syl ⊢ ( 𝜑 → ( ( ( 𝑁 − 𝑆 ) + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( ( 𝑁 − 𝑆 ) + 1 ) ≤ 𝑁 ) )
83 eluz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( ( 𝑁 − 𝑆 ) + 1 ) ) ↔ ( ( ( 𝑁 − 𝑆 ) + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( ( 𝑁 − 𝑆 ) + 1 ) ≤ 𝑁 ) )
84 82 83 sylibr ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ ( ( 𝑁 − 𝑆 ) + 1 ) ) )
85 eluzfz1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( ( 𝑁 − 𝑆 ) + 1 ) ) → ( ( 𝑁 − 𝑆 ) + 1 ) ∈ ( ( ( 𝑁 − 𝑆 ) + 1 ) ... 𝑁 ) )
86 84 85 syl ⊢ ( 𝜑 → ( ( 𝑁 − 𝑆 ) + 1 ) ∈ ( ( ( 𝑁 − 𝑆 ) + 1 ) ... 𝑁 ) )
87 1 2 crctcshwlkn0lem3 ⊢ ( ( 𝜑 ∧ ( ( 𝑁 − 𝑆 ) + 1 ) ∈ ( ( ( 𝑁 − 𝑆 ) + 1 ) ... 𝑁 ) ) → ( 𝑄 ‘ ( ( 𝑁 − 𝑆 ) + 1 ) ) = ( 𝑃 ‘ ( ( ( ( 𝑁 − 𝑆 ) + 1 ) + 𝑆 ) − 𝑁 ) ) )
88 86 87 mpdan ⊢ ( 𝜑 → ( 𝑄 ‘ ( ( 𝑁 − 𝑆 ) + 1 ) ) = ( 𝑃 ‘ ( ( ( ( 𝑁 − 𝑆 ) + 1 ) + 𝑆 ) − 𝑁 ) ) )
89 subcl ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑆 ∈ ℂ ) → ( 𝑁 − 𝑆 ) ∈ ℂ )
90 89 ancoms ⊢ ( ( 𝑆 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( 𝑁 − 𝑆 ) ∈ ℂ )
91 ax-1cn ⊢ 1 ∈ ℂ
92 pncan2 ⊢ ( ( ( 𝑁 − 𝑆 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( 𝑁 − 𝑆 ) + 1 ) − ( 𝑁 − 𝑆 ) ) = 1 )
93 92 eqcomd ⊢ ( ( ( 𝑁 − 𝑆 ) ∈ ℂ ∧ 1 ∈ ℂ ) → 1 = ( ( ( 𝑁 − 𝑆 ) + 1 ) − ( 𝑁 − 𝑆 ) ) )
94 90 91 93 sylancl ⊢ ( ( 𝑆 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → 1 = ( ( ( 𝑁 − 𝑆 ) + 1 ) − ( 𝑁 − 𝑆 ) ) )
95 peano2cn ⊢ ( ( 𝑁 − 𝑆 ) ∈ ℂ → ( ( 𝑁 − 𝑆 ) + 1 ) ∈ ℂ )
96 90 95 syl ⊢ ( ( 𝑆 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( ( 𝑁 − 𝑆 ) + 1 ) ∈ ℂ )
97 simpr ⊢ ( ( 𝑆 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → 𝑁 ∈ ℂ )
98 simpl ⊢ ( ( 𝑆 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → 𝑆 ∈ ℂ )
99 96 97 98 subsub3d ⊢ ( ( 𝑆 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( ( ( 𝑁 − 𝑆 ) + 1 ) − ( 𝑁 − 𝑆 ) ) = ( ( ( ( 𝑁 − 𝑆 ) + 1 ) + 𝑆 ) − 𝑁 ) )
100 94 99 eqtr2d ⊢ ( ( 𝑆 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( ( ( ( 𝑁 − 𝑆 ) + 1 ) + 𝑆 ) − 𝑁 ) = 1 )
101 29 28 100 syl2an ⊢ ( ( 𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( ( ( 𝑁 − 𝑆 ) + 1 ) + 𝑆 ) − 𝑁 ) = 1 )
102 101 3adant3 ⊢ ( ( 𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁 ) → ( ( ( ( 𝑁 − 𝑆 ) + 1 ) + 𝑆 ) − 𝑁 ) = 1 )
103 13 102 sylbi ⊢ ( 𝑆 ∈ ( 1 ..^ 𝑁 ) → ( ( ( ( 𝑁 − 𝑆 ) + 1 ) + 𝑆 ) − 𝑁 ) = 1 )
104 1 103 syl ⊢ ( 𝜑 → ( ( ( ( 𝑁 − 𝑆 ) + 1 ) + 𝑆 ) − 𝑁 ) = 1 )
105 104 fveq2d ⊢ ( 𝜑 → ( 𝑃 ‘ ( ( ( ( 𝑁 − 𝑆 ) + 1 ) + 𝑆 ) − 𝑁 ) ) = ( 𝑃 ‘ 1 ) )
106 88 105 eqtrd ⊢ ( 𝜑 → ( 𝑄 ‘ ( ( 𝑁 − 𝑆 ) + 1 ) ) = ( 𝑃 ‘ 1 ) )
107 3 fveq1i ⊢ ( 𝐻 ‘ ( 𝑁 − 𝑆 ) ) = ( ( 𝐹 cyclShift 𝑆 ) ‘ ( 𝑁 − 𝑆 ) )
108 5 adantr ⊢ ( ( 𝜑 ∧ 𝑆 ∈ ( 1 ..^ 𝑁 ) ) → 𝐹 ∈ Word 𝐴 )
109 71 adantl ⊢ ( ( 𝜑 ∧ 𝑆 ∈ ( 1 ..^ 𝑁 ) ) → 𝑆 ∈ ℤ )
110 elfzofz ⊢ ( 𝑆 ∈ ( 1 ..^ 𝑁 ) → 𝑆 ∈ ( 1 ... 𝑁 ) )
111 ubmelfzo ⊢ ( 𝑆 ∈ ( 1 ... 𝑁 ) → ( 𝑁 − 𝑆 ) ∈ ( 0 ..^ 𝑁 ) )
112 110 111 syl ⊢ ( 𝑆 ∈ ( 1 ..^ 𝑁 ) → ( 𝑁 − 𝑆 ) ∈ ( 0 ..^ 𝑁 ) )
113 112 adantl ⊢ ( ( 𝜑 ∧ 𝑆 ∈ ( 1 ..^ 𝑁 ) ) → ( 𝑁 − 𝑆 ) ∈ ( 0 ..^ 𝑁 ) )
114 34 oveq2i ⊢ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ 𝑁 )
115 113 114 eleqtrrdi ⊢ ( ( 𝜑 ∧ 𝑆 ∈ ( 1 ..^ 𝑁 ) ) → ( 𝑁 − 𝑆 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
116 cshwidxmod ⊢ ( ( 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ∧ ( 𝑁 − 𝑆 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝐹 cyclShift 𝑆 ) ‘ ( 𝑁 − 𝑆 ) ) = ( 𝐹 ‘ ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) )
117 108 109 115 116 syl3anc ⊢ ( ( 𝜑 ∧ 𝑆 ∈ ( 1 ..^ 𝑁 ) ) → ( ( 𝐹 cyclShift 𝑆 ) ‘ ( 𝑁 − 𝑆 ) ) = ( 𝐹 ‘ ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) )
118 1 117 mpdan ⊢ ( 𝜑 → ( ( 𝐹 cyclShift 𝑆 ) ‘ ( 𝑁 − 𝑆 ) ) = ( 𝐹 ‘ ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) )
119 107 118 syl5eq ⊢ ( 𝜑 → ( 𝐻 ‘ ( 𝑁 − 𝑆 ) ) = ( 𝐹 ‘ ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) )
120 simp1 ⊢ ( ( ( 𝑄 ‘ ( 𝑁 − 𝑆 ) ) = ( 𝑃 ‘ ( ( 𝑁 − 𝑆 ) + 𝑆 ) ) ∧ ( 𝑄 ‘ ( ( 𝑁 − 𝑆 ) + 1 ) ) = ( 𝑃 ‘ 1 ) ∧ ( 𝐻 ‘ ( 𝑁 − 𝑆 ) ) = ( 𝐹 ‘ ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) ) → ( 𝑄 ‘ ( 𝑁 − 𝑆 ) ) = ( 𝑃 ‘ ( ( 𝑁 − 𝑆 ) + 𝑆 ) ) )
121 simp2 ⊢ ( ( ( 𝑄 ‘ ( 𝑁 − 𝑆 ) ) = ( 𝑃 ‘ ( ( 𝑁 − 𝑆 ) + 𝑆 ) ) ∧ ( 𝑄 ‘ ( ( 𝑁 − 𝑆 ) + 1 ) ) = ( 𝑃 ‘ 1 ) ∧ ( 𝐻 ‘ ( 𝑁 − 𝑆 ) ) = ( 𝐹 ‘ ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) ) → ( 𝑄 ‘ ( ( 𝑁 − 𝑆 ) + 1 ) ) = ( 𝑃 ‘ 1 ) )
122 120 121 eqeq12d ⊢ ( ( ( 𝑄 ‘ ( 𝑁 − 𝑆 ) ) = ( 𝑃 ‘ ( ( 𝑁 − 𝑆 ) + 𝑆 ) ) ∧ ( 𝑄 ‘ ( ( 𝑁 − 𝑆 ) + 1 ) ) = ( 𝑃 ‘ 1 ) ∧ ( 𝐻 ‘ ( 𝑁 − 𝑆 ) ) = ( 𝐹 ‘ ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) ) → ( ( 𝑄 ‘ ( 𝑁 − 𝑆 ) ) = ( 𝑄 ‘ ( ( 𝑁 − 𝑆 ) + 1 ) ) ↔ ( 𝑃 ‘ ( ( 𝑁 − 𝑆 ) + 𝑆 ) ) = ( 𝑃 ‘ 1 ) ) )
123 simp3 ⊢ ( ( ( 𝑄 ‘ ( 𝑁 − 𝑆 ) ) = ( 𝑃 ‘ ( ( 𝑁 − 𝑆 ) + 𝑆 ) ) ∧ ( 𝑄 ‘ ( ( 𝑁 − 𝑆 ) + 1 ) ) = ( 𝑃 ‘ 1 ) ∧ ( 𝐻 ‘ ( 𝑁 − 𝑆 ) ) = ( 𝐹 ‘ ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) ) → ( 𝐻 ‘ ( 𝑁 − 𝑆 ) ) = ( 𝐹 ‘ ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) )
124 123 fveq2d ⊢ ( ( ( 𝑄 ‘ ( 𝑁 − 𝑆 ) ) = ( 𝑃 ‘ ( ( 𝑁 − 𝑆 ) + 𝑆 ) ) ∧ ( 𝑄 ‘ ( ( 𝑁 − 𝑆 ) + 1 ) ) = ( 𝑃 ‘ 1 ) ∧ ( 𝐻 ‘ ( 𝑁 − 𝑆 ) ) = ( 𝐹 ‘ ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) ) → ( 𝐼 ‘ ( 𝐻 ‘ ( 𝑁 − 𝑆 ) ) ) = ( 𝐼 ‘ ( 𝐹 ‘ ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) ) )
125 120 sneqd ⊢ ( ( ( 𝑄 ‘ ( 𝑁 − 𝑆 ) ) = ( 𝑃 ‘ ( ( 𝑁 − 𝑆 ) + 𝑆 ) ) ∧ ( 𝑄 ‘ ( ( 𝑁 − 𝑆 ) + 1 ) ) = ( 𝑃 ‘ 1 ) ∧ ( 𝐻 ‘ ( 𝑁 − 𝑆 ) ) = ( 𝐹 ‘ ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) ) → { ( 𝑄 ‘ ( 𝑁 − 𝑆 ) ) } = { ( 𝑃 ‘ ( ( 𝑁 − 𝑆 ) + 𝑆 ) ) } )
126 124 125 eqeq12d ⊢ ( ( ( 𝑄 ‘ ( 𝑁 − 𝑆 ) ) = ( 𝑃 ‘ ( ( 𝑁 − 𝑆 ) + 𝑆 ) ) ∧ ( 𝑄 ‘ ( ( 𝑁 − 𝑆 ) + 1 ) ) = ( 𝑃 ‘ 1 ) ∧ ( 𝐻 ‘ ( 𝑁 − 𝑆 ) ) = ( 𝐹 ‘ ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) ) → ( ( 𝐼 ‘ ( 𝐻 ‘ ( 𝑁 − 𝑆 ) ) ) = { ( 𝑄 ‘ ( 𝑁 − 𝑆 ) ) } ↔ ( 𝐼 ‘ ( 𝐹 ‘ ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) ) = { ( 𝑃 ‘ ( ( 𝑁 − 𝑆 ) + 𝑆 ) ) } ) )
127 120 121 preq12d ⊢ ( ( ( 𝑄 ‘ ( 𝑁 − 𝑆 ) ) = ( 𝑃 ‘ ( ( 𝑁 − 𝑆 ) + 𝑆 ) ) ∧ ( 𝑄 ‘ ( ( 𝑁 − 𝑆 ) + 1 ) ) = ( 𝑃 ‘ 1 ) ∧ ( 𝐻 ‘ ( 𝑁 − 𝑆 ) ) = ( 𝐹 ‘ ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) ) → { ( 𝑄 ‘ ( 𝑁 − 𝑆 ) ) , ( 𝑄 ‘ ( ( 𝑁 − 𝑆 ) + 1 ) ) } = { ( 𝑃 ‘ ( ( 𝑁 − 𝑆 ) + 𝑆 ) ) , ( 𝑃 ‘ 1 ) } )
128 127 124 sseq12d ⊢ ( ( ( 𝑄 ‘ ( 𝑁 − 𝑆 ) ) = ( 𝑃 ‘ ( ( 𝑁 − 𝑆 ) + 𝑆 ) ) ∧ ( 𝑄 ‘ ( ( 𝑁 − 𝑆 ) + 1 ) ) = ( 𝑃 ‘ 1 ) ∧ ( 𝐻 ‘ ( 𝑁 − 𝑆 ) ) = ( 𝐹 ‘ ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) ) → ( { ( 𝑄 ‘ ( 𝑁 − 𝑆 ) ) , ( 𝑄 ‘ ( ( 𝑁 − 𝑆 ) + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐻 ‘ ( 𝑁 − 𝑆 ) ) ) ↔ { ( 𝑃 ‘ ( ( 𝑁 − 𝑆 ) + 𝑆 ) ) , ( 𝑃 ‘ 1 ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) ) ) )
129 122 126 128 ifpbi123d ⊢ ( ( ( 𝑄 ‘ ( 𝑁 − 𝑆 ) ) = ( 𝑃 ‘ ( ( 𝑁 − 𝑆 ) + 𝑆 ) ) ∧ ( 𝑄 ‘ ( ( 𝑁 − 𝑆 ) + 1 ) ) = ( 𝑃 ‘ 1 ) ∧ ( 𝐻 ‘ ( 𝑁 − 𝑆 ) ) = ( 𝐹 ‘ ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) ) → ( if- ( ( 𝑄 ‘ ( 𝑁 − 𝑆 ) ) = ( 𝑄 ‘ ( ( 𝑁 − 𝑆 ) + 1 ) ) , ( 𝐼 ‘ ( 𝐻 ‘ ( 𝑁 − 𝑆 ) ) ) = { ( 𝑄 ‘ ( 𝑁 − 𝑆 ) ) } , { ( 𝑄 ‘ ( 𝑁 − 𝑆 ) ) , ( 𝑄 ‘ ( ( 𝑁 − 𝑆 ) + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐻 ‘ ( 𝑁 − 𝑆 ) ) ) ) ↔ if- ( ( 𝑃 ‘ ( ( 𝑁 − 𝑆 ) + 𝑆 ) ) = ( 𝑃 ‘ 1 ) , ( 𝐼 ‘ ( 𝐹 ‘ ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) ) = { ( 𝑃 ‘ ( ( 𝑁 − 𝑆 ) + 𝑆 ) ) } , { ( 𝑃 ‘ ( ( 𝑁 − 𝑆 ) + 𝑆 ) ) , ( 𝑃 ‘ 1 ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) ) ) ) )
130 69 106 119 129 syl3anc ⊢ ( 𝜑 → ( if- ( ( 𝑄 ‘ ( 𝑁 − 𝑆 ) ) = ( 𝑄 ‘ ( ( 𝑁 − 𝑆 ) + 1 ) ) , ( 𝐼 ‘ ( 𝐻 ‘ ( 𝑁 − 𝑆 ) ) ) = { ( 𝑄 ‘ ( 𝑁 − 𝑆 ) ) } , { ( 𝑄 ‘ ( 𝑁 − 𝑆 ) ) , ( 𝑄 ‘ ( ( 𝑁 − 𝑆 ) + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐻 ‘ ( 𝑁 − 𝑆 ) ) ) ) ↔ if- ( ( 𝑃 ‘ ( ( 𝑁 − 𝑆 ) + 𝑆 ) ) = ( 𝑃 ‘ 1 ) , ( 𝐼 ‘ ( 𝐹 ‘ ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) ) = { ( 𝑃 ‘ ( ( 𝑁 − 𝑆 ) + 𝑆 ) ) } , { ( 𝑃 ‘ ( ( 𝑁 − 𝑆 ) + 𝑆 ) ) , ( 𝑃 ‘ 1 ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ ( ( ( 𝑁 − 𝑆 ) + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) ) ) ) )
131 60 130 mpbird ⊢ ( 𝜑 → if- ( ( 𝑄 ‘ ( 𝑁 − 𝑆 ) ) = ( 𝑄 ‘ ( ( 𝑁 − 𝑆 ) + 1 ) ) , ( 𝐼 ‘ ( 𝐻 ‘ ( 𝑁 − 𝑆 ) ) ) = { ( 𝑄 ‘ ( 𝑁 − 𝑆 ) ) } , { ( 𝑄 ‘ ( 𝑁 − 𝑆 ) ) , ( 𝑄 ‘ ( ( 𝑁 − 𝑆 ) + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐻 ‘ ( 𝑁 − 𝑆 ) ) ) ) )
132 131 adantr ⊢ ( ( 𝜑 ∧ 𝐽 = ( 𝑁 − 𝑆 ) ) → if- ( ( 𝑄 ‘ ( 𝑁 − 𝑆 ) ) = ( 𝑄 ‘ ( ( 𝑁 − 𝑆 ) + 1 ) ) , ( 𝐼 ‘ ( 𝐻 ‘ ( 𝑁 − 𝑆 ) ) ) = { ( 𝑄 ‘ ( 𝑁 − 𝑆 ) ) } , { ( 𝑄 ‘ ( 𝑁 − 𝑆 ) ) , ( 𝑄 ‘ ( ( 𝑁 − 𝑆 ) + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐻 ‘ ( 𝑁 − 𝑆 ) ) ) ) )
133 wkslem1 ⊢ ( 𝐽 = ( 𝑁 − 𝑆 ) → ( if- ( ( 𝑄 ‘ 𝐽 ) = ( 𝑄 ‘ ( 𝐽 + 1 ) ) , ( 𝐼 ‘ ( 𝐻 ‘ 𝐽 ) ) = { ( 𝑄 ‘ 𝐽 ) } , { ( 𝑄 ‘ 𝐽 ) , ( 𝑄 ‘ ( 𝐽 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐻 ‘ 𝐽 ) ) ) ↔ if- ( ( 𝑄 ‘ ( 𝑁 − 𝑆 ) ) = ( 𝑄 ‘ ( ( 𝑁 − 𝑆 ) + 1 ) ) , ( 𝐼 ‘ ( 𝐻 ‘ ( 𝑁 − 𝑆 ) ) ) = { ( 𝑄 ‘ ( 𝑁 − 𝑆 ) ) } , { ( 𝑄 ‘ ( 𝑁 − 𝑆 ) ) , ( 𝑄 ‘ ( ( 𝑁 − 𝑆 ) + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐻 ‘ ( 𝑁 − 𝑆 ) ) ) ) ) )
134 133 adantl ⊢ ( ( 𝜑 ∧ 𝐽 = ( 𝑁 − 𝑆 ) ) → ( if- ( ( 𝑄 ‘ 𝐽 ) = ( 𝑄 ‘ ( 𝐽 + 1 ) ) , ( 𝐼 ‘ ( 𝐻 ‘ 𝐽 ) ) = { ( 𝑄 ‘ 𝐽 ) } , { ( 𝑄 ‘ 𝐽 ) , ( 𝑄 ‘ ( 𝐽 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐻 ‘ 𝐽 ) ) ) ↔ if- ( ( 𝑄 ‘ ( 𝑁 − 𝑆 ) ) = ( 𝑄 ‘ ( ( 𝑁 − 𝑆 ) + 1 ) ) , ( 𝐼 ‘ ( 𝐻 ‘ ( 𝑁 − 𝑆 ) ) ) = { ( 𝑄 ‘ ( 𝑁 − 𝑆 ) ) } , { ( 𝑄 ‘ ( 𝑁 − 𝑆 ) ) , ( 𝑄 ‘ ( ( 𝑁 − 𝑆 ) + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐻 ‘ ( 𝑁 − 𝑆 ) ) ) ) ) )
135 132 134 mpbird ⊢ ( ( 𝜑 ∧ 𝐽 = ( 𝑁 − 𝑆 ) ) → if- ( ( 𝑄 ‘ 𝐽 ) = ( 𝑄 ‘ ( 𝐽 + 1 ) ) , ( 𝐼 ‘ ( 𝐻 ‘ 𝐽 ) ) = { ( 𝑄 ‘ 𝐽 ) } , { ( 𝑄 ‘ 𝐽 ) , ( 𝑄 ‘ ( 𝐽 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐻 ‘ 𝐽 ) ) ) )