Theorem swrdccat 14740

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 14739	. . . 4 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(𝐿 + (♯‘𝐵)))) → ((𝐴 ++ 𝐵) substr ⟨𝑀, 𝑁⟩) = if(𝑁 ≤ 𝐿, (𝐴 substr ⟨𝑀, 𝑁⟩), if(𝐿 ≤ 𝑀, (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿)))))))
3	2	imp 406	. . 3 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(𝐿 + (♯‘𝐵))))) → ((𝐴 ++ 𝐵) substr ⟨𝑀, 𝑁⟩) = if(𝑁 ≤ 𝐿, (𝐴 substr ⟨𝑀, 𝑁⟩), if(𝐿 ≤ 𝑀, (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿))))))
4		lencl 14538	. . . . . 6 ⊢ (𝐴 ∈ Word 𝑉 → (♯‘𝐴) ∈ ℕ0)
5	4	adantr 480	. . . . 5 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (♯‘𝐴) ∈ ℕ0)
6	1	eqcomi 2743	. . . . . . 7 ⊢ (♯‘𝐴) = 𝐿
7	6	eleq1i 2824	. . . . . 6 ⊢ ((♯‘𝐴) ∈ ℕ0 ↔ 𝐿 ∈ ℕ0)
8		elfz2nn0 13624	. . . . . . . . 9 ⊢ (𝑀 ∈ (0...𝑁) ↔ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁))
9		iftrue 4504	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ≤ 𝐿 → if(𝑁 ≤ 𝐿, 𝑁, 𝐿) = 𝑁)
10	9	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → if(𝑁 ≤ 𝐿, 𝑁, 𝐿) = 𝑁)
11	10	opeq2d 4853	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩ = ⟨𝑀, 𝑁⟩)
12	11	oveq2d 7415	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → (𝐴 substr ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩) = (𝐴 substr ⟨𝑀, 𝑁⟩))
13		iftrue 4504	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 ≤ (𝑀 − 𝐿) → if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0) = (𝑀 − 𝐿))
14	13	opeq1d 4852	. . . . . . . . . . . . . . . . . . 19 ⊢ (0 ≤ (𝑀 − 𝐿) → ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩ = ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩)
15	14	oveq2d 7415	. . . . . . . . . . . . . . . . . 18 ⊢ (0 ≤ (𝑀 − 𝐿) → (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩) = (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩))
16	15	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((0 ≤ (𝑀 − 𝐿) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿)) → (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩) = (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩))
17		simpr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → 𝐵 ∈ Word 𝑉)
18		nn0z 12605	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐿 ∈ ℕ0 → 𝐿 ∈ ℤ)
19		nn0z 12605	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑀 ∈ ℕ0 → 𝑀 ∈ ℤ)
20	19	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → 𝑀 ∈ ℤ)
21		zsubcl 12626	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑀 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝑀 − 𝐿) ∈ ℤ)
22	20, 21	sylan 580	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℤ) → (𝑀 − 𝐿) ∈ ℤ)
23		nn0z 12605	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ)
24	23	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → 𝑁 ∈ ℤ)
25		zsubcl 12626	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝑁 − 𝐿) ∈ ℤ)
26	24, 25	sylan 580	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℤ) → (𝑁 − 𝐿) ∈ ℤ)
27	22, 26	jca 511	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℤ) → ((𝑀 − 𝐿) ∈ ℤ ∧ (𝑁 − 𝐿) ∈ ℤ))
28	18, 27	sylan2 593	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) → ((𝑀 − 𝐿) ∈ ℤ ∧ (𝑁 − 𝐿) ∈ ℤ))
29	17, 28	anim12i 613	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → (𝐵 ∈ Word 𝑉 ∧ ((𝑀 − 𝐿) ∈ ℤ ∧ (𝑁 − 𝐿) ∈ ℤ)))
30		3anass 1094	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐵 ∈ Word 𝑉 ∧ (𝑀 − 𝐿) ∈ ℤ ∧ (𝑁 − 𝐿) ∈ ℤ) ↔ (𝐵 ∈ Word 𝑉 ∧ ((𝑀 − 𝐿) ∈ ℤ ∧ (𝑁 − 𝐿) ∈ ℤ)))
31	29, 30	sylibr 234	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → (𝐵 ∈ Word 𝑉 ∧ (𝑀 − 𝐿) ∈ ℤ ∧ (𝑁 − 𝐿) ∈ ℤ))
32	31	ad2antrl 728	. . . . . . . . . . . . . . . . . 18 ⊢ ((0 ≤ (𝑀 − 𝐿) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿)) → (𝐵 ∈ Word 𝑉 ∧ (𝑀 − 𝐿) ∈ ℤ ∧ (𝑁 − 𝐿) ∈ ℤ))
33		nn0re 12502	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑀 ∈ ℕ0 → 𝑀 ∈ ℝ)
34		nn0re 12502	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ)
35	33, 34	anim12i 613	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ))
36		nn0re 12502	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐿 ∈ ℕ0 → 𝐿 ∈ ℝ)
37		subge0 11742	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑀 ∈ ℝ ∧ 𝐿 ∈ ℝ) → (0 ≤ (𝑀 − 𝐿) ↔ 𝐿 ≤ 𝑀))
38	37	adantlr 715	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝐿 ∈ ℝ) → (0 ≤ (𝑀 − 𝐿) ↔ 𝐿 ≤ 𝑀))
39		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → 𝑁 ∈ ℝ)
40	39	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝐿 ∈ ℝ) → 𝑁 ∈ ℝ)
41		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝐿 ∈ ℝ) → 𝐿 ∈ ℝ)
42		simpl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → 𝑀 ∈ ℝ)
43	42	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝐿 ∈ ℝ) → 𝑀 ∈ ℝ)
44		letr 11321	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ ∧ 𝑀 ∈ ℝ) → ((𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀) → 𝑁 ≤ 𝑀))
45	40, 41, 43, 44	syl3anc 1372	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝐿 ∈ ℝ) → ((𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀) → 𝑁 ≤ 𝑀))
46	45	expcomd 416	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝐿 ∈ ℝ) → (𝐿 ≤ 𝑀 → (𝑁 ≤ 𝐿 → 𝑁 ≤ 𝑀)))
47	38, 46	sylbid 240	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝐿 ∈ ℝ) → (0 ≤ (𝑀 − 𝐿) → (𝑁 ≤ 𝐿 → 𝑁 ≤ 𝑀)))
48	47	com23 86	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝐿 ∈ ℝ) → (𝑁 ≤ 𝐿 → (0 ≤ (𝑀 − 𝐿) → 𝑁 ≤ 𝑀)))
49	35, 36, 48	syl2an 596	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) → (𝑁 ≤ 𝐿 → (0 ≤ (𝑀 − 𝐿) → 𝑁 ≤ 𝑀)))
50	49	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → (𝑁 ≤ 𝐿 → (0 ≤ (𝑀 − 𝐿) → 𝑁 ≤ 𝑀)))
51	50	imp 406	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → (0 ≤ (𝑀 − 𝐿) → 𝑁 ≤ 𝑀))
52	51	impcom 407	. . . . . . . . . . . . . . . . . . 19 ⊢ ((0 ≤ (𝑀 − 𝐿) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿)) → 𝑁 ≤ 𝑀)
53	34	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → 𝑁 ∈ ℝ)
54	53	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) → 𝑁 ∈ ℝ)
55	33	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → 𝑀 ∈ ℝ)
56	55	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) → 𝑀 ∈ ℝ)
57	36	adantl 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) → 𝐿 ∈ ℝ)
58	54, 56, 57	3jca 1128	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) → (𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝐿 ∈ ℝ))
59	58	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → (𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝐿 ∈ ℝ))
60	59	ad2antrl 728	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((0 ≤ (𝑀 − 𝐿) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿)) → (𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝐿 ∈ ℝ))
61		lesub1 11723	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝐿 ∈ ℝ) → (𝑁 ≤ 𝑀 ↔ (𝑁 − 𝐿) ≤ (𝑀 − 𝐿)))
62	60, 61	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((0 ≤ (𝑀 − 𝐿) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿)) → (𝑁 ≤ 𝑀 ↔ (𝑁 − 𝐿) ≤ (𝑀 − 𝐿)))
63	52, 62	mpbid 232	. . . . . . . . . . . . . . . . . 18 ⊢ ((0 ≤ (𝑀 − 𝐿) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿)) → (𝑁 − 𝐿) ≤ (𝑀 − 𝐿))
64		swrdlend 14658	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 ∈ Word 𝑉 ∧ (𝑀 − 𝐿) ∈ ℤ ∧ (𝑁 − 𝐿) ∈ ℤ) → ((𝑁 − 𝐿) ≤ (𝑀 − 𝐿) → (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩) = ∅))
65	32, 63, 64	sylc 65	. . . . . . . . . . . . . . . . 17 ⊢ ((0 ≤ (𝑀 − 𝐿) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿)) → (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩) = ∅)
66	16, 65	eqtrd 2769	. . . . . . . . . . . . . . . 16 ⊢ ((0 ≤ (𝑀 − 𝐿) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿)) → (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩) = ∅)
67		iffalse 4507	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ 0 ≤ (𝑀 − 𝐿) → if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0) = 0)
68	67	opeq1d 4852	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ 0 ≤ (𝑀 − 𝐿) → ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩ = ⟨0, (𝑁 − 𝐿)⟩)
69	68	oveq2d 7415	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 0 ≤ (𝑀 − 𝐿) → (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩) = (𝐵 substr ⟨0, (𝑁 − 𝐿)⟩))
70	17	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → 𝐵 ∈ Word 𝑉)
71	70	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → 𝐵 ∈ Word 𝑉)
72		0zd 12592	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → 0 ∈ ℤ)
73	24, 18, 25	syl2an 596	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) → (𝑁 − 𝐿) ∈ ℤ)
74	73	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → (𝑁 − 𝐿) ∈ ℤ)
75	74	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → (𝑁 − 𝐿) ∈ ℤ)
76	71, 72, 75	3jca 1128	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → (𝐵 ∈ Word 𝑉 ∧ 0 ∈ ℤ ∧ (𝑁 − 𝐿) ∈ ℤ))
77	53, 36	anim12i 613	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) → (𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ))
78	77	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → (𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ))
79		suble0 11743	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ) → ((𝑁 − 𝐿) ≤ 0 ↔ 𝑁 ≤ 𝐿))
80	78, 79	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → ((𝑁 − 𝐿) ≤ 0 ↔ 𝑁 ≤ 𝐿))
81	80	biimpar 477	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → (𝑁 − 𝐿) ≤ 0)
82		swrdlend 14658	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 ∈ Word 𝑉 ∧ 0 ∈ ℤ ∧ (𝑁 − 𝐿) ∈ ℤ) → ((𝑁 − 𝐿) ≤ 0 → (𝐵 substr ⟨0, (𝑁 − 𝐿)⟩) = ∅))
83	76, 81, 82	sylc 65	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → (𝐵 substr ⟨0, (𝑁 − 𝐿)⟩) = ∅)
84	69, 83	sylan9eq 2789	. . . . . . . . . . . . . . . 16 ⊢ ((¬ 0 ≤ (𝑀 − 𝐿) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿)) → (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩) = ∅)
85	66, 84	pm2.61ian 811	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩) = ∅)
86	12, 85	oveq12d 7417	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → ((𝐴 substr ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩) ++ (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩)) = ((𝐴 substr ⟨𝑀, 𝑁⟩) ++ ∅))
87		swrdcl 14650	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ Word 𝑉 → (𝐴 substr ⟨𝑀, 𝑁⟩) ∈ Word 𝑉)
88		ccatrid 14592	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 substr ⟨𝑀, 𝑁⟩) ∈ Word 𝑉 → ((𝐴 substr ⟨𝑀, 𝑁⟩) ++ ∅) = (𝐴 substr ⟨𝑀, 𝑁⟩))
89	87, 88	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ Word 𝑉 → ((𝐴 substr ⟨𝑀, 𝑁⟩) ++ ∅) = (𝐴 substr ⟨𝑀, 𝑁⟩))
90	89	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝐴 substr ⟨𝑀, 𝑁⟩) ++ ∅) = (𝐴 substr ⟨𝑀, 𝑁⟩))
91	90	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → ((𝐴 substr ⟨𝑀, 𝑁⟩) ++ ∅) = (𝐴 substr ⟨𝑀, 𝑁⟩))
92	91	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → ((𝐴 substr ⟨𝑀, 𝑁⟩) ++ ∅) = (𝐴 substr ⟨𝑀, 𝑁⟩))
93	86, 92	eqtrd 2769	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁 ≤ 𝐿) → ((𝐴 substr ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩) ++ (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩)) = (𝐴 substr ⟨𝑀, 𝑁⟩))
94		iffalse 4507	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ 𝑁 ≤ 𝐿 → if(𝑁 ≤ 𝐿, 𝑁, 𝐿) = 𝐿)
95	94	3ad2ant2 1134	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀) → if(𝑁 ≤ 𝐿, 𝑁, 𝐿) = 𝐿)
96	95	opeq2d 4853	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀) → ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩ = ⟨𝑀, 𝐿⟩)
97	96	oveq2d 7415	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀) → (𝐴 substr ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩) = (𝐴 substr ⟨𝑀, 𝐿⟩))
98		simpl 482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → 𝐴 ∈ Word 𝑉)
99	98, 20, 18	3anim123i 1151	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) → (𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝐿 ∈ ℤ))
100	99	3expb 1120	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → (𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝐿 ∈ ℤ))
101		swrdlend 14658	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝐿 ≤ 𝑀 → (𝐴 substr ⟨𝑀, 𝐿⟩) = ∅))
102	100, 101	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → (𝐿 ≤ 𝑀 → (𝐴 substr ⟨𝑀, 𝐿⟩) = ∅))
103	102	imp 406	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝐿 ≤ 𝑀) → (𝐴 substr ⟨𝑀, 𝐿⟩) = ∅)
104	103	3adant2 1131	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀) → (𝐴 substr ⟨𝑀, 𝐿⟩) = ∅)
105	97, 104	eqtrd 2769	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀) → (𝐴 substr ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩) = ∅)
106	55, 36, 37	syl2an 596	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) → (0 ≤ (𝑀 − 𝐿) ↔ 𝐿 ≤ 𝑀))
107	106	biimprd 248	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) → (𝐿 ≤ 𝑀 → 0 ≤ (𝑀 − 𝐿)))
108	107	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → (𝐿 ≤ 𝑀 → 0 ≤ (𝑀 − 𝐿)))
109	108	imp 406	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝐿 ≤ 𝑀) → 0 ≤ (𝑀 − 𝐿))
110	109	3adant2 1131	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀) → 0 ≤ (𝑀 − 𝐿))
111	110, 14	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀) → ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩ = ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩)
112	111	oveq2d 7415	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀) → (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩) = (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩))
113	105, 112	oveq12d 7417	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀) → ((𝐴 substr ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩) ++ (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩)) = (∅ ++ (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩)))
114		swrdcl 14650	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 ∈ Word 𝑉 → (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩) ∈ Word 𝑉)
115	114	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩) ∈ Word 𝑉)
116		ccatlid 14591	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩) ∈ Word 𝑉 → (∅ ++ (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩)) = (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩))
117	115, 116	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (∅ ++ (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩)) = (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩))
118	117	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → (∅ ++ (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩)) = (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩))
119	118	3ad2ant1 1133	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀) → (∅ ++ (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩)) = (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩))
120	113, 119	eqtrd 2769	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀) → ((𝐴 substr ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩) ++ (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩)) = (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩))
121	94	3ad2ant2 1134	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀) → if(𝑁 ≤ 𝐿, 𝑁, 𝐿) = 𝐿)
122	121	opeq2d 4853	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀) → ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩ = ⟨𝑀, 𝐿⟩)
123	122	oveq2d 7415	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀) → (𝐴 substr ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩) = (𝐴 substr ⟨𝑀, 𝐿⟩))
124	33, 36, 37	syl2an 596	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0) → (0 ≤ (𝑀 − 𝐿) ↔ 𝐿 ≤ 𝑀))
125	124	adantlr 715	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) → (0 ≤ (𝑀 − 𝐿) ↔ 𝐿 ≤ 𝑀))
126	125	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → (0 ≤ (𝑀 − 𝐿) ↔ 𝐿 ≤ 𝑀))
127	126	biimpd 229	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → (0 ≤ (𝑀 − 𝐿) → 𝐿 ≤ 𝑀))
128	127	con3dimp 408	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝐿 ≤ 𝑀) → ¬ 0 ≤ (𝑀 − 𝐿))
129	128	3adant2 1131	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀) → ¬ 0 ≤ (𝑀 − 𝐿))
130	129, 67	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀) → if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0) = 0)
131	130	opeq1d 4852	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀) → ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩ = ⟨0, (𝑁 − 𝐿)⟩)
132	131	oveq2d 7415	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀) → (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩) = (𝐵 substr ⟨0, (𝑁 − 𝐿)⟩))
133	70	3ad2ant1 1133	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀) → 𝐵 ∈ Word 𝑉)
134		simplrr 777	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿) → 𝐿 ∈ ℕ0)
135		simprlr 779	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → 𝑁 ∈ ℕ0)
136	135	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿) → 𝑁 ∈ ℕ0)
137		ltnle 11306	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐿 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝐿 < 𝑁 ↔ ¬ 𝑁 ≤ 𝐿))
138		ltle 11315	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐿 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝐿 < 𝑁 → 𝐿 ≤ 𝑁))
139	137, 138	sylbird 260	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐿 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (¬ 𝑁 ≤ 𝐿 → 𝐿 ≤ 𝑁))
140	36, 53, 139	syl2anr 597	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) → (¬ 𝑁 ≤ 𝐿 → 𝐿 ≤ 𝑁))
141	140	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → (¬ 𝑁 ≤ 𝐿 → 𝐿 ≤ 𝑁))
142	141	imp 406	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿) → 𝐿 ≤ 𝑁)
143		nn0sub2 12646	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐿 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ≤ 𝑁) → (𝑁 − 𝐿) ∈ ℕ0)
144	134, 136, 142, 143	syl3anc 1372	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿) → (𝑁 − 𝐿) ∈ ℕ0)
145	144	3adant3 1132	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀) → (𝑁 − 𝐿) ∈ ℕ0)
146	133, 145	jca 511	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀) → (𝐵 ∈ Word 𝑉 ∧ (𝑁 − 𝐿) ∈ ℕ0))
147		pfxval 14678	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ∈ Word 𝑉 ∧ (𝑁 − 𝐿) ∈ ℕ0) → (𝐵 prefix (𝑁 − 𝐿)) = (𝐵 substr ⟨0, (𝑁 − 𝐿)⟩))
148	146, 147	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀) → (𝐵 prefix (𝑁 − 𝐿)) = (𝐵 substr ⟨0, (𝑁 − 𝐿)⟩))
149	132, 148	eqtr4d 2772	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀) → (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩) = (𝐵 prefix (𝑁 − 𝐿)))
150	123, 149	oveq12d 7417	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀) → ((𝐴 substr ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩) ++ (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩)) = ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿))))
151	93, 120, 150	2if2 4554	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → ((𝐴 substr ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩) ++ (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩)) = if(𝑁 ≤ 𝐿, (𝐴 substr ⟨𝑀, 𝑁⟩), if(𝐿 ≤ 𝑀, (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿))))))
152	151	exp32 420	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝐿 ∈ ℕ0 → ((𝐴 substr ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩) ++ (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩)) = if(𝑁 ≤ 𝐿, (𝐴 substr ⟨𝑀, 𝑁⟩), if(𝐿 ≤ 𝑀, (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿))))))))
153	152	com12 32	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (𝐿 ∈ ℕ0 → ((𝐴 substr ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩) ++ (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩)) = if(𝑁 ≤ 𝐿, (𝐴 substr ⟨𝑀, 𝑁⟩), if(𝐿 ≤ 𝑀, (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿))))))))
154	153	3adant3 1132	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁) → ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (𝐿 ∈ ℕ0 → ((𝐴 substr ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩) ++ (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩)) = if(𝑁 ≤ 𝐿, (𝐴 substr ⟨𝑀, 𝑁⟩), if(𝐿 ≤ 𝑀, (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿))))))))
155	8, 154	sylbi 217	. . . . . . . 8 ⊢ (𝑀 ∈ (0...𝑁) → ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (𝐿 ∈ ℕ0 → ((𝐴 substr ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩) ++ (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩)) = if(𝑁 ≤ 𝐿, (𝐴 substr ⟨𝑀, 𝑁⟩), if(𝐿 ≤ 𝑀, (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿))))))))
156	155	adantr 480	. . . . . . 7 ⊢ ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(𝐿 + (♯‘𝐵)))) → ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (𝐿 ∈ ℕ0 → ((𝐴 substr ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩) ++ (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩)) = if(𝑁 ≤ 𝐿, (𝐴 substr ⟨𝑀, 𝑁⟩), if(𝐿 ≤ 𝑀, (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿))))))))
157	156	com13 88	. . . . . 6 ⊢ (𝐿 ∈ ℕ0 → ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(𝐿 + (♯‘𝐵)))) → ((𝐴 substr ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩) ++ (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩)) = if(𝑁 ≤ 𝐿, (𝐴 substr ⟨𝑀, 𝑁⟩), if(𝐿 ≤ 𝑀, (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿))))))))
158	7, 157	sylbi 217	. . . . 5 ⊢ ((♯‘𝐴) ∈ ℕ0 → ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(𝐿 + (♯‘𝐵)))) → ((𝐴 substr ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩) ++ (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩)) = if(𝑁 ≤ 𝐿, (𝐴 substr ⟨𝑀, 𝑁⟩), if(𝐿 ≤ 𝑀, (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿))))))))
159	5, 158	mpcom 38	. . . 4 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(𝐿 + (♯‘𝐵)))) → ((𝐴 substr ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩) ++ (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩)) = if(𝑁 ≤ 𝐿, (𝐴 substr ⟨𝑀, 𝑁⟩), if(𝐿 ≤ 𝑀, (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿)))))))
160	159	imp 406	. . 3 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(𝐿 + (♯‘𝐵))))) → ((𝐴 substr ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩) ++ (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩)) = if(𝑁 ≤ 𝐿, (𝐴 substr ⟨𝑀, 𝑁⟩), if(𝐿 ≤ 𝑀, (𝐵 substr ⟨(𝑀 − 𝐿), (𝑁 − 𝐿)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿))))))
161	3, 160	eqtr4d 2772	. 2 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(𝐿 + (♯‘𝐵))))) → ((𝐴 ++ 𝐵) substr ⟨𝑀, 𝑁⟩) = ((𝐴 substr ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩) ++ (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩)))
162	161	ex 412	1 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(𝐿 + (♯‘𝐵)))) → ((𝐴 ++ 𝐵) substr ⟨𝑀, 𝑁⟩) = ((𝐴 substr ⟨𝑀, if(𝑁 ≤ 𝐿, 𝑁, 𝐿)⟩) ++ (𝐵 substr ⟨if(0 ≤ (𝑀 − 𝐿), (𝑀 − 𝐿), 0), (𝑁 − 𝐿)⟩))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1539   ∈ wcel 2107  ∅c0 4306  ifcif 4498  ⟨cop 4605   class class class wbr 5116  ‘cfv 6527  (class class class)co 7399  ℝcr 11120  0cc0 11121   + caddc 11124   < clt 11261   ≤ cle 11262   − cmin 11458  ℕ₀cn0 12493  ℤcz 12580  ...cfz 13513  ♯chash 14336  Word cword 14519   ++ cconcat 14575   substr csubstr 14645   prefix cpfx 14675

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-rep 5246  ax-sep 5263  ax-nul 5273  ax-pow 5332  ax-pr 5399  ax-un 7723  ax-cnex 11177  ax-resscn 11178  ax-1cn 11179  ax-icn 11180  ax-addcl 11181  ax-addrcl 11182  ax-mulcl 11183  ax-mulrcl 11184  ax-mulcom 11185  ax-addass 11186  ax-mulass 11187  ax-distr 11188  ax-i2m1 11189  ax-1ne0 11190  ax-1rid 11191  ax-rnegex 11192  ax-rrecex 11193  ax-cnre 11194  ax-pre-lttri 11195  ax-pre-lttrn 11196  ax-pre-ltadd 11197  ax-pre-mulgt0 11198

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-nel 3036  df-ral 3051  df-rex 3060  df-reu 3358  df-rab 3414  df-v 3459  df-sbc 3764  df-csb 3873  df-dif 3927  df-un 3929  df-in 3931  df-ss 3941  df-pss 3944  df-nul 4307  df-if 4499  df-pw 4575  df-sn 4600  df-pr 4602  df-op 4606  df-uni 4881  df-int 4920  df-iun 4966  df-br 5117  df-opab 5179  df-mpt 5199  df-tr 5227  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6287  df-ord 6352  df-on 6353  df-lim 6354  df-suc 6355  df-iota 6480  df-fun 6529  df-fn 6530  df-f 6531  df-f1 6532  df-fo 6533  df-f1o 6534  df-fv 6535  df-riota 7356  df-ov 7402  df-oprab 7403  df-mpo 7404  df-om 7856  df-1st 7982  df-2nd 7983  df-frecs 8274  df-wrecs 8305  df-recs 8379  df-rdg 8418  df-1o 8474  df-er 8713  df-en 8954  df-dom 8955  df-sdom 8956  df-fin 8957  df-card 9945  df-pnf 11263  df-mnf 11264  df-xr 11265  df-ltxr 11266  df-le 11267  df-sub 11460  df-neg 11461  df-nn 12233  df-n0 12494  df-z 12581  df-uz 12845  df-fz 13514  df-fzo 13661  df-hash 14337  df-word 14520  df-concat 14576  df-substr 14646  df-pfx 14676

This theorem is referenced by: (None)