Step | Hyp | Ref
| Expression |
1 | | lencl 13324 |
. . 3
Word |
2 | | eqeq2 2633 |
. . . . . 6
|
3 | 2 | imbi1d 331 |
. . . . 5
|
4 | 3 | ralbidv 2986 |
. . . 4
Word
Word |
5 | | eqeq2 2633 |
. . . . . 6
|
6 | 5 | imbi1d 331 |
. . . . 5
|
7 | 6 | ralbidv 2986 |
. . . 4
Word
Word |
8 | | eqeq2 2633 |
. . . . . 6
|
9 | 8 | imbi1d 331 |
. . . . 5
|
10 | 9 | ralbidv 2986 |
. . . 4
Word
Word |
11 | | eqeq2 2633 |
. . . . . 6
|
12 | 11 | imbi1d 331 |
. . . . 5
|
13 | 12 | ralbidv 2986 |
. . . 4
Word Word |
14 | | hasheq0 13154 |
. . . . . 6
Word
|
15 | | wrdind.5 |
. . . . . . 7
|
16 | | wrdind.1 |
. . . . . . 7
|
17 | 15, 16 | mpbiri 248 |
. . . . . 6
|
18 | 14, 17 | syl6bi 243 |
. . . . 5
Word |
19 | 18 | rgen 2922 |
. . . 4
Word |
20 | | fveq2 6191 |
. . . . . . . 8
|
21 | 20 | eqeq1d 2624 |
. . . . . . 7
|
22 | | wrdind.2 |
. . . . . . 7
|
23 | 21, 22 | imbi12d 334 |
. . . . . 6
|
24 | 23 | cbvralv 3171 |
. . . . 5
Word Word |
25 | | swrdcl 13419 |
. . . . . . . . . . . 12
Word substr
Word |
26 | 25 | ad2antrl 764 |
. . . . . . . . . . 11
Word Word
substr Word |
27 | | simplr 792 |
. . . . . . . . . . 11
Word Word
Word |
28 | | simprl 794 |
. . . . . . . . . . . . 13
Word Word
Word |
29 | | fzossfz 12488 |
. . . . . . . . . . . . . 14
..^ |
30 | | simprr 796 |
. . . . . . . . . . . . . . . 16
Word Word
|
31 | | nn0p1nn 11332 |
. . . . . . . . . . . . . . . . 17
|
32 | 31 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
Word Word
|
33 | 30, 32 | eqeltrd 2701 |
. . . . . . . . . . . . . . 15
Word Word
|
34 | | fzo0end 12560 |
. . . . . . . . . . . . . . 15
..^ |
35 | 33, 34 | syl 17 |
. . . . . . . . . . . . . 14
Word Word
..^ |
36 | 29, 35 | sseldi 3601 |
. . . . . . . . . . . . 13
Word Word
|
37 | | swrd0len 13422 |
. . . . . . . . . . . . 13
Word substr |
38 | 28, 36, 37 | syl2anc 693 |
. . . . . . . . . . . 12
Word Word
substr |
39 | 30 | oveq1d 6665 |
. . . . . . . . . . . 12
Word Word
|
40 | | nn0cn 11302 |
. . . . . . . . . . . . . 14
|
41 | 40 | ad2antrr 762 |
. . . . . . . . . . . . 13
Word Word
|
42 | | ax-1cn 9994 |
. . . . . . . . . . . . 13
|
43 | | pncan 10287 |
. . . . . . . . . . . . 13
|
44 | 41, 42, 43 | sylancl 694 |
. . . . . . . . . . . 12
Word Word
|
45 | 38, 39, 44 | 3eqtrd 2660 |
. . . . . . . . . . 11
Word Word
substr |
46 | | fveq2 6191 |
. . . . . . . . . . . . . 14
substr substr |
47 | 46 | eqeq1d 2624 |
. . . . . . . . . . . . 13
substr
substr |
48 | | vex 3203 |
. . . . . . . . . . . . . . 15
|
49 | 48, 22 | sbcie 3470 |
. . . . . . . . . . . . . 14
|
50 | | dfsbcq 3437 |
. . . . . . . . . . . . . 14
substr
substr |
51 | 49, 50 | syl5bbr 274 |
. . . . . . . . . . . . 13
substr substr |
52 | 47, 51 | imbi12d 334 |
. . . . . . . . . . . 12
substr
substr
substr |
53 | 52 | rspcv 3305 |
. . . . . . . . . . 11
substr
Word Word substr substr |
54 | 26, 27, 45, 53 | syl3c 66 |
. . . . . . . . . 10
Word Word
substr |
55 | 33 | nnge1d 11063 |
. . . . . . . . . . . . 13
Word Word
|
56 | | wrdlenge1n0 13340 |
. . . . . . . . . . . . . 14
Word
|
57 | 56 | ad2antrl 764 |
. . . . . . . . . . . . 13
Word Word
|
58 | 55, 57 | mpbird 247 |
. . . . . . . . . . . 12
Word Word
|
59 | | lswcl 13355 |
. . . . . . . . . . . 12
Word lastS |
60 | 28, 58, 59 | syl2anc 693 |
. . . . . . . . . . 11
Word Word
lastS
|
61 | | oveq1 6657 |
. . . . . . . . . . . . . 14
substr ++ substr ++ |
62 | 61 | sbceq1d 3440 |
. . . . . . . . . . . . 13
substr ++ substr ++ |
63 | 50, 62 | imbi12d 334 |
. . . . . . . . . . . 12
substr
++ substr
substr ++
|
64 | | s1eq 13380 |
. . . . . . . . . . . . . . 15
lastS
lastS |
65 | 64 | oveq2d 6666 |
. . . . . . . . . . . . . 14
lastS
substr ++
substr ++ lastS |
66 | 65 | sbceq1d 3440 |
. . . . . . . . . . . . 13
lastS
substr ++ substr ++ lastS |
67 | 66 | imbi2d 330 |
. . . . . . . . . . . 12
lastS
substr
substr ++
substr
substr ++
lastS |
68 | | wrdind.6 |
. . . . . . . . . . . . 13
Word
|
69 | | ovex 6678 |
. . . . . . . . . . . . . 14
++
|
70 | | wrdind.3 |
. . . . . . . . . . . . . 14
++
|
71 | 69, 70 | sbcie 3470 |
. . . . . . . . . . . . 13
++
|
72 | 68, 49, 71 | 3imtr4g 285 |
. . . . . . . . . . . 12
Word
++ |
73 | 63, 67, 72 | vtocl2ga 3274 |
. . . . . . . . . . 11
substr Word
lastS substr
substr ++
lastS |
74 | 26, 60, 73 | syl2anc 693 |
. . . . . . . . . 10
Word Word
substr
substr ++
lastS |
75 | 54, 74 | mpd 15 |
. . . . . . . . 9
Word Word
substr ++ lastS |
76 | | wrdfin 13323 |
. . . . . . . . . . . . . 14
Word |
77 | 76 | ad2antrl 764 |
. . . . . . . . . . . . 13
Word Word
|
78 | | hashnncl 13157 |
. . . . . . . . . . . . 13
|
79 | 77, 78 | syl 17 |
. . . . . . . . . . . 12
Word Word
|
80 | 33, 79 | mpbid 222 |
. . . . . . . . . . 11
Word Word
|
81 | | swrdccatwrd 13468 |
. . . . . . . . . . . 12
Word substr
++
lastS
|
82 | 81 | eqcomd 2628 |
. . . . . . . . . . 11
Word substr ++ lastS |
83 | 28, 80, 82 | syl2anc 693 |
. . . . . . . . . 10
Word Word
substr ++ lastS |
84 | | sbceq1a 3446 |
. . . . . . . . . 10
substr ++ lastS
substr ++
lastS |
85 | 83, 84 | syl 17 |
. . . . . . . . 9
Word Word
substr ++
lastS |
86 | 75, 85 | mpbird 247 |
. . . . . . . 8
Word Word
|
87 | 86 | expr 643 |
. . . . . . 7
Word Word |
88 | 87 | ralrimiva 2966 |
. . . . . 6
Word Word |
89 | 88 | ex 450 |
. . . . 5
Word Word |
90 | 24, 89 | syl5bi 232 |
. . . 4
Word Word |
91 | 4, 7, 10, 13, 19, 90 | nn0ind 11472 |
. . 3
Word |
92 | 1, 91 | syl 17 |
. 2
Word Word |
93 | | eqidd 2623 |
. 2
Word |
94 | | fveq2 6191 |
. . . . 5
|
95 | 94 | eqeq1d 2624 |
. . . 4
|
96 | | wrdind.4 |
. . . 4
|
97 | 95, 96 | imbi12d 334 |
. . 3
|
98 | 97 | rspcv 3305 |
. 2
Word
Word |
99 | 92, 93, 98 | mp2d 49 |
1
Word |