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 ) ) } ⊆ ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) ) )