Metamath Proof Explorer

Theorem swrdswrdlem

Description: Lemma for swrdswrd . (Contributed by Alexander van der Vekens, 4-Apr-2018)

Ref Expression
Assertion swrdswrdlem 
|- ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) /\ ( K e. ( 0 ... ( N - M ) ) /\ L e. ( K ... ( N - M ) ) ) ) -> ( W e. Word V /\ ( M + K ) e. ( 0 ... ( M + L ) ) /\ ( M + L ) e. ( 0 ... ( # ` W ) ) ) )

Proof

Step Hyp Ref Expression
1 simpl1 
 |-  ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) /\ ( K e. ( 0 ... ( N - M ) ) /\ L e. ( K ... ( N - M ) ) ) ) -> W e. Word V )
2 elfz2 
 |-  ( L e. ( K ... ( N - M ) ) <-> ( ( K e. ZZ /\ ( N - M ) e. ZZ /\ L e. ZZ ) /\ ( K <_ L /\ L <_ ( N - M ) ) ) )
3 elfz2nn0 
 |-  ( K e. ( 0 ... ( N - M ) ) <-> ( K e. NN0 /\ ( N - M ) e. NN0 /\ K <_ ( N - M ) ) )
4 elfz2nn0 
 |-  ( M e. ( 0 ... N ) <-> ( M e. NN0 /\ N e. NN0 /\ M <_ N ) )
5 nn0addcl 
 |-  ( ( M e. NN0 /\ K e. NN0 ) -> ( M + K ) e. NN0 )
6 5 adantrr 
 |-  ( ( M e. NN0 /\ ( K e. NN0 /\ L e. ZZ ) ) -> ( M + K ) e. NN0 )
7 6 adantr 
 |-  ( ( ( M e. NN0 /\ ( K e. NN0 /\ L e. ZZ ) ) /\ K <_ L ) -> ( M + K ) e. NN0 )
8 elnn0z 
 |-  ( K e. NN0 <-> ( K e. ZZ /\ 0 <_ K ) )
9 0red 
 |-  ( ( K e. ZZ /\ L e. ZZ ) -> 0 e. RR )
10 zre 
 |-  ( K e. ZZ -> K e. RR )
11 10 adantr 
 |-  ( ( K e. ZZ /\ L e. ZZ ) -> K e. RR )
12 zre 
 |-  ( L e. ZZ -> L e. RR )
13 12 adantl 
 |-  ( ( K e. ZZ /\ L e. ZZ ) -> L e. RR )
14 letr 
 |-  ( ( 0 e. RR /\ K e. RR /\ L e. RR ) -> ( ( 0 <_ K /\ K <_ L ) -> 0 <_ L ) )
15 9 11 13 14 syl3anc 
 |-  ( ( K e. ZZ /\ L e. ZZ ) -> ( ( 0 <_ K /\ K <_ L ) -> 0 <_ L ) )
16 elnn0z 
 |-  ( L e. NN0 <-> ( L e. ZZ /\ 0 <_ L ) )
17 nn0addcl 
 |-  ( ( M e. NN0 /\ L e. NN0 ) -> ( M + L ) e. NN0 )
18 17 expcom 
 |-  ( L e. NN0 -> ( M e. NN0 -> ( M + L ) e. NN0 ) )
19 16 18 sylbir 
 |-  ( ( L e. ZZ /\ 0 <_ L ) -> ( M e. NN0 -> ( M + L ) e. NN0 ) )
20 19 ex 
 |-  ( L e. ZZ -> ( 0 <_ L -> ( M e. NN0 -> ( M + L ) e. NN0 ) ) )
21 20 adantl 
 |-  ( ( K e. ZZ /\ L e. ZZ ) -> ( 0 <_ L -> ( M e. NN0 -> ( M + L ) e. NN0 ) ) )
22 15 21 syld 
 |-  ( ( K e. ZZ /\ L e. ZZ ) -> ( ( 0 <_ K /\ K <_ L ) -> ( M e. NN0 -> ( M + L ) e. NN0 ) ) )
23 22 expd 
 |-  ( ( K e. ZZ /\ L e. ZZ ) -> ( 0 <_ K -> ( K <_ L -> ( M e. NN0 -> ( M + L ) e. NN0 ) ) ) )
24 23 com34 
 |-  ( ( K e. ZZ /\ L e. ZZ ) -> ( 0 <_ K -> ( M e. NN0 -> ( K <_ L -> ( M + L ) e. NN0 ) ) ) )
