Theorem swrdccat 11485

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 11484	. . . 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 11286	. . . . . 6 ⊢ (𝐴 ∈ Word 𝑉 → (♯‘𝐴) ∈ ℕ0)
5	4	adantr 276	. . . . 5 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (♯‘𝐴) ∈ ℕ0)
6	1	eqcomi 2242	. . . . . . 7 ⊢ (♯‘𝐴) = 𝐿
7	6	eleq1i 2304	. . . . . 6 ⊢ ((♯‘𝐴) ∈ ℕ0 ↔ 𝐿 ∈ ℕ0)
8		elfz2nn0 10497	. . . . . . . . 9 ⊢ (𝑀 ∈ (0...𝑁) ↔ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁))
9		iftrue 3642	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ≤ 𝐿 → if(𝑁 ≤ 𝐿, 𝑁, 𝐿) = 𝑁)
10	9	adantl 277	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → if(𝑁 ≤ 𝐿, 𝑁, 𝐿) = 𝑁)
11	10	opeq2d 3906	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩ = ⟨𝑀, 𝑁⟩)
12	11	oveq2d 6091	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → (𝐴 substr ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩) = (𝐴 substr ⟨𝑀, 𝑁⟩))
13		0z 9634	. . . . . . . . . . . . . . . . 17 ⊢ 0 ∈ ℤ
14		simprll 543	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → 𝑀 ∈ ℕ0)
15	14	adantr 276	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → 𝑀 ∈ ℕ0)
16	15	nn0zd 9745	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → 𝑀 ∈ ℤ)
17		simplrr 542	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → 𝐿 ∈ ℕ0)
18	17	nn0zd 9745	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → 𝐿 ∈ ℤ)
19	16, 18	zsubcld 9752	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → (𝑀 − 𝐿) ∈ ℤ)
20		zdcle 9700	. . . . . . . . . . . . . . . . 17 ⊢ ((0 ∈ ℤ ∧ (𝑀 − 𝐿) ∈ ℤ) → DECID 0 ≤ (𝑀 − 𝐿))
21	13, 19, 20	sylancr 418	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → DECID 0 ≤ (𝑀 − 𝐿))
22		exmiddc 848	. . . . . . . . . . . . . . . . 17 ⊢ (DECID 0 ≤ (𝑀 − 𝐿) → (0 ≤ (𝑀 − 𝐿) ∨ ¬ 0 ≤ (𝑀 − 𝐿)))
23		iftrue 3642	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (0 ≤ (𝑀 − 𝐿) → if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0) = (𝑀 − 𝐿))
24	23	opeq1d 3905	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (0 ≤ (𝑀 − 𝐿) → ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩ = ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩)
25	24	oveq2d 6091	. . . . . . . . . . . . . . . . . . . . 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 9643	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐿 ∈ ℕ0 → 𝐿 ∈ ℤ)
29		nn0z 9643	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑀 ∈ ℕ0 → 𝑀 ∈ ℤ)
30	29	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → 𝑀 ∈ ℤ)
31		zsubcl 9664	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑀 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝑀 − 𝐿) ∈ ℤ)
32	30, 31	sylan 283	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℤ) → (𝑀 − 𝐿) ∈ ℤ)
33		nn0z 9643	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ)
34	33	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → 𝑁 ∈ ℤ)
35		zsubcl 9664	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 1013	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐵 ∈ Word 𝑉 ∧ (𝑀 − 𝐿) ∈ ℤ ∧ (𝑁 − 𝐿) ∈ ℤ) ↔ (𝐵 ∈ Word 𝑉 ∧ ((𝑀 − 𝐿) ∈ ℤ ∧ (𝑁 − 𝐿) ∈ ℤ)))
41	39, 40	sylibr 134	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → (𝐵 ∈ Word 𝑉 ∧ (𝑀 − 𝐿) ∈ ℤ ∧ (𝑁 − 𝐿) ∈ ℤ))
42	41	ad2antrl 494	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((0 ≤ (𝑀 − 𝐿) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿)) → (𝐵 ∈ Word 𝑉 ∧ (𝑀 − 𝐿) ∈ ℤ ∧ (𝑁 − 𝐿) ∈ ℤ))
43		nn0re 9551	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑀 ∈ ℕ0 → 𝑀 ∈ ℝ)
44		nn0re 9551	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ)
45	43, 44	anim12i 338	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ))
46		nn0re 9551	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐿 ∈ ℕ0 → 𝐿 ∈ ℝ)
47		subge0 8793	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑀 ∈ ℝ ∧ 𝐿 ∈ ℝ) → (0 ≤ (𝑀 − 𝐿) ↔ 𝐿 ≤ 𝑀))
48	47	adantlr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝐿 ∈ ℝ) → (0 ≤ (𝑀 − 𝐿) ↔ 𝐿 ≤ 𝑀))
49		simplr 533	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝐿 ∈ ℝ) → 𝑁 ∈ ℝ)
50		simpr 110	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝐿 ∈ ℝ) → 𝐿 ∈ ℝ)
51		simpll 531	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝐿 ∈ ℝ) → 𝑀 ∈ ℝ)
52		letr 8398	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ ∧ 𝑀 ∈ ℝ) → ((𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀) → 𝑁 ≤ 𝑀))
53	49, 50, 51, 52	syl3anc 1278	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝐿 ∈ ℝ) → ((𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀) → 𝑁 ≤ 𝑀))
54	53	expcomd 1491	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1208	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) → (𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝐿 ∈ ℝ))
67	66	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → (𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝐿 ∈ ℝ))
68	67	ad2antrl 494	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((0 ≤ (𝑀 − 𝐿) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿)) → (𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝐿 ∈ ℝ))
69		lesub1 8774	. . . . . . . . . . . . . . . . . . . . . . 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 11408	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐵 ∈ Word 𝑉 ∧ (𝑀 − 𝐿) ∈ ℤ ∧ (𝑁 − 𝐿) ∈ ℤ) → ((𝑁 − 𝐿) ≤ (𝑀 − 𝐿) → (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩) = ∅))
73	42, 71, 72	sylc 62	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((0 ≤ (𝑀 − 𝐿) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿)) → (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩) = ∅)
74	26, 73	eqtrd 2271	. . . . . . . . . . . . . . . . . . 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 3645	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ 0 ≤ (𝑀 − 𝐿) → if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0) = 0)
77	76	opeq1d 3905	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ 0 ≤ (𝑀 − 𝐿) → ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩ = ⟨0, (𝑁 − 𝐿)⟩)
78	77	oveq2d 6091	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ 0 ≤ (𝑀 − 𝐿) → (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩) = (𝐵 substr ⟨0, (𝑁 − 𝐿)⟩))
79		simplr 533	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → 𝐵 ∈ Word 𝑉)
80	79	adantr 276	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → 𝐵 ∈ Word 𝑉)
81		0zd 9635	. . . . . . . . . . . . . . . . . . . . . 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 1208	. . . . . . . . . . . . . . . . . . . . 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 8794	. . . . . . . . . . . . . . . . . . . . . . 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 11408	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐵 ∈ Word 𝑉 ∧ 0 ∈ ℤ ∧ (𝑁 − 𝐿) ∈ ℤ) → ((𝑁 − 𝐿) ≤ 0 → (𝐵 substr ⟨0, (𝑁 − 𝐿)⟩) = ∅))
92	85, 90, 91	sylc 62	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → (𝐵 substr ⟨0, (𝑁 − 𝐿)⟩) = ∅)
93	78, 92	sylan9eq 2291	. . . . . . . . . . . . . . . . . . 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 728	. . . . . . . . . . . . . . . . 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 6093	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → ((𝐴 substr ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩) ++ (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩)) = ((𝐴 substr ⟨𝑀, 𝑁⟩) ++ ∅))
99		simpll 531	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → 𝐴 ∈ Word 𝑉)
100	14	nn0zd 9745	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → 𝑀 ∈ ℤ)
101	34	ad2antrl 494	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → 𝑁 ∈ ℤ)
102		swrdclg 11400	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 substr ⟨𝑀, 𝑁⟩) ∈ Word 𝑉)
103	99, 100, 101, 102	syl3anc 1278	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → (𝐴 substr ⟨𝑀, 𝑁⟩) ∈ Word 𝑉)
104		ccatrid 11353	. . . . . . . . . . . . . . . 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 2271	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → ((𝐴 substr ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩) ++ (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩)) = (𝐴 substr ⟨𝑀, 𝑁⟩))
108		iffalse 3645	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ 𝑁 ≤ 𝐿 → if(𝑁 ≤ 𝐿, 𝑁, 𝐿) = 𝐿)
109	108	3ad2ant2 1050	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀) → if(𝑁 ≤ 𝐿, 𝑁, 𝐿) = 𝐿)
110	109	opeq2d 3906	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀) → ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩ = ⟨𝑀, 𝐿⟩)
111	110	oveq2d 6091	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀) → (𝐴 substr ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩) = (𝐴 substr ⟨𝑀, 𝐿⟩))
112		simpl 109	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → 𝐴 ∈ Word 𝑉)
113	112, 30, 28	3anim123i 1215	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) → (𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝐿 ∈ ℤ))
114	113	3expb 1235	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → (𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝐿 ∈ ℤ))
115		swrdlend 11408	. . . . . . . . . . . . . . . . . . 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 1047	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀) → (𝐴 substr ⟨𝑀, 𝐿⟩) = ∅)
119	111, 118	eqtrd 2271	. . . . . . . . . . . . . . 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 1047	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀) → 0 ≤ (𝑀 − 𝐿))
125	124, 24	syl 14	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀) → ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩ = ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩)
126	125	oveq2d 6091	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀) → (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩) = (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩))
127	119, 126	oveq12d 6093	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀) → ((𝐴 substr ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩) ++ (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩)) = (∅ ++ (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩)))
128		swrdclg 11400	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ∈ Word 𝑉 ∧ (𝑀 − 𝐿) ∈ ℤ ∧ (𝑁 − 𝐿) ∈ ℤ) → (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩) ∈ Word 𝑉)
129		ccatlid 11352	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩) ∈ Word 𝑉 → (∅ ++ (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩)) = (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩))
130	41, 128, 129	3syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → (∅ ++ (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩)) = (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩))
131	130	3ad2ant1 1049	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀) → (∅ ++ (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩)) = (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩))
132	127, 131	eqtrd 2271	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀) → ((𝐴 substr ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩) ++ (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩)) = (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩))
133	108	3ad2ant2 1050	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀) → if(𝑁 ≤ 𝐿, 𝑁, 𝐿) = 𝐿)
134	133	opeq2d 3906	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀) → ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩ = ⟨𝑀, 𝐿⟩)
135	134	oveq2d 6091	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀) → (𝐴 substr ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩) = (𝐴 substr ⟨𝑀, 𝐿⟩))
136	43, 46, 47	syl2an 289	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0) → (0 ≤ (𝑀 − 𝐿) ↔ 𝐿 ≤ 𝑀))
137	136	adantlr 481	. . . . . . . . . . . . . . . . . . . . . 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 644	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝐿 ≤ 𝑀) → ¬ 0 ≤ (𝑀 − 𝐿))
141	140	3adant2 1047	. . . . . . . . . . . . . . . . . 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 3905	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀) → ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩ = ⟨0, (𝑁 − 𝐿)⟩)
144	143	oveq2d 6091	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀) → (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩) = (𝐵 substr ⟨0, (𝑁 − 𝐿)⟩))
145	79	3ad2ant1 1049	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀) → 𝐵 ∈ Word 𝑉)
146		simplrr 542	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿) → 𝐿 ∈ ℕ0)
147		simprlr 544	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → 𝑁 ∈ ℕ0)
148	147	adantr 276	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿) → 𝑁 ∈ ℕ0)
149		zltnle 9669	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐿 < 𝑁 ↔ ¬ 𝑁 ≤ 𝐿))
150	28, 34, 149	syl2anr 290	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) → (𝐿 < 𝑁 ↔ ¬ 𝑁 ≤ 𝐿))
151		ltle 8403	. . . . . . . . . . . . . . . . . . . . . 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 9697	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐿 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ≤ 𝑁) → (𝑁 − 𝐿) ∈ ℕ0)
157	146, 148, 155, 156	syl3anc 1278	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿) → (𝑁 − 𝐿) ∈ ℕ0)
158	157	3adant3 1048	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀) → (𝑁 − 𝐿) ∈ ℕ0)
159		pfxval 11424	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ∈ Word 𝑉 ∧ (𝑁 − 𝐿) ∈ ℕ0) → (𝐵 prefix (𝑁 − 𝐿)) = (𝐵 substr ⟨0, (𝑁 − 𝐿)⟩))
160	145, 158, 159	syl2anc 415	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀) → (𝐵 prefix (𝑁 − 𝐿)) = (𝐵 substr ⟨0, (𝑁 − 𝐿)⟩))
161	144, 160	eqtr4d 2274	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀) → (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩) = (𝐵 prefix (𝑁 − 𝐿)))
162	135, 161	oveq12d 6093	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀) → ((𝐴 substr ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩) ++ (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩)) = ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿))))
163	28	ad2antll 495	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → 𝐿 ∈ ℤ)
164		zdcle 9700	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ) → DECID 𝑁 ≤ 𝐿)
165	101, 163, 164	syl2anc 415	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → DECID 𝑁 ≤ 𝐿)
166	146	nn0zd 9745	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿) → 𝐿 ∈ ℤ)
167	100	adantr 276	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿) → 𝑀 ∈ ℤ)
168		zdcle 9700	. . . . . . . . . . . . . 14 ⊢ ((𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ) → DECID 𝐿 ≤ 𝑀)
169	166, 167, 168	syl2anc 415	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿) → DECID 𝐿 ≤ 𝑀)
170	107, 132, 162, 165, 169	2if2dc 3677	. . . . . . . . . . . 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 1048	. . . . . . . . 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 2274	. 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 720  DECID wdc 846   ∧ w3a 1009   = wceq 1402   ∈ wcel 2209  ∅c0 3520  ifcif 3635  ⟨cop 3708   class class class wbr 4125  ‘cfv 5372  (class class class)co 6075  ℝcr 8168  0cc0 8169   + caddc 8172   < clt 8350   ≤ cle 8351   − cmin 8487  ℕ₀cn0 9542  ℤcz 9623  ...cfz 10390  ♯chash 11192  Word cword 11282   ++ cconcat 11336   substr csubstr 11395   prefix cpfx 11422

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 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-coll 4241  ax-sep 4244  ax-nul 4254  ax-pow 4306  ax-pr 4341  ax-un 4573  ax-setind 4679  ax-iinf 4730  ax-cnex 8260  ax-resscn 8261  ax-1cn 8262  ax-1re 8263  ax-icn 8264  ax-addcl 8265  ax-addrcl 8266  ax-mulcl 8267  ax-addcom 8269  ax-addass 8271  ax-distr 8273  ax-i2m1 8274  ax-0lt1 8275  ax-0id 8277  ax-rnegex 8278  ax-cnre 8280  ax-pre-ltirr 8281  ax-pre-ltwlin 8282  ax-pre-lttrn 8283  ax-pre-apti 8284  ax-pre-ltadd 8285

