# Metamath Proof Explorer

## Theorem pfxccatin12lem2

Description: Lemma 2 for pfxccatin12 . (Contributed by AV, 30-Mar-2018) (Revised by AV, 9-May-2020)

Ref Expression
Hypothesis swrdccatin2.l ${⊢}{L}=\left|{A}\right|$
Assertion pfxccatin12lem2 ${⊢}\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left({M}\in \left(0\dots {L}\right)\wedge {N}\in \left({L}\dots {L}+\left|{B}\right|\right)\right)\right)\to \left(\left({K}\in \left(0..^{N}-{M}\right)\wedge ¬{K}\in \left(0..^{L}-{M}\right)\right)\to \left(\left({A}\mathrm{++}{B}\right)\mathrm{substr}⟨{M},{N}⟩\right)\left({K}\right)=\left({B}\mathrm{prefix}\left({N}-{L}\right)\right)\left({K}-\left|{A}\mathrm{substr}⟨{M},{L}⟩\right|\right)\right)$

### Proof

Step Hyp Ref Expression
1 swrdccatin2.l ${⊢}{L}=\left|{A}\right|$
2 1 pfxccatin12lem2c ${⊢}\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left({M}\in \left(0\dots {L}\right)\wedge {N}\in \left({L}\dots {L}+\left|{B}\right|\right)\right)\right)\to \left({A}\mathrm{++}{B}\in \mathrm{Word}{V}\wedge {M}\in \left(0\dots {N}\right)\wedge {N}\in \left(0\dots \left|{A}\mathrm{++}{B}\right|\right)\right)$
3 simprl ${⊢}\left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left({M}\in \left(0\dots {L}\right)\wedge {N}\in \left({L}\dots {L}+\left|{B}\right|\right)\right)\right)\wedge \left({K}\in \left(0..^{N}-{M}\right)\wedge ¬{K}\in \left(0..^{L}-{M}\right)\right)\right)\to {K}\in \left(0..^{N}-{M}\right)$
4 swrdfv ${⊢}\left(\left({A}\mathrm{++}{B}\in \mathrm{Word}{V}\wedge {M}\in \left(0\dots {N}\right)\wedge {N}\in \left(0\dots \left|{A}\mathrm{++}{B}\right|\right)\right)\wedge {K}\in \left(0..^{N}-{M}\right)\right)\to \left(\left({A}\mathrm{++}{B}\right)\mathrm{substr}⟨{M},{N}⟩\right)\left({K}\right)=\left({A}\mathrm{++}{B}\right)\left({K}+{M}\right)$
5 2 3 4 syl2an2r ${⊢}\left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left({M}\in \left(0\dots {L}\right)\wedge {N}\in \left({L}\dots {L}+\left|{B}\right|\right)\right)\right)\wedge \left({K}\in \left(0..^{N}-{M}\right)\wedge ¬{K}\in \left(0..^{L}-{M}\right)\right)\right)\to \left(\left({A}\mathrm{++}{B}\right)\mathrm{substr}⟨{M},{N}⟩\right)\left({K}\right)=\left({A}\mathrm{++}{B}\right)\left({K}+{M}\right)$
6 elfzoelz ${⊢}{K}\in \left(0..^{N}-{M}\right)\to {K}\in ℤ$
7 elfz2nn0 ${⊢}{M}\in \left(0\dots {L}\right)↔\left({M}\in {ℕ}_{0}\wedge {L}\in {ℕ}_{0}\wedge {M}\le {L}\right)$
8 nn0cn ${⊢}{M}\in {ℕ}_{0}\to {M}\in ℂ$
9 nn0cn ${⊢}{L}\in {ℕ}_{0}\to {L}\in ℂ$
10 8 9 anim12i ${⊢}\left({M}\in {ℕ}_{0}\wedge {L}\in {ℕ}_{0}\right)\to \left({M}\in ℂ\wedge {L}\in ℂ\right)$
11 zcn ${⊢}{K}\in ℤ\to {K}\in ℂ$
12 subcl ${⊢}\left({L}\in ℂ\wedge {M}\in ℂ\right)\to {L}-{M}\in ℂ$
13 12 ancoms ${⊢}\left({M}\in ℂ\wedge {L}\in ℂ\right)\to {L}-{M}\in ℂ$
14 13 anim1ci ${⊢}\left(\left({M}\in ℂ\wedge {L}\in ℂ\right)\wedge {K}\in ℂ\right)\to \left({K}\in ℂ\wedge {L}-{M}\in ℂ\right)$
15 subcl ${⊢}\left({K}\in ℂ\wedge {L}-{M}\in ℂ\right)\to {K}-\left({L}-{M}\right)\in ℂ$
16 14 15 syl ${⊢}\left(\left({M}\in ℂ\wedge {L}\in ℂ\right)\wedge {K}\in ℂ\right)\to {K}-\left({L}-{M}\right)\in ℂ$
17 16 addid1d ${⊢}\left(\left({M}\in ℂ\wedge {L}\in ℂ\right)\wedge {K}\in ℂ\right)\to {K}-\left({L}-{M}\right)+0={K}-\left({L}-{M}\right)$
18 simpr ${⊢}\left(\left({M}\in ℂ\wedge {L}\in ℂ\right)\wedge {K}\in ℂ\right)\to {K}\in ℂ$
19 simplr ${⊢}\left(\left({M}\in ℂ\wedge {L}\in ℂ\right)\wedge {K}\in ℂ\right)\to {L}\in ℂ$
20 simpll ${⊢}\left(\left({M}\in ℂ\wedge {L}\in ℂ\right)\wedge {K}\in ℂ\right)\to {M}\in ℂ$
21 18 19 20 subsub3d ${⊢}\left(\left({M}\in ℂ\wedge {L}\in ℂ\right)\wedge {K}\in ℂ\right)\to {K}-\left({L}-{M}\right)={K}+{M}-{L}$
22 17 21 eqtr2d ${⊢}\left(\left({M}\in ℂ\wedge {L}\in ℂ\right)\wedge {K}\in ℂ\right)\to {K}+{M}-{L}={K}-\left({L}-{M}\right)+0$
23 10 11 22 syl2an ${⊢}\left(\left({M}\in {ℕ}_{0}\wedge {L}\in {ℕ}_{0}\right)\wedge {K}\in ℤ\right)\to {K}+{M}-{L}={K}-\left({L}-{M}\right)+0$
24 oveq2 ${⊢}\left|{A}\right|={L}\to {K}+{M}-\left|{A}\right|={K}+{M}-{L}$
25 24 eqcoms ${⊢}{L}=\left|{A}\right|\to {K}+{M}-\left|{A}\right|={K}+{M}-{L}$
26 25 eqeq1d ${⊢}{L}=\left|{A}\right|\to \left({K}+{M}-\left|{A}\right|={K}-\left({L}-{M}\right)+0↔{K}+{M}-{L}={K}-\left({L}-{M}\right)+0\right)$
27 23 26 syl5ibr ${⊢}{L}=\left|{A}\right|\to \left(\left(\left({M}\in {ℕ}_{0}\wedge {L}\in {ℕ}_{0}\right)\wedge {K}\in ℤ\right)\to {K}+{M}-\left|{A}\right|={K}-\left({L}-{M}\right)+0\right)$
28 1 27 ax-mp ${⊢}\left(\left({M}\in {ℕ}_{0}\wedge {L}\in {ℕ}_{0}\right)\wedge {K}\in ℤ\right)\to {K}+{M}-\left|{A}\right|={K}-\left({L}-{M}\right)+0$
29 28 ex ${⊢}\left({M}\in {ℕ}_{0}\wedge {L}\in {ℕ}_{0}\right)\to \left({K}\in ℤ\to {K}+{M}-\left|{A}\right|={K}-\left({L}-{M}\right)+0\right)$
30 29 3adant3 ${⊢}\left({M}\in {ℕ}_{0}\wedge {L}\in {ℕ}_{0}\wedge {M}\le {L}\right)\to \left({K}\in ℤ\to {K}+{M}-\left|{A}\right|={K}-\left({L}-{M}\right)+0\right)$
31 7 30 sylbi ${⊢}{M}\in \left(0\dots {L}\right)\to \left({K}\in ℤ\to {K}+{M}-\left|{A}\right|={K}-\left({L}-{M}\right)+0\right)$
32 31 ad2antrl ${⊢}\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left({M}\in \left(0\dots {L}\right)\wedge {N}\in \left({L}\dots {L}+\left|{B}\right|\right)\right)\right)\to \left({K}\in ℤ\to {K}+{M}-\left|{A}\right|={K}-\left({L}-{M}\right)+0\right)$
33 6 32 syl5com ${⊢}{K}\in \left(0..^{N}-{M}\right)\to \left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left({M}\in \left(0\dots {L}\right)\wedge {N}\in \left({L}\dots {L}+\left|{B}\right|\right)\right)\right)\to {K}+{M}-\left|{A}\right|={K}-\left({L}-{M}\right)+0\right)$
34 33 adantr ${⊢}\left({K}\in \left(0..^{N}-{M}\right)\wedge ¬{K}\in \left(0..^{L}-{M}\right)\right)\to \left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left({M}\in \left(0\dots {L}\right)\wedge {N}\in \left({L}\dots {L}+\left|{B}\right|\right)\right)\right)\to {K}+{M}-\left|{A}\right|={K}-\left({L}-{M}\right)+0\right)$
35 34 impcom ${⊢}\left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left({M}\in \left(0\dots {L}\right)\wedge {N}\in \left({L}\dots {L}+\left|{B}\right|\right)\right)\right)\wedge \left({K}\in \left(0..^{N}-{M}\right)\wedge ¬{K}\in \left(0..^{L}-{M}\right)\right)\right)\to {K}+{M}-\left|{A}\right|={K}-\left({L}-{M}\right)+0$
36 35 fveq2d ${⊢}\left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left({M}\in \left(0\dots {L}\right)\wedge {N}\in \left({L}\dots {L}+\left|{B}\right|\right)\right)\right)\wedge \left({K}\in \left(0..^{N}-{M}\right)\wedge ¬{K}\in \left(0..^{L}-{M}\right)\right)\right)\to {B}\left({K}+{M}-\left|{A}\right|\right)={B}\left({K}-\left({L}-{M}\right)+0\right)$
37 simpll ${⊢}\left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left({M}\in \left(0\dots {L}\right)\wedge {N}\in \left({L}\dots {L}+\left|{B}\right|\right)\right)\right)\wedge \left({K}\in \left(0..^{N}-{M}\right)\wedge ¬{K}\in \left(0..^{L}-{M}\right)\right)\right)\to \left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)$
38 pfxccatin12lem2a ${⊢}\left({M}\in \left(0\dots {L}\right)\wedge {N}\in \left({L}\dots {L}+\left|{B}\right|\right)\right)\to \left(\left({K}\in \left(0..^{N}-{M}\right)\wedge ¬{K}\in \left(0..^{L}-{M}\right)\right)\to {K}+{M}\in \left({L}..^{L}+\left|{B}\right|\right)\right)$
39 38 adantl ${⊢}\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left({M}\in \left(0\dots {L}\right)\wedge {N}\in \left({L}\dots {L}+\left|{B}\right|\right)\right)\right)\to \left(\left({K}\in \left(0..^{N}-{M}\right)\wedge ¬{K}\in \left(0..^{L}-{M}\right)\right)\to {K}+{M}\in \left({L}..^{L}+\left|{B}\right|\right)\right)$
40 39 imp ${⊢}\left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left({M}\in \left(0\dots {L}\right)\wedge {N}\in \left({L}\dots {L}+\left|{B}\right|\right)\right)\right)\wedge \left({K}\in \left(0..^{N}-{M}\right)\wedge ¬{K}\in \left(0..^{L}-{M}\right)\right)\right)\to {K}+{M}\in \left({L}..^{L}+\left|{B}\right|\right)$
41 id ${⊢}\left|{A}\right|={L}\to \left|{A}\right|={L}$
42 oveq1 ${⊢}\left|{A}\right|={L}\to \left|{A}\right|+\left|{B}\right|={L}+\left|{B}\right|$
43 41 42 oveq12d ${⊢}\left|{A}\right|={L}\to \left(\left|{A}\right|..^\left|{A}\right|+\left|{B}\right|\right)=\left({L}..^{L}+\left|{B}\right|\right)$
44 43 eleq2d ${⊢}\left|{A}\right|={L}\to \left({K}+{M}\in \left(\left|{A}\right|..^\left|{A}\right|+\left|{B}\right|\right)↔{K}+{M}\in \left({L}..^{L}+\left|{B}\right|\right)\right)$
45 44 eqcoms ${⊢}{L}=\left|{A}\right|\to \left({K}+{M}\in \left(\left|{A}\right|..^\left|{A}\right|+\left|{B}\right|\right)↔{K}+{M}\in \left({L}..^{L}+\left|{B}\right|\right)\right)$
46 1 45 ax-mp ${⊢}{K}+{M}\in \left(\left|{A}\right|..^\left|{A}\right|+\left|{B}\right|\right)↔{K}+{M}\in \left({L}..^{L}+\left|{B}\right|\right)$
47 40 46 sylibr ${⊢}\left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left({M}\in \left(0\dots {L}\right)\wedge {N}\in \left({L}\dots {L}+\left|{B}\right|\right)\right)\right)\wedge \left({K}\in \left(0..^{N}-{M}\right)\wedge ¬{K}\in \left(0..^{L}-{M}\right)\right)\right)\to {K}+{M}\in \left(\left|{A}\right|..^\left|{A}\right|+\left|{B}\right|\right)$
48 df-3an ${⊢}\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\wedge {K}+{M}\in \left(\left|{A}\right|..^\left|{A}\right|+\left|{B}\right|\right)\right)↔\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge {K}+{M}\in \left(\left|{A}\right|..^\left|{A}\right|+\left|{B}\right|\right)\right)$
49 37 47 48 sylanbrc ${⊢}\left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left({M}\in \left(0\dots {L}\right)\wedge {N}\in \left({L}\dots {L}+\left|{B}\right|\right)\right)\right)\wedge \left({K}\in \left(0..^{N}-{M}\right)\wedge ¬{K}\in \left(0..^{L}-{M}\right)\right)\right)\to \left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\wedge {K}+{M}\in \left(\left|{A}\right|..^\left|{A}\right|+\left|{B}\right|\right)\right)$
50 ccatval2 ${⊢}\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\wedge {K}+{M}\in \left(\left|{A}\right|..^\left|{A}\right|+\left|{B}\right|\right)\right)\to \left({A}\mathrm{++}{B}\right)\left({K}+{M}\right)={B}\left({K}+{M}-\left|{A}\right|\right)$
51 49 50 syl ${⊢}\left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left({M}\in \left(0\dots {L}\right)\wedge {N}\in \left({L}\dots {L}+\left|{B}\right|\right)\right)\right)\wedge \left({K}\in \left(0..^{N}-{M}\right)\wedge ¬{K}\in \left(0..^{L}-{M}\right)\right)\right)\to \left({A}\mathrm{++}{B}\right)\left({K}+{M}\right)={B}\left({K}+{M}-\left|{A}\right|\right)$
52 simplr ${⊢}\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left({M}\in \left(0\dots {L}\right)\wedge {N}\in \left({L}\dots {L}+\left|{B}\right|\right)\right)\right)\to {B}\in \mathrm{Word}{V}$
53 52 adantr ${⊢}\left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left({M}\in \left(0\dots {L}\right)\wedge {N}\in \left({L}\dots {L}+\left|{B}\right|\right)\right)\right)\wedge \left({K}\in \left(0..^{N}-{M}\right)\wedge ¬{K}\in \left(0..^{L}-{M}\right)\right)\right)\to {B}\in \mathrm{Word}{V}$
54 lencl ${⊢}{B}\in \mathrm{Word}{V}\to \left|{B}\right|\in {ℕ}_{0}$
55 elfzel2 ${⊢}{M}\in \left(0\dots {L}\right)\to {L}\in ℤ$
56 zsubcl ${⊢}\left({N}\in ℤ\wedge {L}\in ℤ\right)\to {N}-{L}\in ℤ$
57 56 ancoms ${⊢}\left({L}\in ℤ\wedge {N}\in ℤ\right)\to {N}-{L}\in ℤ$
58 57 adantr ${⊢}\left(\left({L}\in ℤ\wedge {N}\in ℤ\right)\wedge {L}\le {N}\right)\to {N}-{L}\in ℤ$
59 zre ${⊢}{N}\in ℤ\to {N}\in ℝ$
60 zre ${⊢}{L}\in ℤ\to {L}\in ℝ$
61 subge0 ${⊢}\left({N}\in ℝ\wedge {L}\in ℝ\right)\to \left(0\le {N}-{L}↔{L}\le {N}\right)$
62 59 60 61 syl2anr ${⊢}\left({L}\in ℤ\wedge {N}\in ℤ\right)\to \left(0\le {N}-{L}↔{L}\le {N}\right)$
63 62 biimprd ${⊢}\left({L}\in ℤ\wedge {N}\in ℤ\right)\to \left({L}\le {N}\to 0\le {N}-{L}\right)$
64 63 imp ${⊢}\left(\left({L}\in ℤ\wedge {N}\in ℤ\right)\wedge {L}\le {N}\right)\to 0\le {N}-{L}$
65 elnn0z ${⊢}{N}-{L}\in {ℕ}_{0}↔\left({N}-{L}\in ℤ\wedge 0\le {N}-{L}\right)$
66 58 64 65 sylanbrc ${⊢}\left(\left({L}\in ℤ\wedge {N}\in ℤ\right)\wedge {L}\le {N}\right)\to {N}-{L}\in {ℕ}_{0}$
67 66 expcom ${⊢}{L}\le {N}\to \left(\left({L}\in ℤ\wedge {N}\in ℤ\right)\to {N}-{L}\in {ℕ}_{0}\right)$
68 67 adantr ${⊢}\left({L}\le {N}\wedge {N}\le {L}+\left|{B}\right|\right)\to \left(\left({L}\in ℤ\wedge {N}\in ℤ\right)\to {N}-{L}\in {ℕ}_{0}\right)$
69 68 expcomd ${⊢}\left({L}\le {N}\wedge {N}\le {L}+\left|{B}\right|\right)\to \left({N}\in ℤ\to \left({L}\in ℤ\to {N}-{L}\in {ℕ}_{0}\right)\right)$
70 69 com12 ${⊢}{N}\in ℤ\to \left(\left({L}\le {N}\wedge {N}\le {L}+\left|{B}\right|\right)\to \left({L}\in ℤ\to {N}-{L}\in {ℕ}_{0}\right)\right)$
71 70 3ad2ant3 ${⊢}\left({L}\in ℤ\wedge {L}+\left|{B}\right|\in ℤ\wedge {N}\in ℤ\right)\to \left(\left({L}\le {N}\wedge {N}\le {L}+\left|{B}\right|\right)\to \left({L}\in ℤ\to {N}-{L}\in {ℕ}_{0}\right)\right)$
72 71 imp ${⊢}\left(\left({L}\in ℤ\wedge {L}+\left|{B}\right|\in ℤ\wedge {N}\in ℤ\right)\wedge \left({L}\le {N}\wedge {N}\le {L}+\left|{B}\right|\right)\right)\to \left({L}\in ℤ\to {N}-{L}\in {ℕ}_{0}\right)$
73 72 com12 ${⊢}{L}\in ℤ\to \left(\left(\left({L}\in ℤ\wedge {L}+\left|{B}\right|\in ℤ\wedge {N}\in ℤ\right)\wedge \left({L}\le {N}\wedge {N}\le {L}+\left|{B}\right|\right)\right)\to {N}-{L}\in {ℕ}_{0}\right)$
74 73 adantr ${⊢}\left({L}\in ℤ\wedge \left|{B}\right|\in {ℕ}_{0}\right)\to \left(\left(\left({L}\in ℤ\wedge {L}+\left|{B}\right|\in ℤ\wedge {N}\in ℤ\right)\wedge \left({L}\le {N}\wedge {N}\le {L}+\left|{B}\right|\right)\right)\to {N}-{L}\in {ℕ}_{0}\right)$
75 74 imp ${⊢}\left(\left({L}\in ℤ\wedge \left|{B}\right|\in {ℕ}_{0}\right)\wedge \left(\left({L}\in ℤ\wedge {L}+\left|{B}\right|\in ℤ\wedge {N}\in ℤ\right)\wedge \left({L}\le {N}\wedge {N}\le {L}+\left|{B}\right|\right)\right)\right)\to {N}-{L}\in {ℕ}_{0}$
76 simplr ${⊢}\left(\left({L}\in ℤ\wedge \left|{B}\right|\in {ℕ}_{0}\right)\wedge \left(\left({L}\in ℤ\wedge {L}+\left|{B}\right|\in ℤ\wedge {N}\in ℤ\right)\wedge \left({L}\le {N}\wedge {N}\le {L}+\left|{B}\right|\right)\right)\right)\to \left|{B}\right|\in {ℕ}_{0}$
77 59 3ad2ant3 ${⊢}\left({L}\in ℤ\wedge {L}+\left|{B}\right|\in ℤ\wedge {N}\in ℤ\right)\to {N}\in ℝ$
78 77 adantl ${⊢}\left(\left({L}\in ℤ\wedge \left|{B}\right|\in {ℕ}_{0}\right)\wedge \left({L}\in ℤ\wedge {L}+\left|{B}\right|\in ℤ\wedge {N}\in ℤ\right)\right)\to {N}\in ℝ$
79 60 adantr ${⊢}\left({L}\in ℤ\wedge \left|{B}\right|\in {ℕ}_{0}\right)\to {L}\in ℝ$
80 79 adantr ${⊢}\left(\left({L}\in ℤ\wedge \left|{B}\right|\in {ℕ}_{0}\right)\wedge \left({L}\in ℤ\wedge {L}+\left|{B}\right|\in ℤ\wedge {N}\in ℤ\right)\right)\to {L}\in ℝ$
81 nn0re ${⊢}\left|{B}\right|\in {ℕ}_{0}\to \left|{B}\right|\in ℝ$
82 81 adantl ${⊢}\left({L}\in ℤ\wedge \left|{B}\right|\in {ℕ}_{0}\right)\to \left|{B}\right|\in ℝ$
83 82 adantr ${⊢}\left(\left({L}\in ℤ\wedge \left|{B}\right|\in {ℕ}_{0}\right)\wedge \left({L}\in ℤ\wedge {L}+\left|{B}\right|\in ℤ\wedge {N}\in ℤ\right)\right)\to \left|{B}\right|\in ℝ$
84 lesubadd2 ${⊢}\left({N}\in ℝ\wedge {L}\in ℝ\wedge \left|{B}\right|\in ℝ\right)\to \left({N}-{L}\le \left|{B}\right|↔{N}\le {L}+\left|{B}\right|\right)$
85 84 biimprd ${⊢}\left({N}\in ℝ\wedge {L}\in ℝ\wedge \left|{B}\right|\in ℝ\right)\to \left({N}\le {L}+\left|{B}\right|\to {N}-{L}\le \left|{B}\right|\right)$
86 78 80 83 85 syl3anc ${⊢}\left(\left({L}\in ℤ\wedge \left|{B}\right|\in {ℕ}_{0}\right)\wedge \left({L}\in ℤ\wedge {L}+\left|{B}\right|\in ℤ\wedge {N}\in ℤ\right)\right)\to \left({N}\le {L}+\left|{B}\right|\to {N}-{L}\le \left|{B}\right|\right)$
87 86 ex ${⊢}\left({L}\in ℤ\wedge \left|{B}\right|\in {ℕ}_{0}\right)\to \left(\left({L}\in ℤ\wedge {L}+\left|{B}\right|\in ℤ\wedge {N}\in ℤ\right)\to \left({N}\le {L}+\left|{B}\right|\to {N}-{L}\le \left|{B}\right|\right)\right)$
88 87 com13 ${⊢}{N}\le {L}+\left|{B}\right|\to \left(\left({L}\in ℤ\wedge {L}+\left|{B}\right|\in ℤ\wedge {N}\in ℤ\right)\to \left(\left({L}\in ℤ\wedge \left|{B}\right|\in {ℕ}_{0}\right)\to {N}-{L}\le \left|{B}\right|\right)\right)$
89 88 adantl ${⊢}\left({L}\le {N}\wedge {N}\le {L}+\left|{B}\right|\right)\to \left(\left({L}\in ℤ\wedge {L}+\left|{B}\right|\in ℤ\wedge {N}\in ℤ\right)\to \left(\left({L}\in ℤ\wedge \left|{B}\right|\in {ℕ}_{0}\right)\to {N}-{L}\le \left|{B}\right|\right)\right)$
90 89 impcom ${⊢}\left(\left({L}\in ℤ\wedge {L}+\left|{B}\right|\in ℤ\wedge {N}\in ℤ\right)\wedge \left({L}\le {N}\wedge {N}\le {L}+\left|{B}\right|\right)\right)\to \left(\left({L}\in ℤ\wedge \left|{B}\right|\in {ℕ}_{0}\right)\to {N}-{L}\le \left|{B}\right|\right)$
91 90 impcom ${⊢}\left(\left({L}\in ℤ\wedge \left|{B}\right|\in {ℕ}_{0}\right)\wedge \left(\left({L}\in ℤ\wedge {L}+\left|{B}\right|\in ℤ\wedge {N}\in ℤ\right)\wedge \left({L}\le {N}\wedge {N}\le {L}+\left|{B}\right|\right)\right)\right)\to {N}-{L}\le \left|{B}\right|$
92 75 76 91 3jca ${⊢}\left(\left({L}\in ℤ\wedge \left|{B}\right|\in {ℕ}_{0}\right)\wedge \left(\left({L}\in ℤ\wedge {L}+\left|{B}\right|\in ℤ\wedge {N}\in ℤ\right)\wedge \left({L}\le {N}\wedge {N}\le {L}+\left|{B}\right|\right)\right)\right)\to \left({N}-{L}\in {ℕ}_{0}\wedge \left|{B}\right|\in {ℕ}_{0}\wedge {N}-{L}\le \left|{B}\right|\right)$
93 92 ex ${⊢}\left({L}\in ℤ\wedge \left|{B}\right|\in {ℕ}_{0}\right)\to \left(\left(\left({L}\in ℤ\wedge {L}+\left|{B}\right|\in ℤ\wedge {N}\in ℤ\right)\wedge \left({L}\le {N}\wedge {N}\le {L}+\left|{B}\right|\right)\right)\to \left({N}-{L}\in {ℕ}_{0}\wedge \left|{B}\right|\in {ℕ}_{0}\wedge {N}-{L}\le \left|{B}\right|\right)\right)$
94 elfz2 ${⊢}{N}\in \left({L}\dots {L}+\left|{B}\right|\right)↔\left(\left({L}\in ℤ\wedge {L}+\left|{B}\right|\in ℤ\wedge {N}\in ℤ\right)\wedge \left({L}\le {N}\wedge {N}\le {L}+\left|{B}\right|\right)\right)$
95 elfz2nn0 ${⊢}{N}-{L}\in \left(0\dots \left|{B}\right|\right)↔\left({N}-{L}\in {ℕ}_{0}\wedge \left|{B}\right|\in {ℕ}_{0}\wedge {N}-{L}\le \left|{B}\right|\right)$
96 93 94 95 3imtr4g ${⊢}\left({L}\in ℤ\wedge \left|{B}\right|\in {ℕ}_{0}\right)\to \left({N}\in \left({L}\dots {L}+\left|{B}\right|\right)\to {N}-{L}\in \left(0\dots \left|{B}\right|\right)\right)$
97 96 ex ${⊢}{L}\in ℤ\to \left(\left|{B}\right|\in {ℕ}_{0}\to \left({N}\in \left({L}\dots {L}+\left|{B}\right|\right)\to {N}-{L}\in \left(0\dots \left|{B}\right|\right)\right)\right)$
98 97 com23 ${⊢}{L}\in ℤ\to \left({N}\in \left({L}\dots {L}+\left|{B}\right|\right)\to \left(\left|{B}\right|\in {ℕ}_{0}\to {N}-{L}\in \left(0\dots \left|{B}\right|\right)\right)\right)$
99 55 98 syl ${⊢}{M}\in \left(0\dots {L}\right)\to \left({N}\in \left({L}\dots {L}+\left|{B}\right|\right)\to \left(\left|{B}\right|\in {ℕ}_{0}\to {N}-{L}\in \left(0\dots \left|{B}\right|\right)\right)\right)$
100 99 imp ${⊢}\left({M}\in \left(0\dots {L}\right)\wedge {N}\in \left({L}\dots {L}+\left|{B}\right|\right)\right)\to \left(\left|{B}\right|\in {ℕ}_{0}\to {N}-{L}\in \left(0\dots \left|{B}\right|\right)\right)$
101 54 100 syl5com ${⊢}{B}\in \mathrm{Word}{V}\to \left(\left({M}\in \left(0\dots {L}\right)\wedge {N}\in \left({L}\dots {L}+\left|{B}\right|\right)\right)\to {N}-{L}\in \left(0\dots \left|{B}\right|\right)\right)$
102 101 adantl ${⊢}\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\to \left(\left({M}\in \left(0\dots {L}\right)\wedge {N}\in \left({L}\dots {L}+\left|{B}\right|\right)\right)\to {N}-{L}\in \left(0\dots \left|{B}\right|\right)\right)$
103 102 imp ${⊢}\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left({M}\in \left(0\dots {L}\right)\wedge {N}\in \left({L}\dots {L}+\left|{B}\right|\right)\right)\right)\to {N}-{L}\in \left(0\dots \left|{B}\right|\right)$
104 103 adantr ${⊢}\left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left({M}\in \left(0\dots {L}\right)\wedge {N}\in \left({L}\dots {L}+\left|{B}\right|\right)\right)\right)\wedge \left({K}\in \left(0..^{N}-{M}\right)\wedge ¬{K}\in \left(0..^{L}-{M}\right)\right)\right)\to {N}-{L}\in \left(0\dots \left|{B}\right|\right)$
105 pfxccatin12lem1 ${⊢}\left({M}\in \left(0\dots {L}\right)\wedge {N}\in \left({L}\dots {L}+\left|{B}\right|\right)\right)\to \left(\left({K}\in \left(0..^{N}-{M}\right)\wedge ¬{K}\in \left(0..^{L}-{M}\right)\right)\to {K}-\left({L}-{M}\right)\in \left(0..^{N}-{L}\right)\right)$
106 105 adantl ${⊢}\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left({M}\in \left(0\dots {L}\right)\wedge {N}\in \left({L}\dots {L}+\left|{B}\right|\right)\right)\right)\to \left(\left({K}\in \left(0..^{N}-{M}\right)\wedge ¬{K}\in \left(0..^{L}-{M}\right)\right)\to {K}-\left({L}-{M}\right)\in \left(0..^{N}-{L}\right)\right)$
107 106 imp ${⊢}\left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left({M}\in \left(0\dots {L}\right)\wedge {N}\in \left({L}\dots {L}+\left|{B}\right|\right)\right)\right)\wedge \left({K}\in \left(0..^{N}-{M}\right)\wedge ¬{K}\in \left(0..^{L}-{M}\right)\right)\right)\to {K}-\left({L}-{M}\right)\in \left(0..^{N}-{L}\right)$
108 pfxfv ${⊢}\left({B}\in \mathrm{Word}{V}\wedge {N}-{L}\in \left(0\dots \left|{B}\right|\right)\wedge {K}-\left({L}-{M}\right)\in \left(0..^{N}-{L}\right)\right)\to \left({B}\mathrm{prefix}\left({N}-{L}\right)\right)\left({K}-\left({L}-{M}\right)\right)={B}\left({K}-\left({L}-{M}\right)\right)$
109 53 104 107 108 syl3anc ${⊢}\left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left({M}\in \left(0\dots {L}\right)\wedge {N}\in \left({L}\dots {L}+\left|{B}\right|\right)\right)\right)\wedge \left({K}\in \left(0..^{N}-{M}\right)\wedge ¬{K}\in \left(0..^{L}-{M}\right)\right)\right)\to \left({B}\mathrm{prefix}\left({N}-{L}\right)\right)\left({K}-\left({L}-{M}\right)\right)={B}\left({K}-\left({L}-{M}\right)\right)$
110 6 zcnd ${⊢}{K}\in \left(0..^{N}-{M}\right)\to {K}\in ℂ$
111 110 ad2antrl ${⊢}\left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left({M}\in \left(0\dots {L}\right)\wedge {N}\in \left({L}\dots {L}+\left|{B}\right|\right)\right)\right)\wedge \left({K}\in \left(0..^{N}-{M}\right)\wedge ¬{K}\in \left(0..^{L}-{M}\right)\right)\right)\to {K}\in ℂ$
112 55 zcnd ${⊢}{M}\in \left(0\dots {L}\right)\to {L}\in ℂ$
113 112 ad2antrl ${⊢}\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left({M}\in \left(0\dots {L}\right)\wedge {N}\in \left({L}\dots {L}+\left|{B}\right|\right)\right)\right)\to {L}\in ℂ$
114 113 adantr ${⊢}\left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left({M}\in \left(0\dots {L}\right)\wedge {N}\in \left({L}\dots {L}+\left|{B}\right|\right)\right)\right)\wedge \left({K}\in \left(0..^{N}-{M}\right)\wedge ¬{K}\in \left(0..^{L}-{M}\right)\right)\right)\to {L}\in ℂ$
115 elfzelz ${⊢}{M}\in \left(0\dots {L}\right)\to {M}\in ℤ$
116 115 zcnd ${⊢}{M}\in \left(0\dots {L}\right)\to {M}\in ℂ$
117 116 ad2antrl ${⊢}\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left({M}\in \left(0\dots {L}\right)\wedge {N}\in \left({L}\dots {L}+\left|{B}\right|\right)\right)\right)\to {M}\in ℂ$
118 117 adantr ${⊢}\left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left({M}\in \left(0\dots {L}\right)\wedge {N}\in \left({L}\dots {L}+\left|{B}\right|\right)\right)\right)\wedge \left({K}\in \left(0..^{N}-{M}\right)\wedge ¬{K}\in \left(0..^{L}-{M}\right)\right)\right)\to {M}\in ℂ$
119 114 118 subcld ${⊢}\left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left({M}\in \left(0\dots {L}\right)\wedge {N}\in \left({L}\dots {L}+\left|{B}\right|\right)\right)\right)\wedge \left({K}\in \left(0..^{N}-{M}\right)\wedge ¬{K}\in \left(0..^{L}-{M}\right)\right)\right)\to {L}-{M}\in ℂ$
120 111 119 subcld ${⊢}\left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left({M}\in \left(0\dots {L}\right)\wedge {N}\in \left({L}\dots {L}+\left|{B}\right|\right)\right)\right)\wedge \left({K}\in \left(0..^{N}-{M}\right)\wedge ¬{K}\in \left(0..^{L}-{M}\right)\right)\right)\to {K}-\left({L}-{M}\right)\in ℂ$
121 120 addid1d ${⊢}\left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left({M}\in \left(0\dots {L}\right)\wedge {N}\in \left({L}\dots {L}+\left|{B}\right|\right)\right)\right)\wedge \left({K}\in \left(0..^{N}-{M}\right)\wedge ¬{K}\in \left(0..^{L}-{M}\right)\right)\right)\to {K}-\left({L}-{M}\right)+0={K}-\left({L}-{M}\right)$
122 121 eqcomd ${⊢}\left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left({M}\in \left(0\dots {L}\right)\wedge {N}\in \left({L}\dots {L}+\left|{B}\right|\right)\right)\right)\wedge \left({K}\in \left(0..^{N}-{M}\right)\wedge ¬{K}\in \left(0..^{L}-{M}\right)\right)\right)\to {K}-\left({L}-{M}\right)={K}-\left({L}-{M}\right)+0$
123 122 fveq2d ${⊢}\left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left({M}\in \left(0\dots {L}\right)\wedge {N}\in \left({L}\dots {L}+\left|{B}\right|\right)\right)\right)\wedge \left({K}\in \left(0..^{N}-{M}\right)\wedge ¬{K}\in \left(0..^{L}-{M}\right)\right)\right)\to {B}\left({K}-\left({L}-{M}\right)\right)={B}\left({K}-\left({L}-{M}\right)+0\right)$
124 109 123 eqtrd ${⊢}\left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left({M}\in \left(0\dots {L}\right)\wedge {N}\in \left({L}\dots {L}+\left|{B}\right|\right)\right)\right)\wedge \left({K}\in \left(0..^{N}-{M}\right)\wedge ¬{K}\in \left(0..^{L}-{M}\right)\right)\right)\to \left({B}\mathrm{prefix}\left({N}-{L}\right)\right)\left({K}-\left({L}-{M}\right)\right)={B}\left({K}-\left({L}-{M}\right)+0\right)$
125 36 51 124 3eqtr4d ${⊢}\left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left({M}\in \left(0\dots {L}\right)\wedge {N}\in \left({L}\dots {L}+\left|{B}\right|\right)\right)\right)\wedge \left({K}\in \left(0..^{N}-{M}\right)\wedge ¬{K}\in \left(0..^{L}-{M}\right)\right)\right)\to \left({A}\mathrm{++}{B}\right)\left({K}+{M}\right)=\left({B}\mathrm{prefix}\left({N}-{L}\right)\right)\left({K}-\left({L}-{M}\right)\right)$
126 simpll ${⊢}\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left({M}\in \left(0\dots {L}\right)\wedge {N}\in \left({L}\dots {L}+\left|{B}\right|\right)\right)\right)\to {A}\in \mathrm{Word}{V}$
127 simprl ${⊢}\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left({M}\in \left(0\dots {L}\right)\wedge {N}\in \left({L}\dots {L}+\left|{B}\right|\right)\right)\right)\to {M}\in \left(0\dots {L}\right)$
128 lencl ${⊢}{A}\in \mathrm{Word}{V}\to \left|{A}\right|\in {ℕ}_{0}$
129 elnn0uz ${⊢}\left|{A}\right|\in {ℕ}_{0}↔\left|{A}\right|\in {ℤ}_{\ge 0}$
130 eluzfz2 ${⊢}\left|{A}\right|\in {ℤ}_{\ge 0}\to \left|{A}\right|\in \left(0\dots \left|{A}\right|\right)$
131 129 130 sylbi ${⊢}\left|{A}\right|\in {ℕ}_{0}\to \left|{A}\right|\in \left(0\dots \left|{A}\right|\right)$
132 1 131 eqeltrid ${⊢}\left|{A}\right|\in {ℕ}_{0}\to {L}\in \left(0\dots \left|{A}\right|\right)$
133 128 132 syl ${⊢}{A}\in \mathrm{Word}{V}\to {L}\in \left(0\dots \left|{A}\right|\right)$
134 133 adantr ${⊢}\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\to {L}\in \left(0\dots \left|{A}\right|\right)$
135 134 adantr ${⊢}\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left({M}\in \left(0\dots {L}\right)\wedge {N}\in \left({L}\dots {L}+\left|{B}\right|\right)\right)\right)\to {L}\in \left(0\dots \left|{A}\right|\right)$
136 126 127 135 3jca ${⊢}\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left({M}\in \left(0\dots {L}\right)\wedge {N}\in \left({L}\dots {L}+\left|{B}\right|\right)\right)\right)\to \left({A}\in \mathrm{Word}{V}\wedge {M}\in \left(0\dots {L}\right)\wedge {L}\in \left(0\dots \left|{A}\right|\right)\right)$
137 136 adantr ${⊢}\left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left({M}\in \left(0\dots {L}\right)\wedge {N}\in \left({L}\dots {L}+\left|{B}\right|\right)\right)\right)\wedge \left({K}\in \left(0..^{N}-{M}\right)\wedge ¬{K}\in \left(0..^{L}-{M}\right)\right)\right)\to \left({A}\in \mathrm{Word}{V}\wedge {M}\in \left(0\dots {L}\right)\wedge {L}\in \left(0\dots \left|{A}\right|\right)\right)$
138 swrdlen ${⊢}\left({A}\in \mathrm{Word}{V}\wedge {M}\in \left(0\dots {L}\right)\wedge {L}\in \left(0\dots \left|{A}\right|\right)\right)\to \left|{A}\mathrm{substr}⟨{M},{L}⟩\right|={L}-{M}$
139 137 138 syl ${⊢}\left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left({M}\in \left(0\dots {L}\right)\wedge {N}\in \left({L}\dots {L}+\left|{B}\right|\right)\right)\right)\wedge \left({K}\in \left(0..^{N}-{M}\right)\wedge ¬{K}\in \left(0..^{L}-{M}\right)\right)\right)\to \left|{A}\mathrm{substr}⟨{M},{L}⟩\right|={L}-{M}$
140 139 eqcomd ${⊢}\left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left({M}\in \left(0\dots {L}\right)\wedge {N}\in \left({L}\dots {L}+\left|{B}\right|\right)\right)\right)\wedge \left({K}\in \left(0..^{N}-{M}\right)\wedge ¬{K}\in \left(0..^{L}-{M}\right)\right)\right)\to {L}-{M}=\left|{A}\mathrm{substr}⟨{M},{L}⟩\right|$
141 140 oveq2d ${⊢}\left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left({M}\in \left(0\dots {L}\right)\wedge {N}\in \left({L}\dots {L}+\left|{B}\right|\right)\right)\right)\wedge \left({K}\in \left(0..^{N}-{M}\right)\wedge ¬{K}\in \left(0..^{L}-{M}\right)\right)\right)\to {K}-\left({L}-{M}\right)={K}-\left|{A}\mathrm{substr}⟨{M},{L}⟩\right|$
142 141 fveq2d ${⊢}\left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left({M}\in \left(0\dots {L}\right)\wedge {N}\in \left({L}\dots {L}+\left|{B}\right|\right)\right)\right)\wedge \left({K}\in \left(0..^{N}-{M}\right)\wedge ¬{K}\in \left(0..^{L}-{M}\right)\right)\right)\to \left({B}\mathrm{prefix}\left({N}-{L}\right)\right)\left({K}-\left({L}-{M}\right)\right)=\left({B}\mathrm{prefix}\left({N}-{L}\right)\right)\left({K}-\left|{A}\mathrm{substr}⟨{M},{L}⟩\right|\right)$
143 5 125 142 3eqtrd ${⊢}\left(\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left({M}\in \left(0\dots {L}\right)\wedge {N}\in \left({L}\dots {L}+\left|{B}\right|\right)\right)\right)\wedge \left({K}\in \left(0..^{N}-{M}\right)\wedge ¬{K}\in \left(0..^{L}-{M}\right)\right)\right)\to \left(\left({A}\mathrm{++}{B}\right)\mathrm{substr}⟨{M},{N}⟩\right)\left({K}\right)=\left({B}\mathrm{prefix}\left({N}-{L}\right)\right)\left({K}-\left|{A}\mathrm{substr}⟨{M},{L}⟩\right|\right)$
144 143 ex ${⊢}\left(\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\right)\wedge \left({M}\in \left(0\dots {L}\right)\wedge {N}\in \left({L}\dots {L}+\left|{B}\right|\right)\right)\right)\to \left(\left({K}\in \left(0..^{N}-{M}\right)\wedge ¬{K}\in \left(0..^{L}-{M}\right)\right)\to \left(\left({A}\mathrm{++}{B}\right)\mathrm{substr}⟨{M},{N}⟩\right)\left({K}\right)=\left({B}\mathrm{prefix}\left({N}-{L}\right)\right)\left({K}-\left|{A}\mathrm{substr}⟨{M},{L}⟩\right|\right)\right)$