Metamath Proof Explorer


Theorem repswswrd

Description: A subword of a "repeated symbol word" is again a "repeated symbol word". The assumption N <_ L is required, because otherwise ( L < N ) : ( ( S repeatS L ) substr <. M , N >. ) = (/) , but for M < N ( S repeatS ( N - M ) ) ) =/= (/) ! The proof is relatively long because the border cases ( M = N , -. ( M ..^ N ) C_ ( 0 ..^ L ) must have been considered. (Contributed by AV, 6-Nov-2018)

Ref Expression
Assertion repswswrd ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) → ( ( 𝑆 repeatS 𝐿 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( 𝑆 repeatS ( 𝑁𝑀 ) ) )

Proof

Step Hyp Ref Expression
1 repsw ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) → ( 𝑆 repeatS 𝐿 ) ∈ Word 𝑉 )
2 nn0z ( 𝑀 ∈ ℕ0𝑀 ∈ ℤ )
3 nn0z ( 𝑁 ∈ ℕ0𝑁 ∈ ℤ )
4 2 3 anim12i ( ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) → ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
5 1 4 anim12i ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) → ( ( 𝑆 repeatS 𝐿 ) ∈ Word 𝑉 ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) )
6 3anass ( ( ( 𝑆 repeatS 𝐿 ) ∈ Word 𝑉𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ↔ ( ( 𝑆 repeatS 𝐿 ) ∈ Word 𝑉 ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) )
7 5 6 sylibr ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) → ( ( 𝑆 repeatS 𝐿 ) ∈ Word 𝑉𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
8 7 3adant3 ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) → ( ( 𝑆 repeatS 𝐿 ) ∈ Word 𝑉𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
9 swrdval ( ( ( 𝑆 repeatS 𝐿 ) ∈ Word 𝑉𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑆 repeatS 𝐿 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) = if ( ( 𝑀 ..^ 𝑁 ) ⊆ dom ( 𝑆 repeatS 𝐿 ) , ( 𝑥 ∈ ( 0 ..^ ( 𝑁𝑀 ) ) ↦ ( ( 𝑆 repeatS 𝐿 ) ‘ ( 𝑥 + 𝑀 ) ) ) , ∅ ) )
10 8 9 syl ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) → ( ( 𝑆 repeatS 𝐿 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) = if ( ( 𝑀 ..^ 𝑁 ) ⊆ dom ( 𝑆 repeatS 𝐿 ) , ( 𝑥 ∈ ( 0 ..^ ( 𝑁𝑀 ) ) ↦ ( ( 𝑆 repeatS 𝐿 ) ‘ ( 𝑥 + 𝑀 ) ) ) , ∅ ) )
11 repsf ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) → ( 𝑆 repeatS 𝐿 ) : ( 0 ..^ 𝐿 ) ⟶ 𝑉 )
12 11 3ad2ant1 ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) → ( 𝑆 repeatS 𝐿 ) : ( 0 ..^ 𝐿 ) ⟶ 𝑉 )
13 12 fdmd ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) → dom ( 𝑆 repeatS 𝐿 ) = ( 0 ..^ 𝐿 ) )
14 13 sseq2d ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) → ( ( 𝑀 ..^ 𝑁 ) ⊆ dom ( 𝑆 repeatS 𝐿 ) ↔ ( 𝑀 ..^ 𝑁 ) ⊆ ( 0 ..^ 𝐿 ) ) )
15 14 ifbid ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) → if ( ( 𝑀 ..^ 𝑁 ) ⊆ dom ( 𝑆 repeatS 𝐿 ) , ( 𝑥 ∈ ( 0 ..^ ( 𝑁𝑀 ) ) ↦ ( ( 𝑆 repeatS 𝐿 ) ‘ ( 𝑥 + 𝑀 ) ) ) , ∅ ) = if ( ( 𝑀 ..^ 𝑁 ) ⊆ ( 0 ..^ 𝐿 ) , ( 𝑥 ∈ ( 0 ..^ ( 𝑁𝑀 ) ) ↦ ( ( 𝑆 repeatS 𝐿 ) ‘ ( 𝑥 + 𝑀 ) ) ) , ∅ ) )
16 fzon ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁𝑀 ↔ ( 𝑀 ..^ 𝑁 ) = ∅ ) )
17 4 16 syl ( ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) → ( 𝑁𝑀 ↔ ( 𝑀 ..^ 𝑁 ) = ∅ ) )
18 17 adantl ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) → ( 𝑁𝑀 ↔ ( 𝑀 ..^ 𝑁 ) = ∅ ) )
19 18 biimpac ( ( 𝑁𝑀 ∧ ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) ) → ( 𝑀 ..^ 𝑁 ) = ∅ )
20 0ss ∅ ⊆ ( 0 ..^ 𝐿 )
21 19 20 eqsstrdi ( ( 𝑁𝑀 ∧ ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) ) → ( 𝑀 ..^ 𝑁 ) ⊆ ( 0 ..^ 𝐿 ) )
22 iftrue ( ( 𝑀 ..^ 𝑁 ) ⊆ ( 0 ..^ 𝐿 ) → if ( ( 𝑀 ..^ 𝑁 ) ⊆ ( 0 ..^ 𝐿 ) , ( 𝑥 ∈ ( 0 ..^ ( 𝑁𝑀 ) ) ↦ ( ( 𝑆 repeatS 𝐿 ) ‘ ( 𝑥 + 𝑀 ) ) ) , ∅ ) = ( 𝑥 ∈ ( 0 ..^ ( 𝑁𝑀 ) ) ↦ ( ( 𝑆 repeatS 𝐿 ) ‘ ( 𝑥 + 𝑀 ) ) ) )
23 21 22 syl ( ( 𝑁𝑀 ∧ ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) ) → if ( ( 𝑀 ..^ 𝑁 ) ⊆ ( 0 ..^ 𝐿 ) , ( 𝑥 ∈ ( 0 ..^ ( 𝑁𝑀 ) ) ↦ ( ( 𝑆 repeatS 𝐿 ) ‘ ( 𝑥 + 𝑀 ) ) ) , ∅ ) = ( 𝑥 ∈ ( 0 ..^ ( 𝑁𝑀 ) ) ↦ ( ( 𝑆 repeatS 𝐿 ) ‘ ( 𝑥 + 𝑀 ) ) ) )
24 nn0re ( 𝑀 ∈ ℕ0𝑀 ∈ ℝ )
25 nn0re ( 𝑁 ∈ ℕ0𝑁 ∈ ℝ )
26 24 25 anim12ci ( ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) → ( 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ) )
27 26 adantl ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) → ( 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ) )
28 suble0 ( ( 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → ( ( 𝑁𝑀 ) ≤ 0 ↔ 𝑁𝑀 ) )
29 27 28 syl ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) → ( ( 𝑁𝑀 ) ≤ 0 ↔ 𝑁𝑀 ) )
30 29 biimparc ( ( 𝑁𝑀 ∧ ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) ) → ( 𝑁𝑀 ) ≤ 0 )
31 0z 0 ∈ ℤ
32 zsubcl ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑁𝑀 ) ∈ ℤ )
33 3 2 32 syl2anr ( ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) → ( 𝑁𝑀 ) ∈ ℤ )
34 33 adantl ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) → ( 𝑁𝑀 ) ∈ ℤ )
35 34 adantl ( ( 𝑁𝑀 ∧ ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) ) → ( 𝑁𝑀 ) ∈ ℤ )
36 fzon ( ( 0 ∈ ℤ ∧ ( 𝑁𝑀 ) ∈ ℤ ) → ( ( 𝑁𝑀 ) ≤ 0 ↔ ( 0 ..^ ( 𝑁𝑀 ) ) = ∅ ) )
37 31 35 36 sylancr ( ( 𝑁𝑀 ∧ ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) ) → ( ( 𝑁𝑀 ) ≤ 0 ↔ ( 0 ..^ ( 𝑁𝑀 ) ) = ∅ ) )
38 30 37 mpbid ( ( 𝑁𝑀 ∧ ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) ) → ( 0 ..^ ( 𝑁𝑀 ) ) = ∅ )
39 38 mpteq1d ( ( 𝑁𝑀 ∧ ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) ) → ( 𝑥 ∈ ( 0 ..^ ( 𝑁𝑀 ) ) ↦ ( ( 𝑆 repeatS 𝐿 ) ‘ ( 𝑥 + 𝑀 ) ) ) = ( 𝑥 ∈ ∅ ↦ ( ( 𝑆 repeatS 𝐿 ) ‘ ( 𝑥 + 𝑀 ) ) ) )
40 mpt0 ( 𝑥 ∈ ∅ ↦ ( ( 𝑆 repeatS 𝐿 ) ‘ ( 𝑥 + 𝑀 ) ) ) = ∅
41 oveq2 ( 𝑀 = 𝑁 → ( 𝑁𝑀 ) = ( 𝑁𝑁 ) )
42 41 oveq2d ( 𝑀 = 𝑁 → ( 𝑆 repeatS ( 𝑁𝑀 ) ) = ( 𝑆 repeatS ( 𝑁𝑁 ) ) )
43 nn0cn ( 𝑁 ∈ ℕ0𝑁 ∈ ℂ )
44 43 adantl ( ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℂ )
45 44 subidd ( ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) → ( 𝑁𝑁 ) = 0 )
46 45 adantl ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) → ( 𝑁𝑁 ) = 0 )
47 46 oveq2d ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) → ( 𝑆 repeatS ( 𝑁𝑁 ) ) = ( 𝑆 repeatS 0 ) )
48 repsw0 ( 𝑆𝑉 → ( 𝑆 repeatS 0 ) = ∅ )
49 48 ad2antrr ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) → ( 𝑆 repeatS 0 ) = ∅ )
50 47 49 eqtrd ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) → ( 𝑆 repeatS ( 𝑁𝑁 ) ) = ∅ )
51 42 50 sylan9eqr ( ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) ∧ 𝑀 = 𝑁 ) → ( 𝑆 repeatS ( 𝑁𝑀 ) ) = ∅ )
52 51 ex ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) → ( 𝑀 = 𝑁 → ( 𝑆 repeatS ( 𝑁𝑀 ) ) = ∅ ) )
53 52 adantl ( ( 𝑁𝑀 ∧ ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) ) → ( 𝑀 = 𝑁 → ( 𝑆 repeatS ( 𝑁𝑀 ) ) = ∅ ) )
54 53 com12 ( 𝑀 = 𝑁 → ( ( 𝑁𝑀 ∧ ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) ) → ( 𝑆 repeatS ( 𝑁𝑀 ) ) = ∅ ) )
55 elnn0z ( ( 𝑁𝑀 ) ∈ ℕ0 ↔ ( ( 𝑁𝑀 ) ∈ ℤ ∧ 0 ≤ ( 𝑁𝑀 ) ) )
56 subge0 ( ( 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → ( 0 ≤ ( 𝑁𝑀 ) ↔ 𝑀𝑁 ) )
57 25 24 56 syl2anr ( ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) → ( 0 ≤ ( 𝑁𝑀 ) ↔ 𝑀𝑁 ) )
58 24 25 anim12i ( ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) → ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) )
59 letri3 ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝑀 = 𝑁 ↔ ( 𝑀𝑁𝑁𝑀 ) ) )
60 58 59 syl ( ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) → ( 𝑀 = 𝑁 ↔ ( 𝑀𝑁𝑁𝑀 ) ) )
61 60 biimprd ( ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) → ( ( 𝑀𝑁𝑁𝑀 ) → 𝑀 = 𝑁 ) )
62 61 expd ( ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) → ( 𝑀𝑁 → ( 𝑁𝑀𝑀 = 𝑁 ) ) )
63 57 62 sylbid ( ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) → ( 0 ≤ ( 𝑁𝑀 ) → ( 𝑁𝑀𝑀 = 𝑁 ) ) )
64 63 com23 ( ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) → ( 𝑁𝑀 → ( 0 ≤ ( 𝑁𝑀 ) → 𝑀 = 𝑁 ) ) )
65 64 adantl ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) → ( 𝑁𝑀 → ( 0 ≤ ( 𝑁𝑀 ) → 𝑀 = 𝑁 ) ) )
66 65 impcom ( ( 𝑁𝑀 ∧ ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) ) → ( 0 ≤ ( 𝑁𝑀 ) → 𝑀 = 𝑁 ) )
67 66 com12 ( 0 ≤ ( 𝑁𝑀 ) → ( ( 𝑁𝑀 ∧ ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) ) → 𝑀 = 𝑁 ) )
68 55 67 simplbiim ( ( 𝑁𝑀 ) ∈ ℕ0 → ( ( 𝑁𝑀 ∧ ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) ) → 𝑀 = 𝑁 ) )
69 68 com12 ( ( 𝑁𝑀 ∧ ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) ) → ( ( 𝑁𝑀 ) ∈ ℕ0𝑀 = 𝑁 ) )
70 69 con3d ( ( 𝑁𝑀 ∧ ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) ) → ( ¬ 𝑀 = 𝑁 → ¬ ( 𝑁𝑀 ) ∈ ℕ0 ) )
71 70 impcom ( ( ¬ 𝑀 = 𝑁 ∧ ( 𝑁𝑀 ∧ ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) ) ) → ¬ ( 𝑁𝑀 ) ∈ ℕ0 )
72 df-nel ( ( 𝑁𝑀 ) ∉ ℕ0 ↔ ¬ ( 𝑁𝑀 ) ∈ ℕ0 )
73 71 72 sylibr ( ( ¬ 𝑀 = 𝑁 ∧ ( 𝑁𝑀 ∧ ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) ) ) → ( 𝑁𝑀 ) ∉ ℕ0 )
74 repsundef ( ( 𝑁𝑀 ) ∉ ℕ0 → ( 𝑆 repeatS ( 𝑁𝑀 ) ) = ∅ )
75 73 74 syl ( ( ¬ 𝑀 = 𝑁 ∧ ( 𝑁𝑀 ∧ ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) ) ) → ( 𝑆 repeatS ( 𝑁𝑀 ) ) = ∅ )
76 75 ex ( ¬ 𝑀 = 𝑁 → ( ( 𝑁𝑀 ∧ ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) ) → ( 𝑆 repeatS ( 𝑁𝑀 ) ) = ∅ ) )
77 54 76 pm2.61i ( ( 𝑁𝑀 ∧ ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) ) → ( 𝑆 repeatS ( 𝑁𝑀 ) ) = ∅ )
78 40 77 eqtr4id ( ( 𝑁𝑀 ∧ ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) ) → ( 𝑥 ∈ ∅ ↦ ( ( 𝑆 repeatS 𝐿 ) ‘ ( 𝑥 + 𝑀 ) ) ) = ( 𝑆 repeatS ( 𝑁𝑀 ) ) )
79 23 39 78 3eqtrd ( ( 𝑁𝑀 ∧ ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) ) → if ( ( 𝑀 ..^ 𝑁 ) ⊆ ( 0 ..^ 𝐿 ) , ( 𝑥 ∈ ( 0 ..^ ( 𝑁𝑀 ) ) ↦ ( ( 𝑆 repeatS 𝐿 ) ‘ ( 𝑥 + 𝑀 ) ) ) , ∅ ) = ( 𝑆 repeatS ( 𝑁𝑀 ) ) )
80 79 expcom ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) → ( 𝑁𝑀 → if ( ( 𝑀 ..^ 𝑁 ) ⊆ ( 0 ..^ 𝐿 ) , ( 𝑥 ∈ ( 0 ..^ ( 𝑁𝑀 ) ) ↦ ( ( 𝑆 repeatS 𝐿 ) ‘ ( 𝑥 + 𝑀 ) ) ) , ∅ ) = ( 𝑆 repeatS ( 𝑁𝑀 ) ) ) )
81 80 3adant3 ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) → ( 𝑁𝑀 → if ( ( 𝑀 ..^ 𝑁 ) ⊆ ( 0 ..^ 𝐿 ) , ( 𝑥 ∈ ( 0 ..^ ( 𝑁𝑀 ) ) ↦ ( ( 𝑆 repeatS 𝐿 ) ‘ ( 𝑥 + 𝑀 ) ) ) , ∅ ) = ( 𝑆 repeatS ( 𝑁𝑀 ) ) ) )
82 ltnle ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝑀 < 𝑁 ↔ ¬ 𝑁𝑀 ) )
83 58 82 syl ( ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) → ( 𝑀 < 𝑁 ↔ ¬ 𝑁𝑀 ) )
84 83 bicomd ( ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) → ( ¬ 𝑁𝑀𝑀 < 𝑁 ) )
85 84 3ad2ant2 ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) → ( ¬ 𝑁𝑀𝑀 < 𝑁 ) )
86 22 adantr ( ( ( 𝑀 ..^ 𝑁 ) ⊆ ( 0 ..^ 𝐿 ) ∧ ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) ∧ 𝑀 < 𝑁 ) ) → if ( ( 𝑀 ..^ 𝑁 ) ⊆ ( 0 ..^ 𝐿 ) , ( 𝑥 ∈ ( 0 ..^ ( 𝑁𝑀 ) ) ↦ ( ( 𝑆 repeatS 𝐿 ) ‘ ( 𝑥 + 𝑀 ) ) ) , ∅ ) = ( 𝑥 ∈ ( 0 ..^ ( 𝑁𝑀 ) ) ↦ ( ( 𝑆 repeatS 𝐿 ) ‘ ( 𝑥 + 𝑀 ) ) ) )
87 4 3ad2ant2 ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) → ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
88 87 adantr ( ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) ∧ 𝑀 < 𝑁 ) → ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
89 0zd ( 𝑆𝑉 → 0 ∈ ℤ )
90 nn0z ( 𝐿 ∈ ℕ0𝐿 ∈ ℤ )
91 89 90 anim12i ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) → ( 0 ∈ ℤ ∧ 𝐿 ∈ ℤ ) )
92 91 3ad2ant1 ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) → ( 0 ∈ ℤ ∧ 𝐿 ∈ ℤ ) )
93 92 adantr ( ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) ∧ 𝑀 < 𝑁 ) → ( 0 ∈ ℤ ∧ 𝐿 ∈ ℤ ) )
94 simpr ( ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) ∧ 𝑀 < 𝑁 ) → 𝑀 < 𝑁 )
95 ssfzo12bi ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 0 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ 𝑀 < 𝑁 ) → ( ( 𝑀 ..^ 𝑁 ) ⊆ ( 0 ..^ 𝐿 ) ↔ ( 0 ≤ 𝑀𝑁𝐿 ) ) )
96 88 93 94 95 syl3anc ( ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) ∧ 𝑀 < 𝑁 ) → ( ( 𝑀 ..^ 𝑁 ) ⊆ ( 0 ..^ 𝐿 ) ↔ ( 0 ≤ 𝑀𝑁𝐿 ) ) )
97 simpl1l ( ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) ∧ 𝑀 < 𝑁 ) → 𝑆𝑉 )
98 97 ad2antrr ( ( ( ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) ∧ 𝑀 < 𝑁 ) ∧ ( 0 ≤ 𝑀𝑁𝐿 ) ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑁𝑀 ) ) ) → 𝑆𝑉 )
99 simpl1r ( ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) ∧ 𝑀 < 𝑁 ) → 𝐿 ∈ ℕ0 )
100 99 ad2antrr ( ( ( ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) ∧ 𝑀 < 𝑁 ) ∧ ( 0 ≤ 𝑀𝑁𝐿 ) ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑁𝑀 ) ) ) → 𝐿 ∈ ℕ0 )
101 nn0addcl ( ( 𝑥 ∈ ℕ0𝑀 ∈ ℕ0 ) → ( 𝑥 + 𝑀 ) ∈ ℕ0 )
102 101 expcom ( 𝑀 ∈ ℕ0 → ( 𝑥 ∈ ℕ0 → ( 𝑥 + 𝑀 ) ∈ ℕ0 ) )
103 102 adantr ( ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) → ( 𝑥 ∈ ℕ0 → ( 𝑥 + 𝑀 ) ∈ ℕ0 ) )
104 103 3ad2ant2 ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) → ( 𝑥 ∈ ℕ0 → ( 𝑥 + 𝑀 ) ∈ ℕ0 ) )
105 104 ad2antrr ( ( ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) ∧ 𝑀 < 𝑁 ) ∧ ( 0 ≤ 𝑀𝑁𝐿 ) ) → ( 𝑥 ∈ ℕ0 → ( 𝑥 + 𝑀 ) ∈ ℕ0 ) )
106 elfzonn0 ( 𝑥 ∈ ( 0 ..^ ( 𝑁𝑀 ) ) → 𝑥 ∈ ℕ0 )
107 105 106 impel ( ( ( ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) ∧ 𝑀 < 𝑁 ) ∧ ( 0 ≤ 𝑀𝑁𝐿 ) ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑁𝑀 ) ) ) → ( 𝑥 + 𝑀 ) ∈ ℕ0 )
108 90 adantl ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) → 𝐿 ∈ ℤ )
109 108 3ad2ant1 ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) → 𝐿 ∈ ℤ )
110 109 adantr ( ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) ∧ 𝑀 < 𝑁 ) → 𝐿 ∈ ℤ )
111 nn0re ( 𝐿 ∈ ℕ0𝐿 ∈ ℝ )
112 111 adantl ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) → 𝐿 ∈ ℝ )
113 112 58 anim12ci ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) → ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) ∧ 𝐿 ∈ ℝ ) )
114 df-3an ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ ) ↔ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) ∧ 𝐿 ∈ ℝ ) )
115 113 114 sylibr ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) → ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ ) )
116 ltletr ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ ) → ( ( 𝑀 < 𝑁𝑁𝐿 ) → 𝑀 < 𝐿 ) )
117 115 116 syl ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) → ( ( 𝑀 < 𝑁𝑁𝐿 ) → 𝑀 < 𝐿 ) )
118 elnn0z ( 𝑀 ∈ ℕ0 ↔ ( 𝑀 ∈ ℤ ∧ 0 ≤ 𝑀 ) )
119 0red ( ( 𝑀 ∈ ℤ ∧ ( 𝑆𝑉𝐿 ∈ ℕ0 ) ) → 0 ∈ ℝ )
120 zre ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
121 120 adantr ( ( 𝑀 ∈ ℤ ∧ ( 𝑆𝑉𝐿 ∈ ℕ0 ) ) → 𝑀 ∈ ℝ )
122 112 adantl ( ( 𝑀 ∈ ℤ ∧ ( 𝑆𝑉𝐿 ∈ ℕ0 ) ) → 𝐿 ∈ ℝ )
123 lelttr ( ( 0 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝐿 ∈ ℝ ) → ( ( 0 ≤ 𝑀𝑀 < 𝐿 ) → 0 < 𝐿 ) )
124 119 121 122 123 syl3anc ( ( 𝑀 ∈ ℤ ∧ ( 𝑆𝑉𝐿 ∈ ℕ0 ) ) → ( ( 0 ≤ 𝑀𝑀 < 𝐿 ) → 0 < 𝐿 ) )
125 124 expd ( ( 𝑀 ∈ ℤ ∧ ( 𝑆𝑉𝐿 ∈ ℕ0 ) ) → ( 0 ≤ 𝑀 → ( 𝑀 < 𝐿 → 0 < 𝐿 ) ) )
126 125 impancom ( ( 𝑀 ∈ ℤ ∧ 0 ≤ 𝑀 ) → ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) → ( 𝑀 < 𝐿 → 0 < 𝐿 ) ) )
127 118 126 sylbi ( 𝑀 ∈ ℕ0 → ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) → ( 𝑀 < 𝐿 → 0 < 𝐿 ) ) )
128 127 adantr ( ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) → ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) → ( 𝑀 < 𝐿 → 0 < 𝐿 ) ) )
129 128 impcom ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) → ( 𝑀 < 𝐿 → 0 < 𝐿 ) )
130 117 129 syld ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) → ( ( 𝑀 < 𝑁𝑁𝐿 ) → 0 < 𝐿 ) )
131 130 expcomd ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) → ( 𝑁𝐿 → ( 𝑀 < 𝑁 → 0 < 𝐿 ) ) )
132 131 3impia ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) → ( 𝑀 < 𝑁 → 0 < 𝐿 ) )
133 132 imp ( ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) ∧ 𝑀 < 𝑁 ) → 0 < 𝐿 )
134 elnnz ( 𝐿 ∈ ℕ ↔ ( 𝐿 ∈ ℤ ∧ 0 < 𝐿 ) )
135 110 133 134 sylanbrc ( ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) ∧ 𝑀 < 𝑁 ) → 𝐿 ∈ ℕ )
136 135 ad2antrr ( ( ( ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) ∧ 𝑀 < 𝑁 ) ∧ ( 0 ≤ 𝑀𝑁𝐿 ) ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑁𝑀 ) ) ) → 𝐿 ∈ ℕ )
137 elfzo0 ( 𝑥 ∈ ( 0 ..^ ( 𝑁𝑀 ) ) ↔ ( 𝑥 ∈ ℕ0 ∧ ( 𝑁𝑀 ) ∈ ℕ ∧ 𝑥 < ( 𝑁𝑀 ) ) )
138 nn0readdcl ( ( 𝑥 ∈ ℕ0𝑀 ∈ ℕ0 ) → ( 𝑥 + 𝑀 ) ∈ ℝ )
139 138 expcom ( 𝑀 ∈ ℕ0 → ( 𝑥 ∈ ℕ0 → ( 𝑥 + 𝑀 ) ∈ ℝ ) )
140 139 ad2antrl ( ( 𝐿 ∈ ℕ0 ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) → ( 𝑥 ∈ ℕ0 → ( 𝑥 + 𝑀 ) ∈ ℝ ) )
141 140 impcom ( ( 𝑥 ∈ ℕ0 ∧ ( 𝐿 ∈ ℕ0 ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) ) → ( 𝑥 + 𝑀 ) ∈ ℝ )
142 25 adantl ( ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℝ )
143 142 adantl ( ( 𝐿 ∈ ℕ0 ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) → 𝑁 ∈ ℝ )
144 143 adantl ( ( 𝑥 ∈ ℕ0 ∧ ( 𝐿 ∈ ℕ0 ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) ) → 𝑁 ∈ ℝ )
145 111 ad2antrl ( ( 𝑥 ∈ ℕ0 ∧ ( 𝐿 ∈ ℕ0 ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) ) → 𝐿 ∈ ℝ )
146 141 144 145 3jca ( ( 𝑥 ∈ ℕ0 ∧ ( 𝐿 ∈ ℕ0 ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) ) → ( ( 𝑥 + 𝑀 ) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ ) )
147 146 ex ( 𝑥 ∈ ℕ0 → ( ( 𝐿 ∈ ℕ0 ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) → ( ( 𝑥 + 𝑀 ) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ ) ) )
148 147 adantr ( ( 𝑥 ∈ ℕ0𝑥 < ( 𝑁𝑀 ) ) → ( ( 𝐿 ∈ ℕ0 ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) → ( ( 𝑥 + 𝑀 ) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ ) ) )
149 148 impcom ( ( ( 𝐿 ∈ ℕ0 ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) ∧ ( 𝑥 ∈ ℕ0𝑥 < ( 𝑁𝑀 ) ) ) → ( ( 𝑥 + 𝑀 ) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ ) )
150 149 adantr ( ( ( ( 𝐿 ∈ ℕ0 ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) ∧ ( 𝑥 ∈ ℕ0𝑥 < ( 𝑁𝑀 ) ) ) ∧ 𝑁𝐿 ) → ( ( 𝑥 + 𝑀 ) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ ) )
151 nn0re ( 𝑥 ∈ ℕ0𝑥 ∈ ℝ )
152 151 adantr ( ( 𝑥 ∈ ℕ0 ∧ ( 𝐿 ∈ ℕ0 ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) ) → 𝑥 ∈ ℝ )
153 24 ad2antrl ( ( 𝐿 ∈ ℕ0 ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) → 𝑀 ∈ ℝ )
154 153 adantl ( ( 𝑥 ∈ ℕ0 ∧ ( 𝐿 ∈ ℕ0 ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) ) → 𝑀 ∈ ℝ )
155 152 154 144 ltaddsubd ( ( 𝑥 ∈ ℕ0 ∧ ( 𝐿 ∈ ℕ0 ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) ) → ( ( 𝑥 + 𝑀 ) < 𝑁𝑥 < ( 𝑁𝑀 ) ) )
156 idd ( ( ( 𝑥 ∈ ℕ0 ∧ ( 𝐿 ∈ ℕ0 ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) ) ∧ 𝑁𝐿 ) → ( ( 𝑥 + 𝑀 ) < 𝑁 → ( 𝑥 + 𝑀 ) < 𝑁 ) )
157 156 ex ( ( 𝑥 ∈ ℕ0 ∧ ( 𝐿 ∈ ℕ0 ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) ) → ( 𝑁𝐿 → ( ( 𝑥 + 𝑀 ) < 𝑁 → ( 𝑥 + 𝑀 ) < 𝑁 ) ) )
158 157 com23 ( ( 𝑥 ∈ ℕ0 ∧ ( 𝐿 ∈ ℕ0 ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) ) → ( ( 𝑥 + 𝑀 ) < 𝑁 → ( 𝑁𝐿 → ( 𝑥 + 𝑀 ) < 𝑁 ) ) )
159 155 158 sylbird ( ( 𝑥 ∈ ℕ0 ∧ ( 𝐿 ∈ ℕ0 ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) ) → ( 𝑥 < ( 𝑁𝑀 ) → ( 𝑁𝐿 → ( 𝑥 + 𝑀 ) < 𝑁 ) ) )
160 159 impancom ( ( 𝑥 ∈ ℕ0𝑥 < ( 𝑁𝑀 ) ) → ( ( 𝐿 ∈ ℕ0 ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) → ( 𝑁𝐿 → ( 𝑥 + 𝑀 ) < 𝑁 ) ) )
161 160 impcom ( ( ( 𝐿 ∈ ℕ0 ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) ∧ ( 𝑥 ∈ ℕ0𝑥 < ( 𝑁𝑀 ) ) ) → ( 𝑁𝐿 → ( 𝑥 + 𝑀 ) < 𝑁 ) )
162 161 impac ( ( ( ( 𝐿 ∈ ℕ0 ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) ∧ ( 𝑥 ∈ ℕ0𝑥 < ( 𝑁𝑀 ) ) ) ∧ 𝑁𝐿 ) → ( ( 𝑥 + 𝑀 ) < 𝑁𝑁𝐿 ) )
163 ltletr ( ( ( 𝑥 + 𝑀 ) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ ) → ( ( ( 𝑥 + 𝑀 ) < 𝑁𝑁𝐿 ) → ( 𝑥 + 𝑀 ) < 𝐿 ) )
164 150 162 163 sylc ( ( ( ( 𝐿 ∈ ℕ0 ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) ∧ ( 𝑥 ∈ ℕ0𝑥 < ( 𝑁𝑀 ) ) ) ∧ 𝑁𝐿 ) → ( 𝑥 + 𝑀 ) < 𝐿 )
165 164 exp31 ( ( 𝐿 ∈ ℕ0 ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) → ( ( 𝑥 ∈ ℕ0𝑥 < ( 𝑁𝑀 ) ) → ( 𝑁𝐿 → ( 𝑥 + 𝑀 ) < 𝐿 ) ) )
166 165 com23 ( ( 𝐿 ∈ ℕ0 ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ) → ( 𝑁𝐿 → ( ( 𝑥 ∈ ℕ0𝑥 < ( 𝑁𝑀 ) ) → ( 𝑥 + 𝑀 ) < 𝐿 ) ) )
167 166 ex ( 𝐿 ∈ ℕ0 → ( ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) → ( 𝑁𝐿 → ( ( 𝑥 ∈ ℕ0𝑥 < ( 𝑁𝑀 ) ) → ( 𝑥 + 𝑀 ) < 𝐿 ) ) ) )
168 167 adantl ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) → ( ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) → ( 𝑁𝐿 → ( ( 𝑥 ∈ ℕ0𝑥 < ( 𝑁𝑀 ) ) → ( 𝑥 + 𝑀 ) < 𝐿 ) ) ) )
169 168 3imp ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) → ( ( 𝑥 ∈ ℕ0𝑥 < ( 𝑁𝑀 ) ) → ( 𝑥 + 𝑀 ) < 𝐿 ) )
170 169 ad2antrr ( ( ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) ∧ 𝑀 < 𝑁 ) ∧ ( 0 ≤ 𝑀𝑁𝐿 ) ) → ( ( 𝑥 ∈ ℕ0𝑥 < ( 𝑁𝑀 ) ) → ( 𝑥 + 𝑀 ) < 𝐿 ) )
171 170 com12 ( ( 𝑥 ∈ ℕ0𝑥 < ( 𝑁𝑀 ) ) → ( ( ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) ∧ 𝑀 < 𝑁 ) ∧ ( 0 ≤ 𝑀𝑁𝐿 ) ) → ( 𝑥 + 𝑀 ) < 𝐿 ) )
172 171 3adant2 ( ( 𝑥 ∈ ℕ0 ∧ ( 𝑁𝑀 ) ∈ ℕ ∧ 𝑥 < ( 𝑁𝑀 ) ) → ( ( ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) ∧ 𝑀 < 𝑁 ) ∧ ( 0 ≤ 𝑀𝑁𝐿 ) ) → ( 𝑥 + 𝑀 ) < 𝐿 ) )
173 137 172 sylbi ( 𝑥 ∈ ( 0 ..^ ( 𝑁𝑀 ) ) → ( ( ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) ∧ 𝑀 < 𝑁 ) ∧ ( 0 ≤ 𝑀𝑁𝐿 ) ) → ( 𝑥 + 𝑀 ) < 𝐿 ) )
174 173 impcom ( ( ( ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) ∧ 𝑀 < 𝑁 ) ∧ ( 0 ≤ 𝑀𝑁𝐿 ) ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑁𝑀 ) ) ) → ( 𝑥 + 𝑀 ) < 𝐿 )
175 elfzo0 ( ( 𝑥 + 𝑀 ) ∈ ( 0 ..^ 𝐿 ) ↔ ( ( 𝑥 + 𝑀 ) ∈ ℕ0𝐿 ∈ ℕ ∧ ( 𝑥 + 𝑀 ) < 𝐿 ) )
176 107 136 174 175 syl3anbrc ( ( ( ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) ∧ 𝑀 < 𝑁 ) ∧ ( 0 ≤ 𝑀𝑁𝐿 ) ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑁𝑀 ) ) ) → ( 𝑥 + 𝑀 ) ∈ ( 0 ..^ 𝐿 ) )
177 repswsymb ( ( 𝑆𝑉𝐿 ∈ ℕ0 ∧ ( 𝑥 + 𝑀 ) ∈ ( 0 ..^ 𝐿 ) ) → ( ( 𝑆 repeatS 𝐿 ) ‘ ( 𝑥 + 𝑀 ) ) = 𝑆 )
178 98 100 176 177 syl3anc ( ( ( ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) ∧ 𝑀 < 𝑁 ) ∧ ( 0 ≤ 𝑀𝑁𝐿 ) ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑁𝑀 ) ) ) → ( ( 𝑆 repeatS 𝐿 ) ‘ ( 𝑥 + 𝑀 ) ) = 𝑆 )
179 178 mpteq2dva ( ( ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) ∧ 𝑀 < 𝑁 ) ∧ ( 0 ≤ 𝑀𝑁𝐿 ) ) → ( 𝑥 ∈ ( 0 ..^ ( 𝑁𝑀 ) ) ↦ ( ( 𝑆 repeatS 𝐿 ) ‘ ( 𝑥 + 𝑀 ) ) ) = ( 𝑥 ∈ ( 0 ..^ ( 𝑁𝑀 ) ) ↦ 𝑆 ) )
180 33 3ad2ant2 ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) → ( 𝑁𝑀 ) ∈ ℤ )
181 180 adantr ( ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) ∧ 𝑀 < 𝑁 ) → ( 𝑁𝑀 ) ∈ ℤ )
182 58 3ad2ant2 ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) → ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) )
183 ltle ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝑀 < 𝑁𝑀𝑁 ) )
184 182 183 syl ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) → ( 𝑀 < 𝑁𝑀𝑁 ) )
185 26 3ad2ant2 ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) → ( 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ) )
186 185 56 syl ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) → ( 0 ≤ ( 𝑁𝑀 ) ↔ 𝑀𝑁 ) )
187 184 186 sylibrd ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) → ( 𝑀 < 𝑁 → 0 ≤ ( 𝑁𝑀 ) ) )
188 187 imp ( ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) ∧ 𝑀 < 𝑁 ) → 0 ≤ ( 𝑁𝑀 ) )
189 181 188 55 sylanbrc ( ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) ∧ 𝑀 < 𝑁 ) → ( 𝑁𝑀 ) ∈ ℕ0 )
190 97 189 jca ( ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) ∧ 𝑀 < 𝑁 ) → ( 𝑆𝑉 ∧ ( 𝑁𝑀 ) ∈ ℕ0 ) )
191 190 adantr ( ( ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) ∧ 𝑀 < 𝑁 ) ∧ ( 0 ≤ 𝑀𝑁𝐿 ) ) → ( 𝑆𝑉 ∧ ( 𝑁𝑀 ) ∈ ℕ0 ) )
192 reps ( ( 𝑆𝑉 ∧ ( 𝑁𝑀 ) ∈ ℕ0 ) → ( 𝑆 repeatS ( 𝑁𝑀 ) ) = ( 𝑥 ∈ ( 0 ..^ ( 𝑁𝑀 ) ) ↦ 𝑆 ) )
193 192 eqcomd ( ( 𝑆𝑉 ∧ ( 𝑁𝑀 ) ∈ ℕ0 ) → ( 𝑥 ∈ ( 0 ..^ ( 𝑁𝑀 ) ) ↦ 𝑆 ) = ( 𝑆 repeatS ( 𝑁𝑀 ) ) )
194 191 193 syl ( ( ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) ∧ 𝑀 < 𝑁 ) ∧ ( 0 ≤ 𝑀𝑁𝐿 ) ) → ( 𝑥 ∈ ( 0 ..^ ( 𝑁𝑀 ) ) ↦ 𝑆 ) = ( 𝑆 repeatS ( 𝑁𝑀 ) ) )
195 179 194 eqtrd ( ( ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) ∧ 𝑀 < 𝑁 ) ∧ ( 0 ≤ 𝑀𝑁𝐿 ) ) → ( 𝑥 ∈ ( 0 ..^ ( 𝑁𝑀 ) ) ↦ ( ( 𝑆 repeatS 𝐿 ) ‘ ( 𝑥 + 𝑀 ) ) ) = ( 𝑆 repeatS ( 𝑁𝑀 ) ) )
196 195 ex ( ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) ∧ 𝑀 < 𝑁 ) → ( ( 0 ≤ 𝑀𝑁𝐿 ) → ( 𝑥 ∈ ( 0 ..^ ( 𝑁𝑀 ) ) ↦ ( ( 𝑆 repeatS 𝐿 ) ‘ ( 𝑥 + 𝑀 ) ) ) = ( 𝑆 repeatS ( 𝑁𝑀 ) ) ) )
197 96 196 sylbid ( ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) ∧ 𝑀 < 𝑁 ) → ( ( 𝑀 ..^ 𝑁 ) ⊆ ( 0 ..^ 𝐿 ) → ( 𝑥 ∈ ( 0 ..^ ( 𝑁𝑀 ) ) ↦ ( ( 𝑆 repeatS 𝐿 ) ‘ ( 𝑥 + 𝑀 ) ) ) = ( 𝑆 repeatS ( 𝑁𝑀 ) ) ) )
198 197 impcom ( ( ( 𝑀 ..^ 𝑁 ) ⊆ ( 0 ..^ 𝐿 ) ∧ ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) ∧ 𝑀 < 𝑁 ) ) → ( 𝑥 ∈ ( 0 ..^ ( 𝑁𝑀 ) ) ↦ ( ( 𝑆 repeatS 𝐿 ) ‘ ( 𝑥 + 𝑀 ) ) ) = ( 𝑆 repeatS ( 𝑁𝑀 ) ) )
199 86 198 eqtrd ( ( ( 𝑀 ..^ 𝑁 ) ⊆ ( 0 ..^ 𝐿 ) ∧ ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) ∧ 𝑀 < 𝑁 ) ) → if ( ( 𝑀 ..^ 𝑁 ) ⊆ ( 0 ..^ 𝐿 ) , ( 𝑥 ∈ ( 0 ..^ ( 𝑁𝑀 ) ) ↦ ( ( 𝑆 repeatS 𝐿 ) ‘ ( 𝑥 + 𝑀 ) ) ) , ∅ ) = ( 𝑆 repeatS ( 𝑁𝑀 ) ) )
200 iffalse ( ¬ ( 𝑀 ..^ 𝑁 ) ⊆ ( 0 ..^ 𝐿 ) → if ( ( 𝑀 ..^ 𝑁 ) ⊆ ( 0 ..^ 𝐿 ) , ( 𝑥 ∈ ( 0 ..^ ( 𝑁𝑀 ) ) ↦ ( ( 𝑆 repeatS 𝐿 ) ‘ ( 𝑥 + 𝑀 ) ) ) , ∅ ) = ∅ )
201 200 adantr ( ( ¬ ( 𝑀 ..^ 𝑁 ) ⊆ ( 0 ..^ 𝐿 ) ∧ ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) ∧ 𝑀 < 𝑁 ) ) → if ( ( 𝑀 ..^ 𝑁 ) ⊆ ( 0 ..^ 𝐿 ) , ( 𝑥 ∈ ( 0 ..^ ( 𝑁𝑀 ) ) ↦ ( ( 𝑆 repeatS 𝐿 ) ‘ ( 𝑥 + 𝑀 ) ) ) , ∅ ) = ∅ )
202 96 notbid ( ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) ∧ 𝑀 < 𝑁 ) → ( ¬ ( 𝑀 ..^ 𝑁 ) ⊆ ( 0 ..^ 𝐿 ) ↔ ¬ ( 0 ≤ 𝑀𝑁𝐿 ) ) )
203 ianor ( ¬ ( 0 ≤ 𝑀𝑁𝐿 ) ↔ ( ¬ 0 ≤ 𝑀 ∨ ¬ 𝑁𝐿 ) )
204 nn0ge0 ( 𝑀 ∈ ℕ0 → 0 ≤ 𝑀 )
205 pm2.24 ( 0 ≤ 𝑀 → ( ¬ 0 ≤ 𝑀 → ( 𝑆 repeatS ( 𝑁𝑀 ) ) = ∅ ) )
206 204 205 syl ( 𝑀 ∈ ℕ0 → ( ¬ 0 ≤ 𝑀 → ( 𝑆 repeatS ( 𝑁𝑀 ) ) = ∅ ) )
207 206 adantr ( ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) → ( ¬ 0 ≤ 𝑀 → ( 𝑆 repeatS ( 𝑁𝑀 ) ) = ∅ ) )
208 207 3ad2ant2 ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) → ( ¬ 0 ≤ 𝑀 → ( 𝑆 repeatS ( 𝑁𝑀 ) ) = ∅ ) )
209 208 adantr ( ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) ∧ 𝑀 < 𝑁 ) → ( ¬ 0 ≤ 𝑀 → ( 𝑆 repeatS ( 𝑁𝑀 ) ) = ∅ ) )
210 209 com12 ( ¬ 0 ≤ 𝑀 → ( ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) ∧ 𝑀 < 𝑁 ) → ( 𝑆 repeatS ( 𝑁𝑀 ) ) = ∅ ) )
211 pm2.24 ( 𝑁𝐿 → ( ¬ 𝑁𝐿 → ( 𝑆 repeatS ( 𝑁𝑀 ) ) = ∅ ) )
212 211 3ad2ant3 ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) → ( ¬ 𝑁𝐿 → ( 𝑆 repeatS ( 𝑁𝑀 ) ) = ∅ ) )
213 212 adantr ( ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) ∧ 𝑀 < 𝑁 ) → ( ¬ 𝑁𝐿 → ( 𝑆 repeatS ( 𝑁𝑀 ) ) = ∅ ) )
214 213 com12 ( ¬ 𝑁𝐿 → ( ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) ∧ 𝑀 < 𝑁 ) → ( 𝑆 repeatS ( 𝑁𝑀 ) ) = ∅ ) )
215 210 214 jaoi ( ( ¬ 0 ≤ 𝑀 ∨ ¬ 𝑁𝐿 ) → ( ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) ∧ 𝑀 < 𝑁 ) → ( 𝑆 repeatS ( 𝑁𝑀 ) ) = ∅ ) )
216 203 215 sylbi ( ¬ ( 0 ≤ 𝑀𝑁𝐿 ) → ( ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) ∧ 𝑀 < 𝑁 ) → ( 𝑆 repeatS ( 𝑁𝑀 ) ) = ∅ ) )
217 216 com12 ( ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) ∧ 𝑀 < 𝑁 ) → ( ¬ ( 0 ≤ 𝑀𝑁𝐿 ) → ( 𝑆 repeatS ( 𝑁𝑀 ) ) = ∅ ) )
218 202 217 sylbid ( ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) ∧ 𝑀 < 𝑁 ) → ( ¬ ( 𝑀 ..^ 𝑁 ) ⊆ ( 0 ..^ 𝐿 ) → ( 𝑆 repeatS ( 𝑁𝑀 ) ) = ∅ ) )
219 218 impcom ( ( ¬ ( 𝑀 ..^ 𝑁 ) ⊆ ( 0 ..^ 𝐿 ) ∧ ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) ∧ 𝑀 < 𝑁 ) ) → ( 𝑆 repeatS ( 𝑁𝑀 ) ) = ∅ )
220 201 219 eqtr4d ( ( ¬ ( 𝑀 ..^ 𝑁 ) ⊆ ( 0 ..^ 𝐿 ) ∧ ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) ∧ 𝑀 < 𝑁 ) ) → if ( ( 𝑀 ..^ 𝑁 ) ⊆ ( 0 ..^ 𝐿 ) , ( 𝑥 ∈ ( 0 ..^ ( 𝑁𝑀 ) ) ↦ ( ( 𝑆 repeatS 𝐿 ) ‘ ( 𝑥 + 𝑀 ) ) ) , ∅ ) = ( 𝑆 repeatS ( 𝑁𝑀 ) ) )
221 199 220 pm2.61ian ( ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) ∧ 𝑀 < 𝑁 ) → if ( ( 𝑀 ..^ 𝑁 ) ⊆ ( 0 ..^ 𝐿 ) , ( 𝑥 ∈ ( 0 ..^ ( 𝑁𝑀 ) ) ↦ ( ( 𝑆 repeatS 𝐿 ) ‘ ( 𝑥 + 𝑀 ) ) ) , ∅ ) = ( 𝑆 repeatS ( 𝑁𝑀 ) ) )
222 221 ex ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) → ( 𝑀 < 𝑁 → if ( ( 𝑀 ..^ 𝑁 ) ⊆ ( 0 ..^ 𝐿 ) , ( 𝑥 ∈ ( 0 ..^ ( 𝑁𝑀 ) ) ↦ ( ( 𝑆 repeatS 𝐿 ) ‘ ( 𝑥 + 𝑀 ) ) ) , ∅ ) = ( 𝑆 repeatS ( 𝑁𝑀 ) ) ) )
223 85 222 sylbid ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) → ( ¬ 𝑁𝑀 → if ( ( 𝑀 ..^ 𝑁 ) ⊆ ( 0 ..^ 𝐿 ) , ( 𝑥 ∈ ( 0 ..^ ( 𝑁𝑀 ) ) ↦ ( ( 𝑆 repeatS 𝐿 ) ‘ ( 𝑥 + 𝑀 ) ) ) , ∅ ) = ( 𝑆 repeatS ( 𝑁𝑀 ) ) ) )
224 81 223 pm2.61d ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) → if ( ( 𝑀 ..^ 𝑁 ) ⊆ ( 0 ..^ 𝐿 ) , ( 𝑥 ∈ ( 0 ..^ ( 𝑁𝑀 ) ) ↦ ( ( 𝑆 repeatS 𝐿 ) ‘ ( 𝑥 + 𝑀 ) ) ) , ∅ ) = ( 𝑆 repeatS ( 𝑁𝑀 ) ) )
225 10 15 224 3eqtrd ( ( ( 𝑆𝑉𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐿 ) → ( ( 𝑆 repeatS 𝐿 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( 𝑆 repeatS ( 𝑁𝑀 ) ) )