Theorem swrdccat 11262

Description: The subword of a concatenation of two words as concatenation of subwords of the two concatenated words. (Contributed by Alexander van der Vekens, 29-May-2018.)

Hypothesis

Ref	Expression
swrdccatin2.l	⊢ 𝐿 = (♯‘𝐴)

Assertion

Ref	Expression
swrdccat	⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(𝐿 + (♯‘𝐵)))) → ((𝐴 ++ 𝐵) substr ⟨𝑀, 𝑁⟩) = ((𝐴 substr ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩) ++ (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩))))

Proof of Theorem swrdccat

Step	Hyp	Ref	Expression
1		swrdccatin2.l	. . . . 5 ⊢ 𝐿 = (♯‘𝐴)
2	1	pfxccat3 11261	. . . 4 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(𝐿 + (♯‘𝐵)))) → ((𝐴 ++ 𝐵) substr ⟨𝑀, 𝑁⟩) = if(𝑁 ≤ 𝐿, (𝐴 substr ⟨𝑀, 𝑁⟩), if(𝐿 ≤ 𝑀, (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿)))))))
3	2	imp 124	. . 3 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(𝐿 + (♯‘𝐵))))) → ((𝐴 ++ 𝐵) substr ⟨𝑀, 𝑁⟩) = if(𝑁 ≤ 𝐿, (𝐴 substr ⟨𝑀, 𝑁⟩), if(𝐿 ≤ 𝑀, (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿))))))
4		lencl 11070	. . . . . 6 ⊢ (𝐴 ∈ Word 𝑉 → (♯‘𝐴) ∈ ℕ0)
5	4	adantr 276	. . . . 5 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (♯‘𝐴) ∈ ℕ0)
6	1	eqcomi 2233	. . . . . . 7 ⊢ (♯‘𝐴) = 𝐿
7	6	eleq1i 2295	. . . . . 6 ⊢ ((♯‘𝐴) ∈ ℕ0 ↔ 𝐿 ∈ ℕ0)
8		elfz2nn0 10304	. . . . . . . . 9 ⊢ (𝑀 ∈ (0...𝑁) ↔ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁))
9		iftrue 3607	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ≤ 𝐿 → if(𝑁 ≤ 𝐿, 𝑁, 𝐿) = 𝑁)
10	9	adantl 277	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → if(𝑁 ≤ 𝐿, 𝑁, 𝐿) = 𝑁)
11	10	opeq2d 3863	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩ = ⟨𝑀, 𝑁⟩)
12	11	oveq2d 6016	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → (𝐴 substr ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩) = (𝐴 substr ⟨𝑀, 𝑁⟩))
13		0z 9453	. . . . . . . . . . . . . . . . 17 ⊢ 0 ∈ ℤ
14		simprll 537	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → 𝑀 ∈ ℕ0)
15	14	adantr 276	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → 𝑀 ∈ ℕ0)
16	15	nn0zd 9563	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → 𝑀 ∈ ℤ)
17		simplrr 536	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → 𝐿 ∈ ℕ0)
18	17	nn0zd 9563	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → 𝐿 ∈ ℤ)
19	16, 18	zsubcld 9570	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → (𝑀 − 𝐿) ∈ ℤ)
20		zdcle 9519	. . . . . . . . . . . . . . . . 17 ⊢ ((0 ∈ ℤ ∧ (𝑀 − 𝐿) ∈ ℤ) → DECID 0 ≤ (𝑀 − 𝐿))
21	13, 19, 20	sylancr 414	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → DECID 0 ≤ (𝑀 − 𝐿))
22		exmiddc 841	. . . . . . . . . . . . . . . . 17 ⊢ (DECID 0 ≤ (𝑀 − 𝐿) → (0 ≤ (𝑀 − 𝐿) ∨ ¬ 0 ≤ (𝑀 − 𝐿)))
23		iftrue 3607	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (0 ≤ (𝑀 − 𝐿) → if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0) = (𝑀 − 𝐿))
24	23	opeq1d 3862	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (0 ≤ (𝑀 − 𝐿) → ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩ = ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩)
25	24	oveq2d 6016	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (0 ≤ (𝑀 − 𝐿) → (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩) = (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩))
26	25	adantr 276	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((0 ≤ (𝑀 − 𝐿) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿)) → (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩) = (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩))
27		simpr 110	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → 𝐵 ∈ Word 𝑉)
28		nn0z 9462	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐿 ∈ ℕ0 → 𝐿 ∈ ℤ)
29		nn0z 9462	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑀 ∈ ℕ0 → 𝑀 ∈ ℤ)
30	29	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → 𝑀 ∈ ℤ)
31		zsubcl 9483	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑀 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝑀 − 𝐿) ∈ ℤ)
32	30, 31	sylan 283	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℤ) → (𝑀 − 𝐿) ∈ ℤ)
33		nn0z 9462	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ)
34	33	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → 𝑁 ∈ ℤ)
35		zsubcl 9483	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝑁 − 𝐿) ∈ ℤ)
36	34, 35	sylan 283	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℤ) → (𝑁 − 𝐿) ∈ ℤ)
37	32, 36	jca 306	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℤ) → ((𝑀 − 𝐿) ∈ ℤ ∧ (𝑁 − 𝐿) ∈ ℤ))
38	28, 37	sylan2 286	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) → ((𝑀 − 𝐿) ∈ ℤ ∧ (𝑁 − 𝐿) ∈ ℤ))
39	27, 38	anim12i 338	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → (𝐵 ∈ Word 𝑉 ∧ ((𝑀 − 𝐿) ∈ ℤ ∧ (𝑁 − 𝐿) ∈ ℤ)))
40		3anass 1006	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐵 ∈ Word 𝑉 ∧ (𝑀 − 𝐿) ∈ ℤ ∧ (𝑁 − 𝐿) ∈ ℤ) ↔ (𝐵 ∈ Word 𝑉 ∧ ((𝑀 − 𝐿) ∈ ℤ ∧ (𝑁 − 𝐿) ∈ ℤ)))
41	39, 40	sylibr 134	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → (𝐵 ∈ Word 𝑉 ∧ (𝑀 − 𝐿) ∈ ℤ ∧ (𝑁 − 𝐿) ∈ ℤ))
42	41	ad2antrl 490	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((0 ≤ (𝑀 − 𝐿) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿)) → (𝐵 ∈ Word 𝑉 ∧ (𝑀 − 𝐿) ∈ ℤ ∧ (𝑁 − 𝐿) ∈ ℤ))
43		nn0re 9374	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑀 ∈ ℕ0 → 𝑀 ∈ ℝ)
44		nn0re 9374	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ)
45	43, 44	anim12i 338	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ))
46		nn0re 9374	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐿 ∈ ℕ0 → 𝐿 ∈ ℝ)
47		subge0 8618	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑀 ∈ ℝ ∧ 𝐿 ∈ ℝ) → (0 ≤ (𝑀 − 𝐿) ↔ 𝐿 ≤ 𝑀))
48	47	adantlr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝐿 ∈ ℝ) → (0 ≤ (𝑀 − 𝐿) ↔ 𝐿 ≤ 𝑀))
49		simplr 528	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝐿 ∈ ℝ) → 𝑁 ∈ ℝ)
50		simpr 110	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝐿 ∈ ℝ) → 𝐿 ∈ ℝ)
51		simpll 527	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝐿 ∈ ℝ) → 𝑀 ∈ ℝ)
52		letr 8225	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ ∧ 𝑀 ∈ ℝ) → ((𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀) → 𝑁 ≤ 𝑀))
53	49, 50, 51, 52	syl3anc 1271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝐿 ∈ ℝ) → ((𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀) → 𝑁 ≤ 𝑀))
54	53	expcomd 1484	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝐿 ∈ ℝ) → (𝐿 ≤ 𝑀 → (𝑁 ≤ 𝐿 → 𝑁 ≤ 𝑀)))
55	48, 54	sylbid 150	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝐿 ∈ ℝ) → (0 ≤ (𝑀 − 𝐿) → (𝑁 ≤ 𝐿 → 𝑁 ≤ 𝑀)))
56	55	com23 78	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝐿 ∈ ℝ) → (𝑁 ≤ 𝐿 → (0 ≤ (𝑀 − 𝐿) → 𝑁 ≤ 𝑀)))
57	45, 46, 56	syl2an 289	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) → (𝑁 ≤ 𝐿 → (0 ≤ (𝑀 − 𝐿) → 𝑁 ≤ 𝑀)))
58	57	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → (𝑁 ≤ 𝐿 → (0 ≤ (𝑀 − 𝐿) → 𝑁 ≤ 𝑀)))
59	58	imp 124	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → (0 ≤ (𝑀 − 𝐿) → 𝑁 ≤ 𝑀))
60	59	impcom 125	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((0 ≤ (𝑀 − 𝐿) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿)) → 𝑁 ≤ 𝑀)
61	44	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → 𝑁 ∈ ℝ)
62	61	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) → 𝑁 ∈ ℝ)
63	43	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → 𝑀 ∈ ℝ)
64	63	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) → 𝑀 ∈ ℝ)
65	46	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) → 𝐿 ∈ ℝ)
66	62, 64, 65	3jca 1201	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) → (𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝐿 ∈ ℝ))
67	66	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → (𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝐿 ∈ ℝ))
68	67	ad2antrl 490	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((0 ≤ (𝑀 − 𝐿) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿)) → (𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝐿 ∈ ℝ))
69		lesub1 8599	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝐿 ∈ ℝ) → (𝑁 ≤ 𝑀 ↔ (𝑁 − 𝐿) ≤ (𝑀 − 𝐿)))
70	68, 69	syl 14	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((0 ≤ (𝑀 − 𝐿) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿)) → (𝑁 ≤ 𝑀 ↔ (𝑁 − 𝐿) ≤ (𝑀 − 𝐿)))
71	60, 70	mpbid 147	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((0 ≤ (𝑀 − 𝐿) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿)) → (𝑁 − 𝐿) ≤ (𝑀 − 𝐿))
72		swrdlend 11185	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐵 ∈ Word 𝑉 ∧ (𝑀 − 𝐿) ∈ ℤ ∧ (𝑁 − 𝐿) ∈ ℤ) → ((𝑁 − 𝐿) ≤ (𝑀 − 𝐿) → (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩) = ∅))
73	42, 71, 72	sylc 62	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((0 ≤ (𝑀 − 𝐿) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿)) → (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩) = ∅)
74	26, 73	eqtrd 2262	. . . . . . . . . . . . . . . . . . 19 ⊢ ((0 ≤ (𝑀 − 𝐿) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿)) → (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩) = ∅)
75	74	ex 115	. . . . . . . . . . . . . . . . . 18 ⊢ (0 ≤ (𝑀 − 𝐿) → ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩) = ∅))
76		iffalse 3610	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ 0 ≤ (𝑀 − 𝐿) → if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0) = 0)
77	76	opeq1d 3862	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ 0 ≤ (𝑀 − 𝐿) → ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩ = ⟨0, (𝑁 − 𝐿)⟩)
78	77	oveq2d 6016	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ 0 ≤ (𝑀 − 𝐿) → (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩) = (𝐵 substr ⟨0, (𝑁 − 𝐿)⟩))
79		simplr 528	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → 𝐵 ∈ Word 𝑉)
80	79	adantr 276	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → 𝐵 ∈ Word 𝑉)
81		0zd 9454	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → 0 ∈ ℤ)
82	34, 28, 35	syl2an 289	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) → (𝑁 − 𝐿) ∈ ℤ)
83	82	adantl 277	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → (𝑁 − 𝐿) ∈ ℤ)
84	83	adantr 276	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → (𝑁 − 𝐿) ∈ ℤ)
85	80, 81, 84	3jca 1201	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → (𝐵 ∈ Word 𝑉 ∧ 0 ∈ ℤ ∧ (𝑁 − 𝐿) ∈ ℤ))
86	61, 46	anim12i 338	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) → (𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ))
87	86	adantl 277	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → (𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ))
88		suble0 8619	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ) → ((𝑁 − 𝐿) ≤ 0 ↔ 𝑁 ≤ 𝐿))
89	87, 88	syl 14	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → ((𝑁 − 𝐿) ≤ 0 ↔ 𝑁 ≤ 𝐿))
90	89	biimpar 297	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → (𝑁 − 𝐿) ≤ 0)
91		swrdlend 11185	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐵 ∈ Word 𝑉 ∧ 0 ∈ ℤ ∧ (𝑁 − 𝐿) ∈ ℤ) → ((𝑁 − 𝐿) ≤ 0 → (𝐵 substr ⟨0, (𝑁 − 𝐿)⟩) = ∅))
92	85, 90, 91	sylc 62	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → (𝐵 substr ⟨0, (𝑁 − 𝐿)⟩) = ∅)
93	78, 92	sylan9eq 2282	. . . . . . . . . . . . . . . . . . 19 ⊢ ((¬ 0 ≤ (𝑀 − 𝐿) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿)) → (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩) = ∅)
94	93	ex 115	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ 0 ≤ (𝑀 − 𝐿) → ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩) = ∅))
95	75, 94	jaoi 721	. . . . . . . . . . . . . . . . 17 ⊢ ((0 ≤ (𝑀 − 𝐿) ∨ ¬ 0 ≤ (𝑀 − 𝐿)) → ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩) = ∅))
96	22, 95	syl 14	. . . . . . . . . . . . . . . 16 ⊢ (DECID 0 ≤ (𝑀 − 𝐿) → ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩) = ∅))
97	21, 96	mpcom 36	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩) = ∅)
98	12, 97	oveq12d 6018	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → ((𝐴 substr ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩) ++ (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩)) = ((𝐴 substr ⟨𝑀, 𝑁⟩) ++ ∅))
99		simpll 527	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → 𝐴 ∈ Word 𝑉)
100	14	nn0zd 9563	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → 𝑀 ∈ ℤ)
101	34	ad2antrl 490	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → 𝑁 ∈ ℤ)
102		swrdclg 11177	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 substr ⟨𝑀, 𝑁⟩) ∈ Word 𝑉)
103	99, 100, 101, 102	syl3anc 1271	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → (𝐴 substr ⟨𝑀, 𝑁⟩) ∈ Word 𝑉)
104		ccatrid 11137	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 substr ⟨𝑀, 𝑁⟩) ∈ Word 𝑉 → ((𝐴 substr ⟨𝑀, 𝑁⟩) ++ ∅) = (𝐴 substr ⟨𝑀, 𝑁⟩))
105	103, 104	syl 14	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → ((𝐴 substr ⟨𝑀, 𝑁⟩) ++ ∅) = (𝐴 substr ⟨𝑀, 𝑁⟩))
106	105	adantr 276	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → ((𝐴 substr ⟨𝑀, 𝑁⟩) ++ ∅) = (𝐴 substr ⟨𝑀, 𝑁⟩))
107	98, 106	eqtrd 2262	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → ((𝐴 substr ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩) ++ (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩)) = (𝐴 substr ⟨𝑀, 𝑁⟩))
108		iffalse 3610	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ 𝑁 ≤ 𝐿 → if(𝑁 ≤ 𝐿, 𝑁, 𝐿) = 𝐿)
109	108	3ad2ant2 1043	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀) → if(𝑁 ≤ 𝐿, 𝑁, 𝐿) = 𝐿)
110	109	opeq2d 3863	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀) → ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩ = ⟨𝑀, 𝐿⟩)
111	110	oveq2d 6016	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀) → (𝐴 substr ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩) = (𝐴 substr ⟨𝑀, 𝐿⟩))
112		simpl 109	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → 𝐴 ∈ Word 𝑉)
113	112, 30, 28	3anim123i 1208	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) → (𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝐿 ∈ ℤ))
114	113	3expb 1228	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → (𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝐿 ∈ ℤ))
115		swrdlend 11185	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝐿 ≤ 𝑀 → (𝐴 substr ⟨𝑀, 𝐿⟩) = ∅))
116	114, 115	syl 14	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → (𝐿 ≤ 𝑀 → (𝐴 substr ⟨𝑀, 𝐿⟩) = ∅))
117	116	imp 124	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝐿 ≤ 𝑀) → (𝐴 substr ⟨𝑀, 𝐿⟩) = ∅)
118	117	3adant2 1040	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀) → (𝐴 substr ⟨𝑀, 𝐿⟩) = ∅)
119	111, 118	eqtrd 2262	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀) → (𝐴 substr ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩) = ∅)
120	63, 46, 47	syl2an 289	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) → (0 ≤ (𝑀 − 𝐿) ↔ 𝐿 ≤ 𝑀))
121	120	biimprd 158	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) → (𝐿 ≤ 𝑀 → 0 ≤ (𝑀 − 𝐿)))
122	121	adantl 277	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → (𝐿 ≤ 𝑀 → 0 ≤ (𝑀 − 𝐿)))
123	122	imp 124	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝐿 ≤ 𝑀) → 0 ≤ (𝑀 − 𝐿))
124	123	3adant2 1040	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀) → 0 ≤ (𝑀 − 𝐿))
125	124, 24	syl 14	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀) → ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩ = ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩)
126	125	oveq2d 6016	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀) → (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩) = (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩))
127	119, 126	oveq12d 6018	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀) → ((𝐴 substr ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩) ++ (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩)) = (∅ ++ (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩)))
128		swrdclg 11177	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ∈ Word 𝑉 ∧ (𝑀 − 𝐿) ∈ ℤ ∧ (𝑁 − 𝐿) ∈ ℤ) → (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩) ∈ Word 𝑉)
129		ccatlid 11136	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩) ∈ Word 𝑉 → (∅ ++ (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩)) = (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩))
130	41, 128, 129	3syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → (∅ ++ (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩)) = (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩))
131	130	3ad2ant1 1042	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀) → (∅ ++ (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩)) = (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩))
132	127, 131	eqtrd 2262	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀) → ((𝐴 substr ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩) ++ (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩)) = (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩))
133	108	3ad2ant2 1043	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀) → if(𝑁 ≤ 𝐿, 𝑁, 𝐿) = 𝐿)
134	133	opeq2d 3863	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀) → ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩ = ⟨𝑀, 𝐿⟩)
135	134	oveq2d 6016	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀) → (𝐴 substr ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩) = (𝐴 substr ⟨𝑀, 𝐿⟩))
136	43, 46, 47	syl2an 289	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0) → (0 ≤ (𝑀 − 𝐿) ↔ 𝐿 ≤ 𝑀))
137	136	adantlr 477	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) → (0 ≤ (𝑀 − 𝐿) ↔ 𝐿 ≤ 𝑀))
138	137	adantl 277	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → (0 ≤ (𝑀 − 𝐿) ↔ 𝐿 ≤ 𝑀))
139	138	biimpd 144	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → (0 ≤ (𝑀 − 𝐿) → 𝐿 ≤ 𝑀))
140	139	con3dimp 638	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝐿 ≤ 𝑀) → ¬ 0 ≤ (𝑀 − 𝐿))
141	140	3adant2 1040	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀) → ¬ 0 ≤ (𝑀 − 𝐿))
142	141, 76	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀) → if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0) = 0)
143	142	opeq1d 3862	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀) → ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩ = ⟨0, (𝑁 − 𝐿)⟩)
144	143	oveq2d 6016	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀) → (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩) = (𝐵 substr ⟨0, (𝑁 − 𝐿)⟩))
145	79	3ad2ant1 1042	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀) → 𝐵 ∈ Word 𝑉)
146		simplrr 536	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿) → 𝐿 ∈ ℕ0)
147		simprlr 538	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → 𝑁 ∈ ℕ0)
148	147	adantr 276	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿) → 𝑁 ∈ ℕ0)
149		zltnle 9488	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐿 < 𝑁 ↔ ¬ 𝑁 ≤ 𝐿))
150	28, 34, 149	syl2anr 290	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) → (𝐿 < 𝑁 ↔ ¬ 𝑁 ≤ 𝐿))
151		ltle 8230	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐿 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝐿 < 𝑁 → 𝐿 ≤ 𝑁))
152	46, 61, 151	syl2anr 290	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) → (𝐿 < 𝑁 → 𝐿 ≤ 𝑁))
153	150, 152	sylbird 170	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) → (¬ 𝑁 ≤ 𝐿 → 𝐿 ≤ 𝑁))
154	153	adantl 277	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → (¬ 𝑁 ≤ 𝐿 → 𝐿 ≤ 𝑁))
155	154	imp 124	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿) → 𝐿 ≤ 𝑁)
156		nn0sub2 9516	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐿 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ≤ 𝑁) → (𝑁 − 𝐿) ∈ ℕ0)
157	146, 148, 155, 156	syl3anc 1271	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿) → (𝑁 − 𝐿) ∈ ℕ0)
158	157	3adant3 1041	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀) → (𝑁 − 𝐿) ∈ ℕ0)
159		pfxval 11201	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ∈ Word 𝑉 ∧ (𝑁 − 𝐿) ∈ ℕ0) → (𝐵 prefix (𝑁 − 𝐿)) = (𝐵 substr ⟨0, (𝑁 − 𝐿)⟩))
160	145, 158, 159	syl2anc 411	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀) → (𝐵 prefix (𝑁 − 𝐿)) = (𝐵 substr ⟨0, (𝑁 − 𝐿)⟩))
161	144, 160	eqtr4d 2265	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀) → (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩) = (𝐵 prefix (𝑁 − 𝐿)))
162	135, 161	oveq12d 6018	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀) → ((𝐴 substr ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩) ++ (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩)) = ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿))))
163	28	ad2antll 491	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → 𝐿 ∈ ℤ)
164		zdcle 9519	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ) → DECID 𝑁 ≤ 𝐿)
165	101, 163, 164	syl2anc 411	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → DECID 𝑁 ≤ 𝐿)
166	146	nn0zd 9563	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿) → 𝐿 ∈ ℤ)
167	100	adantr 276	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿) → 𝑀 ∈ ℤ)
168		zdcle 9519	. . . . . . . . . . . . . 14 ⊢ ((𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ) → DECID 𝐿 ≤ 𝑀)
169	166, 167, 168	syl2anc 411	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿) → DECID 𝐿 ≤ 𝑀)
170	107, 132, 162, 165, 169	2if2dc 3642	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → ((𝐴 substr ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩) ++ (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩)) = if(𝑁 ≤ 𝐿, (𝐴 substr ⟨𝑀, 𝑁⟩), if(𝐿 ≤ 𝑀, (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿))))))
171	170	exp32 365	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝐿 ∈ ℕ0 → ((𝐴 substr ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩) ++ (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩)) = if(𝑁 ≤ 𝐿, (𝐴 substr ⟨𝑀, 𝑁⟩), if(𝐿 ≤ 𝑀, (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿))))))))
172	171	com12 30	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (𝐿 ∈ ℕ0 → ((𝐴 substr ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩) ++ (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩)) = if(𝑁 ≤ 𝐿, (𝐴 substr ⟨𝑀, 𝑁⟩), if(𝐿 ≤ 𝑀, (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿))))))))
173	172	3adant3 1041	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁) → ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (𝐿 ∈ ℕ0 → ((𝐴 substr ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩) ++ (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩)) = if(𝑁 ≤ 𝐿, (𝐴 substr ⟨𝑀, 𝑁⟩), if(𝐿 ≤ 𝑀, (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿))))))))
174	8, 173	sylbi 121	. . . . . . . 8 ⊢ (𝑀 ∈ (0...𝑁) → ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (𝐿 ∈ ℕ0 → ((𝐴 substr ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩) ++ (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩)) = if(𝑁 ≤ 𝐿, (𝐴 substr ⟨𝑀, 𝑁⟩), if(𝐿 ≤ 𝑀, (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿))))))))
175	174	adantr 276	. . . . . . 7 ⊢ ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(𝐿 + (♯‘𝐵)))) → ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (𝐿 ∈ ℕ0 → ((𝐴 substr ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩) ++ (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩)) = if(𝑁 ≤ 𝐿, (𝐴 substr ⟨𝑀, 𝑁⟩), if(𝐿 ≤ 𝑀, (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿))))))))
176	175	com13 80	. . . . . 6 ⊢ (𝐿 ∈ ℕ0 → ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(𝐿 + (♯‘𝐵)))) → ((𝐴 substr ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩) ++ (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩)) = if(𝑁 ≤ 𝐿, (𝐴 substr ⟨𝑀, 𝑁⟩), if(𝐿 ≤ 𝑀, (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿))))))))
177	7, 176	sylbi 121	. . . . 5 ⊢ ((♯‘𝐴) ∈ ℕ0 → ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(𝐿 + (♯‘𝐵)))) → ((𝐴 substr ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩) ++ (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩)) = if(𝑁 ≤ 𝐿, (𝐴 substr ⟨𝑀, 𝑁⟩), if(𝐿 ≤ 𝑀, (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿))))))))
178	5, 177	mpcom 36	. . . 4 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(𝐿 + (♯‘𝐵)))) → ((𝐴 substr ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩) ++ (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩)) = if(𝑁 ≤ 𝐿, (𝐴 substr ⟨𝑀, 𝑁⟩), if(𝐿 ≤ 𝑀, (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿)))))))
179	178	imp 124	. . 3 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(𝐿 + (♯‘𝐵))))) → ((𝐴 substr ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩) ++ (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩)) = if(𝑁 ≤ 𝐿, (𝐴 substr ⟨𝑀, 𝑁⟩), if(𝐿 ≤ 𝑀, (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿))))))
180	3, 179	eqtr4d 2265	. 2 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(𝐿 + (♯‘𝐵))))) → ((𝐴 ++ 𝐵) substr ⟨𝑀, 𝑁⟩) = ((𝐴 substr ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩) ++ (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩)))
181	180	ex 115	1 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(𝐿 + (♯‘𝐵)))) → ((𝐴 ++ 𝐵) substr ⟨𝑀, 𝑁⟩) = ((𝐴 substr ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩) ++ (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩))))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ↔ wb 105   ∨ wo 713  DECID wdc 839   ∧ w3a 1002   = wceq 1395   ∈ wcel 2200  ∅c0 3491  ifcif 3602  ⟨cop 3669   class class class wbr 4082  ‘cfv 5317  (class class class)co 6000  ℝcr 7994  0cc0 7995   + caddc 7998   < clt 8177   ≤ cle 8178   − cmin 8313  ℕ₀cn0 9365  ℤcz 9442  ...cfz 10200  ♯chash 10992  Word cword 11066   ++ cconcat 11120   substr csubstr 11172   prefix cpfx 11199

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-coll 4198  ax-sep 4201  ax-nul 4209  ax-pow 4257  ax-pr 4292  ax-un 4523  ax-setind 4628  ax-iinf 4679  ax-cnex 8086  ax-resscn 8087  ax-1cn 8088  ax-1re 8089  ax-icn 8090  ax-addcl 8091  ax-addrcl 8092  ax-mulcl 8093  ax-addcom 8095  ax-addass 8097  ax-distr 8099  ax-i2m1 8100  ax-0lt1 8101  ax-0id 8103  ax-rnegex 8104  ax-cnre 8106  ax-pre-ltirr 8107  ax-pre-ltwlin 8108  ax-pre-lttrn 8109  ax-pre-apti 8110  ax-pre-ltadd 8111

