This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ( 𝑁 − 𝐿 ) ) ) ) ) ) )