Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  efgredlemc Structured version   Visualization version   Unicode version

Theorem efgredlemc 17473
 Description: The reduced word that forms the base of the sequence in efgsval 17459 is uniquely determined, given the ending representation. (Contributed by Mario Carneiro, 1-Oct-2015.)
Hypotheses
Ref Expression
efgval.w Word
efgval.r ~FG
efgval2.m
efgval2.t splice
efgred.d
efgred.s Word ..^
efgredlem.1
efgredlem.2
efgredlem.3
efgredlem.4
efgredlem.5
efgredlemb.k
efgredlemb.l
efgredlemb.p
efgredlemb.q
efgredlemb.u
efgredlemb.v
efgredlemb.6
efgredlemb.7
efgredlemb.8
Assertion
Ref Expression
efgredlemc
Distinct variable groups:   ,,   ,,,   ,,   ,,   ,,,,,,   ,,,,,,,,   ,,,,,   ,,,,,,   ,,,,,   ,,,,,,   ,,   ,,,,,,,,,   ,,,,,,,   ,,   ,,   ,,,,,,,,,,   ,,,,
Allowed substitution hints:   (,,,,,,,,,,)   (,,,,,,,,)   (,,,,,,,,)   (,,,,,,)   (,,,,)   (,,,,)   (,,,)   (,,,,,,,,)   (,,,,)   (,,,,,)   ()   (,,,,,,,,)   (,,,,,,,,)   (,,)   (,,,,,)

