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 oveq2 ⊢ ( 𝑀 = 𝑁 → ( 𝑁 − 𝑀 ) = ( 𝑁 − 𝑁 ) )
41 40 oveq2d ⊢ ( 𝑀 = 𝑁 → ( 𝑆 repeatS ( 𝑁 − 𝑀 ) ) = ( 𝑆 repeatS ( 𝑁 − 𝑁 ) ) )
42 nn0cn ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ )
43 42 adantl ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℂ )
44 43 subidd ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 − 𝑁 ) = 0 )
45 44 adantl ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → ( 𝑁 − 𝑁 ) = 0 )
46 45 oveq2d ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → ( 𝑆 repeatS ( 𝑁 − 𝑁 ) ) = ( 𝑆 repeatS 0 ) )
47 repsw0 ⊢ ( 𝑆 ∈ 𝑉 → ( 𝑆 repeatS 0 ) = ∅ )
48 47 ad2antrr ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → ( 𝑆 repeatS 0 ) = ∅ )
49 46 48 eqtrd ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → ( 𝑆 repeatS ( 𝑁 − 𝑁 ) ) = ∅ )
50 41 49 sylan9eqr ⊢ ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) ∧ 𝑀 = 𝑁 ) → ( 𝑆 repeatS ( 𝑁 − 𝑀 ) ) = ∅ )
51 50 ex ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → ( 𝑀 = 𝑁 → ( 𝑆 repeatS ( 𝑁 − 𝑀 ) ) = ∅ ) )
52 51 adantl ⊢ ( ( 𝑁 ≤ 𝑀 ∧ ( ( 𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) ) → ( 𝑀 = 𝑁 → ( 𝑆 repeatS ( 𝑁 − 𝑀 ) ) = ∅ ) )
53 52 com12 ⊢ ( 𝑀 = 𝑁 → ( ( 𝑁 ≤ 𝑀 ∧ ( ( 𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) ) → ( 𝑆 repeatS ( 𝑁 − 𝑀 ) ) = ∅ ) )
54 elnn0z ⊢ ( ( 𝑁 − 𝑀 ) ∈ ℕ0 ↔ ( ( 𝑁 − 𝑀 ) ∈ ℤ ∧ 0 ≤ ( 𝑁 − 𝑀 ) ) )
55 subge0 ⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → ( 0 ≤ ( 𝑁 − 𝑀 ) ↔ 𝑀 ≤ 𝑁 ) )
56 25 24 55 syl2anr ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 0 ≤ ( 𝑁 − 𝑀 ) ↔ 𝑀 ≤ 𝑁 ) )
57 24 25 anim12i ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) )
58 letri3 ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝑀 = 𝑁 ↔ ( 𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑀 ) ) )
59 57 58 syl ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑀 = 𝑁 ↔ ( 𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑀 ) ) )
60 59 biimprd ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑀 ) → 𝑀 = 𝑁 ) )
61 60 expd ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑀 ≤ 𝑁 → ( 𝑁 ≤ 𝑀 → 𝑀 = 𝑁 ) ) )
62 56 61 sylbid ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 0 ≤ ( 𝑁 − 𝑀 ) → ( 𝑁 ≤ 𝑀 → 𝑀 = 𝑁 ) ) )
63 62 com23 ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 ≤ 𝑀 → ( 0 ≤ ( 𝑁 − 𝑀 ) → 𝑀 = 𝑁 ) ) )
64 63 adantl ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → ( 𝑁 ≤ 𝑀 → ( 0 ≤ ( 𝑁 − 𝑀 ) → 𝑀 = 𝑁 ) ) )
65 64 impcom ⊢ ( ( 𝑁 ≤ 𝑀 ∧ ( ( 𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) ) → ( 0 ≤ ( 𝑁 − 𝑀 ) → 𝑀 = 𝑁 ) )
66 65 com12 ⊢ ( 0 ≤ ( 𝑁 − 𝑀 ) → ( ( 𝑁 ≤ 𝑀 ∧ ( ( 𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) ) → 𝑀 = 𝑁 ) )
67 54 66 simplbiim ⊢ ( ( 𝑁 − 𝑀 ) ∈ ℕ0 → ( ( 𝑁 ≤ 𝑀 ∧ ( ( 𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) ) → 𝑀 = 𝑁 ) )
68 67 com12 ⊢ ( ( 𝑁 ≤ 𝑀 ∧ ( ( 𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) ) → ( ( 𝑁 − 𝑀 ) ∈ ℕ0 → 𝑀 = 𝑁 ) )
69 68 con3d ⊢ ( ( 𝑁 ≤ 𝑀 ∧ ( ( 𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) ) → ( ¬ 𝑀 = 𝑁 → ¬ ( 𝑁 − 𝑀 ) ∈ ℕ0 ) )
70 69 impcom ⊢ ( ( ¬ 𝑀 = 𝑁 ∧ ( 𝑁 ≤ 𝑀 ∧ ( ( 𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) ) ) → ¬ ( 𝑁 − 𝑀 ) ∈ ℕ0 )
71 df-nel ⊢ ( ( 𝑁 − 𝑀 ) ∉ ℕ0 ↔ ¬ ( 𝑁 − 𝑀 ) ∈ ℕ0 )
72 70 71 sylibr ⊢ ( ( ¬ 𝑀 = 𝑁 ∧ ( 𝑁 ≤ 𝑀 ∧ ( ( 𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) ) ) → ( 𝑁 − 𝑀 ) ∉ ℕ0 )
73 repsundef ⊢ ( ( 𝑁 − 𝑀 ) ∉ ℕ0 → ( 𝑆 repeatS ( 𝑁 − 𝑀 ) ) = ∅ )
74 72 73 syl ⊢ ( ( ¬ 𝑀 = 𝑁 ∧ ( 𝑁 ≤ 𝑀 ∧ ( ( 𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) ) ) → ( 𝑆 repeatS ( 𝑁 − 𝑀 ) ) = ∅ )
75 74 ex ⊢ ( ¬ 𝑀 = 𝑁 → ( ( 𝑁 ≤ 𝑀 ∧ ( ( 𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) ) → ( 𝑆 repeatS ( 𝑁 − 𝑀 ) ) = ∅ ) )
76 53 75 pm2.61i ⊢ ( ( 𝑁 ≤ 𝑀 ∧ ( ( 𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) ) → ( 𝑆 repeatS ( 𝑁 − 𝑀 ) ) = ∅ )
77 mpt0 ⊢ ( 𝑥 ∈ ∅ ↦ ( ( 𝑆 repeatS 𝐿 ) ‘ ( 𝑥 + 𝑀 ) ) ) = ∅
78 76 77 syl6reqr ⊢ ( ( 𝑁 ≤ 𝑀 ∧ ( ( 𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ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 57 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 57 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 57 3ad2ant2 ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑁 ≤ 𝐿 ) → ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) )
183 ltle ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝑀 < 𝑁 → 𝑀 ≤ 𝑁 ) )
184 182 183 syl ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑁 ≤ 𝐿 ) → ( 𝑀 < 𝑁 → 𝑀 ≤ 𝑁 ) )
185 26 3ad2ant2 ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑁 ≤ 𝐿 ) → ( 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ) )
186 185 55 syl ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑁 ≤ 𝐿 ) → ( 0 ≤ ( 𝑁 − 𝑀 ) ↔ 𝑀 ≤ 𝑁 ) )
187 184 186 sylibrd ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑁 ≤ 𝐿 ) → ( 𝑀 < 𝑁 → 0 ≤ ( 𝑁 − 𝑀 ) ) )
188 187 imp ⊢ ( ( ( ( 𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑁 ≤ 𝐿 ) ∧ 𝑀 < 𝑁 ) → 0 ≤ ( 𝑁 − 𝑀 ) )
189 181 188 54 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 ( 𝑁 − 𝑀 ) ) )