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

Theorem efgredlemc 16569
 Description: The reduced word that forms the base of the sequence in efgsval 16555 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 11115 . 2
2 efgredlemb.8 . . . . . 6
3 efgval.w . . . . . . . . . . 11 Word
4 fviss 5925 . . . . . . . . . . 11 Word Word
53, 4eqsstri 3534 . . . . . . . . . 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 16554 . . . . . . . . . . . . . 14 Word ..^
1312simp1bi 1011 . . . . . . . . . . . . 13 Word
146, 13syl 16 . . . . . . . . . . . 12 Word
15 eldifi 3626 . . . . . . . . . . . 12 Word Word
16 wrdf 12519 . . . . . . . . . . . 12 Word ..^
1714, 15, 163syl 20 . . . . . . . . . . 11 ..^
18 fzossfz 11814 . . . . . . . . . . . . 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 16564 . . . . . . . . . . . . . . . 16
2524simpld 459 . . . . . . . . . . . . . . 15
26 fzo0end 11872 . . . . . . . . . . . . . . 15 ..^
2725, 26syl 16 . . . . . . . . . . . . . 14 ..^
2819, 27syl5eqel 2559 . . . . . . . . . . . . 13 ..^
2918, 28sseldi 3502 . . . . . . . . . . . 12
30 lencl 12528 . . . . . . . . . . . . . . 15 Word
3114, 15, 303syl 20 . . . . . . . . . . . . . 14
3231nn0zd 10964 . . . . . . . . . . . . 13
33 fzoval 11798 . . . . . . . . . . . . 13 ..^
3432, 33syl 16 . . . . . . . . . . . 12 ..^
3529, 34eleqtrrd 2558 . . . . . . . . . . 11 ..^
3617, 35ffvelrnd 6022 . . . . . . . . . 10
375, 36sseldi 3502 . . . . . . . . 9 Word
38 efgredlemb.p . . . . . . . . . 10
39 elfzuz 11684 . . . . . . . . . 10
40 eluzfz1 11693 . . . . . . . . . 10
4138, 39, 403syl 20 . . . . . . . . 9
42 lencl 12528 . . . . . . . . . . . 12 Word
4337, 42syl 16 . . . . . . . . . . 11
44 nn0uz 11116 . . . . . . . . . . 11
4543, 44syl6eleq 2565 . . . . . . . . . 10
46 eluzfz2 11694 . . . . . . . . . 10
4745, 46syl 16 . . . . . . . . 9
48 ccatswrd 12644 . . . . . . . . 9 Word substr concat substr substr
4937, 41, 38, 47, 48syl13anc 1230 . . . . . . . 8 substr concat substr substr
50 swrdid 12615 . . . . . . . . 9 Word substr
5137, 50syl 16 . . . . . . . 8 substr
5249, 51eqtrd 2508 . . . . . . 7 substr concat substr
533, 7, 8, 9, 10, 11efgsdm 16554 . . . . . . . . . . . . . 14 Word ..^
5453simp1bi 1011 . . . . . . . . . . . . 13 Word
5521, 54syl 16 . . . . . . . . . . . 12 Word
56 eldifi 3626 . . . . . . . . . . . 12 Word Word
57 wrdf 12519 . . . . . . . . . . . 12 Word ..^
5855, 56, 573syl 20 . . . . . . . . . . 11 ..^
59 fzossfz 11814 . . . . . . . . . . . . 13 ..^
60 efgredlemb.l . . . . . . . . . . . . . 14
6124simprd 463 . . . . . . . . . . . . . . 15
62 fzo0end 11872 . . . . . . . . . . . . . . 15 ..^
6361, 62syl 16 . . . . . . . . . . . . . 14 ..^
6460, 63syl5eqel 2559 . . . . . . . . . . . . 13 ..^
6559, 64sseldi 3502 . . . . . . . . . . . 12
66 lencl 12528 . . . . . . . . . . . . . . 15 Word
6755, 56, 663syl 20 . . . . . . . . . . . . . 14
6867nn0zd 10964 . . . . . . . . . . . . 13
69 fzoval 11798 . . . . . . . . . . . . 13 ..^
7068, 69syl 16 . . . . . . . . . . . 12 ..^
7165, 70eleqtrrd 2558 . . . . . . . . . . 11 ..^
7258, 71ffvelrnd 6022 . . . . . . . . . 10
735, 72sseldi 3502 . . . . . . . . 9 Word
74 efgredlemb.q . . . . . . . . . 10
75 elfzuz 11684 . . . . . . . . . 10
76 eluzfz1 11693 . . . . . . . . . 10
7774, 75, 763syl 20 . . . . . . . . 9
78 lencl 12528 . . . . . . . . . . . 12 Word
7973, 78syl 16 . . . . . . . . . . 11
8079, 44syl6eleq 2565 . . . . . . . . . 10
81 eluzfz2 11694 . . . . . . . . . 10
8280, 81syl 16 . . . . . . . . 9
83 ccatswrd 12644 . . . . . . . . 9 Word substr concat substr substr
8473, 77, 74, 82, 83syl13anc 1230 . . . . . . . 8 substr concat substr substr
85 swrdid 12615 . . . . . . . . 9 Word substr
8673, 85syl 16 . . . . . . . 8 substr
8784, 86eqtrd 2508 . . . . . . 7 substr concat substr
8852, 87eqeq12d 2489 . . . . . 6 substr concat substr substr concat substr
892, 88mtbird 301 . . . . 5 substr concat substr substr concat substr
90 efgredlemb.6 . . . . . . . . . . . . 13
91 efgredlemb.u . . . . . . . . . . . . . 14
923, 7, 8, 9efgtval 16547 . . . . . . . . . . . . . 14 splice
9336, 38, 91, 92syl3anc 1228 . . . . . . . . . . . . 13 splice
948efgmf 16537 . . . . . . . . . . . . . . . . 17
9594ffvelrni 6020 . . . . . . . . . . . . . . . 16
9691, 95syl 16 . . . . . . . . . . . . . . 15
9791, 96s2cld 12797 . . . . . . . . . . . . . 14 Word
98 splval 12690 . . . . . . . . . . . . . 14 Word splice substr concat concat substr
9936, 38, 38, 97, 98syl13anc 1230 . . . . . . . . . . . . 13 splice substr concat concat substr
10090, 93, 993eqtrd 2512 . . . . . . . . . . . 12 substr concat concat substr
101 efgredlemb.7 . . . . . . . . . . . . 13
102 efgredlemb.v . . . . . . . . . . . . . 14
1033, 7, 8, 9efgtval 16547 . . . . . . . . . . . . . 14 splice
10472, 74, 102, 103syl3anc 1228 . . . . . . . . . . . . 13 splice
10594ffvelrni 6020 . . . . . . . . . . . . . . . 16
106102, 105syl 16 . . . . . . . . . . . . . . 15
107102, 106s2cld 12797 . . . . . . . . . . . . . 14 Word
108 splval 12690 . . . . . . . . . . . . . 14 Word splice substr concat concat substr
10972, 74, 74, 107, 108syl13anc 1230 . . . . . . . . . . . . 13 splice substr concat concat substr
110101, 104, 1093eqtrd 2512 . . . . . . . . . . . 12 substr concat concat substr
11122, 100, 1103eqtr3d 2516 . . . . . . . . . . 11 substr concat concat substr substr concat concat substr
112111adantr 465 . . . . . . . . . 10 substr concat concat substr substr concat concat substr
113 swrdcl 12609 . . . . . . . . . . . . . 14 Word substr Word
11437, 113syl 16 . . . . . . . . . . . . 13 substr Word
115114adantr 465 . . . . . . . . . . . 12 substr Word
11697adantr 465 . . . . . . . . . . . 12 Word
117 ccatcl 12558 . . . . . . . . . . . 12 substr Word Word substr concat Word
118115, 116, 117syl2anc 661 . . . . . . . . . . 11 substr concat Word
119 swrdcl 12609 . . . . . . . . . . . . 13 Word substr Word
12037, 119syl 16 . . . . . . . . . . . 12 substr Word
121120adantr 465 . . . . . . . . . . 11 substr Word
122 swrdcl 12609 . . . . . . . . . . . . . 14 Word substr Word
12373, 122syl 16 . . . . . . . . . . . . 13 substr Word
124123adantr 465 . . . . . . . . . . . 12 substr Word
125107adantr 465 . . . . . . . . . . . 12 Word
126 ccatcl 12558 . . . . . . . . . . . 12 substr Word Word substr concat Word
127124, 125, 126syl2anc 661 . . . . . . . . . . 11 substr concat Word
128 swrdcl 12609 . . . . . . . . . . . . 13 Word substr Word
12973, 128syl 16 . . . . . . . . . . . 12 substr Word
130129adantr 465 . . . . . . . . . . 11 substr Word
131 swrd0len 12612 . . . . . . . . . . . . . . . 16 Word substr
13237, 38, 131syl2anc 661 . . . . . . . . . . . . . . 15 substr
133 swrd0len 12612 . . . . . . . . . . . . . . . 16 Word substr
13473, 74, 133syl2anc 661 . . . . . . . . . . . . . . 15 substr
135132, 134eqeq12d 2489 . . . . . . . . . . . . . 14 substr substr
136135biimpar 485 . . . . . . . . . . . . 13 substr substr
137 s2len 12815 . . . . . . . . . . . . . . 15
138 s2len 12815 . . . . . . . . . . . . . . 15
139137, 138eqtr4i 2499 . . . . . . . . . . . . . 14
140139a1i 11 . . . . . . . . . . . . 13
141136, 140oveq12d 6302 . . . . . . . . . . . 12 substr substr
142 ccatlen 12559 . . . . . . . . . . . . 13 substr Word Word substr concat substr
143115, 116, 142syl2anc 661 . . . . . . . . . . . 12 substr concat substr
144 ccatlen 12559 . . . . . . . . . . . . 13 substr Word Word substr concat substr
145124, 125, 144syl2anc 661 . . . . . . . . . . . 12 substr concat substr
146141, 143, 1453eqtr4d 2518 . . . . . . . . . . 11 substr concat substr concat
147 ccatopth 12658 . . . . . . . . . . 11 substr concat Word substr Word substr concat Word substr Word substr concat substr concat substr concat concat substr substr concat concat substr substr concat substr concat substr substr
148118, 121, 127, 130, 146, 147syl221anc 1239 . . . . . . . . . 10 substr concat concat substr substr concat concat substr substr concat substr concat substr substr
149112, 148mpbid 210 . . . . . . . . 9 substr concat substr concat substr substr
150149simpld 459 . . . . . . . 8 substr concat substr concat
151 ccatopth 12658 . . . . . . . . 9 substr Word Word substr Word Word substr substr substr concat substr concat substr substr
152115, 116, 124, 125, 136, 151syl221anc 1239 . . . . . . . 8 substr concat substr concat substr substr
153150, 152mpbid 210 . . . . . . 7 substr substr
154153simpld 459 . . . . . 6 substr substr
155149simprd 463 . . . . . 6 substr substr
156154, 155oveq12d 6302 . . . . 5 substr concat substr substr concat substr
15789, 156mtand 659 . . . 4
158157pm2.21d 106 . . 3
159 uzp1 11115 . . . 4
16091s1cld 12578 . . . . . . . . . . . . . . . . 17 Word
161 ccatcl 12558 . . . . . . . . . . . . . . . . 17 substr Word Word substr concat Word
162114, 160, 161syl2anc 661 . . . . . . . . . . . . . . . 16 substr concat Word
16396s1cld 12578 . . . . . . . . . . . . . . . 16 Word
164 ccatass 12570 . . . . . . . . . . . . . . . 16 substr concat Word Word substr Word substr concat concat concat substr substr concat concat concat substr
165162, 163, 120, 164syl3anc 1228 . . . . . . . . . . . . . . 15 substr concat concat concat substr substr concat concat concat substr
166 ccatass 12570 . . . . . . . . . . . . . . . . . . 19 substr Word Word Word substr concat concat substr concat concat
167114, 160, 163, 166syl3anc 1228 . . . . . . . . . . . . . . . . . 18 substr concat concat substr concat concat
168 df-s2 12776 . . . . . . . . . . . . . . . . . . 19 concat
169168oveq2i 6295 . . . . . . . . . . . . . . . . . 18 substr concat substr concat concat
170167, 169syl6eqr 2526 . . . . . . . . . . . . . . . . 17 substr concat concat substr concat
171170oveq1d 6299 . . . . . . . . . . . . . . . 16 substr concat concat concat substr substr concat concat substr
172102s1cld 12578 . . . . . . . . . . . . . . . . . . 19 Word
173106s1cld 12578 . . . . . . . . . . . . . . . . . . 19 Word
174 ccatass 12570 . . . . . . . . . . . . . . . . . . 19 substr Word Word Word substr concat concat substr concat concat
175123, 172, 173, 174syl3anc 1228 . . . . . . . . . . . . . . . . . 18 substr concat concat substr concat concat
176 df-s2 12776 . . . . . . . . . . . . . . . . . . 19 concat
177176oveq2i 6295 . . . . . . . . . . . . . . . . . 18 substr concat substr concat concat
178175, 177syl6eqr 2526 . . . . . . . . . . . . . . . . 17 substr concat concat substr concat
179178oveq1d 6299 . . . . . . . . . . . . . . . 16 substr concat concat concat substr substr concat concat substr
180111, 171, 1793eqtr4d 2518 . . . . . . . . . . . . . . 15 substr concat concat concat substr substr concat concat concat substr
181165, 180eqtr3d 2510 . . . . . . . . . . . . . 14 substr concat concat concat substr substr concat concat concat substr
182181adantr 465 . . . . . . . . . . . . 13 substr concat concat concat substr substr concat concat concat substr
183162adantr 465 . . . . . . . . . . . . . 14 substr concat Word
184163adantr 465 . . . . . . . . . . . . . . 15 Word
185120adantr 465 . . . . . . . . . . . . . . 15 substr Word
186 ccatcl 12558 . . . . . . . . . . . . . . 15 Word substr Word concat substr Word
187184, 185, 186syl2anc 661 . . . . . . . . . . . . . 14 concat substr Word
188 ccatcl 12558 . . . . . . . . . . . . . . . . 17 substr Word Word substr concat Word
189123, 172, 188syl2anc 661 . . . . . . . . . . . . . . . 16 substr concat Word
190189adantr 465 . . . . . . . . . . . . . . 15 substr concat Word
191173adantr 465 . . . . . . . . . . . . . . 15 Word
192 ccatcl 12558 . . . . . . . . . . . . . . 15 substr concat Word Word substr concat concat Word
193190, 191, 192syl2anc 661 . . . . . . . . . . . . . 14 substr concat concat Word
194129adantr 465 . . . . . . . . . . . . . 14 substr Word
195 ccatlen 12559 . . . . . . . . . . . . . . . . . . . 20 substr Word Word substr concat substr
196123, 172, 195syl2anc 661 . . . . . . . . . . . . . . . . . . 19 substr concat substr
197 s1len 12580 . . . . . . . . . . . . . . . . . . . . 21
198197a1i 11 . . . . . . . . . . . . . . . . . . . 20
199134, 198oveq12d 6302 . . . . . . . . . . . . . . . . . . 19 substr
200196, 199eqtrd 2508 . . . . . . . . . . . . . . . . . 18 substr concat
201132, 200eqeq12d 2489 . . . . . . . . . . . . . . . . 17 substr substr concat
202201biimpar 485 . . . . . . . . . . . . . . . 16 substr substr concat
203 s1len 12580 . . . . . . . . . . . . . . . . . 18
204 s1len 12580 . . . . . . . . . . . . . . . . . 18
205203, 204eqtr4i 2499 . . . . . . . . . . . . . . . . 17
206205a1i 11 . . . . . . . . . . . . . . . 16
207202, 206oveq12d 6302 . . . . . . . . . . . . . . 15 substr substr concat
208114adantr 465 . . . . . . . . . . . . . . . 16 substr Word
209160adantr 465 . . . . . . . . . . . . . . . 16 Word
210 ccatlen 12559 . . . . . . . . . . . . . . . 16 substr Word Word substr concat substr
211208, 209, 210syl2anc 661 . . . . . . . . . . . . . . 15 substr concat substr
212 ccatlen 12559 . . . . . . . . . . . . . . . 16 substr concat Word Word substr concat concat substr concat
213190, 191, 212syl2anc 661 . . . . . . . . . . . . . . 15 substr concat concat substr concat
214207, 211, 2133eqtr4d 2518 . . . . . . . . . . . . . 14 substr concat substr concat concat
215 ccatopth 12658 . . . . . . . . . . . . . 14 substr concat Word concat substr Word substr concat concat Word substr Word substr concat substr concat concat substr concat concat concat substr substr concat concat concat substr substr concat substr concat concat concat substr substr
216183, 187, 193, 194, 214, 215syl221anc 1239 . . . . . . . . . . . . 13 substr concat concat concat substr substr concat concat concat substr substr concat substr concat concat concat substr substr
217182, 216mpbid 210 . . . . . . . . . . . 12 substr concat substr concat concat concat substr substr
218217simpld 459 . . . . . . . . . . 11 substr concat substr concat concat
219 ccatopth 12658 . . . . . . . . . . . 12 substr Word Word substr concat Word Word substr substr concat substr concat substr concat concat substr substr concat
220208, 209, 190, 191, 202, 219syl221anc 1239 . . . . . . . . . . 11 substr concat substr concat concat substr substr concat
221218, 220mpbid 210 . . . . . . . . . 10 substr substr concat
222221simpld 459 . . . . . . . . 9 substr substr concat
223222oveq1d 6299 . . . . . . . 8 substr concat substr substr concat concat substr
224123adantr 465 . . . . . . . . 9 substr Word
225172adantr 465 . . . . . . . . 9 Word
226 ccatass 12570 . . . . . . . . 9 substr Word Word substr Word substr concat concat substr substr concat concat substr
227224, 225, 185, 226syl3anc 1228 . . . . . . . 8 substr concat concat substr substr concat concat substr
228221simprd 463 . . . . . . . . . . . . . . 15
229 s111 12586 . . . . . . . . . . . . . . . . 17
23091, 106, 229syl2anc 661 . . . . . . . . . . . . . . . 16
231230adantr 465 . . . . . . . . . . . . . . 15
232228, 231mpbid 210 . . . . . . . . . . . . . 14
233232fveq2d 5870 . . . . . . . . . . . . 13
2348efgmnvl 16538 . . . . . . . . . . . . . . 15
235102, 234syl 16 . . . . . . . . . . . . . 14
236235adantr 465 . . . . . . . . . . . . 13
237233, 236eqtrd 2508 . . . . . . . . . . . 12
238237s1eqd 12576 . . . . . . . . . . 11
239238oveq1d 6299 . . . . . . . . . 10 concat substr concat substr
240217simprd 463 . . . . . . . . . 10 concat substr substr
241239, 240eqtr3d 2510 . . . . . . . . 9 concat substr substr
242241oveq2d 6300 . . . . . . . 8 substr concat concat substr substr concat substr
243223, 227, 2423eqtrd 2512 . . . . . . 7 substr concat substr substr concat substr
24489, 243mtand 659 . . . . . 6
245244pm2.21d 106 . . . . 5
246 elfzelz 11688 . . . . . . . . . . . 12
24774, 246syl 16 . . . . . . . . . . 11
248247zcnd 10967 . . . . . . . . . 10
249 ax-1cn 9550 . . . . . . . . . . 11
250249a1i 11 . . . . . . . . . 10
251248, 250, 250addassd 9618 . . . . . . . . 9
252 df-2 10594 . . . . . . . . . 10
253252oveq2i 6295 . . . . . . . . 9
254251, 253syl6eqr 2526 . . . . . . . 8
255254fveq2d 5870 . . . . . . 7
256255eleq2d 2537 . . . . . 6
2573, 7, 8, 9, 10, 11efgsfo 16563 . . . . . . . . . 10
258 swrdcl 12609 . . . . . . . . . . . . 13 Word substr Word
25937, 258syl 16 . . . . . . . . . . . 12 substr Word
260 ccatcl 12558 . . . . . . . . . . . 12 substr Word substr Word substr concat substr Word
261123, 259, 260syl2anc 661 . . . . . . . . . . 11 substr concat substr Word
2623efgrcl 16539 . . . . . . . . . . . . 13 Word
26336, 262syl 16 . . . . . . . . . . . 12 Word
264263simprd 463 . . . . . . . . . . 11 Word
265261, 264eleqtrrd 2558 . . . . . . . . . 10 substr concat substr
266 foelrn 6040 . . . . . . . . . 10 substr concat substr substr concat substr
267257, 265, 266sylancr 663 . . . . . . . . 9 substr concat substr
268267adantr 465 . . . . . . . 8 substr concat substr
26920ad2antrr 725 . . . . . . . . 9 substr concat substr
2706ad2antrr 725 . . . . . . . . 9 substr concat substr
27121ad2antrr 725 . . . . . . . . 9 substr concat substr
27222ad2antrr 725 . . . . . . . . 9 substr concat substr
27323ad2antrr 725 . . . . . . . . 9 substr concat substr
27438ad2antrr 725 . . . . . . . . 9 substr concat substr
27574ad2antrr 725 . . . . . . . . 9 substr concat substr
27691ad2antrr 725 . . . . . . . . 9 substr concat substr
277102ad2antrr 725 . . . . . . . . 9 substr concat substr
27890ad2antrr 725 . . . . . . . . 9 substr concat substr
279101ad2antrr 725 . . . . . . . . 9 substr concat substr
2802ad2antrr 725 . . . . . . . . 9 substr concat substr
281 simplr 754 . . . . . . . . 9 substr concat substr
282 simprl 755 . . . . . . . . 9 substr concat substr
283 simprr 756 . . . . . . . . . 10 substr concat substr substr concat substr
284283eqcomd 2475 . . . . . . . . 9 substr concat substr substr concat substr
2853, 7, 8, 9, 10, 11, 269, 270, 271, 272, 273, 19, 60, 274, 275, 276, 277, 278, 279, 280, 281, 282, 284efgredlemd 16568 . . . . . . . 8 substr concat substr
286268, 285rexlimddv 2959 . . . . . . 7
287286ex 434 . . . . . 6
288256, 287sylbid 215 . . . . 5
289245, 288jaod 380 . . . 4
290159, 289syl5 32 . . 3
291158, 290jaod 380 . 2
2921, 291syl5 32 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 184   wo 368   wa 369   wceq 1379   wcel 1767  wral 2814  wrex 2815  crab 2818  cvv 3113   cdif 3473  c0 3785  csn 4027  cop 4033  cotp 4035  ciun 4325   class class class wbr 4447   cmpt 4505   cid 4790   cxp 4997   cdm 4999   crn 5000  wf 5584  wfo 5586  cfv 5588  (class class class)co 6284   cmpt2 6286  c1o 7123  c2o 7124  cc 9490  cc0 9492  c1 9493   caddc 9495   clt 9628   cmin 9805  cn 10536  c2 10585  cn0 10795  cz 10864  cuz 11082  cfz 11672  ..^cfzo 11792  chash 12373  Word cword 12500   concat cconcat 12502  cs1 12503   substr csubstr 12504   splice csplice 12505  cs2 12769   ~FG cefg 16530 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4558  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6576  ax-cnex 9548  ax-resscn 9549  ax-1cn 9550  ax-icn 9551  ax-addcl 9552  ax-addrcl 9553  ax-mulcl 9554  ax-mulrcl 9555  ax-mulcom 9556  ax-addass 9557  ax-mulass 9558  ax-distr 9559  ax-i2m1 9560  ax-1ne0 9561  ax-1rid 9562  ax-rnegex 9563  ax-rrecex 9564  ax-cnre 9565  ax-pre-lttri 9566  ax-pre-lttrn 9567  ax-pre-ltadd 9568  ax-pre-mulgt0 9569 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2819  df-rex 2820  df-reu 2821  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-ot 4036  df-uni 4246  df-int 4283  df-iun 4327  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5551  df-fun 5590  df-fn 5591  df-f 5592  df-f1 5593  df-fo 5594  df-f1o 5595  df-fv 5596  df-riota 6245  df-ov 6287  df-oprab 6288  df-mpt2 6289  df-om 6685  df-1st 6784  df-2nd 6785  df-recs 7042  df-rdg 7076  df-1o 7130  df-2o 7131  df-oadd 7134  df-er 7311  df-map 7422  df-pm 7423  df-en 7517  df-dom 7518  df-sdom 7519  df-fin 7520  df-card 8320  df-pnf 9630  df-mnf 9631  df-xr 9632  df-ltxr 9633  df-le 9634  df-sub 9807  df-neg 9808  df-nn 10537  df-2 10594  df-n0 10796  df-z 10865  df-uz 11083  df-rp 11221  df-fz 11673  df-fzo 11793  df-hash 12374  df-word 12508  df-concat 12510  df-s1 12511  df-substr 12512  df-splice 12513  df-s2 12776 This theorem is referenced by:  efgredlemb  16570
 Copyright terms: Public domain W3C validator