Theorem swrdccat 11427

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 11426	. . . 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 11228	. . . . . 6 ⊢ (𝐴 ∈ Word 𝑉 → (♯‘𝐴) ∈ ℕ0)
5	4	adantr 276	. . . . 5 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (♯‘𝐴) ∈ ℕ0)
6	1	eqcomi 2236	. . . . . . 7 ⊢ (♯‘𝐴) = 𝐿
7	6	eleq1i 2298	. . . . . 6 ⊢ ((♯‘𝐴) ∈ ℕ0 ↔ 𝐿 ∈ ℕ0)
8		elfz2nn0 10446	. . . . . . . . 9 ⊢ (𝑀 ∈ (0...𝑁) ↔ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁))
9		iftrue 3627	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ≤ 𝐿 → if(𝑁 ≤ 𝐿, 𝑁, 𝐿) = 𝑁)
10	9	adantl 277	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → if(𝑁 ≤ 𝐿, 𝑁, 𝐿) = 𝑁)
11	10	opeq2d 3890	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩ = ⟨𝑀, 𝑁⟩)
12	11	oveq2d 6066	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → (𝐴 substr ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩) = (𝐴 substr ⟨𝑀, 𝑁⟩))
13		0z 9588	. . . . . . . . . . . . . . . . 17 ⊢ 0 ∈ ℤ
14		simprll 539	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → 𝑀 ∈ ℕ0)
15	14	adantr 276	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → 𝑀 ∈ ℕ0)
16	15	nn0zd 9698	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → 𝑀 ∈ ℤ)
17		simplrr 538	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → 𝐿 ∈ ℕ0)
18	17	nn0zd 9698	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → 𝐿 ∈ ℤ)
19	16, 18	zsubcld 9705	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → (𝑀 − 𝐿) ∈ ℤ)
20		zdcle 9654	. . . . . . . . . . . . . . . . 17 ⊢ ((0 ∈ ℤ ∧ (𝑀 − 𝐿) ∈ ℤ) → DECID 0 ≤ (𝑀 − 𝐿))
21	13, 19, 20	sylancr 414	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → DECID 0 ≤ (𝑀 − 𝐿))
22		exmiddc 844	. . . . . . . . . . . . . . . . 17 ⊢ (DECID 0 ≤ (𝑀 − 𝐿) → (0 ≤ (𝑀 − 𝐿) ∨ ¬ 0 ≤ (𝑀 − 𝐿)))
23		iftrue 3627	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (0 ≤ (𝑀 − 𝐿) → if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0) = (𝑀 − 𝐿))
24	23	opeq1d 3889	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (0 ≤ (𝑀 − 𝐿) → ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩ = ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩)
25	24	oveq2d 6066	. . . . . . . . . . . . . . . . . . . . 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 9597	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐿 ∈ ℕ0 → 𝐿 ∈ ℤ)
29		nn0z 9597	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑀 ∈ ℕ0 → 𝑀 ∈ ℤ)
30	29	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → 𝑀 ∈ ℤ)
31		zsubcl 9618	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑀 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝑀 − 𝐿) ∈ ℤ)
32	30, 31	sylan 283	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℤ) → (𝑀 − 𝐿) ∈ ℤ)
33		nn0z 9597	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ)
34	33	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → 𝑁 ∈ ℤ)
35		zsubcl 9618	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 1009	. . . . . . . . . . . . . . . . . . . . . . 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 9505	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑀 ∈ ℕ0 → 𝑀 ∈ ℝ)
44		nn0re 9505	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ)
45	43, 44	anim12i 338	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ))
46		nn0re 9505	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐿 ∈ ℕ0 → 𝐿 ∈ ℝ)
47		subge0 8749	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑀 ∈ ℝ ∧ 𝐿 ∈ ℝ) → (0 ≤ (𝑀 − 𝐿) ↔ 𝐿 ≤ 𝑀))
48	47	adantlr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝐿 ∈ ℝ) → (0 ≤ (𝑀 − 𝐿) ↔ 𝐿 ≤ 𝑀))
49		simplr 529	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝐿 ∈ ℝ) → 𝑁 ∈ ℝ)
50		simpr 110	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝐿 ∈ ℝ) → 𝐿 ∈ ℝ)
51		simpll 527	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝐿 ∈ ℝ) → 𝑀 ∈ ℝ)
52		letr 8356	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ ∧ 𝑀 ∈ ℝ) → ((𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀) → 𝑁 ≤ 𝑀))
53	49, 50, 51, 52	syl3anc 1274	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝐿 ∈ ℝ) → ((𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀) → 𝑁 ≤ 𝑀))
54	53	expcomd 1487	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1204	. . . . . . . . . . . . . . . . . . . . . . . . 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 8730	. . . . . . . . . . . . . . . . . . . . . . 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 11350	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐵 ∈ Word 𝑉 ∧ (𝑀 − 𝐿) ∈ ℤ ∧ (𝑁 − 𝐿) ∈ ℤ) → ((𝑁 − 𝐿) ≤ (𝑀 − 𝐿) → (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩) = ∅))
73	42, 71, 72	sylc 62	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((0 ≤ (𝑀 − 𝐿) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿)) → (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩) = ∅)
74	26, 73	eqtrd 2265	. . . . . . . . . . . . . . . . . . 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 3630	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ 0 ≤ (𝑀 − 𝐿) → if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0) = 0)
77	76	opeq1d 3889	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ 0 ≤ (𝑀 − 𝐿) → ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩ = ⟨0, (𝑁 − 𝐿)⟩)
78	77	oveq2d 6066	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ 0 ≤ (𝑀 − 𝐿) → (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩) = (𝐵 substr ⟨0, (𝑁 − 𝐿)⟩))
79		simplr 529	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → 𝐵 ∈ Word 𝑉)
80	79	adantr 276	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → 𝐵 ∈ Word 𝑉)
81		0zd 9589	. . . . . . . . . . . . . . . . . . . . . 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 1204	. . . . . . . . . . . . . . . . . . . . 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 8750	. . . . . . . . . . . . . . . . . . . . . . 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 11350	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐵 ∈ Word 𝑉 ∧ 0 ∈ ℤ ∧ (𝑁 − 𝐿) ∈ ℤ) → ((𝑁 − 𝐿) ≤ 0 → (𝐵 substr ⟨0, (𝑁 − 𝐿)⟩) = ∅))
92	85, 90, 91	sylc 62	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → (𝐵 substr ⟨0, (𝑁 − 𝐿)⟩) = ∅)
93	78, 92	sylan9eq 2285	. . . . . . . . . . . . . . . . . . 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 724	. . . . . . . . . . . . . . . . 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 6068	. . . . . . . . . . . . . 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 9698	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → 𝑀 ∈ ℤ)
101	34	ad2antrl 490	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → 𝑁 ∈ ℤ)
102		swrdclg 11342	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 substr ⟨𝑀, 𝑁⟩) ∈ Word 𝑉)
103	99, 100, 101, 102	syl3anc 1274	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → (𝐴 substr ⟨𝑀, 𝑁⟩) ∈ Word 𝑉)
104		ccatrid 11295	. . . . . . . . . . . . . . . 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 2265	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → ((𝐴 substr ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩) ++ (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩)) = (𝐴 substr ⟨𝑀, 𝑁⟩))
108		iffalse 3630	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ 𝑁 ≤ 𝐿 → if(𝑁 ≤ 𝐿, 𝑁, 𝐿) = 𝐿)
109	108	3ad2ant2 1046	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀) → if(𝑁 ≤ 𝐿, 𝑁, 𝐿) = 𝐿)
110	109	opeq2d 3890	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀) → ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩ = ⟨𝑀, 𝐿⟩)
111	110	oveq2d 6066	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀) → (𝐴 substr ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩) = (𝐴 substr ⟨𝑀, 𝐿⟩))
112		simpl 109	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → 𝐴 ∈ Word 𝑉)
113	112, 30, 28	3anim123i 1211	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) → (𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝐿 ∈ ℤ))
114	113	3expb 1231	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → (𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝐿 ∈ ℤ))
115		swrdlend 11350	. . . . . . . . . . . . . . . . . . 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 1043	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀) → (𝐴 substr ⟨𝑀, 𝐿⟩) = ∅)
119	111, 118	eqtrd 2265	. . . . . . . . . . . . . . 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 1043	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀) → 0 ≤ (𝑀 − 𝐿))
125	124, 24	syl 14	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀) → ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩ = ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩)
126	125	oveq2d 6066	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀) → (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩) = (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩))
127	119, 126	oveq12d 6068	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀) → ((𝐴 substr ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩) ++ (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩)) = (∅ ++ (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩)))
128		swrdclg 11342	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ∈ Word 𝑉 ∧ (𝑀 − 𝐿) ∈ ℤ ∧ (𝑁 − 𝐿) ∈ ℤ) → (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩) ∈ Word 𝑉)
129		ccatlid 11294	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩) ∈ Word 𝑉 → (∅ ++ (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩)) = (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩))
130	41, 128, 129	3syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → (∅ ++ (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩)) = (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩))
131	130	3ad2ant1 1045	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀) → (∅ ++ (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩)) = (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩))
132	127, 131	eqtrd 2265	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀) → ((𝐴 substr ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩) ++ (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩)) = (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩))
133	108	3ad2ant2 1046	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀) → if(𝑁 ≤ 𝐿, 𝑁, 𝐿) = 𝐿)
134	133	opeq2d 3890	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀) → ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩ = ⟨𝑀, 𝐿⟩)
135	134	oveq2d 6066	. . . . . . . . . . . . . 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 640	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝐿 ≤ 𝑀) → ¬ 0 ≤ (𝑀 − 𝐿))
141	140	3adant2 1043	. . . . . . . . . . . . . . . . . 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 3889	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀) → ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩ = ⟨0, (𝑁 − 𝐿)⟩)
144	143	oveq2d 6066	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀) → (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩) = (𝐵 substr ⟨0, (𝑁 − 𝐿)⟩))
145	79	3ad2ant1 1045	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀) → 𝐵 ∈ Word 𝑉)
146		simplrr 538	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿) → 𝐿 ∈ ℕ0)
147		simprlr 540	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → 𝑁 ∈ ℕ0)
148	147	adantr 276	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿) → 𝑁 ∈ ℕ0)
149		zltnle 9623	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐿 < 𝑁 ↔ ¬ 𝑁 ≤ 𝐿))
150	28, 34, 149	syl2anr 290	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) → (𝐿 < 𝑁 ↔ ¬ 𝑁 ≤ 𝐿))
151		ltle 8361	. . . . . . . . . . . . . . . . . . . . . 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 9651	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐿 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ≤ 𝑁) → (𝑁 − 𝐿) ∈ ℕ0)
157	146, 148, 155, 156	syl3anc 1274	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿) → (𝑁 − 𝐿) ∈ ℕ0)
158	157	3adant3 1044	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀) → (𝑁 − 𝐿) ∈ ℕ0)
159		pfxval 11366	. . . . . . . . . . . . . . . 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 2268	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀) → (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩) = (𝐵 prefix (𝑁 − 𝐿)))
162	135, 161	oveq12d 6068	. . . . . . . . . . . . 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 9654	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ) → DECID 𝑁 ≤ 𝐿)
165	101, 163, 164	syl2anc 411	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → DECID 𝑁 ≤ 𝐿)
166	146	nn0zd 9698	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿) → 𝐿 ∈ ℤ)
167	100	adantr 276	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿) → 𝑀 ∈ ℤ)
168		zdcle 9654	. . . . . . . . . . . . . 14 ⊢ ((𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ) → DECID 𝐿 ≤ 𝑀)
169	166, 167, 168	syl2anc 411	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿) → DECID 𝐿 ≤ 𝑀)
170	107, 132, 162, 165, 169	2if2dc 3662	. . . . . . . . . . . 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 1044	. . . . . . . . 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 2268	. 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 716  DECID wdc 842   ∧ w3a 1005   = wceq 1398   ∈ wcel 2203  ∅c0 3508  ifcif 3620  ⟨cop 3692   class class class wbr 4109  ‘cfv 5352  (class class class)co 6050  ℝcr 8126  0cc0 8127   + caddc 8130   < clt 8308   ≤ cle 8309   − cmin 8444  ℕ₀cn0 9496  ℤcz 9577  ...cfz 10342  ♯chash 11138  Word cword 11224   ++ cconcat 11278   substr csubstr 11337   prefix cpfx 11364

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 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2205  ax-14 2206  ax-ext 2214  ax-coll 4225  ax-sep 4228  ax-nul 4236  ax-pow 4287  ax-pr 4322  ax-un 4554  ax-setind 4659  ax-iinf 4710  ax-cnex 8218  ax-resscn 8219  ax-1cn 8220  ax-1re 8221  ax-icn 8222  ax-addcl 8223  ax-addrcl 8224  ax-mulcl 8225  ax-addcom 8227  ax-addass 8229  ax-distr 8231  ax-i2m1 8232  ax-0lt1 8233  ax-0id 8235  ax-rnegex 8236  ax-cnre 8238  ax-pre-ltirr 8239  ax-pre-ltwlin 8240  ax-pre-lttrn 8241  ax-pre-apti 8242  ax-pre-ltadd 8243

