Step | Hyp | Ref
| Expression |
1 | | pfxcl 41386 |
. . . . . 6
Word prefix Word |
2 | 1 | 3ad2ant1 1082 |
. . . . 5
Word
prefix
Word |
3 | | swrdcl 13419 |
. . . . . 6
Word substr Word |
4 | 3 | 3ad2ant1 1082 |
. . . . 5
Word
substr
Word |
5 | | ccatcl 13359 |
. . . . 5
prefix Word substr Word prefix ++
substr
Word |
6 | 2, 4, 5 | syl2anc 693 |
. . . 4
Word
prefix ++ substr Word |
7 | | wrdf 13310 |
. . . 4
prefix ++ substr Word prefix ++
substr
..^ prefix
++
substr |
8 | | ffn 6045 |
. . . 4
prefix ++ substr ..^ prefix ++ substr prefix
++
substr ..^ prefix ++ substr |
9 | 6, 7, 8 | 3syl 18 |
. . 3
Word
prefix ++ substr ..^ prefix ++ substr |
10 | | ccatlen 13360 |
. . . . . . 7
prefix Word substr Word prefix
++
substr prefix substr |
11 | 2, 4, 10 | syl2anc 693 |
. . . . . 6
Word
prefix ++ substr prefix substr |
12 | | simp1 1061 |
. . . . . . . . 9
Word
Word |
13 | | fzass4 12379 |
. . . . . . . . . . . 12
|
14 | 13 | biimpri 218 |
. . . . . . . . . . 11
|
15 | 14 | simpld 475 |
. . . . . . . . . 10
|
16 | 15 | 3adant1 1079 |
. . . . . . . . 9
Word
|
17 | | pfxlen 41391 |
. . . . . . . . 9
Word
prefix |
18 | 12, 16, 17 | syl2anc 693 |
. . . . . . . 8
Word
prefix |
19 | | swrdlen 13423 |
. . . . . . . 8
Word
substr |
20 | 18, 19 | oveq12d 6668 |
. . . . . . 7
Word
prefix substr |
21 | | elfzelz 12342 |
. . . . . . . . . . 11
|
22 | 21 | ad2antrl 764 |
. . . . . . . . . 10
Word
|
23 | 22 | zcnd 11483 |
. . . . . . . . 9
Word
|
24 | 23 | 3impb 1260 |
. . . . . . . 8
Word
|
25 | | elfzelz 12342 |
. . . . . . . . . . 11
|
26 | 25 | ad2antll 765 |
. . . . . . . . . 10
Word
|
27 | 26 | zcnd 11483 |
. . . . . . . . 9
Word
|
28 | 27 | 3impb 1260 |
. . . . . . . 8
Word
|
29 | 24, 28 | pncan3d 10395 |
. . . . . . 7
Word
|
30 | 20, 29 | eqtrd 2656 |
. . . . . 6
Word
prefix substr |
31 | 11, 30 | eqtrd 2656 |
. . . . 5
Word
prefix ++ substr |
32 | 31 | oveq2d 6666 |
. . . 4
Word
..^ prefix ++ substr ..^ |
33 | 32 | fneq2d 5982 |
. . 3
Word
prefix ++
substr
..^ prefix
++
substr prefix ++
substr
..^ |
34 | 9, 33 | mpbid 222 |
. 2
Word
prefix ++ substr ..^ |
35 | | pfxfn 41390 |
. . 3
Word
prefix
..^ |
36 | 35 | 3adant2 1080 |
. 2
Word
prefix
..^ |
37 | | simpr 477 |
. . . . 5
Word
..^
..^ |
38 | 21 | 3ad2ant2 1083 |
. . . . . 6
Word
|
39 | 38 | adantr 481 |
. . . . 5
Word
..^
|
40 | | fzospliti 12500 |
. . . . 5
..^ ..^ ..^ |
41 | 37, 39, 40 | syl2anc 693 |
. . . 4
Word
..^ ..^ ..^ |
42 | 2 | adantr 481 |
. . . . . . 7
Word
..^ prefix
Word |
43 | 4 | adantr 481 |
. . . . . . 7
Word
..^ substr
Word |
44 | 18 | oveq2d 6666 |
. . . . . . . . 9
Word
..^ prefix ..^ |
45 | 44 | eleq2d 2687 |
. . . . . . . 8
Word
..^ prefix ..^ |
46 | 45 | biimpar 502 |
. . . . . . 7
Word
..^
..^ prefix |
47 | | ccatval1 13361 |
. . . . . . 7
prefix Word substr Word
..^ prefix
prefix
++
substr prefix |
48 | 42, 43, 46, 47 | syl3anc 1326 |
. . . . . 6
Word
..^ prefix ++
substr
prefix |
49 | 12 | adantr 481 |
. . . . . . 7
Word
..^
Word |
50 | 16 | adantr 481 |
. . . . . . 7
Word
..^
|
51 | | simpr 477 |
. . . . . . 7
Word
..^
..^ |
52 | | pfxfv 41399 |
. . . . . . 7
Word
..^
prefix |
53 | 49, 50, 51, 52 | syl3anc 1326 |
. . . . . 6
Word
..^ prefix |
54 | 48, 53 | eqtrd 2656 |
. . . . 5
Word
..^ prefix ++
substr
|
55 | 2 | adantr 481 |
. . . . . . 7
Word
..^ prefix
Word |
56 | 4 | adantr 481 |
. . . . . . 7
Word
..^ substr
Word |
57 | 18, 30 | oveq12d 6668 |
. . . . . . . . 9
Word
prefix ..^ prefix substr ..^ |
58 | 57 | eleq2d 2687 |
. . . . . . . 8
Word
prefix ..^ prefix substr ..^ |
59 | 58 | biimpar 502 |
. . . . . . 7
Word
..^
prefix ..^ prefix substr
|
60 | | ccatval2 13362 |
. . . . . . 7
prefix Word substr Word
prefix ..^ prefix substr
prefix ++ substr substr prefix |
61 | 55, 56, 59, 60 | syl3anc 1326 |
. . . . . 6
Word
..^ prefix ++
substr
substr prefix |
62 | 18 | oveq2d 6666 |
. . . . . . . . 9
Word
prefix |
63 | 62 | adantr 481 |
. . . . . . . 8
Word
..^ prefix |
64 | 38 | anim1i 592 |
. . . . . . . . . . 11
Word
..^ ..^ |
65 | 64 | ancomd 467 |
. . . . . . . . . 10
Word
..^ ..^
|
66 | | fzosubel 12526 |
. . . . . . . . . 10
..^ ..^ |
67 | 65, 66 | syl 17 |
. . . . . . . . 9
Word
..^ ..^ |
68 | 21 | zcnd 11483 |
. . . . . . . . . . . . . . 15
|
69 | 68 | subidd 10380 |
. . . . . . . . . . . . . 14
|
70 | 69 | eqcomd 2628 |
. . . . . . . . . . . . 13
|
71 | 70 | 3ad2ant2 1083 |
. . . . . . . . . . . 12
Word
|
72 | 71 | oveq1d 6665 |
. . . . . . . . . . 11
Word
..^ ..^ |
73 | 72 | eleq2d 2687 |
. . . . . . . . . 10
Word
..^
..^ |
74 | 73 | adantr 481 |
. . . . . . . . 9
Word
..^ ..^
..^ |
75 | 67, 74 | mpbird 247 |
. . . . . . . 8
Word
..^ ..^ |
76 | 63, 75 | eqeltrd 2701 |
. . . . . . 7
Word
..^ prefix ..^ |
77 | | swrdfv 13424 |
. . . . . . 7
Word
prefix ..^
substr prefix prefix |
78 | 76, 77 | syldan 487 |
. . . . . 6
Word
..^ substr prefix prefix |
79 | 63 | oveq1d 6665 |
. . . . . . . 8
Word
..^ prefix |
80 | | elfzoelz 12470 |
. . . . . . . . . . 11
..^
|
81 | 80 | zcnd 11483 |
. . . . . . . . . 10
..^
|
82 | 81 | adantl 482 |
. . . . . . . . 9
Word
..^
|
83 | 24 | adantr 481 |
. . . . . . . . 9
Word
..^
|
84 | 82, 83 | npcand 10396 |
. . . . . . . 8
Word
..^ |
85 | 79, 84 | eqtrd 2656 |
. . . . . . 7
Word
..^ prefix |
86 | 85 | fveq2d 6195 |
. . . . . 6
Word
..^ prefix |
87 | 61, 78, 86 | 3eqtrd 2660 |
. . . . 5
Word
..^ prefix ++
substr
|
88 | 54, 87 | jaodan 826 |
. . . 4
Word
..^ ..^ prefix ++ substr |
89 | 41, 88 | syldan 487 |
. . 3
Word
..^ prefix ++
substr
|
90 | 12 | adantr 481 |
. . . 4
Word
..^
Word |
91 | | simpl3 1066 |
. . . 4
Word
..^
|
92 | | pfxfv 41399 |
. . . 4
Word
..^
prefix |
93 | 90, 91, 37, 92 | syl3anc 1326 |
. . 3
Word
..^ prefix |
94 | 89, 93 | eqtr4d 2659 |
. 2
Word
..^ prefix ++
substr
prefix |
95 | 34, 36, 94 | eqfnfvd 6314 |
1
Word
prefix ++ substr prefix |