Step | Hyp | Ref
| Expression |
1 | | efgredlemd.c |
. . . . . 6
|
2 | | efgval.w |
. . . . . . . . 9
Word |
3 | | efgval.r |
. . . . . . . . 9
~FG |
4 | | efgval2.m |
. . . . . . . . 9
|
5 | | efgval2.t |
. . . . . . . . 9
splice |
6 | | efgred.d |
. . . . . . . . 9
|
7 | | efgred.s |
. . . . . . . . 9
Word ..^ |
8 | 2, 3, 4, 5, 6, 7 | efgsf 18142 |
. . . . . . . 8
Word
..^ |
9 | 8 | fdmi 6052 |
. . . . . . . . 9
Word
..^ |
10 | 9 | feq2i 6037 |
. . . . . . . 8
Word
..^ |
11 | 8, 10 | mpbir 221 |
. . . . . . 7
|
12 | 11 | ffvelrni 6358 |
. . . . . 6
|
13 | 1, 12 | syl 17 |
. . . . 5
|
14 | | efgredlemb.q |
. . . . . . 7
|
15 | | elfzuz 12338 |
. . . . . . 7
|
16 | 14, 15 | syl 17 |
. . . . . 6
|
17 | | efgredlemd.sc |
. . . . . . . . . 10
substr ++ substr |
18 | 17 | fveq2d 6195 |
. . . . . . . . 9
substr
++
substr |
19 | | fviss 6256 |
. . . . . . . . . . . . 13
Word Word |
20 | 2, 19 | eqsstri 3635 |
. . . . . . . . . . . 12
Word |
21 | | efgredlem.1 |
. . . . . . . . . . . . . 14
|
22 | | efgredlem.2 |
. . . . . . . . . . . . . 14
|
23 | | efgredlem.3 |
. . . . . . . . . . . . . 14
|
24 | | efgredlem.4 |
. . . . . . . . . . . . . 14
|
25 | | efgredlem.5 |
. . . . . . . . . . . . . 14
|
26 | | efgredlemb.k |
. . . . . . . . . . . . . 14
|
27 | | efgredlemb.l |
. . . . . . . . . . . . . 14
|
28 | 2, 3, 4, 5, 6, 7, 21, 22, 23, 24, 25, 26, 27 | efgredlemf 18154 |
. . . . . . . . . . . . 13
|
29 | 28 | simprd 479 |
. . . . . . . . . . . 12
|
30 | 20, 29 | sseldi 3601 |
. . . . . . . . . . 11
Word
|
31 | | swrdcl 13419 |
. . . . . . . . . . 11
Word
substr Word |
32 | 30, 31 | syl 17 |
. . . . . . . . . 10
substr Word |
33 | 28 | simpld 475 |
. . . . . . . . . . . 12
|
34 | 20, 33 | sseldi 3601 |
. . . . . . . . . . 11
Word
|
35 | | swrdcl 13419 |
. . . . . . . . . . 11
Word
substr Word |
36 | 34, 35 | syl 17 |
. . . . . . . . . 10
substr Word |
37 | | ccatlen 13360 |
. . . . . . . . . 10
substr Word substr Word
substr ++ substr substr substr |
38 | 32, 36, 37 | syl2anc 693 |
. . . . . . . . 9
substr ++ substr substr substr |
39 | | swrd0len 13422 |
. . . . . . . . . . . 12
Word
substr |
40 | 30, 14, 39 | syl2anc 693 |
. . . . . . . . . . 11
substr |
41 | | 2nn0 11309 |
. . . . . . . . . . . . . 14
|
42 | | uzaddcl 11744 |
. . . . . . . . . . . . . 14
|
43 | 16, 41, 42 | sylancl 694 |
. . . . . . . . . . . . 13
|
44 | | efgredlemb.p |
. . . . . . . . . . . . . . 15
|
45 | | elfzuz3 12339 |
. . . . . . . . . . . . . . 15
|
46 | 44, 45 | syl 17 |
. . . . . . . . . . . . . 14
|
47 | | efgredlemd.9 |
. . . . . . . . . . . . . 14
|
48 | | uztrn 11704 |
. . . . . . . . . . . . . 14
|
49 | 46, 47, 48 | syl2anc 693 |
. . . . . . . . . . . . 13
|
50 | | elfzuzb 12336 |
. . . . . . . . . . . . 13
|
51 | 43, 49, 50 | sylanbrc 698 |
. . . . . . . . . . . 12
|
52 | | lencl 13324 |
. . . . . . . . . . . . . . 15
Word
|
53 | 34, 52 | syl 17 |
. . . . . . . . . . . . . 14
|
54 | | nn0uz 11722 |
. . . . . . . . . . . . . 14
|
55 | 53, 54 | syl6eleq 2711 |
. . . . . . . . . . . . 13
|
56 | | eluzfz2 12349 |
. . . . . . . . . . . . 13
|
57 | 55, 56 | syl 17 |
. . . . . . . . . . . 12
|
58 | | swrdlen 13423 |
. . . . . . . . . . . 12
Word
substr |
59 | 34, 51, 57, 58 | syl3anc 1326 |
. . . . . . . . . . 11
substr |
60 | 40, 59 | oveq12d 6668 |
. . . . . . . . . 10
substr substr
|
61 | | elfzelz 12342 |
. . . . . . . . . . . . 13
|
62 | 14, 61 | syl 17 |
. . . . . . . . . . . 12
|
63 | 62 | zcnd 11483 |
. . . . . . . . . . 11
|
64 | 53 | nn0cnd 11353 |
. . . . . . . . . . 11
|
65 | | 2z 11409 |
. . . . . . . . . . . . 13
|
66 | | zaddcl 11417 |
. . . . . . . . . . . . 13
|
67 | 62, 65, 66 | sylancl 694 |
. . . . . . . . . . . 12
|
68 | 67 | zcnd 11483 |
. . . . . . . . . . 11
|
69 | 63, 64, 68 | addsubassd 10412 |
. . . . . . . . . 10
|
70 | | 2cn 11091 |
. . . . . . . . . . . 12
|
71 | 70 | a1i 11 |
. . . . . . . . . . 11
|
72 | 63, 64, 71 | pnpcand 10429 |
. . . . . . . . . 10
|
73 | 60, 69, 72 | 3eqtr2d 2662 |
. . . . . . . . 9
substr substr |
74 | 18, 38, 73 | 3eqtrd 2660 |
. . . . . . . 8
|
75 | | elfzelz 12342 |
. . . . . . . . . . 11
|
76 | 44, 75 | syl 17 |
. . . . . . . . . 10
|
77 | | zsubcl 11419 |
. . . . . . . . . 10
|
78 | 76, 65, 77 | sylancl 694 |
. . . . . . . . 9
|
79 | 65 | a1i 11 |
. . . . . . . . 9
|
80 | 76 | zcnd 11483 |
. . . . . . . . . . . 12
|
81 | | npcan 10290 |
. . . . . . . . . . . 12
|
82 | 80, 70, 81 | sylancl 694 |
. . . . . . . . . . 11
|
83 | 82 | fveq2d 6195 |
. . . . . . . . . 10
|
84 | 46, 83 | eleqtrrd 2704 |
. . . . . . . . 9
|
85 | | eluzsub 11717 |
. . . . . . . . 9
|
86 | 78, 79, 84, 85 | syl3anc 1326 |
. . . . . . . 8
|
87 | 74, 86 | eqeltrd 2701 |
. . . . . . 7
|
88 | | eluzsub 11717 |
. . . . . . . 8
|
89 | 62, 79, 47, 88 | syl3anc 1326 |
. . . . . . 7
|
90 | | uztrn 11704 |
. . . . . . 7
|
91 | 87, 89, 90 | syl2anc 693 |
. . . . . 6
|
92 | | elfzuzb 12336 |
. . . . . 6
|
93 | 16, 91, 92 | sylanbrc 698 |
. . . . 5
|
94 | | efgredlemb.v |
. . . . 5
|
95 | 2, 3, 4, 5 | efgtval 18136 |
. . . . 5
splice
|
96 | 13, 93, 94, 95 | syl3anc 1326 |
. . . 4
splice |
97 | | swrdcl 13419 |
. . . . . 6
Word
substr Word |
98 | 34, 97 | syl 17 |
. . . . 5
substr Word |
99 | | wrd0 13330 |
. . . . . 6
Word |
100 | 99 | a1i 11 |
. . . . 5
Word |
101 | 4 | efgmf 18126 |
. . . . . . . 8
|
102 | 101 | ffvelrni 6358 |
. . . . . . 7
|
103 | 94, 102 | syl 17 |
. . . . . 6
|
104 | 94, 103 | s2cld 13616 |
. . . . 5
Word |
105 | | eluzfz1 12348 |
. . . . . . . . . . . . . 14
|
106 | 16, 105 | syl 17 |
. . . . . . . . . . . . 13
|
107 | 62 | zred 11482 |
. . . . . . . . . . . . . . . . 17
|
108 | | nn0addge1 11339 |
. . . . . . . . . . . . . . . . 17
|
109 | 107, 41, 108 | sylancl 694 |
. . . . . . . . . . . . . . . 16
|
110 | | eluz2 11693 |
. . . . . . . . . . . . . . . 16
|
111 | 62, 67, 109, 110 | syl3anbrc 1246 |
. . . . . . . . . . . . . . 15
|
112 | | uztrn 11704 |
. . . . . . . . . . . . . . 15
|
113 | 47, 111, 112 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
114 | | elfzuzb 12336 |
. . . . . . . . . . . . . 14
|
115 | 16, 113, 114 | sylanbrc 698 |
. . . . . . . . . . . . 13
|
116 | | ccatswrd 13456 |
. . . . . . . . . . . . 13
Word
substr ++
substr
substr |
117 | 34, 106, 115, 44, 116 | syl13anc 1328 |
. . . . . . . . . . . 12
substr
++
substr
substr |
118 | 117 | oveq1d 6665 |
. . . . . . . . . . 11
substr ++
substr ++ ++ substr substr ++ ++ substr |
119 | | swrdcl 13419 |
. . . . . . . . . . . . 13
Word
substr Word |
120 | 34, 119 | syl 17 |
. . . . . . . . . . . 12
substr Word |
121 | | efgredlemb.u |
. . . . . . . . . . . . 13
|
122 | 101 | ffvelrni 6358 |
. . . . . . . . . . . . . 14
|
123 | 121, 122 | syl 17 |
. . . . . . . . . . . . 13
|
124 | 121, 123 | s2cld 13616 |
. . . . . . . . . . . 12
Word |
125 | | swrdcl 13419 |
. . . . . . . . . . . . 13
Word
substr Word |
126 | 34, 125 | syl 17 |
. . . . . . . . . . . 12
substr
Word |
127 | | ccatass 13371 |
. . . . . . . . . . . 12
substr Word Word substr Word
substr ++ ++
substr
substr ++ ++ substr |
128 | 120, 124,
126, 127 | syl3anc 1326 |
. . . . . . . . . . 11
substr ++ ++ substr substr ++ ++ substr |
129 | | efgredlemb.6 |
. . . . . . . . . . . . 13
|
130 | 2, 3, 4, 5 | efgtval 18136 |
. . . . . . . . . . . . . 14
splice
|
131 | 33, 44, 121, 130 | syl3anc 1326 |
. . . . . . . . . . . . 13
splice |
132 | | splval 13502 |
. . . . . . . . . . . . . 14
Word splice substr ++ ++ substr |
133 | 33, 44, 44, 124, 132 | syl13anc 1328 |
. . . . . . . . . . . . 13
splice
substr ++ ++ substr |
134 | 129, 131,
133 | 3eqtrd 2660 |
. . . . . . . . . . . 12
substr ++ ++
substr |
135 | | efgredlemb.7 |
. . . . . . . . . . . . 13
|
136 | 2, 3, 4, 5 | efgtval 18136 |
. . . . . . . . . . . . . 14
splice
|
137 | 29, 14, 94, 136 | syl3anc 1326 |
. . . . . . . . . . . . 13
splice |
138 | | splval 13502 |
. . . . . . . . . . . . . 14
Word splice substr ++ ++ substr |
139 | 29, 14, 14, 104, 138 | syl13anc 1328 |
. . . . . . . . . . . . 13
splice
substr ++ ++ substr |
140 | 135, 137,
139 | 3eqtrd 2660 |
. . . . . . . . . . . 12
substr ++ ++
substr |
141 | 24, 134, 140 | 3eqtr3d 2664 |
. . . . . . . . . . 11
substr ++ ++ substr
substr ++ ++
substr |
142 | 118, 128,
141 | 3eqtr2d 2662 |
. . . . . . . . . 10
substr ++
substr ++ ++ substr substr ++ ++ substr |
143 | | swrdcl 13419 |
. . . . . . . . . . . 12
Word
substr Word |
144 | 34, 143 | syl 17 |
. . . . . . . . . . 11
substr Word |
145 | | ccatcl 13359 |
. . . . . . . . . . . 12
Word
substr Word
++
substr
Word |
146 | 124, 126,
145 | syl2anc 693 |
. . . . . . . . . . 11
++ substr Word
|
147 | | ccatass 13371 |
. . . . . . . . . . 11
substr Word substr Word ++ substr Word
substr ++
substr ++ ++ substr substr ++ substr ++ ++
substr
|
148 | 98, 144, 146, 147 | syl3anc 1326 |
. . . . . . . . . 10
substr ++
substr ++ ++ substr substr ++ substr ++ ++
substr
|
149 | | swrdcl 13419 |
. . . . . . . . . . . 12
Word
substr Word |
150 | 30, 149 | syl 17 |
. . . . . . . . . . 11
substr
Word |
151 | | ccatass 13371 |
. . . . . . . . . . 11
substr Word Word substr Word
substr ++ ++
substr
substr ++ ++ substr |
152 | 32, 104, 150, 151 | syl3anc 1326 |
. . . . . . . . . 10
substr ++ ++ substr substr ++ ++ substr |
153 | 142, 148,
152 | 3eqtr3d 2664 |
. . . . . . . . 9
substr
++ substr ++ ++
substr
substr ++ ++ substr |
154 | | ccatcl 13359 |
. . . . . . . . . . 11
substr Word ++ substr Word
substr ++ ++
substr
Word |
155 | 144, 146,
154 | syl2anc 693 |
. . . . . . . . . 10
substr ++ ++
substr
Word |
156 | | ccatcl 13359 |
. . . . . . . . . . 11
Word
substr Word
++
substr
Word |
157 | 104, 150,
156 | syl2anc 693 |
. . . . . . . . . 10
++ substr Word
|
158 | | uztrn 11704 |
. . . . . . . . . . . . . 14
|
159 | 46, 113, 158 | syl2anc 693 |
. . . . . . . . . . . . 13
|
160 | | elfzuzb 12336 |
. . . . . . . . . . . . 13
|
161 | 16, 159, 160 | sylanbrc 698 |
. . . . . . . . . . . 12
|
162 | | swrd0len 13422 |
. . . . . . . . . . . 12
Word
substr |
163 | 34, 161, 162 | syl2anc 693 |
. . . . . . . . . . 11
substr |
164 | 163, 40 | eqtr4d 2659 |
. . . . . . . . . 10
substr substr |
165 | | ccatopth 13470 |
. . . . . . . . . 10
substr
Word
substr ++ ++ substr Word
substr Word ++ substr Word
substr
substr substr ++ substr ++ ++ substr substr
++ ++ substr
substr substr substr ++ ++ substr ++ substr |
166 | 98, 155, 32, 157, 164, 165 | syl221anc 1337 |
. . . . . . . . 9
substr ++ substr ++ ++
substr
substr ++ ++ substr
substr substr substr ++ ++ substr ++ substr |
167 | 153, 166 | mpbid 222 |
. . . . . . . 8
substr
substr
substr ++ ++ substr ++ substr |
168 | 167 | simpld 475 |
. . . . . . 7
substr substr |
169 | 168 | oveq1d 6665 |
. . . . . 6
substr
++
substr substr
++
substr |
170 | | ccatrid 13370 |
. . . . . . . 8
substr Word substr
++
substr |
171 | 98, 170 | syl 17 |
. . . . . . 7
substr
++
substr |
172 | 171 | oveq1d 6665 |
. . . . . 6
substr ++
++ substr substr ++ substr |
173 | 169, 172,
17 | 3eqtr4rd 2667 |
. . . . 5
substr ++ ++ substr |
174 | 163 | eqcomd 2628 |
. . . . 5
substr |
175 | | hash0 13158 |
. . . . . . 7
|
176 | 175 | oveq2i 6661 |
. . . . . 6
|
177 | 63 | addid1d 10236 |
. . . . . 6
|
178 | 176, 177 | syl5req 2669 |
. . . . 5
|
179 | 98, 100, 36, 104, 173, 174, 178 | splval2 13508 |
. . . 4
splice
substr ++ ++ substr |
180 | | elfzuzb 12336 |
. . . . . . . . . . . . . 14
|
181 | 16, 111, 180 | sylanbrc 698 |
. . . . . . . . . . . . 13
|
182 | | elfzuzb 12336 |
. . . . . . . . . . . . . 14
|
183 | 43, 47, 182 | sylanbrc 698 |
. . . . . . . . . . . . 13
|
184 | | ccatswrd 13456 |
. . . . . . . . . . . . 13
Word
substr ++ substr substr |
185 | 34, 181, 183, 44, 184 | syl13anc 1328 |
. . . . . . . . . . . 12
substr ++
substr
substr |
186 | 185 | oveq1d 6665 |
. . . . . . . . . . 11
substr ++ substr ++ ++ substr
substr ++ ++ substr |
187 | | swrdcl 13419 |
. . . . . . . . . . . . 13
Word
substr Word
|
188 | 34, 187 | syl 17 |
. . . . . . . . . . . 12
substr Word |
189 | | swrdcl 13419 |
. . . . . . . . . . . . 13
Word
substr Word |
190 | 34, 189 | syl 17 |
. . . . . . . . . . . 12
substr Word |
191 | | ccatass 13371 |
. . . . . . . . . . . 12
substr Word substr Word ++ substr Word
substr ++ substr ++ ++ substr
substr ++ substr ++ ++ substr |
192 | 188, 190,
146, 191 | syl3anc 1326 |
. . . . . . . . . . 11
substr ++ substr ++ ++ substr
substr ++ substr ++ ++ substr |
193 | 167 | simprd 479 |
. . . . . . . . . . 11
substr ++ ++
substr
++ substr |
194 | 186, 192,
193 | 3eqtr3d 2664 |
. . . . . . . . . 10
substr ++ substr ++ ++
substr
++ substr |
195 | | ccatcl 13359 |
. . . . . . . . . . . 12
substr Word ++ substr Word
substr ++ ++
substr
Word |
196 | 190, 146,
195 | syl2anc 693 |
. . . . . . . . . . 11
substr ++ ++
substr
Word |
197 | | swrdlen 13423 |
. . . . . . . . . . . . . 14
Word
substr |
198 | 34, 181, 51, 197 | syl3anc 1326 |
. . . . . . . . . . . . 13
substr |
199 | | pncan2 10288 |
. . . . . . . . . . . . . 14
|
200 | 63, 70, 199 | sylancl 694 |
. . . . . . . . . . . . 13
|
201 | 198, 200 | eqtrd 2656 |
. . . . . . . . . . . 12
substr |
202 | | s2len 13634 |
. . . . . . . . . . . 12
|
203 | 201, 202 | syl6eqr 2674 |
. . . . . . . . . . 11
substr |
204 | | ccatopth 13470 |
. . . . . . . . . . 11
substr Word substr ++ ++ substr Word Word
substr Word
substr
substr ++ substr ++ ++ substr ++ substr substr
substr ++ ++ substr substr |
205 | 188, 196,
104, 150, 203, 204 | syl221anc 1337 |
. . . . . . . . . 10
substr ++ substr ++ ++ substr ++ substr substr
substr ++ ++ substr substr |
206 | 194, 205 | mpbid 222 |
. . . . . . . . 9
substr
substr ++ ++ substr substr |
207 | 206 | simpld 475 |
. . . . . . . 8
substr |
208 | 207 | oveq2d 6666 |
. . . . . . 7
substr
++
substr substr
++ |
209 | | ccatswrd 13456 |
. . . . . . . 8
Word
substr ++
substr
substr |
210 | 34, 106, 181, 51, 209 | syl13anc 1328 |
. . . . . . 7
substr
++
substr
substr |
211 | 208, 210 | eqtr3d 2658 |
. . . . . 6
substr
++ substr |
212 | 211 | oveq1d 6665 |
. . . . 5
substr ++ ++ substr substr ++
substr |
213 | | eluzfz1 12348 |
. . . . . . 7
|
214 | 43, 213 | syl 17 |
. . . . . 6
|
215 | | ccatswrd 13456 |
. . . . . 6
Word
substr ++ substr substr |
216 | 34, 214, 51, 57, 215 | syl13anc 1328 |
. . . . 5
substr
++ substr
substr |
217 | | swrdid 13428 |
. . . . . 6
Word
substr |
218 | 34, 217 | syl 17 |
. . . . 5
substr |
219 | 212, 216,
218 | 3eqtrd 2660 |
. . . 4
substr ++ ++ substr |
220 | 96, 179, 219 | 3eqtrd 2660 |
. . 3
|
221 | 2, 3, 4, 5 | efgtf 18135 |
. . . . . . 7
splice |
222 | 13, 221 | syl 17 |
. . . . . 6
splice |
223 | 222 | simprd 479 |
. . . . 5
|
224 | | ffn 6045 |
. . . . 5
|
225 | 223, 224 | syl 17 |
. . . 4
|
226 | | fnovrn 6809 |
. . . 4
|
227 | 225, 93, 94, 226 | syl3anc 1326 |
. . 3
|
228 | 220, 227 | eqeltrrd 2702 |
. 2
|
229 | | uztrn 11704 |
. . . . . . 7
|
230 | 89, 16, 229 | syl2anc 693 |
. . . . . 6
|
231 | | elfzuzb 12336 |
. . . . . 6
|
232 | 230, 87, 231 | sylanbrc 698 |
. . . . 5
|
233 | 2, 3, 4, 5 | efgtval 18136 |
. . . . 5
splice |
234 | 13, 232, 121, 233 | syl3anc 1326 |
. . . 4
splice |
235 | | swrdcl 13419 |
. . . . . 6
Word
substr Word
|
236 | 30, 235 | syl 17 |
. . . . 5
substr Word |
237 | | swrdcl 13419 |
. . . . . 6
Word
substr Word |
238 | 30, 237 | syl 17 |
. . . . 5
substr
Word |
239 | | ccatswrd 13456 |
. . . . . . . . . . 11
Word
substr ++ substr substr |
240 | 34, 183, 44, 57, 239 | syl13anc 1328 |
. . . . . . . . . 10
substr ++
substr substr |
241 | 206 | simprd 479 |
. . . . . . . . . . . . . 14
substr ++ ++
substr
substr |
242 | | elfzuzb 12336 |
. . . . . . . . . . . . . . . 16
|
243 | 16, 89, 242 | sylanbrc 698 |
. . . . . . . . . . . . . . 15
|
244 | 2, 3, 4, 5, 6, 7, 21, 22, 23, 24, 25, 26, 27, 44, 14, 121, 94, 129, 135 | efgredlemg 18155 |
. . . . . . . . . . . . . . . . . 18
|
245 | 244, 46 | eqeltrrd 2702 |
. . . . . . . . . . . . . . . . 17
|
246 | | 0le2 11111 |
. . . . . . . . . . . . . . . . . . . 20
|
247 | 246 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
|
248 | 76 | zred 11482 |
. . . . . . . . . . . . . . . . . . . 20
|
249 | | 2re 11090 |
. . . . . . . . . . . . . . . . . . . 20
|
250 | | subge02 10544 |
. . . . . . . . . . . . . . . . . . . 20
|
251 | 248, 249,
250 | sylancl 694 |
. . . . . . . . . . . . . . . . . . 19
|
252 | 247, 251 | mpbid 222 |
. . . . . . . . . . . . . . . . . 18
|
253 | | eluz2 11693 |
. . . . . . . . . . . . . . . . . 18
|
254 | 78, 76, 252, 253 | syl3anbrc 1246 |
. . . . . . . . . . . . . . . . 17
|
255 | | uztrn 11704 |
. . . . . . . . . . . . . . . . 17
|
256 | 245, 254,
255 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
257 | | elfzuzb 12336 |
. . . . . . . . . . . . . . . 16
|
258 | 230, 256,
257 | sylanbrc 698 |
. . . . . . . . . . . . . . 15
|
259 | | lencl 13324 |
. . . . . . . . . . . . . . . . . 18
Word
|
260 | 30, 259 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
261 | 260, 54 | syl6eleq 2711 |
. . . . . . . . . . . . . . . 16
|
262 | | eluzfz2 12349 |
. . . . . . . . . . . . . . . 16
|
263 | 261, 262 | syl 17 |
. . . . . . . . . . . . . . 15
|
264 | | ccatswrd 13456 |
. . . . . . . . . . . . . . 15
Word
substr ++ substr substr |
265 | 30, 243, 258, 263, 264 | syl13anc 1328 |
. . . . . . . . . . . . . 14
substr ++
substr
substr |
266 | 241, 265 | eqtr4d 2659 |
. . . . . . . . . . . . 13
substr ++ ++
substr
substr ++ substr |
267 | | swrdcl 13419 |
. . . . . . . . . . . . . . 15
Word
substr Word
|
268 | 30, 267 | syl 17 |
. . . . . . . . . . . . . 14
substr Word |
269 | | swrdcl 13419 |
. . . . . . . . . . . . . . 15
Word
substr Word |
270 | 30, 269 | syl 17 |
. . . . . . . . . . . . . 14
substr Word |
271 | | swrdlen 13423 |
. . . . . . . . . . . . . . . 16
Word
substr |
272 | 34, 183, 44, 271 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
substr |
273 | | swrdlen 13423 |
. . . . . . . . . . . . . . . . 17
Word
substr |
274 | 30, 243, 258, 273 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
substr |
275 | 80, 63, 71 | sub32d 10424 |
. . . . . . . . . . . . . . . 16
|
276 | 80, 63, 71 | subsub4d 10423 |
. . . . . . . . . . . . . . . 16
|
277 | 274, 275,
276 | 3eqtr2d 2662 |
. . . . . . . . . . . . . . 15
substr |
278 | 272, 277 | eqtr4d 2659 |
. . . . . . . . . . . . . 14
substr substr
|
279 | | ccatopth 13470 |
. . . . . . . . . . . . . 14
substr Word ++ substr Word
substr Word substr Word
substr substr substr ++ ++ substr
substr ++ substr substr substr ++ substr substr |
280 | 190, 146,
268, 270, 278, 279 | syl221anc 1337 |
. . . . . . . . . . . . 13
substr ++ ++ substr
substr ++ substr substr substr ++ substr substr |
281 | 266, 280 | mpbid 222 |
. . . . . . . . . . . 12
substr substr ++ substr substr |
282 | 281 | simpld 475 |
. . . . . . . . . . 11
substr substr |
283 | 281 | simprd 479 |
. . . . . . . . . . . . . 14
++ substr substr |
284 | | elfzuzb 12336 |
. . . . . . . . . . . . . . . 16
|
285 | 230, 254,
284 | sylanbrc 698 |
. . . . . . . . . . . . . . 15
|
286 | | elfzuz 12338 |
. . . . . . . . . . . . . . . . 17
|
287 | 44, 286 | syl 17 |
. . . . . . . . . . . . . . . 16
|
288 | | elfzuzb 12336 |
. . . . . . . . . . . . . . . 16
|
289 | 287, 245,
288 | sylanbrc 698 |
. . . . . . . . . . . . . . 15
|
290 | | ccatswrd 13456 |
. . . . . . . . . . . . . . 15
Word
substr ++ substr substr |
291 | 30, 285, 289, 263, 290 | syl13anc 1328 |
. . . . . . . . . . . . . 14
substr ++
substr substr |
292 | 283, 291 | eqtr4d 2659 |
. . . . . . . . . . . . 13
++ substr substr ++ substr |
293 | | swrdcl 13419 |
. . . . . . . . . . . . . . 15
Word
substr Word |
294 | 30, 293 | syl 17 |
. . . . . . . . . . . . . 14
substr Word |
295 | | s2len 13634 |
. . . . . . . . . . . . . . 15
|
296 | | swrdlen 13423 |
. . . . . . . . . . . . . . . . 17
Word
substr |
297 | 30, 285, 289, 296 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
substr |
298 | | nncan 10310 |
. . . . . . . . . . . . . . . . 17
|
299 | 80, 70, 298 | sylancl 694 |
. . . . . . . . . . . . . . . 16
|
300 | 297, 299 | eqtr2d 2657 |
. . . . . . . . . . . . . . 15
substr |
301 | 295, 300 | syl5eq 2668 |
. . . . . . . . . . . . . 14
substr |
302 | | ccatopth 13470 |
. . . . . . . . . . . . . 14
Word substr Word substr Word
substr
Word
substr ++ substr substr ++ substr
substr
substr
substr |
303 | 124, 126,
294, 238, 301, 302 | syl221anc 1337 |
. . . . . . . . . . . . 13
++ substr substr ++ substr
substr
substr
substr |
304 | 292, 303 | mpbid 222 |
. . . . . . . . . . . 12
substr substr substr |
305 | 304 | simprd 479 |
. . . . . . . . . . 11
substr
substr |
306 | 282, 305 | oveq12d 6668 |
. . . . . . . . . 10
substr ++
substr
substr ++ substr |
307 | 240, 306 | eqtr3d 2658 |
. . . . . . . . 9
substr
substr ++ substr |
308 | 307 | oveq2d 6666 |
. . . . . . . 8
substr
++
substr substr
++ substr ++
substr |
309 | | ccatass 13371 |
. . . . . . . . 9
substr Word substr Word substr Word
substr ++ substr ++ substr substr ++ substr ++ substr |
310 | 32, 268, 238, 309 | syl3anc 1326 |
. . . . . . . 8
substr ++
substr ++ substr
substr ++ substr ++
substr
|
311 | 308, 310 | eqtr4d 2659 |
. . . . . . 7
substr
++
substr substr ++
substr ++ substr |
312 | | ccatswrd 13456 |
. . . . . . . . 9
Word
substr ++
substr
substr |
313 | 30, 106, 243, 258, 312 | syl13anc 1328 |
. . . . . . . 8
substr
++
substr
substr |
314 | 313 | oveq1d 6665 |
. . . . . . 7
substr ++
substr ++ substr
substr ++ substr |
315 | 17, 311, 314 | 3eqtrd 2660 |
. . . . . 6
substr ++
substr
|
316 | | ccatrid 13370 |
. . . . . . . 8
substr
Word substr
++ substr |
317 | 236, 316 | syl 17 |
. . . . . . 7
substr
++ substr |
318 | 317 | oveq1d 6665 |
. . . . . 6
substr ++ ++ substr substr ++
substr
|
319 | 315, 318 | eqtr4d 2659 |
. . . . 5
substr ++ ++ substr |
320 | | swrd0len 13422 |
. . . . . . 7
Word
substr |
321 | 30, 258, 320 | syl2anc 693 |
. . . . . 6
substr |
322 | 321 | eqcomd 2628 |
. . . . 5
substr |
323 | 175 | oveq2i 6661 |
. . . . . 6
|
324 | 78 | zcnd 11483 |
. . . . . . 7
|
325 | 324 | addid1d 10236 |
. . . . . 6
|
326 | 323, 325 | syl5req 2669 |
. . . . 5
|
327 | 236, 100,
238, 124, 319, 322, 326 | splval2 13508 |
. . . 4
splice substr ++
++
substr |
328 | 304 | simpld 475 |
. . . . . . . 8
substr |
329 | 328 | oveq2d 6666 |
. . . . . . 7
substr
++ substr
++ substr |
330 | | eluzfz1 12348 |
. . . . . . . . 9
|
331 | 230, 330 | syl 17 |
. . . . . . . 8
|
332 | | ccatswrd 13456 |
. . . . . . . 8
Word
substr ++ substr substr |
333 | 30, 331, 285, 289, 332 | syl13anc 1328 |
. . . . . . 7
substr
++ substr substr |
334 | 329, 333 | eqtrd 2656 |
. . . . . 6
substr
++
substr |
335 | 334 | oveq1d 6665 |
. . . . 5
substr ++ ++ substr
substr ++ substr |
336 | | eluzfz1 12348 |
. . . . . . 7
|
337 | 287, 336 | syl 17 |
. . . . . 6
|
338 | | ccatswrd 13456 |
. . . . . 6
Word
substr ++ substr substr |
339 | 30, 337, 289, 263, 338 | syl13anc 1328 |
. . . . 5
substr
++
substr substr |
340 | | swrdid 13428 |
. . . . . 6
Word
substr |
341 | 30, 340 | syl 17 |
. . . . 5
substr |
342 | 335, 339,
341 | 3eqtrd 2660 |
. . . 4
substr ++ ++ substr |
343 | 234, 327,
342 | 3eqtrd 2660 |
. . 3
|
344 | | fnovrn 6809 |
. . . 4
|
345 | 225, 232,
121, 344 | syl3anc 1326 |
. . 3
|
346 | 343, 345 | eqeltrrd 2702 |
. 2
|
347 | 228, 346 | jca 554 |
1
|