Step | Hyp | Ref
| Expression |
1 | | ccatcl 13359 |
. . . . 5
Word
Word ++ Word |
2 | 1 | adantr 481 |
. . . 4
Word
Word
++ Word |
3 | | elfz0fzfz0 12444 |
. . . . 5
|
4 | 3 | adantl 482 |
. . . 4
Word
Word
|
5 | | elfzuz2 12346 |
. . . . . . . . 9
|
6 | 5 | adantl 482 |
. . . . . . . 8
Word
Word
|
7 | | fzss1 12380 |
. . . . . . . 8
|
8 | 6, 7 | syl 17 |
. . . . . . 7
Word
Word
|
9 | | ccatlen 13360 |
. . . . . . . . . 10
Word
Word ++ |
10 | | pfxccatin12.l |
. . . . . . . . . . . 12
|
11 | 10 | eqcomi 2631 |
. . . . . . . . . . 11
|
12 | 11 | oveq1i 6660 |
. . . . . . . . . 10
|
13 | 9, 12 | syl6eq 2672 |
. . . . . . . . 9
Word
Word ++ |
14 | 13 | adantr 481 |
. . . . . . . 8
Word
Word
++ |
15 | 14 | oveq2d 6666 |
. . . . . . 7
Word
Word
++ |
16 | 8, 15 | sseqtr4d 3642 |
. . . . . 6
Word
Word
++ |
17 | 16 | sseld 3602 |
. . . . 5
Word
Word
++ |
18 | 17 | impr 649 |
. . . 4
Word
Word
++ |
19 | | swrdvalfn 13426 |
. . . 4
++ Word
++ ++ substr ..^ |
20 | 2, 4, 18, 19 | syl3anc 1326 |
. . 3
Word
Word
++ substr ..^ |
21 | | swrdcl 13419 |
. . . . . . 7
Word substr Word |
22 | | pfxcl 41386 |
. . . . . . 7
Word prefix Word |
23 | 21, 22 | anim12i 590 |
. . . . . 6
Word
Word substr Word prefix Word |
24 | 23 | adantr 481 |
. . . . 5
Word
Word
substr Word
prefix Word |
25 | | ccatvalfn 13365 |
. . . . 5
substr Word prefix Word substr ++ prefix ..^ substr
prefix |
26 | 24, 25 | syl 17 |
. . . 4
Word
Word
substr ++ prefix
..^ substr prefix |
27 | | simpll 790 |
. . . . . . . . 9
Word
Word
Word |
28 | | simprl 794 |
. . . . . . . . 9
Word
Word
|
29 | | lencl 13324 |
. . . . . . . . . . 11
Word |
30 | | elnn0uz 11725 |
. . . . . . . . . . . . 13
|
31 | | eluzfz2 12349 |
. . . . . . . . . . . . 13
|
32 | 30, 31 | sylbi 207 |
. . . . . . . . . . . 12
|
33 | 10, 32 | syl5eqel 2705 |
. . . . . . . . . . 11
|
34 | 29, 33 | syl 17 |
. . . . . . . . . 10
Word |
35 | 34 | ad2antrr 762 |
. . . . . . . . 9
Word
Word
|
36 | | swrdlen 13423 |
. . . . . . . . 9
Word
substr |
37 | 27, 28, 35, 36 | syl3anc 1326 |
. . . . . . . 8
Word
Word
substr |
38 | | simplr 792 |
. . . . . . . . 9
Word
Word
Word |
39 | | lencl 13324 |
. . . . . . . . . . . . 13
Word |
40 | 39 | nn0zd 11480 |
. . . . . . . . . . . 12
Word |
41 | 40 | adantl 482 |
. . . . . . . . . . 11
Word
Word |
42 | | simpr 477 |
. . . . . . . . . . 11
|
43 | 41, 42 | anim12i 590 |
. . . . . . . . . 10
Word
Word
|
44 | | elfzmlbp 12450 |
. . . . . . . . . 10
|
45 | 43, 44 | syl 17 |
. . . . . . . . 9
Word
Word
|
46 | | pfxlen 41391 |
. . . . . . . . 9
Word
prefix |
47 | 38, 45, 46 | syl2anc 693 |
. . . . . . . 8
Word
Word
prefix |
48 | 37, 47 | oveq12d 6668 |
. . . . . . 7
Word
Word
substr prefix |
49 | | elfz2nn0 12431 |
. . . . . . . . . . 11
|
50 | | nn0cn 11302 |
. . . . . . . . . . . . . . . . 17
|
51 | 50 | adantl 482 |
. . . . . . . . . . . . . . . 16
|
52 | 51 | adantl 482 |
. . . . . . . . . . . . . . 15
|
53 | | nn0cn 11302 |
. . . . . . . . . . . . . . . 16
|
54 | 53 | ad2antrl 764 |
. . . . . . . . . . . . . . 15
|
55 | | zcn 11382 |
. . . . . . . . . . . . . . . 16
|
56 | 55 | adantr 481 |
. . . . . . . . . . . . . . 15
|
57 | 52, 54, 56 | 3jca 1242 |
. . . . . . . . . . . . . 14
|
58 | 57 | ex 450 |
. . . . . . . . . . . . 13
|
59 | | elfzelz 12342 |
. . . . . . . . . . . . 13
|
60 | 58, 59 | syl11 33 |
. . . . . . . . . . . 12
|
61 | 60 | 3adant3 1081 |
. . . . . . . . . . 11
|
62 | 49, 61 | sylbi 207 |
. . . . . . . . . 10
|
63 | 62 | imp 445 |
. . . . . . . . 9
|
64 | 63 | adantl 482 |
. . . . . . . 8
Word
Word
|
65 | | npncan3 10319 |
. . . . . . . 8
|
66 | 64, 65 | syl 17 |
. . . . . . 7
Word
Word
|
67 | 48, 66 | eqtr2d 2657 |
. . . . . 6
Word
Word
substr prefix |
68 | 67 | oveq2d 6666 |
. . . . 5
Word
Word
..^ ..^ substr prefix |
69 | 68 | fneq2d 5982 |
. . . 4
Word
Word
substr
++ prefix ..^ substr ++ prefix ..^ substr
prefix |
70 | 26, 69 | mpbird 247 |
. . 3
Word
Word
substr ++ prefix
..^ |
71 | | simprl 794 |
. . . . . 6
..^ Word Word
..^ Word
Word
|
72 | | simpr 477 |
. . . . . . . 8
Word Word
..^
..^ |
73 | 72 | anim2i 593 |
. . . . . . 7
..^ Word Word
..^ ..^ ..^ |
74 | 73 | ancomd 467 |
. . . . . 6
..^ Word Word
..^ ..^ ..^ |
75 | 10 | swrdccatin12lem3 13490 |
. . . . . 6
Word
Word
..^ ..^
++ substr substr |
76 | 71, 74, 75 | sylc 65 |
. . . . 5
..^ Word Word
..^ ++ substr substr |
77 | 24 | ad2antrl 764 |
. . . . . . 7
..^ Word Word
..^ substr
Word prefix Word |
78 | | simpl 473 |
. . . . . . . 8
..^ Word Word
..^ ..^ |
79 | | nn0fz0 12437 |
. . . . . . . . . . . . . . 15
|
80 | 29, 79 | sylib 208 |
. . . . . . . . . . . . . 14
Word |
81 | 10, 80 | syl5eqel 2705 |
. . . . . . . . . . . . 13
Word |
82 | 81 | ad2antrr 762 |
. . . . . . . . . . . 12
Word
Word
|
83 | 27, 28, 82 | 3jca 1242 |
. . . . . . . . . . 11
Word
Word
Word
|
84 | 83 | ad2antrl 764 |
. . . . . . . . . 10
..^ Word Word
..^
Word
|
85 | 84, 36 | syl 17 |
. . . . . . . . 9
..^ Word Word
..^ substr |
86 | 85 | oveq2d 6666 |
. . . . . . . 8
..^ Word Word
..^ ..^ substr ..^ |
87 | 78, 86 | eleqtrrd 2704 |
. . . . . . 7
..^ Word Word
..^ ..^ substr |
88 | | df-3an 1039 |
. . . . . . 7
substr Word prefix Word ..^ substr substr Word
prefix Word ..^ substr |
89 | 77, 87, 88 | sylanbrc 698 |
. . . . . 6
..^ Word Word
..^ substr
Word prefix Word ..^ substr |
90 | | ccatval1 13361 |
. . . . . 6
substr Word prefix Word ..^ substr
substr
++ prefix substr |
91 | 89, 90 | syl 17 |
. . . . 5
..^ Word Word
..^ substr ++ prefix substr |
92 | 76, 91 | eqtr4d 2659 |
. . . 4
..^ Word Word
..^ ++ substr substr ++ prefix
|
93 | | simprl 794 |
. . . . . 6
..^ Word Word
..^
Word Word
|
94 | 72 | anim2i 593 |
. . . . . . 7
..^ Word Word
..^
..^ ..^ |
95 | 94 | ancomd 467 |
. . . . . 6
..^ Word Word
..^
..^ ..^ |
96 | 10 | pfxccatin12lem2 41424 |
. . . . . 6
Word
Word
..^
..^ ++ substr prefix substr |
97 | 93, 95, 96 | sylc 65 |
. . . . 5
..^ Word Word
..^
++ substr prefix
substr |
98 | 24 | ad2antrl 764 |
. . . . . . 7
..^ Word Word
..^
substr Word
prefix Word |
99 | | elfzuz 12338 |
. . . . . . . . . . . . 13
|
100 | | eluzelz 11697 |
. . . . . . . . . . . . . 14
|
101 | | simpll 790 |
. . . . . . . . . . . . . . . . . . 19
|
102 | | simplr 792 |
. . . . . . . . . . . . . . . . . . 19
|
103 | | simpr 477 |
. . . . . . . . . . . . . . . . . . 19
|
104 | 101, 102,
103 | 3jca 1242 |
. . . . . . . . . . . . . . . . . 18
|
105 | 104 | ex 450 |
. . . . . . . . . . . . . . . . 17
|
106 | 105 | ancoms 469 |
. . . . . . . . . . . . . . . 16
|
107 | 106 | 3adant3 1081 |
. . . . . . . . . . . . . . 15
|
108 | 49, 107 | sylbi 207 |
. . . . . . . . . . . . . 14
|
109 | 100, 108 | syl5com 31 |
. . . . . . . . . . . . 13
|
110 | 99, 109 | syl 17 |
. . . . . . . . . . . 12
|
111 | 110 | impcom 446 |
. . . . . . . . . . 11
|
112 | 111 | adantl 482 |
. . . . . . . . . 10
Word
Word
|
113 | 112 | ad2antrl 764 |
. . . . . . . . 9
..^ Word Word
..^
|
114 | | swrdccatin12lem1 13484 |
. . . . . . . . 9
..^
..^ ..^ |
115 | 113, 95, 114 | sylc 65 |
. . . . . . . 8
..^ Word Word
..^
..^ |
116 | 27, 28, 82, 36 | syl3anc 1326 |
. . . . . . . . . 10
Word
Word
substr |
117 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
Word
Word Word |
118 | 117 | adantl 482 |
. . . . . . . . . . . . . . . 16
Word Word
Word |
119 | 41 | adantl 482 |
. . . . . . . . . . . . . . . . 17
Word Word |
120 | | simpl 473 |
. . . . . . . . . . . . . . . . 17
Word Word
|
121 | 119, 120,
44 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
Word Word |
122 | 118, 121 | jca 554 |
. . . . . . . . . . . . . . 15
Word Word Word |
123 | 122 | ex 450 |
. . . . . . . . . . . . . 14
Word Word
Word
|
124 | 123 | adantl 482 |
. . . . . . . . . . . . 13
Word Word
Word |
125 | 124 | impcom 446 |
. . . . . . . . . . . 12
Word
Word
Word |
126 | 125, 46 | syl 17 |
. . . . . . . . . . 11
Word
Word
prefix |
127 | 116, 126 | oveq12d 6668 |
. . . . . . . . . 10
Word
Word
substr prefix |
128 | 116, 127 | oveq12d 6668 |
. . . . . . . . 9
Word
Word
substr ..^ substr prefix ..^ |
129 | 128 | ad2antrl 764 |
. . . . . . . 8
..^ Word Word
..^
substr ..^ substr prefix ..^ |
130 | 115, 129 | eleqtrrd 2704 |
. . . . . . 7
..^ Word Word
..^
substr ..^ substr
prefix |
131 | | df-3an 1039 |
. . . . . . 7
substr Word prefix Word substr ..^ substr
prefix substr Word prefix Word
substr ..^ substr
prefix |
132 | 98, 130, 131 | sylanbrc 698 |
. . . . . 6
..^ Word Word
..^
substr Word
prefix Word substr ..^ substr
prefix |
133 | | ccatval2 13362 |
. . . . . 6
substr Word prefix Word substr ..^ substr
prefix substr ++ prefix
prefix substr |
134 | 132, 133 | syl 17 |
. . . . 5
..^ Word Word
..^
substr
++ prefix prefix substr |
135 | 97, 134 | eqtr4d 2659 |
. . . 4
..^ Word Word
..^
++ substr substr ++ prefix |
136 | 92, 135 | pm2.61ian 831 |
. . 3
Word Word
..^
++ substr substr ++ prefix |
137 | 20, 70, 136 | eqfnfvd 6314 |
. 2
Word
Word
++ substr substr ++ prefix |
138 | 137 | ex 450 |
1
Word
Word
++ substr substr ++ prefix |