25 24 impancom 
 |-  ( ( K e. ZZ /\ 0 <_ K ) -> ( L e. ZZ -> ( M e. NN0 -> ( K <_ L -> ( M + L ) e. NN0 ) ) ) )
26 8 25 sylbi 
 |-  ( K e. NN0 -> ( L e. ZZ -> ( M e. NN0 -> ( K <_ L -> ( M + L ) e. NN0 ) ) ) )
27 26 imp 
 |-  ( ( K e. NN0 /\ L e. ZZ ) -> ( M e. NN0 -> ( K <_ L -> ( M + L ) e. NN0 ) ) )
28 27 impcom 
 |-  ( ( M e. NN0 /\ ( K e. NN0 /\ L e. ZZ ) ) -> ( K <_ L -> ( M + L ) e. NN0 ) )
29 28 imp 
 |-  ( ( ( M e. NN0 /\ ( K e. NN0 /\ L e. ZZ ) ) /\ K <_ L ) -> ( M + L ) e. NN0 )
30 nn0re 
 |-  ( K e. NN0 -> K e. RR )
31 30 adantr 
 |-  ( ( K e. NN0 /\ L e. ZZ ) -> K e. RR )
32 31 adantl 
 |-  ( ( M e. NN0 /\ ( K e. NN0 /\ L e. ZZ ) ) -> K e. RR )
33 12 adantl 
 |-  ( ( K e. NN0 /\ L e. ZZ ) -> L e. RR )
34 33 adantl 
 |-  ( ( M e. NN0 /\ ( K e. NN0 /\ L e. ZZ ) ) -> L e. RR )
35 nn0re 
 |-  ( M e. NN0 -> M e. RR )
36 35 adantr 
 |-  ( ( M e. NN0 /\ ( K e. NN0 /\ L e. ZZ ) ) -> M e. RR )
37 32 34 36 leadd2d 
 |-  ( ( M e. NN0 /\ ( K e. NN0 /\ L e. ZZ ) ) -> ( K <_ L <-> ( M + K ) <_ ( M + L ) ) )
38 37 biimpa 
 |-  ( ( ( M e. NN0 /\ ( K e. NN0 /\ L e. ZZ ) ) /\ K <_ L ) -> ( M + K ) <_ ( M + L ) )
39 7 29 38 3jca 
 |-  ( ( ( M e. NN0 /\ ( K e. NN0 /\ L e. ZZ ) ) /\ K <_ L ) -> ( ( M + K ) e. NN0 /\ ( M + L ) e. NN0 /\ ( M + K ) <_ ( M + L ) ) )
40 39 exp31 
 |-  ( M e. NN0 -> ( ( K e. NN0 /\ L e. ZZ ) -> ( K <_ L -> ( ( M + K ) e. NN0 /\ ( M + L ) e. NN0 /\ ( M + K ) <_ ( M + L ) ) ) ) )
41 40 com23 
 |-  ( M e. NN0 -> ( K <_ L -> ( ( K e. NN0 /\ L e. ZZ ) -> ( ( M + K ) e. NN0 /\ ( M + L ) e. NN0 /\ ( M + K ) <_ ( M + L ) ) ) ) )
42 41 3ad2ant1 
 |-  ( ( M e. NN0 /\ N e. NN0 /\ M <_ N ) -> ( K <_ L -> ( ( K e. NN0 /\ L e. ZZ ) -> ( ( M + K ) e. NN0 /\ ( M + L ) e. NN0 /\ ( M + K ) <_ ( M + L ) ) ) ) )
43 4 42 sylbi 
 |-  ( M e. ( 0 ... N ) -> ( K <_ L -> ( ( K e. NN0 /\ L e. ZZ ) -> ( ( M + K ) e. NN0 /\ ( M + L ) e. NN0 /\ ( M + K ) <_ ( M + L ) ) ) ) )
44 43 3ad2ant3 
 |-  ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) -> ( K <_ L -> ( ( K e. NN0 /\ L e. ZZ ) -> ( ( M + K ) e. NN0 /\ ( M + L ) e. NN0 /\ ( M + K ) <_ ( M + L ) ) ) ) )
45 44 com13 
 |-  ( ( K e. NN0 /\ L e. ZZ ) -> ( K <_ L -> ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) -> ( ( M + K ) e. NN0 /\ ( M + L ) e. NN0 /\ ( M + K ) <_ ( M + L ) ) ) ) )
