Theorem pfxccat3

Description: The subword of a concatenation is either a subword of the first concatenated word or a subword of the second concatenated word or a concatenation of a suffix of the first word with a prefix of the second word. (Contributed by Alexander van der Vekens, 30-Mar-2018) (Revised by AV, 10-May-2020)

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

Proof

Step	Hyp	Ref	Expression
1		swrdccatin2.l	⊢ 𝐿 = ( ♯ ‘ 𝐴 )
2		simpll	⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ 𝑁 ≤ 𝐿 ) → ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) )
3		simplrl	⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ 𝑁 ≤ 𝐿 ) → 𝑀 ∈ ( 0 ... 𝑁 ) )
4		lencl	⊢ ( 𝐴 ∈ Word 𝑉 → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
5		elfznn0	⊢ ( 𝑁 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) → 𝑁 ∈ ℕ0 )
6	5	adantr	⊢ ( ( 𝑁 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ0 ) → 𝑁 ∈ ℕ0 )
7	6	adantr	⊢ ( ( ( 𝑁 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ0 ) ∧ 𝑁 ≤ 𝐿 ) → 𝑁 ∈ ℕ0 )
8		simplr	⊢ ( ( ( 𝑁 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ0 ) ∧ 𝑁 ≤ 𝐿 ) → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
9	1	breq2i	⊢ ( 𝑁 ≤ 𝐿 ↔ 𝑁 ≤ ( ♯ ‘ 𝐴 ) )
10	9	bilani	⊢ ( ( ( 𝑁 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ0 ) ∧ 𝑁 ≤ 𝐿 ) → 𝑁 ≤ ( ♯ ‘ 𝐴 ) )
11		elfz2nn0	⊢ ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ↔ ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ0 ∧ 𝑁 ≤ ( ♯ ‘ 𝐴 ) ) )
12	7 8 10 11	syl3anbrc	⊢ ( ( ( 𝑁 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ0 ) ∧ 𝑁 ≤ 𝐿 ) → 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) )
13	12	exp31	⊢ ( 𝑁 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) → ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 → ( 𝑁 ≤ 𝐿 → 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) ) )
14	13	adantl	⊢ ( ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 → ( 𝑁 ≤ 𝐿 → 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) ) )
15	4 14	syl5com	⊢ ( 𝐴 ∈ Word 𝑉 → ( ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( 𝑁 ≤ 𝐿 → 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) ) )
16	15	adantr	⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( 𝑁 ≤ 𝐿 → 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) ) )
17	16	imp	⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) → ( 𝑁 ≤ 𝐿 → 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) )
18	17	imp	⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ 𝑁 ≤ 𝐿 ) → 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) )
19	3 18	jca	⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ 𝑁 ≤ 𝐿 ) → ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) )
20		swrdccatin1	⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( 𝐴 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) )
21	2 19 20	sylc	⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ 𝑁 ≤ 𝐿 ) → ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( 𝐴 substr ⟨ 𝑀 , 𝑁 ⟩ ) )
22		simp1l	⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ ¬ 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀 ) → ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) )
23	1	eleq1i	⊢ ( 𝐿 ∈ ℕ0 ↔ ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
24		elfz2nn0	⊢ ( 𝑀 ∈ ( 0 ... 𝑁 ) ↔ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) )
25		nn0z	⊢ ( 𝐿 ∈ ℕ0 → 𝐿 ∈ ℤ )
26	25	adantl	⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) ∧ 𝐿 ∈ ℕ0 ) → 𝐿 ∈ ℤ )
27		nn0z	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
28	27	3ad2ant2	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) → 𝑁 ∈ ℤ )
29	28	adantr	⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) ∧ 𝐿 ∈ ℕ0 ) → 𝑁 ∈ ℤ )
30		nn0z	⊢ ( 𝑀 ∈ ℕ0 → 𝑀 ∈ ℤ )
31	30	3ad2ant1	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) → 𝑀 ∈ ℤ )
32	31	adantr	⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) ∧ 𝐿 ∈ ℕ0 ) → 𝑀 ∈ ℤ )
33	26 29 32	3jca	⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) ∧ 𝐿 ∈ ℕ0 ) → ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) )
34	33	adantr	⊢ ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) ∧ 𝐿 ∈ ℕ0 ) ∧ 𝐿 ≤ 𝑀 ) → ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) )
35		simpl3	⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) ∧ 𝐿 ∈ ℕ0 ) → 𝑀 ≤ 𝑁 )
36	35	anim1ci	⊢ ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) ∧ 𝐿 ∈ ℕ0 ) ∧ 𝐿 ≤ 𝑀 ) → ( 𝐿 ≤ 𝑀 ∧ 𝑀 ≤ 𝑁 ) )
37		elfz2	⊢ ( 𝑀 ∈ ( 𝐿 ... 𝑁 ) ↔ ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ ( 𝐿 ≤ 𝑀 ∧ 𝑀 ≤ 𝑁 ) ) )
38	34 36 37	sylanbrc	⊢ ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) ∧ 𝐿 ∈ ℕ0 ) ∧ 𝐿 ≤ 𝑀 ) → 𝑀 ∈ ( 𝐿 ... 𝑁 ) )
39	38	exp31	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) → ( 𝐿 ∈ ℕ0 → ( 𝐿 ≤ 𝑀 → 𝑀 ∈ ( 𝐿 ... 𝑁 ) ) ) )
40	24 39	sylbi	⊢ ( 𝑀 ∈ ( 0 ... 𝑁 ) → ( 𝐿 ∈ ℕ0 → ( 𝐿 ≤ 𝑀 → 𝑀 ∈ ( 𝐿 ... 𝑁 ) ) ) )
41	40	adantr	⊢ ( ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( 𝐿 ∈ ℕ0 → ( 𝐿 ≤ 𝑀 → 𝑀 ∈ ( 𝐿 ... 𝑁 ) ) ) )
42	41	com12	⊢ ( 𝐿 ∈ ℕ0 → ( ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( 𝐿 ≤ 𝑀 → 𝑀 ∈ ( 𝐿 ... 𝑁 ) ) ) )
43	23 42	sylbir	⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 → ( ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( 𝐿 ≤ 𝑀 → 𝑀 ∈ ( 𝐿 ... 𝑁 ) ) ) )
44	4 43	syl	⊢ ( 𝐴 ∈ Word 𝑉 → ( ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( 𝐿 ≤ 𝑀 → 𝑀 ∈ ( 𝐿 ... 𝑁 ) ) ) )
45	44	adantr	⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( 𝐿 ≤ 𝑀 → 𝑀 ∈ ( 𝐿 ... 𝑁 ) ) ) )
46	45	imp	⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) → ( 𝐿 ≤ 𝑀 → 𝑀 ∈ ( 𝐿 ... 𝑁 ) ) )
47	46	a1d	⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) → ( ¬ 𝑁 ≤ 𝐿 → ( 𝐿 ≤ 𝑀 → 𝑀 ∈ ( 𝐿 ... 𝑁 ) ) ) )
48	47	3imp	⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ ¬ 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀 ) → 𝑀 ∈ ( 𝐿 ... 𝑁 ) )
49		elfz2nn0	⊢ ( 𝑁 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ↔ ( 𝑁 ∈ ℕ0 ∧ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ℕ0 ∧ 𝑁 ≤ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) )
50		nn0z	⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 → ( ♯ ‘ 𝐴 ) ∈ ℤ )
51	1 50	eqeltrid	⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 → 𝐿 ∈ ℤ )
52	51	adantr	⊢ ( ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 ∧ ¬ 𝑁 ≤ 𝐿 ) → 𝐿 ∈ ℤ )
53	52	adantl	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ℕ0 ∧ 𝑁 ≤ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 ∧ ¬ 𝑁 ≤ 𝐿 ) ) → 𝐿 ∈ ℤ )
54		nn0z	⊢ ( ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ℕ0 → ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ℤ )
55	54	3ad2ant2	⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ℕ0 ∧ 𝑁 ≤ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) → ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ℤ )
56	55	adantr	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ℕ0 ∧ 𝑁 ≤ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 ∧ ¬ 𝑁 ≤ 𝐿 ) ) → ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ℤ )
57	27	3ad2ant1	⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ℕ0 ∧ 𝑁 ≤ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) → 𝑁 ∈ ℤ )
58	57	adantr	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ℕ0 ∧ 𝑁 ≤ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 ∧ ¬ 𝑁 ≤ 𝐿 ) ) → 𝑁 ∈ ℤ )
59	53 56 58	3jca	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ℕ0 ∧ 𝑁 ≤ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 ∧ ¬ 𝑁 ≤ 𝐿 ) ) → ( 𝐿 ∈ ℤ ∧ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
60	1	eqcomi	⊢ ( ♯ ‘ 𝐴 ) = 𝐿
61	60	eleq1i	⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 ↔ 𝐿 ∈ ℕ0 )
62		nn0re	⊢ ( 𝐿 ∈ ℕ0 → 𝐿 ∈ ℝ )
63		nn0re	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
64		ltnle	⊢ ( ( 𝐿 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝐿 < 𝑁 ↔ ¬ 𝑁 ≤ 𝐿 ) )
65	62 63 64	syl2anr	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) → ( 𝐿 < 𝑁 ↔ ¬ 𝑁 ≤ 𝐿 ) )
66	65	bicomd	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) → ( ¬ 𝑁 ≤ 𝐿 ↔ 𝐿 < 𝑁 ) )
67		ltle	⊢ ( ( 𝐿 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝐿 < 𝑁 → 𝐿 ≤ 𝑁 ) )
68	62 63 67	syl2anr	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) → ( 𝐿 < 𝑁 → 𝐿 ≤ 𝑁 ) )
69	66 68	sylbid	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) → ( ¬ 𝑁 ≤ 𝐿 → 𝐿 ≤ 𝑁 ) )
70	69	ex	⊢ ( 𝑁 ∈ ℕ0 → ( 𝐿 ∈ ℕ0 → ( ¬ 𝑁 ≤ 𝐿 → 𝐿 ≤ 𝑁 ) ) )
71	61 70	biimtrid	⊢ ( 𝑁 ∈ ℕ0 → ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 → ( ¬ 𝑁 ≤ 𝐿 → 𝐿 ≤ 𝑁 ) ) )
72	71	3ad2ant1	⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ℕ0 ∧ 𝑁 ≤ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) → ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 → ( ¬ 𝑁 ≤ 𝐿 → 𝐿 ≤ 𝑁 ) ) )
73	72	imp32	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ℕ0 ∧ 𝑁 ≤ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 ∧ ¬ 𝑁 ≤ 𝐿 ) ) → 𝐿 ≤ 𝑁 )
74		simpl3	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ℕ0 ∧ 𝑁 ≤ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 ∧ ¬ 𝑁 ≤ 𝐿 ) ) → 𝑁 ≤ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) )
75	73 74	jca	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ℕ0 ∧ 𝑁 ≤ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 ∧ ¬ 𝑁 ≤ 𝐿 ) ) → ( 𝐿 ≤ 𝑁 ∧ 𝑁 ≤ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) )
76		elfz2	⊢ ( 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ↔ ( ( 𝐿 ∈ ℤ ∧ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐿 ≤ 𝑁 ∧ 𝑁 ≤ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) )
77	59 75 76	sylanbrc	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ℕ0 ∧ 𝑁 ≤ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 ∧ ¬ 𝑁 ≤ 𝐿 ) ) → 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) )
78	77	exp32	⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ℕ0 ∧ 𝑁 ≤ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) → ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 → ( ¬ 𝑁 ≤ 𝐿 → 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) )
79	49 78	sylbi	⊢ ( 𝑁 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) → ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 → ( ¬ 𝑁 ≤ 𝐿 → 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) )
80	79	adantl	⊢ ( ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 → ( ¬ 𝑁 ≤ 𝐿 → 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) )
81	4 80	syl5com	⊢ ( 𝐴 ∈ Word 𝑉 → ( ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( ¬ 𝑁 ≤ 𝐿 → 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) )
82	81	adantr	⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( ¬ 𝑁 ≤ 𝐿 → 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) )
83	82	imp	⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) → ( ¬ 𝑁 ≤ 𝐿 → 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) )
84	83	a1dd	⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) → ( ¬ 𝑁 ≤ 𝐿 → ( 𝐿 ≤ 𝑀 → 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) )
85	84	3imp	⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ ¬ 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀 ) → 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) )
86	48 85	jca	⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ ¬ 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀 ) → ( 𝑀 ∈ ( 𝐿 ... 𝑁 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) )
87	1	swrdccatin2	⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( ( 𝑀 ∈ ( 𝐿 ... 𝑁 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( 𝑁 − 𝐿 ) ⟩ ) ) )
88	22 86 87	sylc	⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ ¬ 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀 ) → ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( 𝑁 − 𝐿 ) ⟩ ) )
89		simp1l	⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀 ) → ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) )
90		nn0re	⊢ ( 𝑀 ∈ ℕ0 → 𝑀 ∈ ℝ )
91	90	adantr	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → 𝑀 ∈ ℝ )
92		ltnle	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝐿 ∈ ℝ ) → ( 𝑀 < 𝐿 ↔ ¬ 𝐿 ≤ 𝑀 ) )
93	91 62 92	syl2anr	⊢ ( ( 𝐿 ∈ ℕ0 ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → ( 𝑀 < 𝐿 ↔ ¬ 𝐿 ≤ 𝑀 ) )
94	93	bicomd	⊢ ( ( 𝐿 ∈ ℕ0 ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → ( ¬ 𝐿 ≤ 𝑀 ↔ 𝑀 < 𝐿 ) )
95		simpll	⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) ∧ 𝑀 < 𝐿 ) → 𝑀 ∈ ℕ0 )
96		simplr	⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) ∧ 𝑀 < 𝐿 ) → 𝐿 ∈ ℕ0 )
97		ltle	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝐿 ∈ ℝ ) → ( 𝑀 < 𝐿 → 𝑀 ≤ 𝐿 ) )
98	90 62 97	syl2an	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) → ( 𝑀 < 𝐿 → 𝑀 ≤ 𝐿 ) )
99	98	imp	⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) ∧ 𝑀 < 𝐿 ) → 𝑀 ≤ 𝐿 )
100		elfz2nn0	⊢ ( 𝑀 ∈ ( 0 ... 𝐿 ) ↔ ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝑀 ≤ 𝐿 ) )
101	95 96 99 100	syl3anbrc	⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) ∧ 𝑀 < 𝐿 ) → 𝑀 ∈ ( 0 ... 𝐿 ) )
102	101	exp31	⊢ ( 𝑀 ∈ ℕ0 → ( 𝐿 ∈ ℕ0 → ( 𝑀 < 𝐿 → 𝑀 ∈ ( 0 ... 𝐿 ) ) ) )
103	102	adantr	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝐿 ∈ ℕ0 → ( 𝑀 < 𝐿 → 𝑀 ∈ ( 0 ... 𝐿 ) ) ) )
104	103	impcom	⊢ ( ( 𝐿 ∈ ℕ0 ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → ( 𝑀 < 𝐿 → 𝑀 ∈ ( 0 ... 𝐿 ) ) )
105	94 104	sylbid	⊢ ( ( 𝐿 ∈ ℕ0 ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → ( ¬ 𝐿 ≤ 𝑀 → 𝑀 ∈ ( 0 ... 𝐿 ) ) )
106	105	expcom	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝐿 ∈ ℕ0 → ( ¬ 𝐿 ≤ 𝑀 → 𝑀 ∈ ( 0 ... 𝐿 ) ) ) )
107	106	3adant3	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) → ( 𝐿 ∈ ℕ0 → ( ¬ 𝐿 ≤ 𝑀 → 𝑀 ∈ ( 0 ... 𝐿 ) ) ) )
108	24 107	sylbi	⊢ ( 𝑀 ∈ ( 0 ... 𝑁 ) → ( 𝐿 ∈ ℕ0 → ( ¬ 𝐿 ≤ 𝑀 → 𝑀 ∈ ( 0 ... 𝐿 ) ) ) )
109	61 108	biimtrid	⊢ ( 𝑀 ∈ ( 0 ... 𝑁 ) → ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 → ( ¬ 𝐿 ≤ 𝑀 → 𝑀 ∈ ( 0 ... 𝐿 ) ) ) )
110	109	adantr	⊢ ( ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 → ( ¬ 𝐿 ≤ 𝑀 → 𝑀 ∈ ( 0 ... 𝐿 ) ) ) )
111	4 110	syl5com	⊢ ( 𝐴 ∈ Word 𝑉 → ( ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( ¬ 𝐿 ≤ 𝑀 → 𝑀 ∈ ( 0 ... 𝐿 ) ) ) )
112	111	adantr	⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( ¬ 𝐿 ≤ 𝑀 → 𝑀 ∈ ( 0 ... 𝐿 ) ) ) )
113	112	imp	⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) → ( ¬ 𝐿 ≤ 𝑀 → 𝑀 ∈ ( 0 ... 𝐿 ) ) )
114	113	a1d	⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) → ( ¬ 𝑁 ≤ 𝐿 → ( ¬ 𝐿 ≤ 𝑀 → 𝑀 ∈ ( 0 ... 𝐿 ) ) ) )
115	114	3imp	⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀 ) → 𝑀 ∈ ( 0 ... 𝐿 ) )
116	63	3ad2ant1	⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ℕ0 ∧ 𝑁 ≤ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) → 𝑁 ∈ ℝ )
117	64	bicomd	⊢ ( ( 𝐿 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ¬ 𝑁 ≤ 𝐿 ↔ 𝐿 < 𝑁 ) )
118	62 116 117	syl2an	⊢ ( ( 𝐿 ∈ ℕ0 ∧ ( 𝑁 ∈ ℕ0 ∧ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ℕ0 ∧ 𝑁 ≤ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( ¬ 𝑁 ≤ 𝐿 ↔ 𝐿 < 𝑁 ) )
119	25	adantr	⊢ ( ( 𝐿 ∈ ℕ0 ∧ ( 𝑁 ∈ ℕ0 ∧ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ℕ0 ∧ 𝑁 ≤ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → 𝐿 ∈ ℤ )
120	55	adantl	⊢ ( ( 𝐿 ∈ ℕ0 ∧ ( 𝑁 ∈ ℕ0 ∧ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ℕ0 ∧ 𝑁 ≤ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ℤ )
121	57	adantl	⊢ ( ( 𝐿 ∈ ℕ0 ∧ ( 𝑁 ∈ ℕ0 ∧ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ℕ0 ∧ 𝑁 ≤ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → 𝑁 ∈ ℤ )
122	119 120 121	3jca	⊢ ( ( 𝐿 ∈ ℕ0 ∧ ( 𝑁 ∈ ℕ0 ∧ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ℕ0 ∧ 𝑁 ≤ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( 𝐿 ∈ ℤ ∧ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
123	122	adantr	⊢ ( ( ( 𝐿 ∈ ℕ0 ∧ ( 𝑁 ∈ ℕ0 ∧ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ℕ0 ∧ 𝑁 ≤ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ∧ 𝐿 < 𝑁 ) → ( 𝐿 ∈ ℤ ∧ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
124	62 116 67	syl2an	⊢ ( ( 𝐿 ∈ ℕ0 ∧ ( 𝑁 ∈ ℕ0 ∧ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ℕ0 ∧ 𝑁 ≤ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( 𝐿 < 𝑁 → 𝐿 ≤ 𝑁 ) )
125	124	imp	⊢ ( ( ( 𝐿 ∈ ℕ0 ∧ ( 𝑁 ∈ ℕ0 ∧ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ℕ0 ∧ 𝑁 ≤ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ∧ 𝐿 < 𝑁 ) → 𝐿 ≤ 𝑁 )
126		simplr3	⊢ ( ( ( 𝐿 ∈ ℕ0 ∧ ( 𝑁 ∈ ℕ0 ∧ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ℕ0 ∧ 𝑁 ≤ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ∧ 𝐿 < 𝑁 ) → 𝑁 ≤ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) )
127	125 126	jca	⊢ ( ( ( 𝐿 ∈ ℕ0 ∧ ( 𝑁 ∈ ℕ0 ∧ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ℕ0 ∧ 𝑁 ≤ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ∧ 𝐿 < 𝑁 ) → ( 𝐿 ≤ 𝑁 ∧ 𝑁 ≤ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) )
128	123 127 76	sylanbrc	⊢ ( ( ( 𝐿 ∈ ℕ0 ∧ ( 𝑁 ∈ ℕ0 ∧ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ℕ0 ∧ 𝑁 ≤ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ∧ 𝐿 < 𝑁 ) → 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) )
129	128	ex	⊢ ( ( 𝐿 ∈ ℕ0 ∧ ( 𝑁 ∈ ℕ0 ∧ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ℕ0 ∧ 𝑁 ≤ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( 𝐿 < 𝑁 → 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) )
130	118 129	sylbid	⊢ ( ( 𝐿 ∈ ℕ0 ∧ ( 𝑁 ∈ ℕ0 ∧ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ℕ0 ∧ 𝑁 ≤ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( ¬ 𝑁 ≤ 𝐿 → 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) )
131	130	ex	⊢ ( 𝐿 ∈ ℕ0 → ( ( 𝑁 ∈ ℕ0 ∧ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ℕ0 ∧ 𝑁 ≤ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) → ( ¬ 𝑁 ≤ 𝐿 → 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) )
132	61 131	sylbi	⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 → ( ( 𝑁 ∈ ℕ0 ∧ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ℕ0 ∧ 𝑁 ≤ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) → ( ¬ 𝑁 ≤ 𝐿 → 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) )
133	4 132	syl	⊢ ( 𝐴 ∈ Word 𝑉 → ( ( 𝑁 ∈ ℕ0 ∧ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ℕ0 ∧ 𝑁 ≤ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) → ( ¬ 𝑁 ≤ 𝐿 → 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) )
134	133	adantr	⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( ( 𝑁 ∈ ℕ0 ∧ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ℕ0 ∧ 𝑁 ≤ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) → ( ¬ 𝑁 ≤ 𝐿 → 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) )
135	134	com12	⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ℕ0 ∧ 𝑁 ≤ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) → ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( ¬ 𝑁 ≤ 𝐿 → 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) )
136	49 135	sylbi	⊢ ( 𝑁 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) → ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( ¬ 𝑁 ≤ 𝐿 → 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) )
137	136	adantl	⊢ ( ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( ¬ 𝑁 ≤ 𝐿 → 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) )
138	137	impcom	⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) → ( ¬ 𝑁 ≤ 𝐿 → 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) )
139	138	a1dd	⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) → ( ¬ 𝑁 ≤ 𝐿 → ( ¬ 𝐿 ≤ 𝑀 → 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) )
140	139	3imp	⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀 ) → 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) )
141	115 140	jca	⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀 ) → ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) )
142	1	pfxccatin12	⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) ) )
143	89 141 142	sylc	⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀 ) → ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) )
144	21 88 143	2if2	⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) → ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) = if ( 𝑁 ≤ 𝐿 , ( 𝐴 substr ⟨ 𝑀 , 𝑁 ⟩ ) , if ( 𝐿 ≤ 𝑀 , ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( 𝑁 − 𝐿 ) ⟩ ) , ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) ) ) )
145	144	ex	⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) = if ( 𝑁 ≤ 𝐿 , ( 𝐴 substr ⟨ 𝑀 , 𝑁 ⟩ ) , if ( 𝐿 ≤ 𝑀 , ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( 𝑁 − 𝐿 ) ⟩ ) , ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) ) ) ) )