Metamath Proof Explorer

Theorem crctcshwlkn0lem7

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 crctcshwlkn0lem7 ( 𝜑 → ∀ 𝑗 ∈ ( 0 ..^ 𝑁 ) 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 1 2 3 4 5 6 crctcshwlkn0lem4 ⊢ ( 𝜑 → ∀ 𝑗 ∈ ( 0 ..^ ( 𝑁 − 𝑆 ) ) if- ( ( 𝑄 ‘ 𝑗 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) , ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) = { ( 𝑄 ‘ 𝑗 ) } , { ( 𝑄 ‘ 𝑗 ) , ( 𝑄 ‘ ( 𝑗 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) ) )
9 eqidd ⊢ ( 𝜑 → ( 𝑁 − 𝑆 ) = ( 𝑁 − 𝑆 ) )
10 1 2 3 4 5 6 7 crctcshwlkn0lem6 ⊢ ( ( 𝜑 ∧ ( 𝑁 − 𝑆 ) = ( 𝑁 − 𝑆 ) ) → if- ( ( 𝑄 ‘ ( 𝑁 − 𝑆 ) ) = ( 𝑄 ‘ ( ( 𝑁 − 𝑆 ) + 1 ) ) , ( 𝐼 ‘ ( 𝐻 ‘ ( 𝑁 − 𝑆 ) ) ) = { ( 𝑄 ‘ ( 𝑁 − 𝑆 ) ) } , { ( 𝑄 ‘ ( 𝑁 − 𝑆 ) ) , ( 𝑄 ‘ ( ( 𝑁 − 𝑆 ) + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐻 ‘ ( 𝑁 − 𝑆 ) ) ) ) )
11 9 10 mpdan ⊢ ( 𝜑 → if- ( ( 𝑄 ‘ ( 𝑁 − 𝑆 ) ) = ( 𝑄 ‘ ( ( 𝑁 − 𝑆 ) + 1 ) ) , ( 𝐼 ‘ ( 𝐻 ‘ ( 𝑁 − 𝑆 ) ) ) = { ( 𝑄 ‘ ( 𝑁 − 𝑆 ) ) } , { ( 𝑄 ‘ ( 𝑁 − 𝑆 ) ) , ( 𝑄 ‘ ( ( 𝑁 − 𝑆 ) + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐻 ‘ ( 𝑁 − 𝑆 ) ) ) ) )
12 ovex ⊢ ( 𝑁 − 𝑆 ) ∈ V
13 wkslem1 ⊢ ( 𝑗 = ( 𝑁 − 𝑆 ) → ( if- ( ( 𝑄 ‘ 𝑗 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) , ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) = { ( 𝑄 ‘ 𝑗 ) } , { ( 𝑄 ‘ 𝑗 ) , ( 𝑄 ‘ ( 𝑗 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) ) ↔ if- ( ( 𝑄 ‘ ( 𝑁 − 𝑆 ) ) = ( 𝑄 ‘ ( ( 𝑁 − 𝑆 ) + 1 ) ) , ( 𝐼 ‘ ( 𝐻 ‘ ( 𝑁 − 𝑆 ) ) ) = { ( 𝑄 ‘ ( 𝑁 − 𝑆 ) ) } , { ( 𝑄 ‘ ( 𝑁 − 𝑆 ) ) , ( 𝑄 ‘ ( ( 𝑁 − 𝑆 ) + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐻 ‘ ( 𝑁 − 𝑆 ) ) ) ) ) )
14 12 13 ralsn ⊢ ( ∀ 𝑗 ∈ { ( 𝑁 − 𝑆 ) } if- ( ( 𝑄 ‘ 𝑗 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) , ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) = { ( 𝑄 ‘ 𝑗 ) } , { ( 𝑄 ‘ 𝑗 ) , ( 𝑄 ‘ ( 𝑗 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) ) ↔ if- ( ( 𝑄 ‘ ( 𝑁 − 𝑆 ) ) = ( 𝑄 ‘ ( ( 𝑁 − 𝑆 ) + 1 ) ) , ( 𝐼 ‘ ( 𝐻 ‘ ( 𝑁 − 𝑆 ) ) ) = { ( 𝑄 ‘ ( 𝑁 − 𝑆 ) ) } , { ( 𝑄 ‘ ( 𝑁 − 𝑆 ) ) , ( 𝑄 ‘ ( ( 𝑁 − 𝑆 ) + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐻 ‘ ( 𝑁 − 𝑆 ) ) ) ) )
15 11 14 sylibr ⊢ ( 𝜑 → ∀ 𝑗 ∈ { ( 𝑁 − 𝑆 ) } if- ( ( 𝑄 ‘ 𝑗 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) , ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) = { ( 𝑄 ‘ 𝑗 ) } , { ( 𝑄 ‘ 𝑗 ) , ( 𝑄 ‘ ( 𝑗 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) ) )
16 ralunb ⊢ ( ∀ 𝑗 ∈ ( ( 0 ..^ ( 𝑁 − 𝑆 ) ) ∪ { ( 𝑁 − 𝑆 ) } ) if- ( ( 𝑄 ‘ 𝑗 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) , ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) = { ( 𝑄 ‘ 𝑗 ) } , { ( 𝑄 ‘ 𝑗 ) , ( 𝑄 ‘ ( 𝑗 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) ) ↔ ( ∀ 𝑗 ∈ ( 0 ..^ ( 𝑁 − 𝑆 ) ) if- ( ( 𝑄 ‘ 𝑗 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) , ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) = { ( 𝑄 ‘ 𝑗 ) } , { ( 𝑄 ‘ 𝑗 ) , ( 𝑄 ‘ ( 𝑗 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) ) ∧ ∀ 𝑗 ∈ { ( 𝑁 − 𝑆 ) } if- ( ( 𝑄 ‘ 𝑗 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) , ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) = { ( 𝑄 ‘ 𝑗 ) } , { ( 𝑄 ‘ 𝑗 ) , ( 𝑄 ‘ ( 𝑗 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) ) ) )
17 8 15 16 sylanbrc ⊢ ( 𝜑 → ∀ 𝑗 ∈ ( ( 0 ..^ ( 𝑁 − 𝑆 ) ) ∪ { ( 𝑁 − 𝑆 ) } ) if- ( ( 𝑄 ‘ 𝑗 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) , ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) = { ( 𝑄 ‘ 𝑗 ) } , { ( 𝑄 ‘ 𝑗 ) , ( 𝑄 ‘ ( 𝑗 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) ) )
18 elfzo1 ⊢ ( 𝑆 ∈ ( 1 ..^ 𝑁 ) ↔ ( 𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁 ) )
19 nnz ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
20 nnz ⊢ ( 𝑆 ∈ ℕ → 𝑆 ∈ ℤ )
21 zsubcl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑆 ∈ ℤ ) → ( 𝑁 − 𝑆 ) ∈ ℤ )
22 19 20 21 syl2anr ⊢ ( ( 𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 − 𝑆 ) ∈ ℤ )
23 22 3adant3 ⊢ ( ( 𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁 ) → ( 𝑁 − 𝑆 ) ∈ ℤ )
24 nnre ⊢ ( 𝑆 ∈ ℕ → 𝑆 ∈ ℝ )
25 nnre ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
26 posdif ⊢ ( ( 𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝑆 < 𝑁 ↔ 0 < ( 𝑁 − 𝑆 ) ) )
27 0re ⊢ 0 ∈ ℝ
28 resubcl ⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑆 ∈ ℝ ) → ( 𝑁 − 𝑆 ) ∈ ℝ )
29 28 ancoms ⊢ ( ( 𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝑁 − 𝑆 ) ∈ ℝ )
30 ltle ⊢ ( ( 0 ∈ ℝ ∧ ( 𝑁 − 𝑆 ) ∈ ℝ ) → ( 0 < ( 𝑁 − 𝑆 ) → 0 ≤ ( 𝑁 − 𝑆 ) ) )
31 27 29 30 sylancr ⊢ ( ( 𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 0 < ( 𝑁 − 𝑆 ) → 0 ≤ ( 𝑁 − 𝑆 ) ) )
32 26 31 sylbid ⊢ ( ( 𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝑆 < 𝑁 → 0 ≤ ( 𝑁 − 𝑆 ) ) )
33 24 25 32 syl2an ⊢ ( ( 𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑆 < 𝑁 → 0 ≤ ( 𝑁 − 𝑆 ) ) )
34 33 3impia ⊢ ( ( 𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁 ) → 0 ≤ ( 𝑁 − 𝑆 ) )
35 elnn0z ⊢ ( ( 𝑁 − 𝑆 ) ∈ ℕ0 ↔ ( ( 𝑁 − 𝑆 ) ∈ ℤ ∧ 0 ≤ ( 𝑁 − 𝑆 ) ) )
36 23 34 35 sylanbrc ⊢ ( ( 𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁 ) → ( 𝑁 − 𝑆 ) ∈ ℕ0 )
37 elnn0uz ⊢ ( ( 𝑁 − 𝑆 ) ∈ ℕ0 ↔ ( 𝑁 − 𝑆 ) ∈ ( ℤ≥ ‘ 0 ) )
38 36 37 sylib ⊢ ( ( 𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁 ) → ( 𝑁 − 𝑆 ) ∈ ( ℤ≥ ‘ 0 ) )
39 fzosplitsn ⊢ ( ( 𝑁 − 𝑆 ) ∈ ( ℤ≥ ‘ 0 ) → ( 0 ..^ ( ( 𝑁 − 𝑆 ) + 1 ) ) = ( ( 0 ..^ ( 𝑁 − 𝑆 ) ) ∪ { ( 𝑁 − 𝑆 ) } ) )
40 38 39 syl ⊢ ( ( 𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁 ) → ( 0 ..^ ( ( 𝑁 − 𝑆 ) + 1 ) ) = ( ( 0 ..^ ( 𝑁 − 𝑆 ) ) ∪ { ( 𝑁 − 𝑆 ) } ) )
41 18 40 sylbi ⊢ ( 𝑆 ∈ ( 1 ..^ 𝑁 ) → ( 0 ..^ ( ( 𝑁 − 𝑆 ) + 1 ) ) = ( ( 0 ..^ ( 𝑁 − 𝑆 ) ) ∪ { ( 𝑁 − 𝑆 ) } ) )
42 1 41 syl ⊢ ( 𝜑 → ( 0 ..^ ( ( 𝑁 − 𝑆 ) + 1 ) ) = ( ( 0 ..^ ( 𝑁 − 𝑆 ) ) ∪ { ( 𝑁 − 𝑆 ) } ) )
43 17 42 raleqtrrdv ⊢ ( 𝜑 → ∀ 𝑗 ∈ ( 0 ..^ ( ( 𝑁 − 𝑆 ) + 1 ) ) if- ( ( 𝑄 ‘ 𝑗 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) , ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) = { ( 𝑄 ‘ 𝑗 ) } , { ( 𝑄 ‘ 𝑗 ) , ( 𝑄 ‘ ( 𝑗 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) ) )
44 1 2 3 4 5 6 crctcshwlkn0lem5 ⊢ ( 𝜑 → ∀ 𝑗 ∈ ( ( ( 𝑁 − 𝑆 ) + 1 ) ..^ 𝑁 ) if- ( ( 𝑄 ‘ 𝑗 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) , ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) = { ( 𝑄 ‘ 𝑗 ) } , { ( 𝑄 ‘ 𝑗 ) , ( 𝑄 ‘ ( 𝑗 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) ) )
45 ralunb ⊢ ( ∀ 𝑗 ∈ ( ( 0 ..^ ( ( 𝑁 − 𝑆 ) + 1 ) ) ∪ ( ( ( 𝑁 − 𝑆 ) + 1 ) ..^ 𝑁 ) ) if- ( ( 𝑄 ‘ 𝑗 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) , ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) = { ( 𝑄 ‘ 𝑗 ) } , { ( 𝑄 ‘ 𝑗 ) , ( 𝑄 ‘ ( 𝑗 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) ) ↔ ( ∀ 𝑗 ∈ ( 0 ..^ ( ( 𝑁 − 𝑆 ) + 1 ) ) if- ( ( 𝑄 ‘ 𝑗 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) , ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) = { ( 𝑄 ‘ 𝑗 ) } , { ( 𝑄 ‘ 𝑗 ) , ( 𝑄 ‘ ( 𝑗 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) ) ∧ ∀ 𝑗 ∈ ( ( ( 𝑁 − 𝑆 ) + 1 ) ..^ 𝑁 ) if- ( ( 𝑄 ‘ 𝑗 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) , ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) = { ( 𝑄 ‘ 𝑗 ) } , { ( 𝑄 ‘ 𝑗 ) , ( 𝑄 ‘ ( 𝑗 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) ) ) )
46 43 44 45 sylanbrc ⊢ ( 𝜑 → ∀ 𝑗 ∈ ( ( 0 ..^ ( ( 𝑁 − 𝑆 ) + 1 ) ) ∪ ( ( ( 𝑁 − 𝑆 ) + 1 ) ..^ 𝑁 ) ) if- ( ( 𝑄 ‘ 𝑗 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) , ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) = { ( 𝑄 ‘ 𝑗 ) } , { ( 𝑄 ‘ 𝑗 ) , ( 𝑄 ‘ ( 𝑗 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) ) )
47 nnsub ⊢ ( ( 𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑆 < 𝑁 ↔ ( 𝑁 − 𝑆 ) ∈ ℕ ) )
48 47 biimp3a ⊢ ( ( 𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁 ) → ( 𝑁 − 𝑆 ) ∈ ℕ )
49 nnnn0 ⊢ ( ( 𝑁 − 𝑆 ) ∈ ℕ → ( 𝑁 − 𝑆 ) ∈ ℕ0 )
50 peano2nn0 ⊢ ( ( 𝑁 − 𝑆 ) ∈ ℕ0 → ( ( 𝑁 − 𝑆 ) + 1 ) ∈ ℕ0 )
51 48 49 50 3syl ⊢ ( ( 𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁 ) → ( ( 𝑁 − 𝑆 ) + 1 ) ∈ ℕ0 )
52 nnnn0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
53 52 3ad2ant2 ⊢ ( ( 𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁 ) → 𝑁 ∈ ℕ0 )
54 25 anim1i ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ℕ ) → ( 𝑁 ∈ ℝ ∧ 𝑆 ∈ ℕ ) )
55 54 ancoms ⊢ ( ( 𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 ∈ ℝ ∧ 𝑆 ∈ ℕ ) )
56 crctcshwlkn0lem1 ⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑆 ∈ ℕ ) → ( ( 𝑁 − 𝑆 ) + 1 ) ≤ 𝑁 )
57 55 56 syl ⊢ ( ( 𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑁 − 𝑆 ) + 1 ) ≤ 𝑁 )
58 57 3adant3 ⊢ ( ( 𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁 ) → ( ( 𝑁 − 𝑆 ) + 1 ) ≤ 𝑁 )
59 elfz2nn0 ⊢ ( ( ( 𝑁 − 𝑆 ) + 1 ) ∈ ( 0 ... 𝑁 ) ↔ ( ( ( 𝑁 − 𝑆 ) + 1 ) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 − 𝑆 ) + 1 ) ≤ 𝑁 ) )
60 51 53 58 59 syl3anbrc ⊢ ( ( 𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁 ) → ( ( 𝑁 − 𝑆 ) + 1 ) ∈ ( 0 ... 𝑁 ) )
61 18 60 sylbi ⊢ ( 𝑆 ∈ ( 1 ..^ 𝑁 ) → ( ( 𝑁 − 𝑆 ) + 1 ) ∈ ( 0 ... 𝑁 ) )
62 fzosplit ⊢ ( ( ( 𝑁 − 𝑆 ) + 1 ) ∈ ( 0 ... 𝑁 ) → ( 0 ..^ 𝑁 ) = ( ( 0 ..^ ( ( 𝑁 − 𝑆 ) + 1 ) ) ∪ ( ( ( 𝑁 − 𝑆 ) + 1 ) ..^ 𝑁 ) ) )
63 1 61 62 3syl ⊢ ( 𝜑 → ( 0 ..^ 𝑁 ) = ( ( 0 ..^ ( ( 𝑁 − 𝑆 ) + 1 ) ) ∪ ( ( ( 𝑁 − 𝑆 ) + 1 ) ..^ 𝑁 ) ) )
64 46 63 raleqtrrdv ⊢ ( 𝜑 → ∀ 𝑗 ∈ ( 0 ..^ 𝑁 ) if- ( ( 𝑄 ‘ 𝑗 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) , ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) = { ( 𝑄 ‘ 𝑗 ) } , { ( 𝑄 ‘ 𝑗 ) , ( 𝑄 ‘ ( 𝑗 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) ) )