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