46 45 ex 
 |-  ( K e. NN0 -> ( L e. ZZ -> ( K <_ L -> ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) -> ( ( M + K ) e. NN0 /\ ( M + L ) e. NN0 /\ ( M + K ) <_ ( M + L ) ) ) ) ) )
47 46 3ad2ant1 
 |-  ( ( K e. NN0 /\ ( N - M ) e. NN0 /\ K <_ ( N - M ) ) -> ( L e. ZZ -> ( K <_ L -> ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) -> ( ( M + K ) e. NN0 /\ ( M + L ) e. NN0 /\ ( M + K ) <_ ( M + L ) ) ) ) ) )
48 3 47 sylbi 
 |-  ( K e. ( 0 ... ( N - M ) ) -> ( L e. ZZ -> ( K <_ L -> ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) -> ( ( M + K ) e. NN0 /\ ( M + L ) e. NN0 /\ ( M + K ) <_ ( M + L ) ) ) ) ) )
49 48 com13 
 |-  ( K <_ L -> ( L e. ZZ -> ( K e. ( 0 ... ( N - M ) ) -> ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) -> ( ( M + K ) e. NN0 /\ ( M + L ) e. NN0 /\ ( M + K ) <_ ( M + L ) ) ) ) ) )
50 49 adantr 
 |-  ( ( K <_ L /\ L <_ ( N - M ) ) -> ( L e. ZZ -> ( K e. ( 0 ... ( N - M ) ) -> ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) -> ( ( M + K ) e. NN0 /\ ( M + L ) e. NN0 /\ ( M + K ) <_ ( M + L ) ) ) ) ) )
51 50 com12 
 |-  ( L e. ZZ -> ( ( K <_ L /\ L <_ ( N - M ) ) -> ( K e. ( 0 ... ( N - M ) ) -> ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) -> ( ( M + K ) e. NN0 /\ ( M + L ) e. NN0 /\ ( M + K ) <_ ( M + L ) ) ) ) ) )
52 51 3ad2ant3 
 |-  ( ( K e. ZZ /\ ( N - M ) e. ZZ /\ L e. ZZ ) -> ( ( K <_ L /\ L <_ ( N - M ) ) -> ( K e. ( 0 ... ( N - M ) ) -> ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) -> ( ( M + K ) e. NN0 /\ ( M + L ) e. NN0 /\ ( M + K ) <_ ( M + L ) ) ) ) ) )
53 52 imp 
 |-  ( ( ( K e. ZZ /\ ( N - M ) e. ZZ /\ L e. ZZ ) /\ ( K <_ L /\ L <_ ( N - M ) ) ) -> ( K e. ( 0 ... ( N - M ) ) -> ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) -> ( ( M + K ) e. NN0 /\ ( M + L ) e. NN0 /\ ( M + K ) <_ ( M + L ) ) ) ) )
54 2 53 sylbi 
 |-  ( L e. ( K ... ( N - M ) ) -> ( K e. ( 0 ... ( N - M ) ) -> ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) -> ( ( M + K ) e. NN0 /\ ( M + L ) e. NN0 /\ ( M + K ) <_ ( M + L ) ) ) ) )
55 54 impcom 
 |-  ( ( K e. ( 0 ... ( N - M ) ) /\ L e. ( K ... ( N - M ) ) ) -> ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) -> ( ( M + K ) e. NN0 /\ ( M + L ) e. NN0 /\ ( M + K ) <_ ( M + L ) ) ) )
56 55 impcom 
 |-  ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) /\ ( K e. ( 0 ... ( N - M ) ) /\ L e. ( K ... ( N - M ) ) ) ) -> ( ( M + K ) e. NN0 /\ ( M + L ) e. NN0 /\ ( M + K ) <_ ( M + L ) ) )
57 elfz2nn0 
 |-  ( ( M + K ) e. ( 0 ... ( M + L ) ) <-> ( ( M + K ) e. NN0 /\ ( M + L ) e. NN0 /\ ( M + K ) <_ ( M + L ) ) )
58 56 57 sylibr 
 |-  ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) /\ ( K e. ( 0 ... ( N - M ) ) /\ L e. ( K ... ( N - M ) ) ) ) -> ( M + K ) e. ( 0 ... ( M + L ) ) )