This theorem depends on definitions:  df-bi 117  df-dc 840  df-3or 1003  df-3an 1004  df-tru 1398  df-fal 1401  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ne 2401  df-nel 2496  df-ral 2513  df-rex 2514  df-reu 2515  df-rab 2517  df-v 2801  df-sbc 3029  df-csb 3125  df-dif 3199  df-un 3201  df-in 3203  df-ss 3210  df-nul 3492  df-if 3603  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3888  df-int 3923  df-iun 3966  df-br 4083  df-opab 4145  df-mpt 4146  df-tr 4182  df-id 4383  df-iord 4456  df-on 4458  df-ilim 4459  df-suc 4461  df-iom 4682  df-xp 4724  df-rel 4725  df-cnv 4726  df-co 4727  df-dm 4728  df-rn 4729  df-res 4730  df-ima 4731  df-iota 5277  df-fun 5319  df-fn 5320  df-f 5321  df-f1 5322  df-fo 5323  df-f1o 5324  df-fv 5325  df-riota 5953  df-ov 6003  df-oprab 6004  df-mpo 6005  df-1st 6284  df-2nd 6285  df-recs 6449  df-frec 6535  df-1o 6560  df-er 6678  df-en 6886  df-dom 6887  df-fin 6888  df-pnf 8179  df-mnf 8180  df-xr 8181  df-ltxr 8182  df-le 8183  df-sub 8315  df-neg 8316  df-inn 9107  df-n0 9366  df-z 9443  df-uz 9719  df-fz 10201  df-fzo 10335  df-ihash 10993  df-word 11067  df-concat 11121  df-substr 11173  df-pfx 11200

This theorem is referenced by: (None)