Theorem repswswrd 14799

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 14790	. . . . . 6 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) → (𝑆 repeatS 𝐿) ∈ Word 𝑉)
2		nn0z 12594	. . . . . . 7 ⊢ (𝑀 ∈ ℕ0 → 𝑀 ∈ ℤ)
3		nn0z 12594	. . . . . . 7 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ)
4	2, 3	anim12i 622	. . . . . 6 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
5	1, 4	anim12i 622	. . . . 5 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → ((𝑆 repeatS 𝐿) ∈ Word 𝑉 ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)))
6		3anass 1107	. . . . 5 ⊢ (((𝑆 repeatS 𝐿) ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ↔ ((𝑆 repeatS 𝐿) ∈ Word 𝑉 ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)))
7	5, 6	sylibr 236	. . . 4 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → ((𝑆 repeatS 𝐿) ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
8	7	3adant3 1146	. . 3 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → ((𝑆 repeatS 𝐿) ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
9		swrdval 14659	. . 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 14788	. . . . . 6 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) → (𝑆 repeatS 𝐿):(0..^𝐿)⟶𝑉)
12	11	3ad2ant1 1147	. . . . 5 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (𝑆 repeatS 𝐿):(0..^𝐿)⟶𝑉)
13	12	fdmd 6704	. . . 4 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → dom (𝑆 repeatS 𝐿) = (0..^𝐿))
14	13	sseq2d 3970	. . 3 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → ((𝑀..^𝑁) ⊆ dom (𝑆 repeatS 𝐿) ↔ (𝑀..^𝑁) ⊆ (0..^𝐿)))
15	14	ifbid 4506	. 2 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → if((𝑀..^𝑁) ⊆ dom (𝑆 repeatS 𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅))
16		fzon 13688	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ≤ 𝑀 ↔ (𝑀..^𝑁) = ∅))
17	4, 16	syl 17	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑁 ≤ 𝑀 ↔ (𝑀..^𝑁) = ∅))
18	17	adantl 485	. . . . . . . . 9 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑁 ≤ 𝑀 ↔ (𝑀..^𝑁) = ∅))
19	18	biimpac 482	. . . . . . . 8 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (𝑀..^𝑁) = ∅)
20		0ss 4356	. . . . . . . 8 ⊢ ∅ ⊆ (0..^𝐿)
21	19, 20	eqsstrdi 3982	. . . . . . 7 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (𝑀..^𝑁) ⊆ (0..^𝐿))
22		iftrue 4488	. . . . . . 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 12492	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℕ0 → 𝑀 ∈ ℝ)
25		nn0re 12492	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ)
26	24, 25	anim12ci 623	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ))
27	26	adantl 485	. . . . . . . . . 10 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ))
28		suble0 11703	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ) → ((𝑁 − 𝑀) ≤ 0 ↔ 𝑁 ≤ 𝑀))
29	27, 28	syl 17	. . . . . . . . 9 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → ((𝑁 − 𝑀) ≤ 0 ↔ 𝑁 ≤ 𝑀))
30	29	biimparc 483	. . . . . . . 8 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (𝑁 − 𝑀) ≤ 0)
31		0z 12581	. . . . . . . . 9 ⊢ 0 ∈ ℤ
32		zsubcl 12615	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑁 − 𝑀) ∈ ℤ)
33	3, 2, 32	syl2anr 606	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑁 − 𝑀) ∈ ℤ)
34	33	adantl 485	. . . . . . . . . 10 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑁 − 𝑀) ∈ ℤ)
35	34	adantl 485	. . . . . . . . 9 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (𝑁 − 𝑀) ∈ ℤ)
36		fzon 13688	. . . . . . . . 9 ⊢ ((0 ∈ ℤ ∧ (𝑁 − 𝑀) ∈ ℤ) → ((𝑁 − 𝑀) ≤ 0 ↔ (0..^(𝑁 − 𝑀)) = ∅))
37	31, 35, 36	sylancr 596	. . . . . . . 8 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → ((𝑁 − 𝑀) ≤ 0 ↔ (0..^(𝑁 − 𝑀)) = ∅))
38	30, 37	mpbid 234	. . . . . . 7 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (0..^(𝑁 − 𝑀)) = ∅)
39	38	mpteq1d 5192	. . . . . 6 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))) = (𝑥 ∈ ∅ ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))))
40		mpt0 6665	. . . . . . 7 ⊢ (𝑥 ∈ ∅ ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))) = ∅
41		oveq2 7406	. . . . . . . . . . . . 13 ⊢ (𝑀 = 𝑁 → (𝑁 − 𝑀) = (𝑁 − 𝑁))
42	41	oveq2d 7414	. . . . . . . . . . . 12 ⊢ (𝑀 = 𝑁 → (𝑆 repeatS (𝑁 − 𝑀)) = (𝑆 repeatS (𝑁 − 𝑁)))
43		nn0cn 12493	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ)
44	43	adantl 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → 𝑁 ∈ ℂ)
45	44	subidd 11532	. . . . . . . . . . . . . . 15 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑁 − 𝑁) = 0)
46	45	adantl 485	. . . . . . . . . . . . . 14 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑁 − 𝑁) = 0)
47	46	oveq2d 7414	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑆 repeatS (𝑁 − 𝑁)) = (𝑆 repeatS 0))
48		repsw0 14792	. . . . . . . . . . . . . 14 ⊢ (𝑆 ∈ 𝑉 → (𝑆 repeatS 0) = ∅)
49	48	ad2antrr 736	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑆 repeatS 0) = ∅)
50	47, 49	eqtrd 2799	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑆 repeatS (𝑁 − 𝑁)) = ∅)
51	42, 50	sylan9eqr 2821	. . . . . . . . . . 11 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑀 = 𝑁) → (𝑆 repeatS (𝑁 − 𝑀)) = ∅)
52	51	ex 416	. . . . . . . . . 10 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑀 = 𝑁 → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
53	52	adantl 485	. . . . . . . . 9 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (𝑀 = 𝑁 → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
54	53	com12 32	. . . . . . . 8 ⊢ (𝑀 = 𝑁 → ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
55		elnn0z 12583	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 − 𝑀) ∈ ℕ0 ↔ ((𝑁 − 𝑀) ∈ ℤ ∧ 0 ≤ (𝑁 − 𝑀)))
56		subge0 11702	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ) → (0 ≤ (𝑁 − 𝑀) ↔ 𝑀 ≤ 𝑁))
57	25, 24, 56	syl2anr 606	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (0 ≤ (𝑁 − 𝑀) ↔ 𝑀 ≤ 𝑁))
58	24, 25	anim12i 622	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ))
59		letri3 11270	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑀 = 𝑁 ↔ (𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑀)))
60	58, 59	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀 = 𝑁 ↔ (𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑀)))
61	60	biimprd 250	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → ((𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑀) → 𝑀 = 𝑁))
62	61	expd 419	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀 ≤ 𝑁 → (𝑁 ≤ 𝑀 → 𝑀 = 𝑁)))
63	57, 62	sylbid 242	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (0 ≤ (𝑁 − 𝑀) → (𝑁 ≤ 𝑀 → 𝑀 = 𝑁)))
64	63	com23 86	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑁 ≤ 𝑀 → (0 ≤ (𝑁 − 𝑀) → 𝑀 = 𝑁)))
65	64	adantl 485	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑁 ≤ 𝑀 → (0 ≤ (𝑁 − 𝑀) → 𝑀 = 𝑁)))
66	65	impcom 411	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (0 ≤ (𝑁 − 𝑀) → 𝑀 = 𝑁))
67	66	com12 32	. . . . . . . . . . . . . . 15 ⊢ (0 ≤ (𝑁 − 𝑀) → ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → 𝑀 = 𝑁))
68	55, 67	simplbiim 512	. . . . . . . . . . . . . 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 411	. . . . . . . . . . 11 ⊢ ((¬ 𝑀 = 𝑁 ∧ (𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)))) → ¬ (𝑁 − 𝑀) ∈ ℕ0)
72		df-nel 3064	. . . . . . . . . . 11 ⊢ ((𝑁 − 𝑀) ∉ ℕ0 ↔ ¬ (𝑁 − 𝑀) ∈ ℕ0)
73	71, 72	sylibr 236	. . . . . . . . . 10 ⊢ ((¬ 𝑀 = 𝑁 ∧ (𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)))) → (𝑁 − 𝑀) ∉ ℕ0)
74		repsundef 14786	. . . . . . . . . 10 ⊢ ((𝑁 − 𝑀) ∉ ℕ0 → (𝑆 repeatS (𝑁 − 𝑀)) = ∅)
75	73, 74	syl 17	. . . . . . . . 9 ⊢ ((¬ 𝑀 = 𝑁 ∧ (𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)))) → (𝑆 repeatS (𝑁 − 𝑀)) = ∅)
76	75	ex 416	. . . . . . . 8 ⊢ (¬ 𝑀 = 𝑁 → ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
77	54, 76	pm2.61i 183	. . . . . . 7 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (𝑆 repeatS (𝑁 − 𝑀)) = ∅)
78	40, 77	eqtr4id 2818	. . . . . 6 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (𝑥 ∈ ∅ ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))) = (𝑆 repeatS (𝑁 − 𝑀)))
79	23, 39, 78	3eqtrd 2803	. . . . 5 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁 − 𝑀)))
80	79	expcom 417	. . . 4 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑁 ≤ 𝑀 → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁 − 𝑀))))
81	80	3adant3 1146	. . 3 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (𝑁 ≤ 𝑀 → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁 − 𝑀))))
82		ltnle 11264	. . . . . . 7 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑀 < 𝑁 ↔ ¬ 𝑁 ≤ 𝑀))
83	58, 82	syl 17	. . . . . 6 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀 < 𝑁 ↔ ¬ 𝑁 ≤ 𝑀))
84	83	bicomd 225	. . . . 5 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (¬ 𝑁 ≤ 𝑀 ↔ 𝑀 < 𝑁))
85	84	3ad2ant2 1148	. . . 4 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (¬ 𝑁 ≤ 𝑀 ↔ 𝑀 < 𝑁))
86	22	adantr 484	. . . . . . 7 ⊢ (((𝑀..^𝑁) ⊆ (0..^𝐿) ∧ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁)) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))))
87	4	3ad2ant2 1148	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
88	87	adantr 484	. . . . . . . . . 10 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
89		0zd 12582	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ 𝑉 → 0 ∈ ℤ)
90		nn0z 12594	. . . . . . . . . . . . 13 ⊢ (𝐿 ∈ ℕ0 → 𝐿 ∈ ℤ)
91	89, 90	anim12i 622	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) → (0 ∈ ℤ ∧ 𝐿 ∈ ℤ))
92	91	3ad2ant1 1147	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (0 ∈ ℤ ∧ 𝐿 ∈ ℤ))
93	92	adantr 484	. . . . . . . . . 10 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (0 ∈ ℤ ∧ 𝐿 ∈ ℤ))
94		simpr 488	. . . . . . . . . 10 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → 𝑀 < 𝑁)
95		ssfzo12bi 13769	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ 𝑀 < 𝑁) → ((𝑀..^𝑁) ⊆ (0..^𝐿) ↔ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)))
96	88, 93, 94, 95	syl3anc 1392	. . . . . . . . 9 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → ((𝑀..^𝑁) ⊆ (0..^𝐿) ↔ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)))
97		simpl1l 1239	. . . . . . . . . . . . . 14 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → 𝑆 ∈ 𝑉)
98	97	ad2antrr 736	. . . . . . . . . . . . 13 ⊢ ((((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → 𝑆 ∈ 𝑉)
99		simpl1r 1240	. . . . . . . . . . . . . 14 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → 𝐿 ∈ ℕ0)
100	99	ad2antrr 736	. . . . . . . . . . . . 13 ⊢ ((((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → 𝐿 ∈ ℕ0)
101		nn0addcl 12518	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0) → (𝑥 + 𝑀) ∈ ℕ0)
102	101	expcom 417	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑀 ∈ ℕ0 → (𝑥 ∈ ℕ0 → (𝑥 + 𝑀) ∈ ℕ0))
103	102	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑥 ∈ ℕ0 → (𝑥 + 𝑀) ∈ ℕ0))
104	103	3ad2ant2 1148	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (𝑥 ∈ ℕ0 → (𝑥 + 𝑀) ∈ ℕ0))
105	104	ad2antrr 736	. . . . . . . . . . . . . . 15 ⊢ (((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) → (𝑥 ∈ ℕ0 → (𝑥 + 𝑀) ∈ ℕ0))
106		elfzonn0 13715	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (0..^(𝑁 − 𝑀)) → 𝑥 ∈ ℕ0)
107	105, 106	impel 513	. . . . . . . . . . . . . 14 ⊢ ((((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → (𝑥 + 𝑀) ∈ ℕ0)
108	90	adantl 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) → 𝐿 ∈ ℤ)
109	108	3ad2ant1 1147	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → 𝐿 ∈ ℤ)
110	109	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → 𝐿 ∈ ℤ)
111		nn0re 12492	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐿 ∈ ℕ0 → 𝐿 ∈ ℝ)
112	111	adantl 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) → 𝐿 ∈ ℝ)
113	112, 58	anim12ci 623	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝐿 ∈ ℝ))
114		df-3an 1101	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ) ↔ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝐿 ∈ ℝ))
115	113, 114	sylibr 236	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ))
116		ltletr 11277	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ) → ((𝑀 < 𝑁 ∧ 𝑁 ≤ 𝐿) → 𝑀 < 𝐿))
117	115, 116	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → ((𝑀 < 𝑁 ∧ 𝑁 ≤ 𝐿) → 𝑀 < 𝐿))
118		elnn0z 12583	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑀 ∈ ℕ0 ↔ (𝑀 ∈ ℤ ∧ 0 ≤ 𝑀))
119		0red 11186	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑀 ∈ ℤ ∧ (𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0)) → 0 ∈ ℝ)
120		zre 12574	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℝ)
121	120	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑀 ∈ ℤ ∧ (𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0)) → 𝑀 ∈ ℝ)
122	112	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑀 ∈ ℤ ∧ (𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0)) → 𝐿 ∈ ℝ)
123		lelttr 11275	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((0 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝐿 ∈ ℝ) → ((0 ≤ 𝑀 ∧ 𝑀 < 𝐿) → 0 < 𝐿))
124	119, 121, 122, 123	syl3anc 1392	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑀 ∈ ℤ ∧ (𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0)) → ((0 ≤ 𝑀 ∧ 𝑀 < 𝐿) → 0 < 𝐿))
125	124	expd 419	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑀 ∈ ℤ ∧ (𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0)) → (0 ≤ 𝑀 → (𝑀 < 𝐿 → 0 < 𝐿)))
126	125	impancom 455	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑀 ∈ ℤ ∧ 0 ≤ 𝑀) → ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) → (𝑀 < 𝐿 → 0 < 𝐿)))
127	118, 126	sylbi 219	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑀 ∈ ℕ0 → ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) → (𝑀 < 𝐿 → 0 < 𝐿)))
128	127	adantr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) → (𝑀 < 𝐿 → 0 < 𝐿)))
129	128	impcom 411	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑀 < 𝐿 → 0 < 𝐿))
130	117, 129	syld 47	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → ((𝑀 < 𝑁 ∧ 𝑁 ≤ 𝐿) → 0 < 𝐿))
131	130	expcomd 420	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑁 ≤ 𝐿 → (𝑀 < 𝑁 → 0 < 𝐿)))
132	131	3impia 1131	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (𝑀 < 𝑁 → 0 < 𝐿))
133	132	imp 410	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → 0 < 𝐿)
134		elnnz 12580	. . . . . . . . . . . . . . . 16 ⊢ (𝐿 ∈ ℕ ↔ (𝐿 ∈ ℤ ∧ 0 < 𝐿))
135	110, 133, 134	sylanbrc 592	. . . . . . . . . . . . . . 15 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → 𝐿 ∈ ℕ)
136	135	ad2antrr 736	. . . . . . . . . . . . . 14 ⊢ ((((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → 𝐿 ∈ ℕ)
137		elfzo0 13708	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↔ (𝑥 ∈ ℕ0 ∧ (𝑁 − 𝑀) ∈ ℕ ∧ 𝑥 < (𝑁 − 𝑀)))
138		nn0readdcl 12550	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑥 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0) → (𝑥 + 𝑀) ∈ ℝ)
139	138	expcom 417	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑀 ∈ ℕ0 → (𝑥 ∈ ℕ0 → (𝑥 + 𝑀) ∈ ℝ))
140	139	ad2antrl 738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑥 ∈ ℕ0 → (𝑥 + 𝑀) ∈ ℝ))
141	140	impcom 411	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (𝑥 + 𝑀) ∈ ℝ)
142	25	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → 𝑁 ∈ ℝ)
143	142	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → 𝑁 ∈ ℝ)
144	143	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → 𝑁 ∈ ℝ)
145	111	ad2antrl 738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → 𝐿 ∈ ℝ)
146	141, 144, 145	3jca 1142	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → ((𝑥 + 𝑀) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ))
147	146	ex 416	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 ∈ ℕ0 → ((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → ((𝑥 + 𝑀) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ)))
148	147	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀)) → ((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → ((𝑥 + 𝑀) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ)))
149	148	impcom 411	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) ∧ (𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀))) → ((𝑥 + 𝑀) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ))
150	149	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) ∧ (𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀))) ∧ 𝑁 ≤ 𝐿) → ((𝑥 + 𝑀) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ))
151		nn0re 12492	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑥 ∈ ℕ0 → 𝑥 ∈ ℝ)
152	151	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → 𝑥 ∈ ℝ)
153	24	ad2antrl 738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → 𝑀 ∈ ℝ)
154	153	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → 𝑀 ∈ ℝ)
155	152, 154, 144	ltaddsubd 11789	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → ((𝑥 + 𝑀) < 𝑁 ↔ 𝑥 < (𝑁 − 𝑀)))
156		idd 24	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) ∧ 𝑁 ≤ 𝐿) → ((𝑥 + 𝑀) < 𝑁 → (𝑥 + 𝑀) < 𝑁))
157	156	ex 416	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (𝑁 ≤ 𝐿 → ((𝑥 + 𝑀) < 𝑁 → (𝑥 + 𝑀) < 𝑁)))
158	157	com23 86	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → ((𝑥 + 𝑀) < 𝑁 → (𝑁 ≤ 𝐿 → (𝑥 + 𝑀) < 𝑁)))
159	155, 158	sylbird 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (𝑥 < (𝑁 − 𝑀) → (𝑁 ≤ 𝐿 → (𝑥 + 𝑀) < 𝑁)))
160	159	impancom 455	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀)) → ((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑁 ≤ 𝐿 → (𝑥 + 𝑀) < 𝑁)))
161	160	impcom 411	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) ∧ (𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀))) → (𝑁 ≤ 𝐿 → (𝑥 + 𝑀) < 𝑁))
162	161	impac 560	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) ∧ (𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀))) ∧ 𝑁 ≤ 𝐿) → ((𝑥 + 𝑀) < 𝑁 ∧ 𝑁 ≤ 𝐿))
163		ltletr 11277	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑥 + 𝑀) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ) → (((𝑥 + 𝑀) < 𝑁 ∧ 𝑁 ≤ 𝐿) → (𝑥 + 𝑀) < 𝐿))
164	150, 162, 163	sylc 65	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) ∧ (𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀))) ∧ 𝑁 ≤ 𝐿) → (𝑥 + 𝑀) < 𝐿)
165	164	exp31 423	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → ((𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀)) → (𝑁 ≤ 𝐿 → (𝑥 + 𝑀) < 𝐿)))
166	165	com23 86	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑁 ≤ 𝐿 → ((𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀)) → (𝑥 + 𝑀) < 𝐿)))
167	166	ex 416	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐿 ∈ ℕ0 → ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑁 ≤ 𝐿 → ((𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀)) → (𝑥 + 𝑀) < 𝐿))))
168	167	adantl 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) → ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑁 ≤ 𝐿 → ((𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀)) → (𝑥 + 𝑀) < 𝐿))))
169	168	3imp 1124	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → ((𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀)) → (𝑥 + 𝑀) < 𝐿))
170	169	ad2antrr 736	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) → ((𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀)) → (𝑥 + 𝑀) < 𝐿))
171	170	com12 32	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀)) → (((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) → (𝑥 + 𝑀) < 𝐿))
172	171	3adant2 1145	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℕ0 ∧ (𝑁 − 𝑀) ∈ ℕ ∧ 𝑥 < (𝑁 − 𝑀)) → (((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) → (𝑥 + 𝑀) < 𝐿))
173	137, 172	sylbi 219	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (0..^(𝑁 − 𝑀)) → (((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) → (𝑥 + 𝑀) < 𝐿))
174	173	impcom 411	. . . . . . . . . . . . . 14 ⊢ ((((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → (𝑥 + 𝑀) < 𝐿)
175		elfzo0 13708	. . . . . . . . . . . . . 14 ⊢ ((𝑥 + 𝑀) ∈ (0..^𝐿) ↔ ((𝑥 + 𝑀) ∈ ℕ0 ∧ 𝐿 ∈ ℕ ∧ (𝑥 + 𝑀) < 𝐿))
176	107, 136, 174, 175	syl3anbrc 1358	. . . . . . . . . . . . 13 ⊢ ((((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → (𝑥 + 𝑀) ∈ (0..^𝐿))
177		repswsymb 14789	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0 ∧ (𝑥 + 𝑀) ∈ (0..^𝐿)) → ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀)) = 𝑆)
178	98, 100, 176, 177	syl3anc 1392	. . . . . . . . . . . 12 ⊢ ((((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀)) = 𝑆)
179	178	mpteq2dva 5195	. . . . . . . . . . 11 ⊢ (((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) → (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))) = (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ 𝑆))
180	33	3ad2ant2 1148	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (𝑁 − 𝑀) ∈ ℤ)
181	180	adantr 484	. . . . . . . . . . . . . . 15 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (𝑁 − 𝑀) ∈ ℤ)
182	58	3ad2ant2 1148	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ))
183		ltle 11273	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑀 < 𝑁 → 𝑀 ≤ 𝑁))
184	182, 183	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (𝑀 < 𝑁 → 𝑀 ≤ 𝑁))
185	26	3ad2ant2 1148	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ))
186	185, 56	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (0 ≤ (𝑁 − 𝑀) ↔ 𝑀 ≤ 𝑁))
187	184, 186	sylibrd 261	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (𝑀 < 𝑁 → 0 ≤ (𝑁 − 𝑀)))
188	187	imp 410	. . . . . . . . . . . . . . 15 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → 0 ≤ (𝑁 − 𝑀))
189	181, 188, 55	sylanbrc 592	. . . . . . . . . . . . . 14 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (𝑁 − 𝑀) ∈ ℕ0)
190	97, 189	jca 519	. . . . . . . . . . . . 13 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (𝑆 ∈ 𝑉 ∧ (𝑁 − 𝑀) ∈ ℕ0))
191	190	adantr 484	. . . . . . . . . . . 12 ⊢ (((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) → (𝑆 ∈ 𝑉 ∧ (𝑁 − 𝑀) ∈ ℕ0))
192		reps 14785	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ 𝑉 ∧ (𝑁 − 𝑀) ∈ ℕ0) → (𝑆 repeatS (𝑁 − 𝑀)) = (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ 𝑆))
193	192	eqcomd 2770	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ 𝑉 ∧ (𝑁 − 𝑀) ∈ ℕ0) → (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ 𝑆) = (𝑆 repeatS (𝑁 − 𝑀)))
194	191, 193	syl 17	. . . . . . . . . . 11 ⊢ (((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) → (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ 𝑆) = (𝑆 repeatS (𝑁 − 𝑀)))
195	179, 194	eqtrd 2799	. . . . . . . . . 10 ⊢ (((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) → (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))) = (𝑆 repeatS (𝑁 − 𝑀)))
196	195	ex 416	. . . . . . . . 9 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → ((0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿) → (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))) = (𝑆 repeatS (𝑁 − 𝑀))))
197	96, 196	sylbid 242	. . . . . . . 8 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → ((𝑀..^𝑁) ⊆ (0..^𝐿) → (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))) = (𝑆 repeatS (𝑁 − 𝑀))))
198	197	impcom 411	. . . . . . 7 ⊢ (((𝑀..^𝑁) ⊆ (0..^𝐿) ∧ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁)) → (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))) = (𝑆 repeatS (𝑁 − 𝑀)))
199	86, 198	eqtrd 2799	. . . . . 6 ⊢ (((𝑀..^𝑁) ⊆ (0..^𝐿) ∧ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁)) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁 − 𝑀)))
200		iffalse 4491	. . . . . . . 8 ⊢ (¬ (𝑀..^𝑁) ⊆ (0..^𝐿) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = ∅)
201	200	adantr 484	. . . . . . 7 ⊢ ((¬ (𝑀..^𝑁) ⊆ (0..^𝐿) ∧ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁)) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = ∅)
202	96	notbid 320	. . . . . . . . 9 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (¬ (𝑀..^𝑁) ⊆ (0..^𝐿) ↔ ¬ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)))
203		ianor 995	. . . . . . . . . . 11 ⊢ (¬ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿) ↔ (¬ 0 ≤ 𝑀 ∨ ¬ 𝑁 ≤ 𝐿))
204		nn0ge0 12508	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 ∈ ℕ0 → 0 ≤ 𝑀)
205		pm2.24 124	. . . . . . . . . . . . . . . . 17 ⊢ (0 ≤ 𝑀 → (¬ 0 ≤ 𝑀 → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
206	204, 205	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑀 ∈ ℕ0 → (¬ 0 ≤ 𝑀 → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
207	206	adantr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (¬ 0 ≤ 𝑀 → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
208	207	3ad2ant2 1148	. . . . . . . . . . . . . 14 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (¬ 0 ≤ 𝑀 → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
209	208	adantr 484	. . . . . . . . . . . . 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 1149	. . . . . . . . . . . . . 14 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (¬ 𝑁 ≤ 𝐿 → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
213	212	adantr 484	. . . . . . . . . . . . 13 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (¬ 𝑁 ≤ 𝐿 → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
214	213	com12 32	. . . . . . . . . . . 12 ⊢ (¬ 𝑁 ≤ 𝐿 → ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
215	210, 214	jaoi 868	. . . . . . . . . . 11 ⊢ ((¬ 0 ≤ 𝑀 ∨ ¬ 𝑁 ≤ 𝐿) → ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
216	203, 215	sylbi 219	. . . . . . . . . 10 ⊢ (¬ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿) → ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
217	216	com12 32	. . . . . . . . 9 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (¬ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿) → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
218	202, 217	sylbid 242	. . . . . . . 8 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (¬ (𝑀..^𝑁) ⊆ (0..^𝐿) → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
219	218	impcom 411	. . . . . . 7 ⊢ ((¬ (𝑀..^𝑁) ⊆ (0..^𝐿) ∧ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁)) → (𝑆 repeatS (𝑁 − 𝑀)) = ∅)
220	201, 219	eqtr4d 2802	. . . . . 6 ⊢ ((¬ (𝑀..^𝑁) ⊆ (0..^𝐿) ∧ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁)) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁 − 𝑀)))
221	199, 220	pm2.61ian 821	. . . . 5 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁 − 𝑀)))
222	221	ex 416	. . . 4 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (𝑀 < 𝑁 → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁 − 𝑀))))
223	85, 222	sylbid 242	. . 3 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (¬ 𝑁 ≤ 𝑀 → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁 − 𝑀))))
224	81, 223	pm2.61d 180	. 2 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁 − 𝑀)))
225	10, 15, 224	3eqtrd 2803	1 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → ((𝑆 repeatS 𝐿) substr ⟨𝑀, 𝑁⟩) = (𝑆 repeatS (𝑁 − 𝑀)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 399   ∨ wo 858   ∧ w3a 1099   = wceq 1562   ∈ wcel 2144   ∉ wnel 3063   ⊆ wss 3906  ∅c0 4287  ifcif 4482  ⟨cop 4590   class class class wbr 5102   ↦ cmpt 5183  dom cdm 5649  ⟶wf 6519  ‘cfv 6523  (class class class)co 7398  ℂcc 11073  ℝcr 11074  0cc0 11075   + caddc 11078   < clt 11218   ≤ cle 11219   − cmin 11416  ℕcn 12212  ℕ₀cn0 12483  ℤcz 12570  ..^cfzo 13661  Word cword 14528   substr csubstr 14656   repeatS creps 14783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2214  ax-ext 2736  ax-rep 5229  ax-sep 5248  ax-nul 5258  ax-pow 5324  ax-pr 5392  ax-un 7720  ax-cnex 11131  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151  ax-pre-mulgt0 11152

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1100  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-nf 1806  df-sb 2093  df-mo 2568  df-eu 2598  df-clab 2743  df-cleq 2756  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3064  df-ral 3079  df-rex 3089  df-reu 3370  df-rab 3417  df-v 3458  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4288  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5544  df-eprel 5549  df-po 5557  df-so 5558  df-fr 5602  df-we 5604  df-xp 5655  df-rel 5656  df-cnv 5657  df-co 5658  df-dm 5659  df-rn 5660  df-res 5661  df-ima 5662  df-pred 6290  df-ord 6351  df-on 6352  df-lim 6353  df-suc 6354  df-iota 6479  df-fun 6525  df-fn 6526  df-f 6527  df-f1 6528  df-fo 6529  df-f1o 6530  df-fv 6531  df-riota 7355  df-ov 7401  df-oprab 7402  df-mpo 7403  df-om 7849  df-1st 7972  df-2nd 7973  df-frecs 8264  df-wrecs 8295  df-recs 8344  df-rdg 8383  df-1o 8439  df-er 8680  df-en 8930  df-dom 8931  df-sdom 8932  df-fin 8933  df-card 9899  df-pnf 11220  df-mnf 11221  df-xr 11222  df-ltxr 11223  df-le 11224  df-sub 11418  df-neg 11419  df-nn 12213  df-n0 12484  df-z 12571  df-uz 12842  df-fz 13515  df-fzo 13662  df-hash 14346  df-word 14529  df-substr 14657  df-reps 14784

This theorem is referenced by:  repswcshw  14827