Theorem repswswrd 14857

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 14848	. . . . . 6 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) → (𝑆 repeatS 𝐿) ∈ Word 𝑉)
2		nn0z 12642	. . . . . . 7 ⊢ (𝑀 ∈ ℕ0 → 𝑀 ∈ ℤ)
3		nn0z 12642	. . . . . . 7 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ)
4	2, 3	anim12i 625	. . . . . 6 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
5	1, 4	anim12i 625	. . . . 5 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → ((𝑆 repeatS 𝐿) ∈ Word 𝑉 ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)))
6		3anass 1111	. . . . 5 ⊢ (((𝑆 repeatS 𝐿) ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ↔ ((𝑆 repeatS 𝐿) ∈ Word 𝑉 ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)))
7	5, 6	sylibr 237	. . . 4 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → ((𝑆 repeatS 𝐿) ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
8	7	3adant3 1150	. . 3 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → ((𝑆 repeatS 𝐿) ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
9		swrdval 14713	. . 3 ⊢ (((𝑆 repeatS 𝐿) ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑆 repeatS 𝐿) substr ⟨𝑀, 𝑁⟩) = if((𝑀..^𝑁) ⊆ dom (𝑆 repeatS 𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅))
10	8, 9	syl 18	. 2 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → ((𝑆 repeatS 𝐿) substr ⟨𝑀, 𝑁⟩) = if((𝑀..^𝑁) ⊆ dom (𝑆 repeatS 𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅))
11		repsf 14846	. . . . . 6 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) → (𝑆 repeatS 𝐿):(0..^𝐿)⟶𝑉)
12	11	3ad2ant1 1151	. . . . 5 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (𝑆 repeatS 𝐿):(0..^𝐿)⟶𝑉)
13	12	fdmd 6717	. . . 4 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → dom (𝑆 repeatS 𝐿) = (0..^𝐿))
14	13	sseq2d 3966	. . 3 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → ((𝑀..^𝑁) ⊆ dom (𝑆 repeatS 𝐿) ↔ (𝑀..^𝑁) ⊆ (0..^𝐿)))
15	14	ifbid 4509	. 2 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → if((𝑀..^𝑁) ⊆ dom (𝑆 repeatS 𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅))
16		fzon 13738	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ≤ 𝑀 ↔ (𝑀..^𝑁) = ∅))
17	4, 16	syl 18	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑁 ≤ 𝑀 ↔ (𝑀..^𝑁) = ∅))
18	17	adantl 487	. . . . . . . . 9 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑁 ≤ 𝑀 ↔ (𝑀..^𝑁) = ∅))
19	18	biimpac 484	. . . . . . . 8 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (𝑀..^𝑁) = ∅)
20		0ss 4353	. . . . . . . 8 ⊢ ∅ ⊆ (0..^𝐿)
21	19, 20	eqsstrdi 3978	. . . . . . 7 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (𝑀..^𝑁) ⊆ (0..^𝐿))
22		iftrue 4491	. . . . . . 7 ⊢ ((𝑀..^𝑁) ⊆ (0..^𝐿) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))))
23	21, 22	syl 18	. . . . . 6 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))))
24		nn0re 12540	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℕ0 → 𝑀 ∈ ℝ)
25		nn0re 12540	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ)
26	24, 25	anim12ci 626	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ))
27	26	adantl 487	. . . . . . . . . 10 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ))
28		suble0 11755	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ) → ((𝑁 − 𝑀) ≤ 0 ↔ 𝑁 ≤ 𝑀))
29	27, 28	syl 18	. . . . . . . . 9 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → ((𝑁 − 𝑀) ≤ 0 ↔ 𝑁 ≤ 𝑀))
30	29	biimparc 485	. . . . . . . 8 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (𝑁 − 𝑀) ≤ 0)
31		0z 12629	. . . . . . . . 9 ⊢ 0 ∈ ℤ
32		zsubcl 12663	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑁 − 𝑀) ∈ ℤ)
33	3, 2, 32	syl2anr 609	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑁 − 𝑀) ∈ ℤ)
34	33	adantl 487	. . . . . . . . . 10 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑁 − 𝑀) ∈ ℤ)
35	34	adantl 487	. . . . . . . . 9 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (𝑁 − 𝑀) ∈ ℤ)
36		fzon 13738	. . . . . . . . 9 ⊢ ((0 ∈ ℤ ∧ (𝑁 − 𝑀) ∈ ℤ) → ((𝑁 − 𝑀) ≤ 0 ↔ (0..^(𝑁 − 𝑀)) = ∅))
37	31, 35, 36	sylancr 599	. . . . . . . 8 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → ((𝑁 − 𝑀) ≤ 0 ↔ (0..^(𝑁 − 𝑀)) = ∅))
38	30, 37	mpbid 235	. . . . . . 7 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (0..^(𝑁 − 𝑀)) = ∅)
39	38	mpteq1d 5199	. . . . . 6 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))) = (𝑥 ∈ ∅ ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))))
40		mpt0 6678	. . . . . . 7 ⊢ (𝑥 ∈ ∅ ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))) = ∅
41		oveq2 7424	. . . . . . . . . . . . 13 ⊢ (𝑀 = 𝑁 → (𝑁 − 𝑀) = (𝑁 − 𝑁))
42	41	oveq2d 7432	. . . . . . . . . . . 12 ⊢ (𝑀 = 𝑁 → (𝑆 repeatS (𝑁 − 𝑀)) = (𝑆 repeatS (𝑁 − 𝑁)))
43		nn0cn 12541	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ)
44	43	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → 𝑁 ∈ ℂ)
45	44	subidd 11584	. . . . . . . . . . . . . . 15 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑁 − 𝑁) = 0)
46	45	adantl 487	. . . . . . . . . . . . . 14 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑁 − 𝑁) = 0)
47	46	oveq2d 7432	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑆 repeatS (𝑁 − 𝑁)) = (𝑆 repeatS 0))
48		repsw0 14850	. . . . . . . . . . . . . 14 ⊢ (𝑆 ∈ 𝑉 → (𝑆 repeatS 0) = ∅)
49	48	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑆 repeatS 0) = ∅)
50	47, 49	eqtrd 2797	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑆 repeatS (𝑁 − 𝑁)) = ∅)
51	42, 50	sylan9eqr 2819	. . . . . . . . . . 11 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑀 = 𝑁) → (𝑆 repeatS (𝑁 − 𝑀)) = ∅)
52	51	ex 418	. . . . . . . . . 10 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑀 = 𝑁 → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
53	52	adantl 487	. . . . . . . . 9 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (𝑀 = 𝑁 → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
54	53	com12 33	. . . . . . . 8 ⊢ (𝑀 = 𝑁 → ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
55		elnn0z 12631	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 − 𝑀) ∈ ℕ0 ↔ ((𝑁 − 𝑀) ∈ ℤ ∧ 0 ≤ (𝑁 − 𝑀)))
56		subge0 11754	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ) → (0 ≤ (𝑁 − 𝑀) ↔ 𝑀 ≤ 𝑁))
57	25, 24, 56	syl2anr 609	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (0 ≤ (𝑁 − 𝑀) ↔ 𝑀 ≤ 𝑁))
58	24, 25	anim12i 625	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ))
59		letri3 11322	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑀 = 𝑁 ↔ (𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑀)))
60	58, 59	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀 = 𝑁 ↔ (𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑀)))
61	60	biimprd 251	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → ((𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑀) → 𝑀 = 𝑁))
62	61	expd 421	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀 ≤ 𝑁 → (𝑁 ≤ 𝑀 → 𝑀 = 𝑁)))
63	57, 62	sylbid 243	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (0 ≤ (𝑁 − 𝑀) → (𝑁 ≤ 𝑀 → 𝑀 = 𝑁)))
64	63	com23 87	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑁 ≤ 𝑀 → (0 ≤ (𝑁 − 𝑀) → 𝑀 = 𝑁)))
65	64	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑁 ≤ 𝑀 → (0 ≤ (𝑁 − 𝑀) → 𝑀 = 𝑁)))
66	65	impcom 413	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (0 ≤ (𝑁 − 𝑀) → 𝑀 = 𝑁))
67	66	com12 33	. . . . . . . . . . . . . . 15 ⊢ (0 ≤ (𝑁 − 𝑀) → ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → 𝑀 = 𝑁))
68	55, 67	simplbiim 514	. . . . . . . . . . . . . 14 ⊢ ((𝑁 − 𝑀) ∈ ℕ0 → ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → 𝑀 = 𝑁))
69	68	com12 33	. . . . . . . . . . . . 13 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → ((𝑁 − 𝑀) ∈ ℕ0 → 𝑀 = 𝑁))
70	69	con3d 153	. . . . . . . . . . . 12 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (¬ 𝑀 = 𝑁 → ¬ (𝑁 − 𝑀) ∈ ℕ0))
71	70	impcom 413	. . . . . . . . . . 11 ⊢ ((¬ 𝑀 = 𝑁 ∧ (𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)))) → ¬ (𝑁 − 𝑀) ∈ ℕ0)
72		df-nel 3064	. . . . . . . . . . 11 ⊢ ((𝑁 − 𝑀) ∉ ℕ0 ↔ ¬ (𝑁 − 𝑀) ∈ ℕ0)
73	71, 72	sylibr 237	. . . . . . . . . 10 ⊢ ((¬ 𝑀 = 𝑁 ∧ (𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)))) → (𝑁 − 𝑀) ∉ ℕ0)
74		repsundef 14844	. . . . . . . . . 10 ⊢ ((𝑁 − 𝑀) ∉ ℕ0 → (𝑆 repeatS (𝑁 − 𝑀)) = ∅)
75	73, 74	syl 18	. . . . . . . . 9 ⊢ ((¬ 𝑀 = 𝑁 ∧ (𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)))) → (𝑆 repeatS (𝑁 − 𝑀)) = ∅)
76	75	ex 418	. . . . . . . 8 ⊢ (¬ 𝑀 = 𝑁 → ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
77	54, 76	pm2.61i 184	. . . . . . 7 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (𝑆 repeatS (𝑁 − 𝑀)) = ∅)
78	40, 77	eqtr4id 2816	. . . . . 6 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (𝑥 ∈ ∅ ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))) = (𝑆 repeatS (𝑁 − 𝑀)))
79	23, 39, 78	3eqtrd 2801	. . . . 5 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁 − 𝑀)))
80	79	expcom 419	. . . 4 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑁 ≤ 𝑀 → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁 − 𝑀))))
81	80	3adant3 1150	. . 3 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (𝑁 ≤ 𝑀 → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁 − 𝑀))))
82		ltnle 11316	. . . . . . 7 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑀 < 𝑁 ↔ ¬ 𝑁 ≤ 𝑀))
83	58, 82	syl 18	. . . . . 6 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀 < 𝑁 ↔ ¬ 𝑁 ≤ 𝑀))
84	83	bicomd 226	. . . . 5 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (¬ 𝑁 ≤ 𝑀 ↔ 𝑀 < 𝑁))
85	84	3ad2ant2 1152	. . . 4 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (¬ 𝑁 ≤ 𝑀 ↔ 𝑀 < 𝑁))
86	22	adantr 486	. . . . . . 7 ⊢ (((𝑀..^𝑁) ⊆ (0..^𝐿) ∧ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁)) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))))
87	4	3ad2ant2 1152	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
88	87	adantr 486	. . . . . . . . . 10 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
89		0zd 12630	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ 𝑉 → 0 ∈ ℤ)
90		nn0z 12642	. . . . . . . . . . . . 13 ⊢ (𝐿 ∈ ℕ0 → 𝐿 ∈ ℤ)
91	89, 90	anim12i 625	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) → (0 ∈ ℤ ∧ 𝐿 ∈ ℤ))
92	91	3ad2ant1 1151	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (0 ∈ ℤ ∧ 𝐿 ∈ ℤ))
93	92	adantr 486	. . . . . . . . . 10 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (0 ∈ ℤ ∧ 𝐿 ∈ ℤ))
94		simpr 490	. . . . . . . . . 10 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → 𝑀 < 𝑁)
95		ssfzo12bi 13819	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ 𝑀 < 𝑁) → ((𝑀..^𝑁) ⊆ (0..^𝐿) ↔ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)))
96	88, 93, 94, 95	syl3anc 1398	. . . . . . . . 9 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → ((𝑀..^𝑁) ⊆ (0..^𝐿) ↔ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)))
97		simpl1l 1243	. . . . . . . . . . . . . 14 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → 𝑆 ∈ 𝑉)
98	97	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ ((((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → 𝑆 ∈ 𝑉)
99		simpl1r 1244	. . . . . . . . . . . . . 14 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → 𝐿 ∈ ℕ0)
100	99	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ ((((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → 𝐿 ∈ ℕ0)
101		nn0addcl 12566	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0) → (𝑥 + 𝑀) ∈ ℕ0)
102	101	expcom 419	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑀 ∈ ℕ0 → (𝑥 ∈ ℕ0 → (𝑥 + 𝑀) ∈ ℕ0))
103	102	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑥 ∈ ℕ0 → (𝑥 + 𝑀) ∈ ℕ0))
104	103	3ad2ant2 1152	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (𝑥 ∈ ℕ0 → (𝑥 + 𝑀) ∈ ℕ0))
105	104	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ (((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) → (𝑥 ∈ ℕ0 → (𝑥 + 𝑀) ∈ ℕ0))
106		elfzonn0 13765	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (0..^(𝑁 − 𝑀)) → 𝑥 ∈ ℕ0)
107	105, 106	impel 515	. . . . . . . . . . . . . 14 ⊢ ((((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → (𝑥 + 𝑀) ∈ ℕ0)
108	90	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) → 𝐿 ∈ ℤ)
109	108	3ad2ant1 1151	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → 𝐿 ∈ ℤ)
110	109	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → 𝐿 ∈ ℤ)
111		nn0re 12540	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐿 ∈ ℕ0 → 𝐿 ∈ ℝ)
112	111	adantl 487	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) → 𝐿 ∈ ℝ)
113	112, 58	anim12ci 626	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝐿 ∈ ℝ))
114		df-3an 1105	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ) ↔ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝐿 ∈ ℝ))
115	113, 114	sylibr 237	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ))
116		ltletr 11329	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ) → ((𝑀 < 𝑁 ∧ 𝑁 ≤ 𝐿) → 𝑀 < 𝐿))
117	115, 116	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → ((𝑀 < 𝑁 ∧ 𝑁 ≤ 𝐿) → 𝑀 < 𝐿))
118		elnn0z 12631	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑀 ∈ ℕ0 ↔ (𝑀 ∈ ℤ ∧ 0 ≤ 𝑀))
119		0red 11238	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑀 ∈ ℤ ∧ (𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0)) → 0 ∈ ℝ)
120		zre 12622	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℝ)
121	120	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑀 ∈ ℤ ∧ (𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0)) → 𝑀 ∈ ℝ)
122	112	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑀 ∈ ℤ ∧ (𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0)) → 𝐿 ∈ ℝ)
123		lelttr 11327	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((0 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝐿 ∈ ℝ) → ((0 ≤ 𝑀 ∧ 𝑀 < 𝐿) → 0 < 𝐿))
124	119, 121, 122, 123	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑀 ∈ ℤ ∧ (𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0)) → ((0 ≤ 𝑀 ∧ 𝑀 < 𝐿) → 0 < 𝐿))
125	124	expd 421	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑀 ∈ ℤ ∧ (𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0)) → (0 ≤ 𝑀 → (𝑀 < 𝐿 → 0 < 𝐿)))
126	125	impancom 457	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑀 ∈ ℤ ∧ 0 ≤ 𝑀) → ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) → (𝑀 < 𝐿 → 0 < 𝐿)))
127	118, 126	sylbi 220	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑀 ∈ ℕ0 → ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) → (𝑀 < 𝐿 → 0 < 𝐿)))
128	127	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) → (𝑀 < 𝐿 → 0 < 𝐿)))
129	128	impcom 413	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑀 < 𝐿 → 0 < 𝐿))
130	117, 129	syld 48	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → ((𝑀 < 𝑁 ∧ 𝑁 ≤ 𝐿) → 0 < 𝐿))
131	130	expcomd 422	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑁 ≤ 𝐿 → (𝑀 < 𝑁 → 0 < 𝐿)))
132	131	3impia 1135	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (𝑀 < 𝑁 → 0 < 𝐿))
133	132	imp 412	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → 0 < 𝐿)
134		elnnz 12628	. . . . . . . . . . . . . . . 16 ⊢ (𝐿 ∈ ℕ ↔ (𝐿 ∈ ℤ ∧ 0 < 𝐿))
135	110, 133, 134	sylanbrc 595	. . . . . . . . . . . . . . 15 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → 𝐿 ∈ ℕ)
136	135	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ ((((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → 𝐿 ∈ ℕ)
137		elfzo0 13758	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↔ (𝑥 ∈ ℕ0 ∧ (𝑁 − 𝑀) ∈ ℕ ∧ 𝑥 < (𝑁 − 𝑀)))
138		nn0readdcl 12598	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑥 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0) → (𝑥 + 𝑀) ∈ ℝ)
139	138	expcom 419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑀 ∈ ℕ0 → (𝑥 ∈ ℕ0 → (𝑥 + 𝑀) ∈ ℝ))
140	139	ad2antrl 741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑥 ∈ ℕ0 → (𝑥 + 𝑀) ∈ ℝ))
141	140	impcom 413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (𝑥 + 𝑀) ∈ ℝ)
142	25	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → 𝑁 ∈ ℝ)
143	142	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → 𝑁 ∈ ℝ)
144	143	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → 𝑁 ∈ ℝ)
145	111	ad2antrl 741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → 𝐿 ∈ ℝ)
146	141, 144, 145	3jca 1146	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → ((𝑥 + 𝑀) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ))
147	146	ex 418	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 ∈ ℕ0 → ((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → ((𝑥 + 𝑀) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ)))
148	147	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀)) → ((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → ((𝑥 + 𝑀) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ)))
149	148	impcom 413	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) ∧ (𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀))) → ((𝑥 + 𝑀) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ))
150	149	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) ∧ (𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀))) ∧ 𝑁 ≤ 𝐿) → ((𝑥 + 𝑀) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ))
151		nn0re 12540	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑥 ∈ ℕ0 → 𝑥 ∈ ℝ)
152	151	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → 𝑥 ∈ ℝ)
153	24	ad2antrl 741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → 𝑀 ∈ ℝ)
154	153	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → 𝑀 ∈ ℝ)
155	152, 154, 144	ltaddsubd 11841	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → ((𝑥 + 𝑀) < 𝑁 ↔ 𝑥 < (𝑁 − 𝑀)))
156		idd 25	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) ∧ 𝑁 ≤ 𝐿) → ((𝑥 + 𝑀) < 𝑁 → (𝑥 + 𝑀) < 𝑁))
157	156	ex 418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (𝑁 ≤ 𝐿 → ((𝑥 + 𝑀) < 𝑁 → (𝑥 + 𝑀) < 𝑁)))
158	157	com23 87	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → ((𝑥 + 𝑀) < 𝑁 → (𝑁 ≤ 𝐿 → (𝑥 + 𝑀) < 𝑁)))
159	155, 158	sylbird 263	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (𝑥 < (𝑁 − 𝑀) → (𝑁 ≤ 𝐿 → (𝑥 + 𝑀) < 𝑁)))
160	159	impancom 457	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀)) → ((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑁 ≤ 𝐿 → (𝑥 + 𝑀) < 𝑁)))
161	160	impcom 413	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) ∧ (𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀))) → (𝑁 ≤ 𝐿 → (𝑥 + 𝑀) < 𝑁))
162	161	impac 562	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) ∧ (𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀))) ∧ 𝑁 ≤ 𝐿) → ((𝑥 + 𝑀) < 𝑁 ∧ 𝑁 ≤ 𝐿))
163		ltletr 11329	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑥 + 𝑀) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ) → (((𝑥 + 𝑀) < 𝑁 ∧ 𝑁 ≤ 𝐿) → (𝑥 + 𝑀) < 𝐿))
164	150, 162, 163	sylc 66	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) ∧ (𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀))) ∧ 𝑁 ≤ 𝐿) → (𝑥 + 𝑀) < 𝐿)
165	164	exp31 425	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → ((𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀)) → (𝑁 ≤ 𝐿 → (𝑥 + 𝑀) < 𝐿)))
166	165	com23 87	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑁 ≤ 𝐿 → ((𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀)) → (𝑥 + 𝑀) < 𝐿)))
167	166	ex 418	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐿 ∈ ℕ0 → ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑁 ≤ 𝐿 → ((𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀)) → (𝑥 + 𝑀) < 𝐿))))
168	167	adantl 487	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) → ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑁 ≤ 𝐿 → ((𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀)) → (𝑥 + 𝑀) < 𝐿))))
169	168	3imp 1128	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → ((𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀)) → (𝑥 + 𝑀) < 𝐿))
170	169	ad2antrr 739	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) → ((𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀)) → (𝑥 + 𝑀) < 𝐿))
171	170	com12 33	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀)) → (((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) → (𝑥 + 𝑀) < 𝐿))
172	171	3adant2 1149	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℕ0 ∧ (𝑁 − 𝑀) ∈ ℕ ∧ 𝑥 < (𝑁 − 𝑀)) → (((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) → (𝑥 + 𝑀) < 𝐿))
173	137, 172	sylbi 220	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (0..^(𝑁 − 𝑀)) → (((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) → (𝑥 + 𝑀) < 𝐿))
174	173	impcom 413	. . . . . . . . . . . . . 14 ⊢ ((((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → (𝑥 + 𝑀) < 𝐿)
175		elfzo0 13758	. . . . . . . . . . . . . 14 ⊢ ((𝑥 + 𝑀) ∈ (0..^𝐿) ↔ ((𝑥 + 𝑀) ∈ ℕ0 ∧ 𝐿 ∈ ℕ ∧ (𝑥 + 𝑀) < 𝐿))
176	107, 136, 174, 175	syl3anbrc 1362	. . . . . . . . . . . . 13 ⊢ ((((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → (𝑥 + 𝑀) ∈ (0..^𝐿))
177		repswsymb 14847	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0 ∧ (𝑥 + 𝑀) ∈ (0..^𝐿)) → ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀)) = 𝑆)
178	98, 100, 176, 177	syl3anc 1398	. . . . . . . . . . . 12 ⊢ ((((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀)) = 𝑆)
179	178	mpteq2dva 5202	. . . . . . . . . . 11 ⊢ (((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) → (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))) = (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ 𝑆))
180	33	3ad2ant2 1152	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (𝑁 − 𝑀) ∈ ℤ)
181	180	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (𝑁 − 𝑀) ∈ ℤ)
182	58	3ad2ant2 1152	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ))
183		ltle 11325	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑀 < 𝑁 → 𝑀 ≤ 𝑁))
184	182, 183	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (𝑀 < 𝑁 → 𝑀 ≤ 𝑁))
185	26	3ad2ant2 1152	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ))
186	185, 56	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (0 ≤ (𝑁 − 𝑀) ↔ 𝑀 ≤ 𝑁))
187	184, 186	sylibrd 262	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (𝑀 < 𝑁 → 0 ≤ (𝑁 − 𝑀)))
188	187	imp 412	. . . . . . . . . . . . . . 15 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → 0 ≤ (𝑁 − 𝑀))
189	181, 188, 55	sylanbrc 595	. . . . . . . . . . . . . 14 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (𝑁 − 𝑀) ∈ ℕ0)
190	97, 189	jca 521	. . . . . . . . . . . . 13 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (𝑆 ∈ 𝑉 ∧ (𝑁 − 𝑀) ∈ ℕ0))
191	190	adantr 486	. . . . . . . . . . . 12 ⊢ (((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) → (𝑆 ∈ 𝑉 ∧ (𝑁 − 𝑀) ∈ ℕ0))
192		reps 14843	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ 𝑉 ∧ (𝑁 − 𝑀) ∈ ℕ0) → (𝑆 repeatS (𝑁 − 𝑀)) = (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ 𝑆))
193	192	eqcomd 2768	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ 𝑉 ∧ (𝑁 − 𝑀) ∈ ℕ0) → (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ 𝑆) = (𝑆 repeatS (𝑁 − 𝑀)))
194	191, 193	syl 18	. . . . . . . . . . 11 ⊢ (((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) → (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ 𝑆) = (𝑆 repeatS (𝑁 − 𝑀)))
195	179, 194	eqtrd 2797	. . . . . . . . . 10 ⊢ (((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) → (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))) = (𝑆 repeatS (𝑁 − 𝑀)))
196	195	ex 418	. . . . . . . . 9 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → ((0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿) → (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))) = (𝑆 repeatS (𝑁 − 𝑀))))
197	96, 196	sylbid 243	. . . . . . . 8 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → ((𝑀..^𝑁) ⊆ (0..^𝐿) → (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))) = (𝑆 repeatS (𝑁 − 𝑀))))
198	197	impcom 413	. . . . . . 7 ⊢ (((𝑀..^𝑁) ⊆ (0..^𝐿) ∧ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁)) → (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))) = (𝑆 repeatS (𝑁 − 𝑀)))
199	86, 198	eqtrd 2797	. . . . . 6 ⊢ (((𝑀..^𝑁) ⊆ (0..^𝐿) ∧ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁)) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁 − 𝑀)))
200		iffalse 4494	. . . . . . . 8 ⊢ (¬ (𝑀..^𝑁) ⊆ (0..^𝐿) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = ∅)
201	200	adantr 486	. . . . . . 7 ⊢ ((¬ (𝑀..^𝑁) ⊆ (0..^𝐿) ∧ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁)) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = ∅)
202	96	notbid 321	. . . . . . . . 9 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (¬ (𝑀..^𝑁) ⊆ (0..^𝐿) ↔ ¬ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)))
203		ianor 997	. . . . . . . . . . 11 ⊢ (¬ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿) ↔ (¬ 0 ≤ 𝑀 ∨ ¬ 𝑁 ≤ 𝐿))
204		nn0ge0 12556	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 ∈ ℕ0 → 0 ≤ 𝑀)
205		pm2.24 125	. . . . . . . . . . . . . . . . 17 ⊢ (0 ≤ 𝑀 → (¬ 0 ≤ 𝑀 → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
206	204, 205	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝑀 ∈ ℕ0 → (¬ 0 ≤ 𝑀 → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
207	206	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (¬ 0 ≤ 𝑀 → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
208	207	3ad2ant2 1152	. . . . . . . . . . . . . 14 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (¬ 0 ≤ 𝑀 → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
209	208	adantr 486	. . . . . . . . . . . . 13 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (¬ 0 ≤ 𝑀 → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
210	209	com12 33	. . . . . . . . . . . 12 ⊢ (¬ 0 ≤ 𝑀 → ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
211		pm2.24 125	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ≤ 𝐿 → (¬ 𝑁 ≤ 𝐿 → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
212	211	3ad2ant3 1153	. . . . . . . . . . . . . 14 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (¬ 𝑁 ≤ 𝐿 → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
213	212	adantr 486	. . . . . . . . . . . . 13 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (¬ 𝑁 ≤ 𝐿 → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
214	213	com12 33	. . . . . . . . . . . 12 ⊢ (¬ 𝑁 ≤ 𝐿 → ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
215	210, 214	jaoi 871	. . . . . . . . . . 11 ⊢ ((¬ 0 ≤ 𝑀 ∨ ¬ 𝑁 ≤ 𝐿) → ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
216	203, 215	sylbi 220	. . . . . . . . . 10 ⊢ (¬ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿) → ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
217	216	com12 33	. . . . . . . . 9 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (¬ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿) → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
218	202, 217	sylbid 243	. . . . . . . 8 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (¬ (𝑀..^𝑁) ⊆ (0..^𝐿) → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
219	218	impcom 413	. . . . . . 7 ⊢ ((¬ (𝑀..^𝑁) ⊆ (0..^𝐿) ∧ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁)) → (𝑆 repeatS (𝑁 − 𝑀)) = ∅)
220	201, 219	eqtr4d 2800	. . . . . 6 ⊢ ((¬ (𝑀..^𝑁) ⊆ (0..^𝐿) ∧ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁)) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁 − 𝑀)))
221	199, 220	pm2.61ian 824	. . . . 5 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁 − 𝑀)))
222	221	ex 418	. . . 4 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (𝑀 < 𝑁 → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁 − 𝑀))))
223	85, 222	sylbid 243	. . 3 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (¬ 𝑁 ≤ 𝑀 → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁 − 𝑀))))
224	81, 223	pm2.61d 181	. 2 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁 − 𝑀)))
225	10, 15, 224	3eqtrd 2801	1 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → ((𝑆 repeatS 𝐿) substr ⟨𝑀, 𝑁⟩) = (𝑆 repeatS (𝑁 − 𝑀)))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145   ∉ wnel 3063   ⊆ wss 3902  ∅c0 4282  ifcif 4485  ⟨cop 4593   class class class wbr 5107   ↦ cmpt 5190  dom cdm 5659  ⟶wf 6533  ‘cfv 6537  (class class class)co 7416  ℂcc 11125  ℝcr 11126  0cc0 11127   + caddc 11130   < clt 11270   ≤ cle 11271   − cmin 11468  ℕcn 12260  ℕ₀cn0 12531  ℤcz 12618  ..^cfzo 13711  Word cword 14580   substr csubstr 14710   repeatS creps 14841

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-rep 5236  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7739  ax-cnex 11183  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-mulcom 11191  ax-addass 11192  ax-mulass 11193  ax-distr 11194  ax-i2m1 11195  ax-1ne0 11196  ax-1rid 11197  ax-rnegex 11198  ax-rrecex 11199  ax-cnre 11200  ax-pre-lttri 11201  ax-pre-lttrn 11202  ax-pre-ltadd 11203  ax-pre-mulgt0 11204

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-int 4911  df-iun 4956  df-br 5108  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7373  df-ov 7419  df-oprab 7420  df-mpo 7421  df-om 7866  df-1st 7989  df-2nd 7990  df-frecs 8283  df-wrecs 8314  df-recs 8363  df-rdg 8402  df-1o 8458  df-er 8699  df-en 8956  df-dom 8957  df-sdom 8958  df-fin 8959  df-card 9947  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276  df-sub 11470  df-neg 11471  df-nn 12261  df-n0 12532  df-z 12619  df-uz 12891  df-fz 13564  df-fzo 13712  df-hash 14397  df-word 14581  df-substr 14711  df-reps 14842

This theorem is used by:  repswcshw  14885