Theorem repswswrd 13382

Description: A subword of a "repeated symbol word" is again a "repeated symbol word". The assumption N <_ L is required, because otherwise ( L < N ): ((𝑆 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 13373	. . . . . 6 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) → (𝑆 repeatS 𝐿) ∈ Word 𝑉)
2		nn0z 11277	. . . . . . 7 ⊢ (𝑀 ∈ ℕ0 → 𝑀 ∈ ℤ)
3		nn0z 11277	. . . . . . 7 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ)
4	2, 3	anim12i 588	. . . . . 6 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
5	1, 4	anim12i 588	. . . . 5 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → ((𝑆 repeatS 𝐿) ∈ Word 𝑉 ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)))
6		3anass 1035	. . . . 5 ⊢ (((𝑆 repeatS 𝐿) ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ↔ ((𝑆 repeatS 𝐿) ∈ Word 𝑉 ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)))
7	5, 6	sylibr 223	. . . 4 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → ((𝑆 repeatS 𝐿) ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
8	7	3adant3 1074	. . 3 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → ((𝑆 repeatS 𝐿) ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
9		swrdval 13269	. . 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 13371	. . . . . 6 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) → (𝑆 repeatS 𝐿):(0..^𝐿)⟶𝑉)
12	11	3ad2ant1 1075	. . . . 5 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (𝑆 repeatS 𝐿):(0..^𝐿)⟶𝑉)
13		fdm 5964	. . . . 5 ⊢ ((𝑆 repeatS 𝐿):(0..^𝐿)⟶𝑉 → dom (𝑆 repeatS 𝐿) = (0..^𝐿))
14	12, 13	syl 17	. . . 4 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → dom (𝑆 repeatS 𝐿) = (0..^𝐿))
15	14	sseq2d 3596	. . 3 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → ((𝑀..^𝑁) ⊆ dom (𝑆 repeatS 𝐿) ↔ (𝑀..^𝑁) ⊆ (0..^𝐿)))
16	15	ifbid 4058	. 2 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → if((𝑀..^𝑁) ⊆ dom (𝑆 repeatS 𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅))
17		fzon 12358	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ≤ 𝑀 ↔ (𝑀..^𝑁) = ∅))
18	4, 17	syl 17	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑁 ≤ 𝑀 ↔ (𝑀..^𝑁) = ∅))
19	18	adantl 481	. . . . . . . . 9 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑁 ≤ 𝑀 ↔ (𝑀..^𝑁) = ∅))
20	19	biimpac 502	. . . . . . . 8 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (𝑀..^𝑁) = ∅)
21		0ss 3924	. . . . . . . 8 ⊢ ∅ ⊆ (0..^𝐿)
22	20, 21	syl6eqss 3618	. . . . . . 7 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (𝑀..^𝑁) ⊆ (0..^𝐿))
23		iftrue 4042	. . . . . . 7 ⊢ ((𝑀..^𝑁) ⊆ (0..^𝐿) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))))
24	22, 23	syl 17	. . . . . 6 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))))
25		nn0re 11178	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℕ0 → 𝑀 ∈ ℝ)
26		nn0re 11178	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ)
27	25, 26	anim12ci 589	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ))
28	27	adantl 481	. . . . . . . . . 10 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ))
29		suble0 10421	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ) → ((𝑁 − 𝑀) ≤ 0 ↔ 𝑁 ≤ 𝑀))
30	28, 29	syl 17	. . . . . . . . 9 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → ((𝑁 − 𝑀) ≤ 0 ↔ 𝑁 ≤ 𝑀))
31	30	biimparc 503	. . . . . . . 8 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (𝑁 − 𝑀) ≤ 0)
32		0z 11265	. . . . . . . . 9 ⊢ 0 ∈ ℤ
33		zsubcl 11296	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑁 − 𝑀) ∈ ℤ)
34	3, 2, 33	syl2anr 494	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑁 − 𝑀) ∈ ℤ)
35	34	adantl 481	. . . . . . . . . 10 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑁 − 𝑀) ∈ ℤ)
36	35	adantl 481	. . . . . . . . 9 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (𝑁 − 𝑀) ∈ ℤ)
37		fzon 12358	. . . . . . . . 9 ⊢ ((0 ∈ ℤ ∧ (𝑁 − 𝑀) ∈ ℤ) → ((𝑁 − 𝑀) ≤ 0 ↔ (0..^(𝑁 − 𝑀)) = ∅))
38	32, 36, 37	sylancr 694	. . . . . . . 8 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → ((𝑁 − 𝑀) ≤ 0 ↔ (0..^(𝑁 − 𝑀)) = ∅))
39	31, 38	mpbid 221	. . . . . . 7 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (0..^(𝑁 − 𝑀)) = ∅)
40	39	mpteq1d 4666	. . . . . 6 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))) = (𝑥 ∈ ∅ ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))))
41		oveq2 6557	. . . . . . . . . . . . 13 ⊢ (𝑀 = 𝑁 → (𝑁 − 𝑀) = (𝑁 − 𝑁))
42	41	oveq2d 6565	. . . . . . . . . . . 12 ⊢ (𝑀 = 𝑁 → (𝑆 repeatS (𝑁 − 𝑀)) = (𝑆 repeatS (𝑁 − 𝑁)))
43		nn0cn 11179	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ)
44	43	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → 𝑁 ∈ ℂ)
45	44	subidd 10259	. . . . . . . . . . . . . . 15 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑁 − 𝑁) = 0)
46	45	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑁 − 𝑁) = 0)
47	46	oveq2d 6565	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑆 repeatS (𝑁 − 𝑁)) = (𝑆 repeatS 0))
48		repsw0 13375	. . . . . . . . . . . . . 14 ⊢ (𝑆 ∈ 𝑉 → (𝑆 repeatS 0) = ∅)
49	48	ad2antrr 758	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑆 repeatS 0) = ∅)
50	47, 49	eqtrd 2644	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑆 repeatS (𝑁 − 𝑁)) = ∅)
51	42, 50	sylan9eqr 2666	. . . . . . . . . . 11 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑀 = 𝑁) → (𝑆 repeatS (𝑁 − 𝑀)) = ∅)
52	51	ex 449	. . . . . . . . . 10 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑀 = 𝑁 → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
53	52	adantl 481	. . . . . . . . 9 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (𝑀 = 𝑁 → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
54	53	com12 32	. . . . . . . 8 ⊢ (𝑀 = 𝑁 → ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
55		elnn0z 11267	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 − 𝑀) ∈ ℕ0 ↔ ((𝑁 − 𝑀) ∈ ℤ ∧ 0 ≤ (𝑁 − 𝑀)))
56		subge0 10420	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ) → (0 ≤ (𝑁 − 𝑀) ↔ 𝑀 ≤ 𝑁))
57	26, 25, 56	syl2anr 494	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (0 ≤ (𝑁 − 𝑀) ↔ 𝑀 ≤ 𝑁))
58	25, 26	anim12i 588	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ))
59		letri3 10002	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑀 = 𝑁 ↔ (𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑀)))
60	58, 59	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀 = 𝑁 ↔ (𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑀)))
61	60	biimprd 237	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → ((𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑀) → 𝑀 = 𝑁))
62	61	expd 451	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀 ≤ 𝑁 → (𝑁 ≤ 𝑀 → 𝑀 = 𝑁)))
63	57, 62	sylbid 229	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (0 ≤ (𝑁 − 𝑀) → (𝑁 ≤ 𝑀 → 𝑀 = 𝑁)))
64	63	com23 84	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑁 ≤ 𝑀 → (0 ≤ (𝑁 − 𝑀) → 𝑀 = 𝑁)))
65	64	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑁 ≤ 𝑀 → (0 ≤ (𝑁 − 𝑀) → 𝑀 = 𝑁)))
66	65	impcom 445	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (0 ≤ (𝑁 − 𝑀) → 𝑀 = 𝑁))
67	66	com12 32	. . . . . . . . . . . . . . . 16 ⊢ (0 ≤ (𝑁 − 𝑀) → ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → 𝑀 = 𝑁))
68	67	adantl 481	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 − 𝑀) ∈ ℤ ∧ 0 ≤ (𝑁 − 𝑀)) → ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → 𝑀 = 𝑁))
69	55, 68	sylbi 206	. . . . . . . . . . . . . 14 ⊢ ((𝑁 − 𝑀) ∈ ℕ0 → ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → 𝑀 = 𝑁))
70	69	com12 32	. . . . . . . . . . . . 13 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → ((𝑁 − 𝑀) ∈ ℕ0 → 𝑀 = 𝑁))
71	70	con3d 147	. . . . . . . . . . . 12 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (¬ 𝑀 = 𝑁 → ¬ (𝑁 − 𝑀) ∈ ℕ0))
72	71	impcom 445	. . . . . . . . . . 11 ⊢ ((¬ 𝑀 = 𝑁 ∧ (𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)))) → ¬ (𝑁 − 𝑀) ∈ ℕ0)
73		df-nel 2783	. . . . . . . . . . 11 ⊢ ((𝑁 − 𝑀) ∉ ℕ0 ↔ ¬ (𝑁 − 𝑀) ∈ ℕ0)
74	72, 73	sylibr 223	. . . . . . . . . 10 ⊢ ((¬ 𝑀 = 𝑁 ∧ (𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)))) → (𝑁 − 𝑀) ∉ ℕ0)
75		repsundef 13369	. . . . . . . . . 10 ⊢ ((𝑁 − 𝑀) ∉ ℕ0 → (𝑆 repeatS (𝑁 − 𝑀)) = ∅)
76	74, 75	syl 17	. . . . . . . . 9 ⊢ ((¬ 𝑀 = 𝑁 ∧ (𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)))) → (𝑆 repeatS (𝑁 − 𝑀)) = ∅)
77	76	ex 449	. . . . . . . 8 ⊢ (¬ 𝑀 = 𝑁 → ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
78	54, 77	pm2.61i 175	. . . . . . 7 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (𝑆 repeatS (𝑁 − 𝑀)) = ∅)
79		mpt0 5934	. . . . . . 7 ⊢ (𝑥 ∈ ∅ ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))) = ∅
80	78, 79	syl6reqr 2663	. . . . . 6 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (𝑥 ∈ ∅ ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))) = (𝑆 repeatS (𝑁 − 𝑀)))
81	24, 40, 80	3eqtrd 2648	. . . . 5 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁 − 𝑀)))
82	81	expcom 450	. . . 4 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑁 ≤ 𝑀 → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁 − 𝑀))))
83	82	3adant3 1074	. . 3 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (𝑁 ≤ 𝑀 → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁 − 𝑀))))
84		ltnle 9996	. . . . . . 7 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑀 < 𝑁 ↔ ¬ 𝑁 ≤ 𝑀))
85	58, 84	syl 17	. . . . . 6 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀 < 𝑁 ↔ ¬ 𝑁 ≤ 𝑀))
86	85	bicomd 212	. . . . 5 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (¬ 𝑁 ≤ 𝑀 ↔ 𝑀 < 𝑁))
87	86	3ad2ant2 1076	. . . 4 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (¬ 𝑁 ≤ 𝑀 ↔ 𝑀 < 𝑁))
88	23	adantr 480	. . . . . . 7 ⊢ (((𝑀..^𝑁) ⊆ (0..^𝐿) ∧ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁)) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))))
89	4	3ad2ant2 1076	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
90	89	adantr 480	. . . . . . . . . 10 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
91		0zd 11266	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ 𝑉 → 0 ∈ ℤ)
92		nn0z 11277	. . . . . . . . . . . . 13 ⊢ (𝐿 ∈ ℕ0 → 𝐿 ∈ ℤ)
93	91, 92	anim12i 588	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) → (0 ∈ ℤ ∧ 𝐿 ∈ ℤ))
94	93	3ad2ant1 1075	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (0 ∈ ℤ ∧ 𝐿 ∈ ℤ))
95	94	adantr 480	. . . . . . . . . 10 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (0 ∈ ℤ ∧ 𝐿 ∈ ℤ))
96		simpr 476	. . . . . . . . . 10 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → 𝑀 < 𝑁)
97		ssfzo12bi 12429	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ 𝑀 < 𝑁) → ((𝑀..^𝑁) ⊆ (0..^𝐿) ↔ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)))
98	90, 95, 96, 97	syl3anc 1318	. . . . . . . . 9 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → ((𝑀..^𝑁) ⊆ (0..^𝐿) ↔ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)))
99		simpl1l 1105	. . . . . . . . . . . . . 14 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → 𝑆 ∈ 𝑉)
100	99	ad2antrr 758	. . . . . . . . . . . . 13 ⊢ ((((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → 𝑆 ∈ 𝑉)
101		simpl1r 1106	. . . . . . . . . . . . . 14 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → 𝐿 ∈ ℕ0)
102	101	ad2antrr 758	. . . . . . . . . . . . 13 ⊢ ((((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → 𝐿 ∈ ℕ0)
103		elfzonn0 12380	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (0..^(𝑁 − 𝑀)) → 𝑥 ∈ ℕ0)
104		nn0addcl 11205	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0) → (𝑥 + 𝑀) ∈ ℕ0)
105	104	expcom 450	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑀 ∈ ℕ0 → (𝑥 ∈ ℕ0 → (𝑥 + 𝑀) ∈ ℕ0))
106	105	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑥 ∈ ℕ0 → (𝑥 + 𝑀) ∈ ℕ0))
107	106	3ad2ant2 1076	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (𝑥 ∈ ℕ0 → (𝑥 + 𝑀) ∈ ℕ0))
108	107	ad2antrr 758	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) → (𝑥 ∈ ℕ0 → (𝑥 + 𝑀) ∈ ℕ0))
109	103, 108	syl5com 31	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (0..^(𝑁 − 𝑀)) → (((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) → (𝑥 + 𝑀) ∈ ℕ0))
110	109	impcom 445	. . . . . . . . . . . . . 14 ⊢ ((((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → (𝑥 + 𝑀) ∈ ℕ0)
111	92	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) → 𝐿 ∈ ℤ)
112	111	3ad2ant1 1075	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → 𝐿 ∈ ℤ)
113	112	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → 𝐿 ∈ ℤ)
114		nn0re 11178	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐿 ∈ ℕ0 → 𝐿 ∈ ℝ)
115	114	adantl 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) → 𝐿 ∈ ℝ)
116	115, 58	anim12ci 589	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝐿 ∈ ℝ))
117		df-3an 1033	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ) ↔ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝐿 ∈ ℝ))
118	116, 117	sylibr 223	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ))
119		ltletr 10008	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ) → ((𝑀 < 𝑁 ∧ 𝑁 ≤ 𝐿) → 𝑀 < 𝐿))
120	118, 119	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → ((𝑀 < 𝑁 ∧ 𝑁 ≤ 𝐿) → 𝑀 < 𝐿))
121		elnn0z 11267	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑀 ∈ ℕ0 ↔ (𝑀 ∈ ℤ ∧ 0 ≤ 𝑀))
122		0red 9920	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑀 ∈ ℤ ∧ (𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0)) → 0 ∈ ℝ)
123		zre 11258	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℝ)
124	123	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑀 ∈ ℤ ∧ (𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0)) → 𝑀 ∈ ℝ)
125	115	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑀 ∈ ℤ ∧ (𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0)) → 𝐿 ∈ ℝ)
126		lelttr 10007	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((0 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝐿 ∈ ℝ) → ((0 ≤ 𝑀 ∧ 𝑀 < 𝐿) → 0 < 𝐿))
127	122, 124, 125, 126	syl3anc 1318	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑀 ∈ ℤ ∧ (𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0)) → ((0 ≤ 𝑀 ∧ 𝑀 < 𝐿) → 0 < 𝐿))
128	127	expd 451	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑀 ∈ ℤ ∧ (𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0)) → (0 ≤ 𝑀 → (𝑀 < 𝐿 → 0 < 𝐿)))
129	128	impancom 455	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑀 ∈ ℤ ∧ 0 ≤ 𝑀) → ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) → (𝑀 < 𝐿 → 0 < 𝐿)))
130	121, 129	sylbi 206	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑀 ∈ ℕ0 → ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) → (𝑀 < 𝐿 → 0 < 𝐿)))
131	130	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) → (𝑀 < 𝐿 → 0 < 𝐿)))
132	131	impcom 445	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑀 < 𝐿 → 0 < 𝐿))
133	120, 132	syld 46	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → ((𝑀 < 𝑁 ∧ 𝑁 ≤ 𝐿) → 0 < 𝐿))
134	133	expcomd 453	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑁 ≤ 𝐿 → (𝑀 < 𝑁 → 0 < 𝐿)))
135	134	3impia 1253	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (𝑀 < 𝑁 → 0 < 𝐿))
136	135	imp 444	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → 0 < 𝐿)
137		elnnz 11264	. . . . . . . . . . . . . . . 16 ⊢ (𝐿 ∈ ℕ ↔ (𝐿 ∈ ℤ ∧ 0 < 𝐿))
138	113, 136, 137	sylanbrc 695	. . . . . . . . . . . . . . 15 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → 𝐿 ∈ ℕ)
139	138	ad2antrr 758	. . . . . . . . . . . . . 14 ⊢ ((((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → 𝐿 ∈ ℕ)
140		elfzo0 12376	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↔ (𝑥 ∈ ℕ0 ∧ (𝑁 − 𝑀) ∈ ℕ ∧ 𝑥 < (𝑁 − 𝑀)))
141		nn0readdcl 11234	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑥 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0) → (𝑥 + 𝑀) ∈ ℝ)
142	141	expcom 450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑀 ∈ ℕ0 → (𝑥 ∈ ℕ0 → (𝑥 + 𝑀) ∈ ℝ))
143	142	ad2antrl 760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑥 ∈ ℕ0 → (𝑥 + 𝑀) ∈ ℝ))
144	143	impcom 445	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (𝑥 + 𝑀) ∈ ℝ)
145	26	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → 𝑁 ∈ ℝ)
146	145	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → 𝑁 ∈ ℝ)
147	146	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → 𝑁 ∈ ℝ)
148	114	ad2antrl 760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → 𝐿 ∈ ℝ)
149	144, 147, 148	3jca 1235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → ((𝑥 + 𝑀) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ))
150	149	ex 449	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 ∈ ℕ0 → ((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → ((𝑥 + 𝑀) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ)))
151	150	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀)) → ((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → ((𝑥 + 𝑀) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ)))
152	151	impcom 445	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) ∧ (𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀))) → ((𝑥 + 𝑀) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ))
153	152	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) ∧ (𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀))) ∧ 𝑁 ≤ 𝐿) → ((𝑥 + 𝑀) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ))
154		nn0re 11178	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑥 ∈ ℕ0 → 𝑥 ∈ ℝ)
155	154	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → 𝑥 ∈ ℝ)
156	25	ad2antrl 760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → 𝑀 ∈ ℝ)
157	156	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → 𝑀 ∈ ℝ)
158	155, 157, 147	ltaddsubd 10506	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → ((𝑥 + 𝑀) < 𝑁 ↔ 𝑥 < (𝑁 − 𝑀)))
159		idd 24	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) ∧ 𝑁 ≤ 𝐿) → ((𝑥 + 𝑀) < 𝑁 → (𝑥 + 𝑀) < 𝑁))
160	159	ex 449	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (𝑁 ≤ 𝐿 → ((𝑥 + 𝑀) < 𝑁 → (𝑥 + 𝑀) < 𝑁)))
161	160	com23 84	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → ((𝑥 + 𝑀) < 𝑁 → (𝑁 ≤ 𝐿 → (𝑥 + 𝑀) < 𝑁)))
162	158, 161	sylbird 249	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (𝑥 < (𝑁 − 𝑀) → (𝑁 ≤ 𝐿 → (𝑥 + 𝑀) < 𝑁)))
163	162	impancom 455	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀)) → ((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑁 ≤ 𝐿 → (𝑥 + 𝑀) < 𝑁)))
164	163	impcom 445	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) ∧ (𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀))) → (𝑁 ≤ 𝐿 → (𝑥 + 𝑀) < 𝑁))
165	164	impac 649	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) ∧ (𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀))) ∧ 𝑁 ≤ 𝐿) → ((𝑥 + 𝑀) < 𝑁 ∧ 𝑁 ≤ 𝐿))
166		ltletr 10008	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑥 + 𝑀) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ) → (((𝑥 + 𝑀) < 𝑁 ∧ 𝑁 ≤ 𝐿) → (𝑥 + 𝑀) < 𝐿))
167	153, 165, 166	sylc 63	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) ∧ (𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀))) ∧ 𝑁 ≤ 𝐿) → (𝑥 + 𝑀) < 𝐿)
168	167	exp31 628	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → ((𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀)) → (𝑁 ≤ 𝐿 → (𝑥 + 𝑀) < 𝐿)))
169	168	com23 84	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (𝑁 ≤ 𝐿 → ((𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀)) → (𝑥 + 𝑀) < 𝐿)))
170	169	ex 449	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐿 ∈ ℕ0 → ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑁 ≤ 𝐿 → ((𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀)) → (𝑥 + 𝑀) < 𝐿))))
171	170	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) → ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑁 ≤ 𝐿 → ((𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀)) → (𝑥 + 𝑀) < 𝐿))))
172	171	3imp 1249	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → ((𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀)) → (𝑥 + 𝑀) < 𝐿))
173	172	ad2antrr 758	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) → ((𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀)) → (𝑥 + 𝑀) < 𝐿))
174	173	com12 32	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀)) → (((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) → (𝑥 + 𝑀) < 𝐿))
175	174	3adant2 1073	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℕ0 ∧ (𝑁 − 𝑀) ∈ ℕ ∧ 𝑥 < (𝑁 − 𝑀)) → (((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) → (𝑥 + 𝑀) < 𝐿))
176	140, 175	sylbi 206	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (0..^(𝑁 − 𝑀)) → (((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) → (𝑥 + 𝑀) < 𝐿))
177	176	impcom 445	. . . . . . . . . . . . . 14 ⊢ ((((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → (𝑥 + 𝑀) < 𝐿)
178		elfzo0 12376	. . . . . . . . . . . . . 14 ⊢ ((𝑥 + 𝑀) ∈ (0..^𝐿) ↔ ((𝑥 + 𝑀) ∈ ℕ0 ∧ 𝐿 ∈ ℕ ∧ (𝑥 + 𝑀) < 𝐿))
179	110, 139, 177, 178	syl3anbrc 1239	. . . . . . . . . . . . 13 ⊢ ((((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → (𝑥 + 𝑀) ∈ (0..^𝐿))
180		repswsymb 13372	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0 ∧ (𝑥 + 𝑀) ∈ (0..^𝐿)) → ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀)) = 𝑆)
181	100, 102, 179, 180	syl3anc 1318	. . . . . . . . . . . 12 ⊢ ((((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀)) = 𝑆)
182	181	mpteq2dva 4672	. . . . . . . . . . 11 ⊢ (((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) → (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))) = (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ 𝑆))
183	34	3ad2ant2 1076	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (𝑁 − 𝑀) ∈ ℤ)
184	183	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (𝑁 − 𝑀) ∈ ℤ)
185	58	3ad2ant2 1076	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ))
186		ltle 10005	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑀 < 𝑁 → 𝑀 ≤ 𝑁))
187	185, 186	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (𝑀 < 𝑁 → 𝑀 ≤ 𝑁))
188	27	3ad2ant2 1076	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ))
189	188, 56	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (0 ≤ (𝑁 − 𝑀) ↔ 𝑀 ≤ 𝑁))
190	187, 189	sylibrd 248	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (𝑀 < 𝑁 → 0 ≤ (𝑁 − 𝑀)))
191	190	imp 444	. . . . . . . . . . . . . . 15 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → 0 ≤ (𝑁 − 𝑀))
192	184, 191, 55	sylanbrc 695	. . . . . . . . . . . . . 14 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (𝑁 − 𝑀) ∈ ℕ0)
193	99, 192	jca 553	. . . . . . . . . . . . 13 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (𝑆 ∈ 𝑉 ∧ (𝑁 − 𝑀) ∈ ℕ0))
194	193	adantr 480	. . . . . . . . . . . 12 ⊢ (((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) → (𝑆 ∈ 𝑉 ∧ (𝑁 − 𝑀) ∈ ℕ0))
195		reps 13368	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ 𝑉 ∧ (𝑁 − 𝑀) ∈ ℕ0) → (𝑆 repeatS (𝑁 − 𝑀)) = (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ 𝑆))
196	195	eqcomd 2616	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ 𝑉 ∧ (𝑁 − 𝑀) ∈ ℕ0) → (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ 𝑆) = (𝑆 repeatS (𝑁 − 𝑀)))
197	194, 196	syl 17	. . . . . . . . . . 11 ⊢ (((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) → (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ 𝑆) = (𝑆 repeatS (𝑁 − 𝑀)))
198	182, 197	eqtrd 2644	. . . . . . . . . 10 ⊢ (((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) → (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))) = (𝑆 repeatS (𝑁 − 𝑀)))
199	198	ex 449	. . . . . . . . 9 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → ((0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿) → (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))) = (𝑆 repeatS (𝑁 − 𝑀))))
200	98, 199	sylbid 229	. . . . . . . 8 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → ((𝑀..^𝑁) ⊆ (0..^𝐿) → (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))) = (𝑆 repeatS (𝑁 − 𝑀))))
201	200	impcom 445	. . . . . . 7 ⊢ (((𝑀..^𝑁) ⊆ (0..^𝐿) ∧ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁)) → (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))) = (𝑆 repeatS (𝑁 − 𝑀)))
202	88, 201	eqtrd 2644	. . . . . 6 ⊢ (((𝑀..^𝑁) ⊆ (0..^𝐿) ∧ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁)) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁 − 𝑀)))
203		iffalse 4045	. . . . . . . 8 ⊢ (¬ (𝑀..^𝑁) ⊆ (0..^𝐿) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = ∅)
204	203	adantr 480	. . . . . . 7 ⊢ ((¬ (𝑀..^𝑁) ⊆ (0..^𝐿) ∧ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁)) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = ∅)
205	98	notbid 307	. . . . . . . . 9 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (¬ (𝑀..^𝑁) ⊆ (0..^𝐿) ↔ ¬ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)))
206		ianor 508	. . . . . . . . . . 11 ⊢ (¬ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿) ↔ (¬ 0 ≤ 𝑀 ∨ ¬ 𝑁 ≤ 𝐿))
207		nn0ge0 11195	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 ∈ ℕ0 → 0 ≤ 𝑀)
208		pm2.24 120	. . . . . . . . . . . . . . . . 17 ⊢ (0 ≤ 𝑀 → (¬ 0 ≤ 𝑀 → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
209	207, 208	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑀 ∈ ℕ0 → (¬ 0 ≤ 𝑀 → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
210	209	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (¬ 0 ≤ 𝑀 → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
211	210	3ad2ant2 1076	. . . . . . . . . . . . . 14 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (¬ 0 ≤ 𝑀 → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
212	211	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (¬ 0 ≤ 𝑀 → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
213	212	com12 32	. . . . . . . . . . . 12 ⊢ (¬ 0 ≤ 𝑀 → ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
214		pm2.24 120	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ≤ 𝐿 → (¬ 𝑁 ≤ 𝐿 → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
215	214	3ad2ant3 1077	. . . . . . . . . . . . . 14 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (¬ 𝑁 ≤ 𝐿 → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
216	215	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (¬ 𝑁 ≤ 𝐿 → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
217	216	com12 32	. . . . . . . . . . . 12 ⊢ (¬ 𝑁 ≤ 𝐿 → ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
218	213, 217	jaoi 393	. . . . . . . . . . 11 ⊢ ((¬ 0 ≤ 𝑀 ∨ ¬ 𝑁 ≤ 𝐿) → ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
219	206, 218	sylbi 206	. . . . . . . . . 10 ⊢ (¬ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿) → ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
220	219	com12 32	. . . . . . . . 9 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (¬ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿) → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
221	205, 220	sylbid 229	. . . . . . . 8 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (¬ (𝑀..^𝑁) ⊆ (0..^𝐿) → (𝑆 repeatS (𝑁 − 𝑀)) = ∅))
222	221	impcom 445	. . . . . . 7 ⊢ ((¬ (𝑀..^𝑁) ⊆ (0..^𝐿) ∧ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁)) → (𝑆 repeatS (𝑁 − 𝑀)) = ∅)
223	204, 222	eqtr4d 2647	. . . . . 6 ⊢ ((¬ (𝑀..^𝑁) ⊆ (0..^𝐿) ∧ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁)) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁 − 𝑀)))
224	202, 223	pm2.61ian 827	. . . . 5 ⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁 − 𝑀)))
225	224	ex 449	. . . 4 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (𝑀 < 𝑁 → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁 − 𝑀))))
226	87, 225	sylbid 229	. . 3 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → (¬ 𝑁 ≤ 𝑀 → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁 − 𝑀))))
227	83, 226	pm2.61d 169	. 2 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁 − 𝑀)))
228	10, 16, 227	3eqtrd 2648	1 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → ((𝑆 repeatS 𝐿) substr ⟨𝑀, 𝑁⟩) = (𝑆 repeatS (𝑁 − 𝑀)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977   ∉ wnel 2781   ⊆ wss 3540  ∅c0 3874  ifcif 4036  ⟨cop 4131   class class class wbr 4583   ↦ cmpt 4643  dom cdm 5038  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549  ℂcc 9813  ℝcr 9814  0cc0 9815   + caddc 9818   < clt 9953   ≤ cle 9954   − cmin 10145  ℕcn 10897  ℕ₀cn0 11169  ℤcz 11254  ..^cfzo 12334  Word cword 13146   substr csubstr 13150   repeatS creps 13153

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-card 8648  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-nn 10898  df-n0 11170  df-z 11255  df-uz 11564  df-fz 12198  df-fzo 12335  df-hash 12980  df-word 13154  df-substr 13158  df-reps 13161

This theorem is referenced by:  repswcshw  13409