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 
|- L = ( # ` A )
Assertion pfxccat3 
|- ( ( A e. Word V /\ B e. Word V ) -> ( ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( L + ( # ` B ) ) ) ) -> ( ( A ++ B ) substr <. M , N >. ) = if ( N <_ L , ( A substr <. M , N >. ) , if ( L <_ M , ( B substr <. ( M - L ) , ( N - L ) >. ) , ( ( A substr <. M , L >. ) ++ ( B prefix ( N - L ) ) ) ) ) ) )

Proof

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