Theorem repswswrd 14734

Description: A subword of a "repeated symbol word" is again a "repeated symbol word". The assumption 𝑁 ≤ 𝐿 is required, because otherwise (𝐿 < 𝑁): ((𝑆 repeatS 𝐿) substr ⟨𝑀, 𝑁⟩) = ∅, but for M < N (𝑆 repeatS (𝑁 − 𝑀))) ≠ ∅! The proof is relatively long because the border cases (𝑀 = 𝑁, ¬ (𝑀..^𝑁) ⊆ (0..^𝐿) must have been considered. (Contributed by AV, 6-Nov-2018.)

Assertion

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

Proof of Theorem repswswrd

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		repsw 14725	. . . . . 6 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) → (𝑆 repeatS 𝐿) ∈ Word 𝑉)
2		nn0z 12583	. . . . . . 7 ⊢ (𝑀 ∈ ℕ0 → 𝑀 ∈ ℤ)
3		nn0z 12583	. . . . . . 7 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ)
4	2, 3	anim12i 614	. . . . . 6 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
5	1, 4	anim12i 614	. . . . 5 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → ((𝑆 repeatS 𝐿) ∈ Word 𝑉 ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)))
6		3anass 1096	. . . . 5 ⊢ (((𝑆 repeatS 𝐿) ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ↔ ((𝑆 repeatS 𝐿) ∈ Word 𝑉 ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)))
7	5, 6	sylibr 233	. . . 4 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → ((𝑆 repeatS 𝐿) ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
8	7	3adant3 1133	. . 3 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → ((𝑆 repeatS 𝐿) ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
9		swrdval 14593	. . 3 ⊢ (((𝑆 repeatS 𝐿) ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑆 repeatS 𝐿) substr ⟨𝑀, 𝑁⟩) = if((𝑀..^𝑁) ⊆ dom (𝑆 repeatS 𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅))
10	8, 9	syl 17	. 2 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → ((𝑆 repeatS 𝐿) substr ⟨𝑀, 𝑁⟩) = if((𝑀..^𝑁) ⊆ dom (𝑆 repeatS 𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅))
11		repsf 14723	. . . . . 6 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) → (𝑆 repeatS 𝐿):(0..^𝐿)⟶𝑉)
12	11	3ad2ant1 1134	. . . . 5 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (𝑆 repeatS 𝐿):(0..^𝐿)⟶𝑉)
13	12	fdmd 6729	. . . 4 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → dom (𝑆 repeatS 𝐿) = (0..^𝐿))
14	13	sseq2d 4015	. . 3 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → ((𝑀..^𝑁) ⊆ dom (𝑆 repeatS 𝐿) ↔ (𝑀..^𝑁) ⊆ (0..^𝐿)))
15	14	ifbid 4552	. 2 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → if((𝑀..^𝑁) ⊆ dom (𝑆 repeatS 𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅))
16		fzon 13653	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ≤ 𝑀 ↔ (𝑀..^𝑁) = ∅))
17	4, 16	syl 17	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑁 ≤ 𝑀 ↔ (𝑀..^𝑁) = ∅))
18	17	adantl 483	. . . . . . . . 9 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑁 ≤ 𝑀 ↔ (𝑀..^𝑁) = ∅))
19	18	biimpac 480	. . . . . . . 8 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (𝑀..^𝑁) = ∅)
20		0ss 4397	. . . . . . . 8 ⊢ ∅ ⊆ (0..^𝐿)
21	19, 20	eqsstrdi 4037	. . . . . . 7 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (𝑀..^𝑁) ⊆ (0..^𝐿))
22		iftrue 4535	. . . . . . 7 ⊢ ((𝑀..^𝑁) ⊆ (0..^𝐿) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))))
23	21, 22	syl 17	. . . . . 6 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))))
24		nn0re 12481	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℕ0 → 𝑀 ∈ ℝ)
25		nn0re 12481	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ)
26	24, 25	anim12ci 615	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ))
27	26	adantl 483	. . . . . . . . . 10 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ))
28		suble0 11728	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ) → ((𝑁 − 𝑀) ≤ 0 ↔ 𝑁 ≤ 𝑀))
29	27, 28	syl 17	. . . . . . . . 9 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → ((𝑁 − 𝑀) ≤ 0 ↔ 𝑁 ≤ 𝑀))
30	29	biimparc 481	. . . . . . . 8 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (𝑁 − 𝑀) ≤ 0)
31		0z 12569	. . . . . . . . 9 ⊢ 0 ∈ ℤ
32		zsubcl 12604	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑁 − 𝑀) ∈ ℤ)
33	3, 2, 32	syl2anr 598	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑁 − 𝑀) ∈ ℤ)
34	33	adantl 483	. . . . . . . . . 10 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑁 − 𝑀) ∈ ℤ)
35	34	adantl 483	. . . . . . . . 9 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (𝑁 − 𝑀) ∈ ℤ)
36		fzon 13653	. . . . . . . . 9 ⊢ ((0 ∈ ℤ ∧ (𝑁 − 𝑀) ∈ ℤ) → ((𝑁 − 𝑀) ≤ 0 ↔ (0..^(𝑁 − 𝑀)) = ∅))
37	31, 35, 36	sylancr 588	. . . . . . . 8 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → ((𝑁 − 𝑀) ≤ 0 ↔ (0..^(𝑁 − 𝑀)) = ∅))
38	30, 37	mpbid 231	. . . . . . 7 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (0..^(𝑁 − 𝑀)) = ∅)
39	38	mpteq1d 5244	. . . . . 6 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))) = (𝑥 ∈ ∅ ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))))
40		mpt0 6693	. . . . . . 7 ⊢ (𝑥 ∈ ∅ ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))) = ∅
41		oveq2 7417	. . . . . . . . . . . . 13 ⊢ (𝑀 = 𝑁 → (𝑁 − 𝑀) = (𝑁 − 𝑁))
42	41	oveq2d 7425	. . . . . . . . . . . 12 ⊢ (𝑀 = 𝑁 → (𝑆 repeatS (𝑁 − 𝑀)) = (𝑆 repeatS (𝑁 − 𝑁)))
43		nn0cn 12482	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ)
44	43	adantl 483	. . . . . . . . . . . . . . . 16 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → 𝑁 ∈ ℂ)
45	44	subidd 11559	. . . . . . . . . . . . . . 15 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑁 − 𝑁) = 0)
46	45	adantl 483	. . . . . . . . . . . . . 14 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑁 − 𝑁) = 0)
47	46	oveq2d 7425	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑆 repeatS (𝑁 − 𝑁)) = (𝑆 repeatS 0))
48		repsw0 14727	. . . . . . . . . . . . . 14 ⊢ (𝑆 ∈ 𝑉 → (𝑆 repeatS 0) = ∅)
49	48	ad2antrr 725	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑆 repeatS 0) = ∅)
50	47, 49	eqtrd 2773	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑆 repeatS (𝑁 − 𝑁)) = ∅)
51	42, 50	sylan9eqr 2795	. . . . . . . . . . 11 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑀 = 𝑁) → (𝑆 repeatS (𝑁 − 𝑀)) = ∅)
52	51	ex 414	. . . . . . . . . 10 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑀 = 𝑁 → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
53	52	adantl 483	. . . . . . . . 9 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (𝑀 = 𝑁 → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
54	53	com12 32	. . . . . . . 8 ⊢ (𝑀 = 𝑁 → ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
55		elnn0z 12571	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 − 𝑀) ∈ ℕ0 ↔ ((𝑁 − 𝑀) ∈ ℤ ∧ 0 ≤ (𝑁 − 𝑀)))
56		subge0 11727	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ) → (0 ≤ (𝑁 − 𝑀) ↔ 𝑀 ≤ 𝑁))
57	25, 24, 56	syl2anr 598	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (0 ≤ (𝑁 − 𝑀) ↔ 𝑀 ≤ 𝑁))
58	24, 25	anim12i 614	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ))
59		letri3 11299	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑀 = 𝑁 ↔ (𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑀)))
60	58, 59	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀 = 𝑁 ↔ (𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑀)))
61	60	biimprd 247	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → ((𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑀) → 𝑀 = 𝑁))
62	61	expd 417	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀 ≤ 𝑁 → (𝑁 ≤ 𝑀 → 𝑀 = 𝑁)))
63	57, 62	sylbid 239	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (0 ≤ (𝑁 − 𝑀) → (𝑁 ≤ 𝑀 → 𝑀 = 𝑁)))
64	63	com23 86	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑁 ≤ 𝑀 → (0 ≤ (𝑁 − 𝑀) → 𝑀 = 𝑁)))
65	64	adantl 483	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑁 ≤ 𝑀 → (0 ≤ (𝑁 − 𝑀) → 𝑀 = 𝑁)))
66	65	impcom 409	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (0 ≤ (𝑁 − 𝑀) → 𝑀 = 𝑁))
67	66	com12 32	. . . . . . . . . . . . . . 15 ⊢ (0 ≤ (𝑁 − 𝑀) → ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → 𝑀 = 𝑁))
68	55, 67	simplbiim 506	. . . . . . . . . . . . . 14 ⊢ ((𝑁 − 𝑀) ∈ ℕ0 → ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → 𝑀 = 𝑁))
69	68	com12 32	. . . . . . . . . . . . 13 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → ((𝑁 − 𝑀) ∈ ℕ0 → 𝑀 = 𝑁))
70	69	con3d 152	. . . . . . . . . . . 12 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (¬ 𝑀 = 𝑁 → ¬ (𝑁 − 𝑀) ∈ ℕ0))
71	70	impcom 409	. . . . . . . . . . 11 ⊢ ((¬ 𝑀 = 𝑁 ∧ (𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)))) → ¬ (𝑁 − 𝑀) ∈ ℕ0)
72		df-nel 3048	. . . . . . . . . . 11 ⊢ ((𝑁 − 𝑀) ∉ ℕ0 ↔ ¬ (𝑁 − 𝑀) ∈ ℕ0)
73	71, 72	sylibr 233	. . . . . . . . . 10 ⊢ ((¬ 𝑀 = 𝑁 ∧ (𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)))) → (𝑁 − 𝑀) ∉ ℕ0)
74		repsundef 14721	. . . . . . . . . 10 ⊢ ((𝑁 − 𝑀) ∉ ℕ0 → (𝑆 repeatS (𝑁 − 𝑀)) = ∅)
75	73, 74	syl 17	. . . . . . . . 9 ⊢ ((¬ 𝑀 = 𝑁 ∧ (𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)))) → (𝑆 repeatS (𝑁 − 𝑀)) = ∅)
76	75	ex 414	. . . . . . . 8 ⊢ (¬ 𝑀 = 𝑁 → ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
77	54, 76	pm2.61i 182	. . . . . . 7 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (𝑆 repeatS (𝑁 − 𝑀)) = ∅)
78	40, 77	eqtr4id 2792	. . . . . 6 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (𝑥 ∈ ∅ ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))) = (𝑆 repeatS (𝑁 − 𝑀)))
79	23, 39, 78	3eqtrd 2777	. . . . 5 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁 − 𝑀)))
80	79	expcom 415	. . . 4 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑁 ≤ 𝑀 → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁 − 𝑀))))
81	80	3adant3 1133	. . 3 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (𝑁 ≤ 𝑀 → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁 − 𝑀))))
82		ltnle 11293	. . . . . . 7 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑀 < 𝑁 ↔ ¬ 𝑁 ≤ 𝑀))
83	58, 82	syl 17	. . . . . 6 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀 < 𝑁 ↔ ¬ 𝑁 ≤ 𝑀))
84	83	bicomd 222	. . . . 5 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (¬ 𝑁 ≤ 𝑀 ↔ 𝑀 < 𝑁))
85	84	3ad2ant2 1135	. . . 4 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (¬ 𝑁 ≤ 𝑀 ↔ 𝑀 < 𝑁))
86	22	adantr 482	. . . . . . 7 ⊢ (((𝑀..^𝑁) ⊆ (0..^𝐿) ∧ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁)) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))))
87	4	3ad2ant2 1135	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
88	87	adantr 482	. . . . . . . . . 10 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
89		0zd 12570	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ 𝑉 → 0 ∈ ℤ)
90		nn0z 12583	. . . . . . . . . . . . 13 ⊢ (𝐿 ∈ ℕ0 → 𝐿 ∈ ℤ)
91	89, 90	anim12i 614	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) → (0 ∈ ℤ ∧ 𝐿 ∈ ℤ))
92	91	3ad2ant1 1134	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (0 ∈ ℤ ∧ 𝐿 ∈ ℤ))
93	92	adantr 482	. . . . . . . . . 10 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (0 ∈ ℤ ∧ 𝐿 ∈ ℤ))
94		simpr 486	. . . . . . . . . 10 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → 𝑀 < 𝑁)
95		ssfzo12bi 13727	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ 𝑀 < 𝑁) → ((𝑀..^𝑁) ⊆ (0..^𝐿) ↔ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)))
96	88, 93, 94, 95	syl3anc 1372	. . . . . . . . 9 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → ((𝑀..^𝑁) ⊆ (0..^𝐿) ↔ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)))
97		simpl1l 1225	. . . . . . . . . . . . . 14 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → 𝑆 ∈ 𝑉)
98	97	ad2antrr 725	. . . . . . . . . . . . 13 ⊢ ((((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → 𝑆 ∈ 𝑉)
99		simpl1r 1226	. . . . . . . . . . . . . 14 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → 𝐿 ∈ ℕ0)
100	99	ad2antrr 725	. . . . . . . . . . . . 13 ⊢ ((((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → 𝐿 ∈ ℕ0)
101		nn0addcl 12507	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0) → (𝑥 + 𝑀) ∈ ℕ0)
102	101	expcom 415	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑀 ∈ ℕ0 → (𝑥 ∈ ℕ0 → (𝑥 + 𝑀) ∈ ℕ0))
103	102	adantr 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑥 ∈ ℕ0 → (𝑥 + 𝑀) ∈ ℕ0))
104	103	3ad2ant2 1135	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (𝑥 ∈ ℕ0 → (𝑥 + 𝑀) ∈ ℕ0))
105	104	ad2antrr 725	. . . . . . . . . . . . . . 15 ⊢ (((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) → (𝑥 ∈ ℕ0 → (𝑥 + 𝑀) ∈ ℕ0))
106		elfzonn0 13677	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (0..^(𝑁 − 𝑀)) → 𝑥 ∈ ℕ0)
107	105, 106	impel 507	. . . . . . . . . . . . . 14 ⊢ ((((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → (𝑥 + 𝑀) ∈ ℕ0)
108	90	adantl 483	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) → 𝐿 ∈ ℤ)
109	108	3ad2ant1 1134	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → 𝐿 ∈ ℤ)
110	109	adantr 482	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → 𝐿 ∈ ℤ)
111		nn0re 12481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐿 ∈ ℕ0 → 𝐿 ∈ ℝ)
112	111	adantl 483	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) → 𝐿 ∈ ℝ)
113	112, 58	anim12ci 615	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝐿 ∈ ℝ))
114		df-3an 1090	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ) ↔ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝐿 ∈ ℝ))
115	113, 114	sylibr 233	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ))
116		ltletr 11306	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ) → ((𝑀 < 𝑁 ∧ 𝑁 ≤ 𝐿) → 𝑀 < 𝐿))
117	115, 116	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → ((𝑀 < 𝑁 ∧ 𝑁 ≤ 𝐿) → 𝑀 < 𝐿))
118		elnn0z 12571	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑀 ∈ ℕ0 ↔ (𝑀 ∈ ℤ ∧ 0 ≤ 𝑀))
119		0red 11217	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑀 ∈ ℤ ∧ (𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0)) → 0 ∈ ℝ)
120		zre 12562	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℝ)
121	120	adantr 482	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑀 ∈ ℤ ∧ (𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0)) → 𝑀 ∈ ℝ)
122	112	adantl 483	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑀 ∈ ℤ ∧ (𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0)) → 𝐿 ∈ ℝ)
123		lelttr 11304	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((0 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝐿 ∈ ℝ) → ((0 ≤ 𝑀 ∧ 𝑀 < 𝐿) → 0 < 𝐿))
124	119, 121, 122, 123	syl3anc 1372	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑀 ∈ ℤ ∧ (𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0)) → ((0 ≤ 𝑀 ∧ 𝑀 < 𝐿) → 0 < 𝐿))
125	124	expd 417	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑀 ∈ ℤ ∧ (𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0)) → (0 ≤ 𝑀 → (𝑀 < 𝐿 → 0 < 𝐿)))
126	125	impancom 453	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑀 ∈ ℤ ∧ 0 ≤ 𝑀) → ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) → (𝑀 < 𝐿 → 0 < 𝐿)))
127	118, 126	sylbi 216	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑀 ∈ ℕ0 → ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) → (𝑀 < 𝐿 → 0 < 𝐿)))
128	127	adantr 482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) → (𝑀 < 𝐿 → 0 < 𝐿)))
129	128	impcom 409	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑀 < 𝐿 → 0 < 𝐿))
130	117, 129	syld 47	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → ((𝑀 < 𝑁 ∧ 𝑁 ≤ 𝐿) → 0 < 𝐿))
131	130	expcomd 418	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑁 ≤ 𝐿 → (𝑀 < 𝑁 → 0 < 𝐿)))
132	131	3impia 1118	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (𝑀 < 𝑁 → 0 < 𝐿))
133	132	imp 408	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → 0 < 𝐿)
134		elnnz 12568	. . . . . . . . . . . . . . . 16 ⊢ (𝐿 ∈ ℕ ↔ (𝐿 ∈ ℤ ∧ 0 < 𝐿))
135	110, 133, 134	sylanbrc 584	. . . . . . . . . . . . . . 15 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → 𝐿 ∈ ℕ)
136	135	ad2antrr 725	. . . . . . . . . . . . . 14 ⊢ ((((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → 𝐿 ∈ ℕ)
137		elfzo0 13673	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↔ (𝑥 ∈ ℕ0 ∧ (𝑁 − 𝑀) ∈ ℕ ∧ 𝑥 < (𝑁 − 𝑀)))
138		nn0readdcl 12538	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑥 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0) → (𝑥 + 𝑀) ∈ ℝ)
139	138	expcom 415	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑀 ∈ ℕ0 → (𝑥 ∈ ℕ0 → (𝑥 + 𝑀) ∈ ℝ))
140	139	ad2antrl 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑥 ∈ ℕ0 → (𝑥 + 𝑀) ∈ ℝ))
141	140	impcom 409	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (𝑥 + 𝑀) ∈ ℝ)
142	25	adantl 483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → 𝑁 ∈ ℝ)
143	142	adantl 483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → 𝑁 ∈ ℝ)
144	143	adantl 483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → 𝑁 ∈ ℝ)
145	111	ad2antrl 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → 𝐿 ∈ ℝ)
146	141, 144, 145	3jca 1129	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → ((𝑥 + 𝑀) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ))
147	146	ex 414	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 ∈ ℕ0 → ((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → ((𝑥 + 𝑀) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ)))
148	147	adantr 482	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀)) → ((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → ((𝑥 + 𝑀) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ)))
149	148	impcom 409	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) ∧ (𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀))) → ((𝑥 + 𝑀) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ))
150	149	adantr 482	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) ∧ (𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀))) ∧ 𝑁 ≤ 𝐿) → ((𝑥 + 𝑀) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ))
151		nn0re 12481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑥 ∈ ℕ0 → 𝑥 ∈ ℝ)
152	151	adantr 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → 𝑥 ∈ ℝ)
153	24	ad2antrl 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → 𝑀 ∈ ℝ)
154	153	adantl 483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → 𝑀 ∈ ℝ)
155	152, 154, 144	ltaddsubd 11814	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → ((𝑥 + 𝑀) < 𝑁 ↔ 𝑥 < (𝑁 − 𝑀)))
156		idd 24	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) ∧ 𝑁 ≤ 𝐿) → ((𝑥 + 𝑀) < 𝑁 → (𝑥 + 𝑀) < 𝑁))
157	156	ex 414	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (𝑁 ≤ 𝐿 → ((𝑥 + 𝑀) < 𝑁 → (𝑥 + 𝑀) < 𝑁)))
158	157	com23 86	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → ((𝑥 + 𝑀) < 𝑁 → (𝑁 ≤ 𝐿 → (𝑥 + 𝑀) < 𝑁)))
159	155, 158	sylbird 260	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (𝑥 < (𝑁 − 𝑀) → (𝑁 ≤ 𝐿 → (𝑥 + 𝑀) < 𝑁)))
160	159	impancom 453	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀)) → ((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑁 ≤ 𝐿 → (𝑥 + 𝑀) < 𝑁)))
161	160	impcom 409	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) ∧ (𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀))) → (𝑁 ≤ 𝐿 → (𝑥 + 𝑀) < 𝑁))
162	161	impac 554	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) ∧ (𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀))) ∧ 𝑁 ≤ 𝐿) → ((𝑥 + 𝑀) < 𝑁 ∧ 𝑁 ≤ 𝐿))
163		ltletr 11306	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑥 + 𝑀) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ) → (((𝑥 + 𝑀) < 𝑁 ∧ 𝑁 ≤ 𝐿) → (𝑥 + 𝑀) < 𝐿))
164	150, 162, 163	sylc 65	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) ∧ (𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀))) ∧ 𝑁 ≤ 𝐿) → (𝑥 + 𝑀) < 𝐿)
165	164	exp31 421	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → ((𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀)) → (𝑁 ≤ 𝐿 → (𝑥 + 𝑀) < 𝐿)))
166	165	com23 86	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑁 ≤ 𝐿 → ((𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀)) → (𝑥 + 𝑀) < 𝐿)))
167	166	ex 414	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐿 ∈ ℕ0 → ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑁 ≤ 𝐿 → ((𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀)) → (𝑥 + 𝑀) < 𝐿))))
168	167	adantl 483	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) → ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑁 ≤ 𝐿 → ((𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀)) → (𝑥 + 𝑀) < 𝐿))))
169	168	3imp 1112	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → ((𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀)) → (𝑥 + 𝑀) < 𝐿))
170	169	ad2antrr 725	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) → ((𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀)) → (𝑥 + 𝑀) < 𝐿))
171	170	com12 32	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀)) → (((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) → (𝑥 + 𝑀) < 𝐿))
172	171	3adant2 1132	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℕ0 ∧ (𝑁 − 𝑀) ∈ ℕ ∧ 𝑥 < (𝑁 − 𝑀)) → (((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) → (𝑥 + 𝑀) < 𝐿))
173	137, 172	sylbi 216	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (0..^(𝑁 − 𝑀)) → (((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) → (𝑥 + 𝑀) < 𝐿))
174	173	impcom 409	. . . . . . . . . . . . . 14 ⊢ ((((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → (𝑥 + 𝑀) < 𝐿)
175		elfzo0 13673	. . . . . . . . . . . . . 14 ⊢ ((𝑥 + 𝑀) ∈ (0..^𝐿) ↔ ((𝑥 + 𝑀) ∈ ℕ0 ∧ 𝐿 ∈ ℕ ∧ (𝑥 + 𝑀) < 𝐿))
176	107, 136, 174, 175	syl3anbrc 1344	. . . . . . . . . . . . 13 ⊢ ((((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → (𝑥 + 𝑀) ∈ (0..^𝐿))
177		repswsymb 14724	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0 ∧ (𝑥 + 𝑀) ∈ (0..^𝐿)) → ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀)) = 𝑆)
178	98, 100, 176, 177	syl3anc 1372	. . . . . . . . . . . 12 ⊢ ((((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀)) = 𝑆)
179	178	mpteq2dva 5249	. . . . . . . . . . 11 ⊢ (((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) → (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))) = (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ 𝑆))
180	33	3ad2ant2 1135	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (𝑁 − 𝑀) ∈ ℤ)
181	180	adantr 482	. . . . . . . . . . . . . . 15 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (𝑁 − 𝑀) ∈ ℤ)
182	58	3ad2ant2 1135	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ))
183		ltle 11302	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑀 < 𝑁 → 𝑀 ≤ 𝑁))
184	182, 183	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (𝑀 < 𝑁 → 𝑀 ≤ 𝑁))
185	26	3ad2ant2 1135	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ))
186	185, 56	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (0 ≤ (𝑁 − 𝑀) ↔ 𝑀 ≤ 𝑁))
187	184, 186	sylibrd 259	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (𝑀 < 𝑁 → 0 ≤ (𝑁 − 𝑀)))
188	187	imp 408	. . . . . . . . . . . . . . 15 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → 0 ≤ (𝑁 − 𝑀))
189	181, 188, 55	sylanbrc 584	. . . . . . . . . . . . . 14 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (𝑁 − 𝑀) ∈ ℕ0)
190	97, 189	jca 513	. . . . . . . . . . . . 13 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (𝑆 ∈ 𝑉 ∧ (𝑁 − 𝑀) ∈ ℕ0))
191	190	adantr 482	. . . . . . . . . . . 12 ⊢ (((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) → (𝑆 ∈ 𝑉 ∧ (𝑁 − 𝑀) ∈ ℕ0))
192		reps 14720	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ 𝑉 ∧ (𝑁 − 𝑀) ∈ ℕ0) → (𝑆 repeatS (𝑁 − 𝑀)) = (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ 𝑆))
193	192	eqcomd 2739	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ 𝑉 ∧ (𝑁 − 𝑀) ∈ ℕ0) → (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ 𝑆) = (𝑆 repeatS (𝑁 − 𝑀)))
194	191, 193	syl 17	. . . . . . . . . . 11 ⊢ (((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) → (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ 𝑆) = (𝑆 repeatS (𝑁 − 𝑀)))
195	179, 194	eqtrd 2773	. . . . . . . . . 10 ⊢ (((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) → (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))) = (𝑆 repeatS (𝑁 − 𝑀)))
196	195	ex 414	. . . . . . . . 9 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → ((0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿) → (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))) = (𝑆 repeatS (𝑁 − 𝑀))))
197	96, 196	sylbid 239	. . . . . . . 8 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → ((𝑀..^𝑁) ⊆ (0..^𝐿) → (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))) = (𝑆 repeatS (𝑁 − 𝑀))))
198	197	impcom 409	. . . . . . 7 ⊢ (((𝑀..^𝑁) ⊆ (0..^𝐿) ∧ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁)) → (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))) = (𝑆 repeatS (𝑁 − 𝑀)))
199	86, 198	eqtrd 2773	. . . . . 6 ⊢ (((𝑀..^𝑁) ⊆ (0..^𝐿) ∧ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁)) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁 − 𝑀)))
200		iffalse 4538	. . . . . . . 8 ⊢ (¬ (𝑀..^𝑁) ⊆ (0..^𝐿) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = ∅)
201	200	adantr 482	. . . . . . 7 ⊢ ((¬ (𝑀..^𝑁) ⊆ (0..^𝐿) ∧ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁)) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = ∅)
202	96	notbid 318	. . . . . . . . 9 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (¬ (𝑀..^𝑁) ⊆ (0..^𝐿) ↔ ¬ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)))
203		ianor 981	. . . . . . . . . . 11 ⊢ (¬ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿) ↔ (¬ 0 ≤ 𝑀 ∨ ¬ 𝑁 ≤ 𝐿))
204		nn0ge0 12497	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 ∈ ℕ0 → 0 ≤ 𝑀)
205		pm2.24 124	. . . . . . . . . . . . . . . . 17 ⊢ (0 ≤ 𝑀 → (¬ 0 ≤ 𝑀 → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
206	204, 205	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑀 ∈ ℕ0 → (¬ 0 ≤ 𝑀 → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
207	206	adantr 482	. . . . . . . . . . . . . . 15 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (¬ 0 ≤ 𝑀 → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
208	207	3ad2ant2 1135	. . . . . . . . . . . . . 14 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (¬ 0 ≤ 𝑀 → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
209	208	adantr 482	. . . . . . . . . . . . 13 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (¬ 0 ≤ 𝑀 → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
210	209	com12 32	. . . . . . . . . . . 12 ⊢ (¬ 0 ≤ 𝑀 → ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
211		pm2.24 124	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ≤ 𝐿 → (¬ 𝑁 ≤ 𝐿 → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
212	211	3ad2ant3 1136	. . . . . . . . . . . . . 14 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (¬ 𝑁 ≤ 𝐿 → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
213	212	adantr 482	. . . . . . . . . . . . 13 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (¬ 𝑁 ≤ 𝐿 → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
214	213	com12 32	. . . . . . . . . . . 12 ⊢ (¬ 𝑁 ≤ 𝐿 → ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
215	210, 214	jaoi 856	. . . . . . . . . . 11 ⊢ ((¬ 0 ≤ 𝑀 ∨ ¬ 𝑁 ≤ 𝐿) → ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
216	203, 215	sylbi 216	. . . . . . . . . 10 ⊢ (¬ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿) → ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
217	216	com12 32	. . . . . . . . 9 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (¬ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿) → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
218	202, 217	sylbid 239	. . . . . . . 8 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (¬ (𝑀..^𝑁) ⊆ (0..^𝐿) → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
219	218	impcom 409	. . . . . . 7 ⊢ ((¬ (𝑀..^𝑁) ⊆ (0..^𝐿) ∧ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁)) → (𝑆 repeatS (𝑁 − 𝑀)) = ∅)
220	201, 219	eqtr4d 2776	. . . . . 6 ⊢ ((¬ (𝑀..^𝑁) ⊆ (0..^𝐿) ∧ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁)) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁 − 𝑀)))
221	199, 220	pm2.61ian 811	. . . . 5 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁 − 𝑀)))
222	221	ex 414	. . . 4 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (𝑀 < 𝑁 → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁 − 𝑀))))
223	85, 222	sylbid 239	. . 3 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (¬ 𝑁 ≤ 𝑀 → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁 − 𝑀))))
224	81, 223	pm2.61d 179	. 2 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁 − 𝑀)))
225	10, 15, 224	3eqtrd 2777	1 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → ((𝑆 repeatS 𝐿) substr ⟨𝑀, 𝑁⟩) = (𝑆 repeatS (𝑁 − 𝑀)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 397   ∨ wo 846   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107   ∉ wnel 3047   ⊆ wss 3949  ∅c0 4323  ifcif 4529  ⟨cop 4635   class class class wbr 5149   ↦ cmpt 5232  dom cdm 5677  ⟶wf 6540  ‘cfv 6544  (class class class)co 7409  ℂcc 11108  ℝcr 11109  0cc0 11110   + caddc 11113   < clt 11248   ≤ cle 11249   − cmin 11444  ℕcn 12212  ℕ₀cn0 12472  ℤcz 12558  ..^cfzo 13627  Word cword 14464   substr csubstr 14590   repeatS creps 14718

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-1st 7975  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466  df-er 8703  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-card 9934  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447  df-nn 12213  df-n0 12473  df-z 12559  df-uz 12823  df-fz 13485  df-fzo 13628  df-hash 14291  df-word 14465  df-substr 14591  df-reps 14719

This theorem is referenced by:  repswcshw  14762