59 elfz2nn0 
 |-  ( N e. ( 0 ... ( # ` W ) ) <-> ( N e. NN0 /\ ( # ` W ) e. NN0 /\ N <_ ( # ` W ) ) )
60 28 com12 
 |-  ( K <_ L -> ( ( M e. NN0 /\ ( K e. NN0 /\ L e. ZZ ) ) -> ( M + L ) e. NN0 ) )
61 60 adantr 
 |-  ( ( K <_ L /\ L <_ ( N - M ) ) -> ( ( M e. NN0 /\ ( K e. NN0 /\ L e. ZZ ) ) -> ( M + L ) e. NN0 ) )
62 61 impcom 
 |-  ( ( ( M e. NN0 /\ ( K e. NN0 /\ L e. ZZ ) ) /\ ( K <_ L /\ L <_ ( N - M ) ) ) -> ( M + L ) e. NN0 )
63 62 adantr 
 |-  ( ( ( ( M e. NN0 /\ ( K e. NN0 /\ L e. ZZ ) ) /\ ( K <_ L /\ L <_ ( N - M ) ) ) /\ ( N e. NN0 /\ ( # ` W ) e. NN0 /\ N <_ ( # ` W ) ) ) -> ( M + L ) e. NN0 )
64 simpr2 
 |-  ( ( ( ( M e. NN0 /\ ( K e. NN0 /\ L e. ZZ ) ) /\ ( K <_ L /\ L <_ ( N - M ) ) ) /\ ( N e. NN0 /\ ( # ` W ) e. NN0 /\ N <_ ( # ` W ) ) ) -> ( # ` W ) e. NN0 )
65 nn0re 
 |-  ( N e. NN0 -> N e. RR )
66 65 35 anim12i 
 |-  ( ( N e. NN0 /\ M e. NN0 ) -> ( N e. RR /\ M e. RR ) )
67 nn0re 
 |-  ( ( # ` W ) e. NN0 -> ( # ` W ) e. RR )
68 66 67 anim12i 
 |-  ( ( ( N e. NN0 /\ M e. NN0 ) /\ ( # ` W ) e. NN0 ) -> ( ( N e. RR /\ M e. RR ) /\ ( # ` W ) e. RR ) )
69 simpllr 
 |-  ( ( ( ( N e. RR /\ M e. RR ) /\ ( # ` W ) e. RR ) /\ L e. RR ) -> M e. RR )
70 simpr 
 |-  ( ( ( ( N e. RR /\ M e. RR ) /\ ( # ` W ) e. RR ) /\ L e. RR ) -> L e. RR )
71 simplll 
 |-  ( ( ( ( N e. RR /\ M e. RR ) /\ ( # ` W ) e. RR ) /\ L e. RR ) -> N e. RR )
72 69 70 71 leaddsub2d 
 |-  ( ( ( ( N e. RR /\ M e. RR ) /\ ( # ` W ) e. RR ) /\ L e. RR ) -> ( ( M + L ) <_ N <-> L <_ ( N - M ) ) )
73 readdcl 
 |-  ( ( M e. RR /\ L e. RR ) -> ( M + L ) e. RR )
74 73 ad4ant24 
 |-  ( ( ( ( N e. RR /\ M e. RR ) /\ ( # ` W ) e. RR ) /\ L e. RR ) -> ( M + L ) e. RR )
75 simpr 
 |-  ( ( ( N e. RR /\ M e. RR ) /\ ( # ` W ) e. RR ) -> ( # ` W ) e. RR )
76 75 adantr 
 |-  ( ( ( ( N e. RR /\ M e. RR ) /\ ( # ` W ) e. RR ) /\ L e. RR ) -> ( # ` W ) e. RR )
77 letr 
 |-  ( ( ( M + L ) e. RR /\ N e. RR /\ ( # ` W ) e. RR ) -> ( ( ( M + L ) <_ N /\ N <_ ( # ` W ) ) -> ( M + L ) <_ ( # ` W ) ) )
78 77 expd 
 |-  ( ( ( M + L ) e. RR /\ N e. RR /\ ( # ` W ) e. RR ) -> ( ( M + L ) <_ N -> ( N <_ ( # ` W ) -> ( M + L ) <_ ( # ` W ) ) ) )
79 74 71 76 78 syl3anc 
 |-  ( ( ( ( N e. RR /\ M e. RR ) /\ ( # ` W ) e. RR ) /\ L e. RR ) -> ( ( M + L ) <_ N -> ( N <_ ( # ` W ) -> ( M + L ) <_ ( # ` W ) ) ) )
80 79 a1ddd 
 |-  ( ( ( ( N e. RR /\ M e. RR ) /\ ( # ` W ) e. RR ) /\ L e. RR ) -> ( ( M + L ) <_ N -> ( N <_ ( # ` W ) -> ( 0 <_ L -> ( M + L ) <_ ( # ` W ) ) ) ) )
81 72 80 sylbird 
 |-  ( ( ( ( N e. RR /\ M e. RR ) /\ ( # ` W ) e. RR ) /\ L e. RR ) -> ( L <_ ( N - M ) -> ( N <_ ( # ` W ) -> ( 0 <_ L -> ( M + L ) <_ ( # ` W ) ) ) ) )
82 81 com23 
 |-  ( ( ( ( N e. RR /\ M e. RR ) /\ ( # ` W ) e. RR ) /\ L e. RR ) -> ( N <_ ( # ` W ) -> ( L <_ ( N - M ) -> ( 0 <_ L -> ( M + L ) <_ ( # ` W ) ) ) ) )
83 68 12 82 syl2an 
 |-  ( ( ( ( N e. NN0 /\ M e. NN0 ) /\ ( # ` W ) e. NN0 ) /\ L e. ZZ ) -> ( N <_ ( # ` W ) -> ( L <_ ( N - M ) -> ( 0 <_ L -> ( M + L ) <_ ( # ` W ) ) ) ) )
84 83 ex 
 |-  ( ( ( N e. NN0 /\ M e. NN0 ) /\ ( # ` W ) e. NN0 ) -> ( L e. ZZ -> ( N <_ ( # ` W ) -> ( L <_ ( N - M ) -> ( 0 <_ L -> ( M + L ) <_ ( # ` W ) ) ) ) ) )
85 84 com25 
 |-  ( ( ( N e. NN0 /\ M e. NN0 ) /\ ( # ` W ) e. NN0 ) -> ( 0 <_ L -> ( N <_ ( # ` W ) -> ( L <_ ( N - M ) -> ( L e. ZZ -> ( M + L ) <_ ( # ` W ) ) ) ) ) )
86 85 ex 
 |-  ( ( N e. NN0 /\ M e. NN0 ) -> ( ( # ` W ) e. NN0 -> ( 0 <_ L -> ( N <_ ( # ` W ) -> ( L <_ ( N - M ) -> ( L e. ZZ -> ( M + L ) <_ ( # ` W ) ) ) ) ) ) )
87 86 com24 
 |-  ( ( N e. NN0 /\ M e. NN0 ) -> ( N <_ ( # ` W ) -> ( 0 <_ L -> ( ( # ` W ) e. NN0 -> ( L <_ ( N - M ) -> ( L e. ZZ -> ( M + L ) <_ ( # ` W ) ) ) ) ) ) )
88 87 ex 
 |-  ( N e. NN0 -> ( M e. NN0 -> ( N <_ ( # ` W ) -> ( 0 <_ L -> ( ( # ` W ) e. NN0 -> ( L <_ ( N - M ) -> ( L e. ZZ -> ( M + L ) <_ ( # ` W ) ) ) ) ) ) ) )
89 88 com25 
 |-  ( N e. NN0 -> ( ( # ` W ) e. NN0 -> ( N <_ ( # ` W ) -> ( 0 <_ L -> ( M e. NN0 -> ( L <_ ( N - M ) -> ( L e. ZZ -> ( M + L ) <_ ( # ` W ) ) ) ) ) ) ) )
90 89 3imp 
 |-  ( ( N e. NN0 /\ ( # ` W ) e. NN0 /\ N <_ ( # ` W ) ) -> ( 0 <_ L -> ( M e. NN0 -> ( L <_ ( N - M ) -> ( L e. ZZ -> ( M + L ) <_ ( # ` W ) ) ) ) ) )
91 90 com15 
 |-  ( L e. ZZ -> ( 0 <_ L -> ( M e. NN0 -> ( L <_ ( N - M ) -> ( ( N e. NN0 /\ ( # ` W ) e. NN0 /\ N <_ ( # ` W ) ) -> ( M + L ) <_ ( # ` W ) ) ) ) ) )
92 91 adantl 
 |-  ( ( K e. ZZ /\ L e. ZZ ) -> ( 0 <_ L -> ( M e. NN0 -> ( L <_ ( N - M ) -> ( ( N e. NN0 /\ ( # ` W ) e. NN0 /\ N <_ ( # ` W ) ) -> ( M + L ) <_ ( # ` W ) ) ) ) ) )
93 15 92 syld 
 |-  ( ( K e. ZZ /\ L e. ZZ ) -> ( ( 0 <_ K /\ K <_ L ) -> ( M e. NN0 -> ( L <_ ( N - M ) -> ( ( N e. NN0 /\ ( # ` W ) e. NN0 /\ N <_ ( # ` W ) ) -> ( M + L ) <_ ( # ` W ) ) ) ) ) )
94 93 expd 
 |-  ( ( K e. ZZ /\ L e. ZZ ) -> ( 0 <_ K -> ( K <_ L -> ( M e. NN0 -> ( L <_ ( N - M ) -> ( ( N e. NN0 /\ ( # ` W ) e. NN0 /\ N <_ ( # ` W ) ) -> ( M + L ) <_ ( # ` W ) ) ) ) ) ) )
95 94 com35 
 |-  ( ( K e. ZZ /\ L e. ZZ ) -> ( 0 <_ K -> ( L <_ ( N - M ) -> ( M e. NN0 -> ( K <_ L -> ( ( N e. NN0 /\ ( # ` W ) e. NN0 /\ N <_ ( # ` W ) ) -> ( M + L ) <_ ( # ` W ) ) ) ) ) ) )
96 95 com25 
 |-  ( ( K e. ZZ /\ L e. ZZ ) -> ( K <_ L -> ( L <_ ( N - M ) -> ( M e. NN0 -> ( 0 <_ K -> ( ( N e. NN0 /\ ( # ` W ) e. NN0 /\ N <_ ( # ` W ) ) -> ( M + L ) <_ ( # ` W ) ) ) ) ) ) )
97 96 impd 
 |-  ( ( K e. ZZ /\ L e. ZZ ) -> ( ( K <_ L /\ L <_ ( N - M ) ) -> ( M e. NN0 -> ( 0 <_ K -> ( ( N e. NN0 /\ ( # ` W ) e. NN0 /\ N <_ ( # ` W ) ) -> ( M + L ) <_ ( # ` W ) ) ) ) ) )
98 97 com24 
 |-  ( ( K e. ZZ /\ L e. ZZ ) -> ( 0 <_ K -> ( M e. NN0 -> ( ( K <_ L /\ L <_ ( N - M ) ) -> ( ( N e. NN0 /\ ( # ` W ) e. NN0 /\ N <_ ( # ` W ) ) -> ( M + L ) <_ ( # ` W ) ) ) ) ) )
99 98 impancom 
 |-  ( ( K e. ZZ /\ 0 <_ K ) -> ( L e. ZZ -> ( M e. NN0 -> ( ( K <_ L /\ L <_ ( N - M ) ) -> ( ( N e. NN0 /\ ( # ` W ) e. NN0 /\ N <_ ( # ` W ) ) -> ( M + L ) <_ ( # ` W ) ) ) ) ) )
100 8 99 sylbi 
 |-  ( K e. NN0 -> ( L e. ZZ -> ( M e. NN0 -> ( ( K <_ L /\ L <_ ( N - M ) ) -> ( ( N e. NN0 /\ ( # ` W ) e. NN0 /\ N <_ ( # ` W ) ) -> ( M + L ) <_ ( # ` W ) ) ) ) ) )
101 100 imp 
 |-  ( ( K e. NN0 /\ L e. ZZ ) -> ( M e. NN0 -> ( ( K <_ L /\ L <_ ( N - M ) ) -> ( ( N e. NN0 /\ ( # ` W ) e. NN0 /\ N <_ ( # ` W ) ) -> ( M + L ) <_ ( # ` W ) ) ) ) )
102 101 impcom 
 |-  ( ( M e. NN0 /\ ( K e. NN0 /\ L e. ZZ ) ) -> ( ( K <_ L /\ L <_ ( N - M ) ) -> ( ( N e. NN0 /\ ( # ` W ) e. NN0 /\ N <_ ( # ` W ) ) -> ( M + L ) <_ ( # ` W ) ) ) )
103 102 imp 
 |-  ( ( ( M e. NN0 /\ ( K e. NN0 /\ L e. ZZ ) ) /\ ( K <_ L /\ L <_ ( N - M ) ) ) -> ( ( N e. NN0 /\ ( # ` W ) e. NN0 /\ N <_ ( # ` W ) ) -> ( M + L ) <_ ( # ` W ) ) )
104 103 imp 
 |-  ( ( ( ( M e. NN0 /\ ( K e. NN0 /\ L e. ZZ ) ) /\ ( K <_ L /\ L <_ ( N - M ) ) ) /\ ( N e. NN0 /\ ( # ` W ) e. NN0 /\ N <_ ( # ` W ) ) ) -> ( M + L ) <_ ( # ` W ) )
105 63 64 104 3jca 
 |-  ( ( ( ( M e. NN0 /\ ( K e. NN0 /\ L e. ZZ ) ) /\ ( K <_ L /\ L <_ ( N - M ) ) ) /\ ( N e. NN0 /\ ( # ` W ) e. NN0 /\ N <_ ( # ` W ) ) ) -> ( ( M + L ) e. NN0 /\ ( # ` W ) e. NN0 /\ ( M + L ) <_ ( # ` W ) ) )
106 105 exp41 
 |-  ( M e. NN0 -> ( ( K e. NN0 /\ L e. ZZ ) -> ( ( K <_ L /\ L <_ ( N - M ) ) -> ( ( N e. NN0 /\ ( # ` W ) e. NN0 /\ N <_ ( # ` W ) ) -> ( ( M + L ) e. NN0 /\ ( # ` W ) e. NN0 /\ ( M + L ) <_ ( # ` W ) ) ) ) ) )
107 106 com24 
 |-  ( M e. NN0 -> ( ( N e. NN0 /\ ( # ` W ) e. NN0 /\ N <_ ( # ` W ) ) -> ( ( K <_ L /\ L <_ ( N - M ) ) -> ( ( K e. NN0 /\ L e. ZZ ) -> ( ( M + L ) e. NN0 /\ ( # ` W ) e. NN0 /\ ( M + L ) <_ ( # ` W ) ) ) ) ) )
108 107 3ad2ant1 
 |-  ( ( M e. NN0 /\ N e. NN0 /\ M <_ N ) -> ( ( N e. NN0 /\ ( # ` W ) e. NN0 /\ N <_ ( # ` W ) ) -> ( ( K <_ L /\ L <_ ( N - M ) ) -> ( ( K e. NN0 /\ L e. ZZ ) -> ( ( M + L ) e. NN0 /\ ( # ` W ) e. NN0 /\ ( M + L ) <_ ( # ` W ) ) ) ) ) )
109 4 108 sylbi 
 |-  ( M e. ( 0 ... N ) -> ( ( N e. NN0 /\ ( # ` W ) e. NN0 /\ N <_ ( # ` W ) ) -> ( ( K <_ L /\ L <_ ( N - M ) ) -> ( ( K e. NN0 /\ L e. ZZ ) -> ( ( M + L ) e. NN0 /\ ( # ` W ) e. NN0 /\ ( M + L ) <_ ( # ` W ) ) ) ) ) )
110 109 com12 
 |-  ( ( N e. NN0 /\ ( # ` W ) e. NN0 /\ N <_ ( # ` W ) ) -> ( M e. ( 0 ... N ) -> ( ( K <_ L /\ L <_ ( N - M ) ) -> ( ( K e. NN0 /\ L e. ZZ ) -> ( ( M + L ) e. NN0 /\ ( # ` W ) e. NN0 /\ ( M + L ) <_ ( # ` W ) ) ) ) ) )
111 59 110 sylbi 
 |-  ( N e. ( 0 ... ( # ` W ) ) -> ( M e. ( 0 ... N ) -> ( ( K <_ L /\ L <_ ( N - M ) ) -> ( ( K e. NN0 /\ L e. ZZ ) -> ( ( M + L ) e. NN0 /\ ( # ` W ) e. NN0 /\ ( M + L ) <_ ( # ` W ) ) ) ) ) )
112 111 imp 
 |-  ( ( N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) -> ( ( K <_ L /\ L <_ ( N - M ) ) -> ( ( K e. NN0 /\ L e. ZZ ) -> ( ( M + L ) e. NN0 /\ ( # ` W ) e. NN0 /\ ( M + L ) <_ ( # ` W ) ) ) ) )
113 112 3adant1 
 |-  ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) -> ( ( K <_ L /\ L <_ ( N - M ) ) -> ( ( K e. NN0 /\ L e. ZZ ) -> ( ( M + L ) e. NN0 /\ ( # ` W ) e. NN0 /\ ( M + L ) <_ ( # ` W ) ) ) ) )
114 113 com13 
 |-  ( ( K e. NN0 /\ L e. ZZ ) -> ( ( K <_ L /\ L <_ ( N - M ) ) -> ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) -> ( ( M + L ) e. NN0 /\ ( # ` W ) e. NN0 /\ ( M + L ) <_ ( # ` W ) ) ) ) )
115 114 ex 
 |-  ( K e. NN0 -> ( L e. ZZ -> ( ( K <_ L /\ L <_ ( N - M ) ) -> ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) -> ( ( M + L ) e. NN0 /\ ( # ` W ) e. NN0 /\ ( M + L ) <_ ( # ` W ) ) ) ) ) )
116 115 3ad2ant1 
 |-  ( ( K e. NN0 /\ ( N - M ) e. NN0 /\ K <_ ( N - M ) ) -> ( L e. ZZ -> ( ( K <_ L /\ L <_ ( N - M ) ) -> ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) -> ( ( M + L ) e. NN0 /\ ( # ` W ) e. NN0 /\ ( M + L ) <_ ( # ` W ) ) ) ) ) )
117 3 116 sylbi 
 |-  ( K e. ( 0 ... ( N - M ) ) -> ( L e. ZZ -> ( ( K <_ L /\ L <_ ( N - M ) ) -> ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) -> ( ( M + L ) e. NN0 /\ ( # ` W ) e. NN0 /\ ( M + L ) <_ ( # ` W ) ) ) ) ) )
118 117 com3l 
 |-  ( L e. ZZ -> ( ( K <_ L /\ L <_ ( N - M ) ) -> ( K e. ( 0 ... ( N - M ) ) -> ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) -> ( ( M + L ) e. NN0 /\ ( # ` W ) e. NN0 /\ ( M + L ) <_ ( # ` W ) ) ) ) ) )
119 118 3ad2ant3 
 |-  ( ( K e. ZZ /\ ( N - M ) e. ZZ /\ L e. ZZ ) -> ( ( K <_ L /\ L <_ ( N - M ) ) -> ( K e. ( 0 ... ( N - M ) ) -> ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) -> ( ( M + L ) e. NN0 /\ ( # ` W ) e. NN0 /\ ( M + L ) <_ ( # ` W ) ) ) ) ) )
120 119 imp 
 |-  ( ( ( K e. ZZ /\ ( N - M ) e. ZZ /\ L e. ZZ ) /\ ( K <_ L /\ L <_ ( N - M ) ) ) -> ( K e. ( 0 ... ( N - M ) ) -> ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) -> ( ( M + L ) e. NN0 /\ ( # ` W ) e. NN0 /\ ( M + L ) <_ ( # ` W ) ) ) ) )
121 2 120 sylbi 
 |-  ( L e. ( K ... ( N - M ) ) -> ( K e. ( 0 ... ( N - M ) ) -> ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) -> ( ( M + L ) e. NN0 /\ ( # ` W ) e. NN0 /\ ( M + L ) <_ ( # ` W ) ) ) ) )
122 121 impcom 
 |-  ( ( K e. ( 0 ... ( N - M ) ) /\ L e. ( K ... ( N - M ) ) ) -> ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) -> ( ( M + L ) e. NN0 /\ ( # ` W ) e. NN0 /\ ( M + L ) <_ ( # ` W ) ) ) )
123 122 impcom 
 |-  ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) /\ ( K e. ( 0 ... ( N - M ) ) /\ L e. ( K ... ( N - M ) ) ) ) -> ( ( M + L ) e. NN0 /\ ( # ` W ) e. NN0 /\ ( M + L ) <_ ( # ` W ) ) )
124 elfz2nn0 
 |-  ( ( M + L ) e. ( 0 ... ( # ` W ) ) <-> ( ( M + L ) e. NN0 /\ ( # ` W ) e. NN0 /\ ( M + L ) <_ ( # ` W ) ) )
125 123 124 sylibr 
 |-  ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) /\ ( K e. ( 0 ... ( N - M ) ) /\ L e. ( K ... ( N - M ) ) ) ) -> ( M + L ) e. ( 0 ... ( # ` W ) ) )
126 1 58 125 3jca 
 |-  ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) /\ ( K e. ( 0 ... ( N - M ) ) /\ L e. ( K ... ( N - M ) ) ) ) -> ( W e. Word V /\ ( M + K ) e. ( 0 ... ( M + L ) ) /\ ( M + L ) e. ( 0 ... ( # ` W ) ) ) )