This theorem depends on definitions:  df-bi 117  df-dc 847  df-3or 1010  df-3an 1011  df-tru 1405  df-fal 1408  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-nel 2516  df-ral 2533  df-rex 2534  df-reu 2535  df-rab 2537  df-v 2823  df-sbc 3052  df-csb 3148  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-nul 3521  df-if 3636  df-pw 3687  df-sn 3711  df-pr 3712  df-op 3714  df-uni 3931  df-int 3966  df-iun 4009  df-br 4126  df-opab 4188  df-mpt 4189  df-tr 4225  df-id 4433  df-iord 4506  df-on 4508  df-ilim 4509  df-suc 4511  df-iom 4733  df-xp 4775  df-rel 4776  df-cnv 4777  df-co 4778  df-dm 4779  df-rn 4780  df-res 4781  df-ima 4782  df-iota 5332  df-fun 5374  df-fn 5375  df-f 5376  df-f1 5377  df-fo 5378  df-f1o 5379  df-fv 5380  df-riota 6028  df-ov 6078  df-oprab 6079  df-mpo 6080  df-1st 6364  df-2nd 6365  df-recs 6566  df-frec 6652  df-1o 6677  df-er 6797  df-en 7013  df-dom 7014  df-fin 7015  df-pnf 8352  df-mnf 8353  df-xr 8354  df-ltxr 8355  df-le 8356  df-sub 8489  df-neg 8490  df-inn 9284  df-n0 9543  df-z 9624  df-uz 9901  df-fz 10391  df-fzo 10528  df-ihash 11193  df-word 11283  df-concat 11337  df-substr 11396  df-pfx 11423

This theorem is referenced by: (None)