Proof of Theorem efgredlemc
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 uzp1 11216 . 2
2 efgredlemb.8 . . . . . 6
3 efgval.w . . . . . . . . . . 11 Word
4 fviss 5938 . . . . . . . . . . 11 Word Word
53, 4eqsstri 3448 . . . . . . . . . 10 Word
6 efgredlem.2 . . . . . . . . . . . . 13
7 efgval.r . . . . . . . . . . . . . . 15 ~FG
8 efgval2.m . . . . . . . . . . . . . . 15
9 efgval2.t . . . . . . . . . . . . . . 15 splice
10 efgred.d . . . . . . . . . . . . . . 15
11 efgred.s . . . . . . . . . . . . . . 15 Word ..^
123, 7, 8, 9, 10, 11efgsdm 17458 . . . . . . . . . . . . . 14 Word ..^
1312simp1bi 1045 . . . . . . . . . . . . 13 Word
146, 13syl 17 . . . . . . . . . . . 12 Word
15 eldifi 3544 . . . . . . . . . . . 12 Word Word
16 wrdf 12723 . . . . . . . . . . . 12 Word ..^
1714, 15, 163syl 18 . . . . . . . . . . 11 ..^
18 fzossfz 11965 . . . . . . . . . . . . 13 ..^
19 efgredlemb.k . . . . . . . . . . . . . 14
20 efgredlem.1 . . . . . . . . . . . . . . . . 17
21 efgredlem.3 . . . . . . . . . . . . . . . . 17
22 efgredlem.4 . . . . . . . . . . . . . . . . 17
23 efgredlem.5 . . . . . . . . . . . . . . . . 17
243, 7, 8, 9, 10, 11, 20, 6, 21, 22, 23efgredlema 17468 . . . . . . . . . . . . . . . 16
2524simpld 466 . . . . . . . . . . . . . . 15
26 fzo0end 12032 . . . . . . . . . . . . . . 15 ..^
2725, 26syl 17 . . . . . . . . . . . . . 14 ..^
2819, 27syl5eqel 2553 . . . . . . . . . . . . 13 ..^
2918, 28sseldi 3416 . . . . . . . . . . . 12
30 lencl 12737 . . . . . . . . . . . . . . 15 Word
3114, 15, 303syl 18 . . . . . . . . . . . . . 14
3231nn0zd 11061 . . . . . . . . . . . . 13
33 fzoval 11948 . . . . . . . . . . . . 13 ..^
3432, 33syl 17 . . . . . . . . . . . 12 ..^
3529, 34eleqtrrd 2552 . . . . . . . . . . 11 ..^
3617, 35ffvelrnd 6038 . . . . . . . . . 10
375, 36sseldi 3416 . . . . . . . . 9 Word
38 efgredlemb.p . . . . . . . . . 10
39 elfzuz 11822 . . . . . . . . . 10
40 eluzfz1 11832 . . . . . . . . . 10
4138, 39, 403syl 18 . . . . . . . . 9
42 lencl 12737 . . . . . . . . . . . 12 Word
4337, 42syl 17 . . . . . . . . . . 11
44 nn0uz 11217 . . . . . . . . . . 11
4543, 44syl6eleq 2559 . . . . . . . . . 10
46 eluzfz2 11833 . . . . . . . . . 10
4745, 46syl 17 . . . . . . . . 9
48 ccatswrd 12866 . . . . . . . . 9 Word substr ++ substr substr
4937, 41, 38, 47, 48syl13anc 1294 . . . . . . . 8 substr ++ substr substr
50 swrdid 12838 . . . . . . . . 9 Word substr
5137, 50syl 17 . . . . . . . 8 substr
5249, 51eqtrd 2505 . . . . . . 7 substr ++ substr
533, 7, 8, 9, 10, 11efgsdm 17458 . . . . . . . . . . . . . 14 Word ..^
5453simp1bi 1045 . . . . . . . . . . . . 13 Word
5521, 54syl 17 . . . . . . . . . . . 12 Word
56 eldifi 3544 . . . . . . . . . . . 12 Word Word
57 wrdf 12723 . . . . . . . . . . . 12 Word ..^
5855, 56, 573syl 18 . . . . . . . . . . 11 ..^
59 fzossfz 11965 . . . . . . . . . . . . 13 ..^
60 efgredlemb.l . . . . . . . . . . . . . 14
6124simprd 470 . . . . . . . . . . . . . . 15
62 fzo0end 12032 . . . . . . . . . . . . . . 15 ..^
6361, 62syl 17 . . . . . . . . . . . . . 14 ..^
6460, 63syl5eqel 2553 . . . . . . . . . . . . 13 ..^
6559, 64sseldi 3416 . . . . . . . . . . . 12
66 lencl 12737 . . . . . . . . . . . . . . 15 Word
6755, 56, 663syl 18 . . . . . . . . . . . . . 14
6867nn0zd 11061 . . . . . . . . . . . . 13
69 fzoval 11948 . . . . . . . . . . . . 13 ..^
7068, 69syl 17 . . . . . . . . . . . 12 ..^
7165, 70eleqtrrd 2552 . . . . . . . . . . 11 ..^
7258, 71ffvelrnd 6038 . . . . . . . . . 10
735, 72sseldi 3416 . . . . . . . . 9 Word
74 efgredlemb.q . . . . . . . . . 10
75 elfzuz 11822 . . . . . . . . . 10
76 eluzfz1 11832 . . . . . . . . . 10
7774, 75, 763syl 18 . . . . . . . . 9
78 lencl 12737 . . . . . . . . . . . 12 Word
7973, 78syl 17 . . . . . . . . . . 11
8079, 44syl6eleq 2559 . . . . . . . . . 10
81 eluzfz2 11833 . . . . . . . . . 10
8280, 81syl 17 . . . . . . . . 9
83 ccatswrd 12866 . . . . . . . . 9 Word substr ++ substr substr
8473, 77, 74, 82, 83syl13anc 1294 . . . . . . . 8 substr ++ substr substr
85 swrdid 12838 . . . . . . . . 9 Word substr
8673, 85syl 17 . . . . . . . 8 substr
8784, 86eqtrd 2505 . . . . . . 7 substr ++ substr
8852, 87eqeq12d 2486 . . . . . 6 substr ++ substr substr ++ substr
892, 88mtbird 308 . . . . 5 substr ++ substr substr ++ substr
90 efgredlemb.6 . . . . . . . . . . . . 13
91 efgredlemb.u . . . . . . . . . . . . . 14
923, 7, 8, 9efgtval 17451 . . . . . . . . . . . . . 14 splice
9336, 38, 91, 92syl3anc 1292 . . . . . . . . . . . . 13 splice
948efgmf 17441 . . . . . . . . . . . . . . . . 17
9594ffvelrni 6036 . . . . . . . . . . . . . . . 16
9691, 95syl 17 . . . . . . . . . . . . . . 15
9791, 96s2cld 13025 . . . . . . . . . . . . . 14 Word
98 splval 12912 . . . . . . . . . . . . . 14 Word splice substr ++ ++ substr
9936, 38, 38, 97, 98syl13anc 1294 . . . . . . . . . . . . 13 splice substr ++ ++ substr
10090, 93, 993eqtrd 2509 . . . . . . . . . . . 12 substr ++ ++ substr
101 efgredlemb.7 . . . . . . . . . . . . 13
102 efgredlemb.v . . . . . . . . . . . . . 14
1033, 7, 8, 9efgtval 17451 . . . . . . . . . . . . . 14 splice
10472, 74, 102, 103syl3anc 1292 . . . . . . . . . . . . 13 splice
10594ffvelrni 6036 . . . . . . . . . . . . . . . 16
106102, 105syl 17 . . . . . . . . . . . . . . 15
107102, 106s2cld 13025 . . . . . . . . . . . . . 14 Word
108 splval 12912 . . . . . . . . . . . . . 14 Word splice substr ++ ++ substr
10972, 74, 74, 107, 108syl13anc 1294 . . . . . . . . . . . . 13 splice substr ++ ++ substr
110101, 104, 1093eqtrd 2509 . . . . . . . . . . . 12 substr ++ ++ substr
11122, 100, 1103eqtr3d 2513 . . . . . . . . . . 11 substr ++ ++ substr substr ++ ++ substr
112111adantr 472 . . . . . . . . . 10 substr ++ ++ substr substr ++ ++ substr
113 swrdcl 12829 . . . . . . . . . . . . . 14 Word substr Word
11437, 113syl 17 . . . . . . . . . . . . 13 substr Word
115114adantr 472 . . . . . . . . . . . 12 substr Word
11697adantr 472 . . . . . . . . . . . 12 Word
117 ccatcl 12771 . . . . . . . . . . . 12 substr Word Word substr ++ Word
118115, 116, 117syl2anc 673 . . . . . . . . . . 11 substr ++ Word
119 swrdcl 12829 . . . . . . . . . . . . 13 Word substr Word
12037, 119syl 17 . . . . . . . . . . . 12 substr Word
121120adantr 472 . . . . . . . . . . 11 substr Word
122 swrdcl 12829 . . . . . . . . . . . . . 14 Word substr Word
12373, 122syl 17 . . . . . . . . . . . . 13 substr Word
124123adantr 472 . . . . . . . . . . . 12 substr Word
125107adantr 472 . . . . . . . . . . . 12 Word
126 ccatcl 12771 . . . . . . . . . . . 12 substr Word Word substr ++ Word
127124, 125, 126syl2anc 673 . . . . . . . . . . 11 substr ++ Word
128 swrdcl 12829 . . . . . . . . . . . . 13 Word substr Word
12973, 128syl 17 . . . . . . . . . . . 12 substr Word
130129adantr 472 . . . . . . . . . . 11 substr Word
131 swrd0len 12832 . . . . . . . . . . . . . . . 16 Word substr
13237, 38, 131syl2anc 673 . . . . . . . . . . . . . . 15 substr
133 swrd0len 12832 . . . . . . . . . . . . . . . 16 Word substr
13473, 74, 133syl2anc 673 . . . . . . . . . . . . . . 15 substr
135132, 134eqeq12d 2486 . . . . . . . . . . . . . 14 substr substr
136135biimpar 493 . . . . . . . . . . . . 13 substr substr
137 s2len 13043 . . . . . . . . . . . . . . 15
138 s2len 13043 . . . . . . . . . . . . . . 15
139137, 138eqtr4i 2496 . . . . . . . . . . . . . 14
140139a1i 11 . . . . . . . . . . . . 13
141136, 140oveq12d 6326 . . . . . . . . . . . 12 substr substr
142 ccatlen 12772 . . . . . . . . . . . . 13 substr Word Word substr ++ substr
143115, 116, 142syl2anc 673 . . . . . . . . . . . 12 substr ++ substr
144 ccatlen 12772 . . . . . . . . . . . . 13 substr Word Word substr ++ substr
145124, 125, 144syl2anc 673 . . . . . . . . . . . 12 substr ++ substr
146141, 143, 1453eqtr4d 2515 . . . . . . . . . . 11 substr ++ substr ++
147 ccatopth 12880 . . . . . . . . . . 11 substr ++ Word substr Word substr ++ Word substr Word substr ++ substr ++ substr ++ ++ substr substr ++ ++ substr substr ++ substr ++ substr substr
148118, 121, 127, 130, 146, 147syl221anc 1303 . . . . . . . . . 10 substr ++ ++ substr substr ++ ++ substr substr ++ substr ++ substr substr
149112, 148mpbid 215 . . . . . . . . 9 substr ++ substr ++ substr substr
150149simpld 466 . . . . . . . 8 substr ++ substr ++
151 ccatopth 12880 . . . . . . . . 9 substr Word Word substr Word Word substr substr substr ++ substr ++ substr substr
152115, 116, 124, 125, 136, 151syl221anc 1303 . . . . . . . 8 substr ++ substr ++ substr substr
153150, 152mpbid 215 . . . . . . 7 substr substr
154153simpld 466 . . . . . 6 substr substr
155149simprd 470 . . . . . 6 substr substr
156154, 155oveq12d 6326 . . . . 5 substr ++ substr substr ++ substr
15789, 156mtand 671 . . . 4
158157pm2.21d 109 . . 3
159 uzp1 11216 . . . 4
16091s1cld 12795 . . . . . . . . . . . . . . . . 17 Word
161 ccatcl 12771 . . . . . . . . . . . . . . . . 17 substr Word Word substr ++ Word
162114, 160, 161syl2anc 673 . . . . . . . . . . . . . . . 16 substr ++ Word
16396s1cld 12795 . . . . . . . . . . . . . . . 16 Word
164 ccatass 12783 . . . . . . . . . . . . . . . 16 substr ++ Word Word substr Word substr ++ ++ ++ substr substr ++ ++ ++ substr
165162, 163, 120, 164syl3anc 1292 . . . . . . . . . . . . . . 15 substr ++ ++ ++ substr substr ++ ++ ++ substr
166 ccatass 12783 . . . . . . . . . . . . . . . . . . 19 substr Word Word Word substr ++ ++ substr ++ ++
167114, 160, 163, 166syl3anc 1292 . . . . . . . . . . . . . . . . . 18 substr ++ ++ substr ++ ++
168 df-s2 13003 . . . . . . . . . . . . . . . . . . 19 ++
169168oveq2i 6319 . . . . . . . . . . . . . . . . . 18 substr ++ substr ++ ++
170167, 169syl6eqr 2523 . . . . . . . . . . . . . . . . 17 substr ++ ++ substr ++
171170oveq1d 6323 . . . . . . . . . . . . . . . 16 substr ++ ++ ++ substr substr ++ ++ substr
172102s1cld 12795 . . . . . . . . . . . . . . . . . . 19 Word
173106s1cld 12795 . . . . . . . . . . . . . . . . . . 19 Word
174 ccatass 12783 . . . . . . . . . . . . . . . . . . 19 substr Word Word Word substr ++ ++ substr ++ ++
175123, 172, 173, 174syl3anc 1292 . . . . . . . . . . . . . . . . . 18 substr ++ ++ substr ++ ++
176 df-s2 13003 . . . . . . . . . . . . . . . . . . 19 ++
177176oveq2i 6319 . . . . . . . . . . . . . . . . . 18 substr ++ substr ++ ++
178175, 177syl6eqr 2523 . . . . . . . . . . . . . . . . 17 substr ++ ++ substr ++
179178oveq1d 6323 . . . . . . . . . . . . . . . 16 substr ++ ++ ++ substr substr ++ ++ substr
180111, 171, 1793eqtr4d 2515 . . . . . . . . . . . . . . 15 substr ++ ++ ++ substr substr ++ ++ ++ substr
181165, 180eqtr3d 2507 . . . . . . . . . . . . . 14 substr ++ ++ ++ substr substr ++ ++ ++ substr
182181adantr 472 . . . . . . . . . . . . 13 substr ++ ++ ++ substr substr ++ ++ ++ substr
183162adantr 472 . . . . . . . . . . . . . 14 substr ++ Word
184163adantr 472 . . . . . . . . . . . . . . 15 Word
185120adantr 472 . . . . . . . . . . . . . . 15 substr Word
186 ccatcl 12771 . . . . . . . . . . . . . . 15 Word substr Word ++ substr Word
187184, 185, 186syl2anc 673 . . . . . . . . . . . . . 14 ++ substr Word
188 ccatcl 12771 . . . . . . . . . . . . . . . . 17 substr Word Word substr ++ Word
189123, 172, 188syl2anc 673 . . . . . . . . . . . . . . . 16 substr ++ Word
190189adantr 472 . . . . . . . . . . . . . . 15 substr ++ Word
191173adantr 472 . . . . . . . . . . . . . . 15 Word
192 ccatcl 12771 . . . . . . . . . . . . . . 15 substr ++ Word Word substr ++ ++ Word
193190, 191, 192syl2anc 673 . . . . . . . . . . . . . 14 substr ++ ++ Word
194129adantr 472 . . . . . . . . . . . . . 14 substr Word
195 ccatlen 12772 . . . . . . . . . . . . . . . . . . . 20 substr Word Word substr ++ substr
196123, 172, 195syl2anc 673 . . . . . . . . . . . . . . . . . . 19 substr ++ substr
197 s1len 12797 . . . . . . . . . . . . . . . . . . . . 21
198197a1i 11 . . . . . . . . . . . . . . . . . . . 20
199134, 198oveq12d 6326 . . . . . . . . . . . . . . . . . . 19 substr
200196, 199eqtrd 2505 . . . . . . . . . . . . . . . . . 18 substr ++
201132, 200eqeq12d 2486 . . . . . . . . . . . . . . . . 17 substr substr ++
202201biimpar 493 . . . . . . . . . . . . . . . 16 substr substr ++
203 s1len 12797 . . . . . . . . . . . . . . . . . 18
204 s1len 12797 . . . . . . . . . . . . . . . . . 18
205203, 204eqtr4i 2496 . . . . . . . . . . . . . . . . 17
206205a1i 11 . . . . . . . . . . . . . . . 16
207202, 206oveq12d 6326 . . . . . . . . . . . . . . 15 substr substr ++
208114adantr 472 . . . . . . . . . . . . . . . 16 substr Word
209160adantr 472 . . . . . . . . . . . . . . . 16 Word
210 ccatlen 12772 . . . . . . . . . . . . . . . 16 substr Word Word substr ++ substr
211208, 209, 210syl2anc 673 . . . . . . . . . . . . . . 15 substr ++ substr
212 ccatlen 12772 . . . . . . . . . . . . . . . 16 substr ++ Word Word substr ++ ++ substr ++
213190, 191, 212syl2anc 673 . . . . . . . . . . . . . . 15 substr ++ ++ substr ++
214207, 211, 2133eqtr4d 2515 . . . . . . . . . . . . . 14 substr ++ substr ++ ++
215 ccatopth 12880 . . . . . . . . . . . . . 14 substr ++ Word ++ substr Word substr ++ ++ Word substr Word substr ++ substr ++ ++ substr ++ ++ ++ substr substr ++ ++ ++ substr substr ++ substr ++ ++ ++ substr substr
216183, 187, 193, 194, 214, 215syl221anc 1303 . . . . . . . . . . . . 13 substr ++ ++ ++ substr substr ++ ++ ++ substr substr ++ substr ++ ++ ++ substr substr
217182, 216mpbid 215 . . . . . . . . . . . 12 substr ++ substr ++ ++ ++ substr substr
218217simpld 466 . . . . . . . . . . 11 substr ++ substr ++ ++
219 ccatopth 12880 . . . . . . . . . . . 12 substr Word Word substr ++ Word Word substr substr ++ substr ++ substr ++ ++ substr substr ++
220208, 209, 190, 191, 202, 219syl221anc 1303 . . . . . . . . . . 11 substr ++ substr ++ ++ substr substr ++
221218, 220mpbid 215 . . . . . . . . . 10 substr substr ++
222221simpld 466 . . . . . . . . 9 substr substr ++
223222oveq1d 6323 . . . . . . . 8 substr ++ substr substr ++ ++ substr
224123adantr 472 . . . . . . . . 9 substr Word
225172adantr 472 . . . . . . . . 9 Word
226 ccatass 12783 . . . . . . . . 9 substr Word Word substr Word substr ++ ++ substr substr ++ ++ substr
227224, 225, 185, 226syl3anc 1292 . . . . . . . 8 substr ++ ++ substr substr ++ ++ substr
228221simprd 470 . . . . . . . . . . . . . . 15
229 s111 12806 . . . . . . . . . . . . . . . . 17
23091, 106, 229syl2anc 673 . . . . . . . . . . . . . . . 16
231230adantr 472 . . . . . . . . . . . . . . 15
232228, 231mpbid 215 . . . . . . . . . . . . . 14
233232fveq2d 5883 . . . . . . . . . . . . 13
2348efgmnvl 17442 . . . . . . . . . . . . . . 15
235102, 234syl 17 . . . . . . . . . . . . . 14
236235adantr 472 . . . . . . . . . . . . 13
237233, 236eqtrd 2505 . . . . . . . . . . . 12
238237s1eqd 12793 . . . . . . . . . . 11
239238oveq1d 6323 . . . . . . . . . 10 ++ substr ++ substr
240217simprd 470 . . . . . . . . . 10 ++ substr substr
241239, 240eqtr3d 2507 . . . . . . . . 9 ++ substr substr
242241oveq2d 6324 . . . . . . . 8 substr ++ ++ substr substr ++ substr
243223, 227, 2423eqtrd 2509 . . . . . . 7 substr ++ substr substr ++ substr
24489, 243mtand 671 . . . . . 6
245244pm2.21d 109 . . . . 5
246 elfzelz 11826 . . . . . . . . . . . 12
24774, 246syl 17 . . . . . . . . . . 11
248247zcnd 11064 . . . . . . . . . 10
249 1cnd 9677 . . . . . . . . . 10
250248, 249, 249addassd 9683 . . . . . . . . 9
251 df-2 10690 . . . . . . . . . 10
252251oveq2i 6319 . . . . . . . . 9
253250, 252syl6eqr 2523 . . . . . . . 8
254253fveq2d 5883 . . . . . . 7
255254eleq2d 2534 . . . . . 6
2563, 7, 8, 9, 10, 11efgsfo 17467 . . . . . . . . . 10
257 swrdcl 12829 . . . . . . . . . . . . 13 Word substr Word
25837, 257syl 17 . . . . . . . . . . . 12 substr Word
259 ccatcl 12771 . . . . . . . . . . . 12 substr Word substr Word substr ++ substr Word
260123, 258, 259syl2anc 673 . . . . . . . . . . 11 substr ++ substr Word
2613efgrcl 17443 . . . . . . . . . . . . 13 Word
26236, 261syl 17 . . . . . . . . . . . 12 Word
263262simprd 470 . . . . . . . . . . 11 Word
264260, 263eleqtrrd 2552 . . . . . . . . . 10 substr ++ substr
265 foelrn 6056 . . . . . . . . . 10 substr ++ substr substr ++ substr
266256, 264, 265sylancr 676 . . . . . . . . 9 substr ++ substr
267266adantr 472 . . . . . . . 8 substr ++ substr
26820ad2antrr 740 . . . . . . . . 9 substr ++ substr
2696ad2antrr 740 . . . . . . . . 9 substr ++ substr
27021ad2antrr 740 . . . . . . . . 9 substr ++ substr
27122ad2antrr 740 . . . . . . . . 9 substr ++ substr
27223ad2antrr 740 . . . . . . . . 9 substr ++ substr
27338ad2antrr 740 . . . . . . . . 9 substr ++ substr
27474ad2antrr 740 . . . . . . . . 9 substr ++ substr
27591ad2antrr 740 . . . . . . . . 9 substr ++ substr
276102ad2antrr 740 . . . . . . . . 9 substr ++ substr
27790ad2antrr 740 . . . . . . . . 9 substr ++ substr
278101ad2antrr 740 . . . . . . . . 9 substr ++ substr
2792ad2antrr 740 . . . . . . . . 9 substr ++ substr
280 simplr 770 . . . . . . . . 9 substr ++ substr
281 simprl 772 . . . . . . . . 9 substr ++ substr
282 simprr 774 . . . . . . . . . 10 substr ++ substr substr ++ substr
283282eqcomd 2477 . . . . . . . . 9 substr ++ substr substr ++ substr
2843, 7, 8, 9, 10, 11, 268, 269, 270, 271, 272, 19, 60, 273, 274, 275, 276, 277, 278, 279, 280, 281, 283efgredlemd 17472 . . . . . . . 8 substr ++ substr
285267, 284rexlimddv 2875 . . . . . . 7
286285ex 441 . . . . . 6
287255, 286sylbid 223 . . . . 5
288245, 287jaod 387 . . . 4
289159, 288syl5 32 . . 3
290158, 289jaod 387 . 2
2911, 290syl5 32 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 189   wo 375   wa 376   wceq 1452   wcel 1904  wral 2756  wrex 2757  crab 2760  cvv 3031   cdif 3387  c0 3722  csn 3959  cop 3965  cotp 3967  ciun 4269   class class class wbr 4395   cmpt 4454   cid 4749   cxp 4837   cdm 4839   crn 4840  wf 5585  wfo 5587  cfv 5589  (class class class)co 6308   cmpt2 6310  c1o 7193  c2o 7194  cc0 9557  c1 9558   caddc 9560   clt 9693   cmin 9880  cn 10631  c2 10681  cn0 10893  cz 10961  cuz 11182  cfz 11810  ..^cfzo 11942  chash 12553  Word cword 12703   ++ cconcat 12705  cs1 12706   substr csubstr 12707   splice csplice 12708  cs2 12996   ~FG cefg 17434 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602  ax-cnex 9613  ax-resscn 9614  ax-1cn 9615  ax-icn 9616  ax-addcl 9617  ax-addrcl 9618  ax-mulcl 9619  ax-mulrcl 9620  ax-mulcom 9621  ax-addass 9622  ax-mulass 9623  ax-distr 9624  ax-i2m1 9625  ax-1ne0 9626  ax-1rid 9627  ax-rnegex 9628  ax-rrecex 9629  ax-cnre 9630  ax-pre-lttri 9631  ax-pre-lttrn 9632  ax-pre-ltadd 9633  ax-pre-mulgt0 9634 This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-nel 2644  df-ral 2761  df-rex 2762  df-reu 2763  df-rmo 2764  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-ot 3968  df-uni 4191  df-int 4227  df-iun 4271  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-pred 5387  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-riota 6270  df-ov 6311  df-oprab 6312  df-mpt2 6313  df-om 6712  df-1st 6812  df-2nd 6813  df-wrecs 7046  df-recs 7108  df-rdg 7146  df-1o 7200  df-2o 7201  df-oadd 7204  df-er 7381  df-map 7492  df-pm 7493  df-en 7588  df-dom 7589  df-sdom 7590  df-fin 7591  df-card 8391  df-cda 8616  df-pnf 9695  df-mnf 9696  df-xr 9697  df-ltxr 9698  df-le 9699  df-sub 9882  df-neg 9883  df-nn 10632  df-2 10690  df-n0 10894  df-z 10962  df-uz 11183  df-rp 11326  df-fz 11811  df-fzo 11943  df-hash 12554  df-word 12711  df-concat 12713  df-s1 12714  df-substr 12715  df-splice 12716  df-s2 13003 This theorem is referenced by:  efgredlemb  17474
 Copyright terms: Public domain W3C validator