This theorem depends on definitions:  df-bi 117  df-dc 843  df-3or 1006  df-3an 1007  df-tru 1401  df-fal 1404  df-nf 1510  df-sb 1812  df-eu 2083  df-mo 2084  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ne 2413  df-nel 2508  df-ral 2525  df-rex 2526  df-reu 2527  df-rab 2529  df-v 2815  df-sbc 3043  df-csb 3139  df-dif 3213  df-un 3215  df-in 3217  df-ss 3224  df-nul 3509  df-if 3621  df-pw 3671  df-sn 3695  df-pr 3696  df-op 3698  df-uni 3915  df-int 3950  df-iun 3993  df-br 4110  df-opab 4172  df-mpt 4173  df-tr 4209  df-id 4414  df-iord 4487  df-on 4489  df-ilim 4490  df-suc 4492  df-iom 4713  df-xp 4755  df-rel 4756  df-cnv 4757  df-co 4758  df-dm 4759  df-rn 4760  df-res 4761  df-ima 4762  df-iota 5312  df-fun 5354  df-fn 5355  df-f 5356  df-f1 5357  df-fo 5358  df-f1o 5359  df-fv 5360  df-riota 6003  df-ov 6053  df-oprab 6054  df-mpo 6055  df-1st 6334  df-2nd 6335  df-recs 6536  df-frec 6622  df-1o 6647  df-er 6767  df-en 6976  df-dom 6977  df-fin 6978  df-pnf 8310  df-mnf 8311  df-xr 8312  df-ltxr 8313  df-le 8314  df-sub 8446  df-neg 8447  df-inn 9238  df-n0 9497  df-z 9578  df-uz 9854  df-fz 10343  df-fzo 10477  df-ihash 11139  df-word 11225  df-concat 11279  df-substr 11338  df-pfx 11365

This theorem is referenced by: (None)