efgredlemc - Metamath Proof Explorer

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

Theorem efgredlemc 18158

Description: The reduced word that forms the base of the sequence in efgsval 18144 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.

Step	Hyp	Ref	Expression
1		uzp1 11721	. 2 $\/$
2		efgredlemb.8	. . . . . 6
3		efgval.w	. . . . . . . . . . 11 Word
4		fviss 6256	. . . . . . . . . . 11 Word Word
5	3, 4	eqsstri 3635	. . . . . . . . . 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 $\$ $/\$ ..^
12	3, 7, 8, 9, 10, 11	efgsdm 18143	. . . . . . . . . . . . . 14 Word $\$ $/\$ $/\$ ..^
13	12	simp1bi 1076	. . . . . . . . . . . . 13 Word $\$
14	6, 13	syl 17	. . . . . . . . . . . 12 Word $\$
15		eldifi 3732	. . . . . . . . . . . 12 Word $\$ Word
16		wrdf 13310	. . . . . . . . . . . 12 Word ..^
17	14, 15, 16	3syl 18	. . . . . . . . . . 11 ..^
18		fzossfz 12488	. . . . . . . . . . . . 13 ..^
19		efgredlemb.k	. . . . . . . . . . . . . 14
20		efgredlem.1	. . . . . . . . . . . . . . . . 17
21		efgredlem.3	. . . . . . . . . . . . . . . . 17
22		efgredlem.4	. . . . . . . . . . . . . . . . 17
23		efgredlem.5	. . . . . . . . . . . . . . . . 17
24	3, 7, 8, 9, 10, 11, 20, 6, 21, 22, 23	efgredlema 18153	. . . . . . . . . . . . . . . 16 $/\$
25	24	simpld 475	. . . . . . . . . . . . . . 15
26		fzo0end 12560	. . . . . . . . . . . . . . 15 ..^
27	25, 26	syl 17	. . . . . . . . . . . . . 14 ..^
28	19, 27	syl5eqel 2705	. . . . . . . . . . . . 13 ..^
29	18, 28	sseldi 3601	. . . . . . . . . . . 12
30		lencl 13324	. . . . . . . . . . . . . . 15 Word
31	14, 15, 30	3syl 18	. . . . . . . . . . . . . 14
32	31	nn0zd 11480	. . . . . . . . . . . . 13
33		fzoval 12471	. . . . . . . . . . . . 13 ..^
34	32, 33	syl 17	. . . . . . . . . . . 12 ..^
35	29, 34	eleqtrrd 2704	. . . . . . . . . . 11 ..^
36	17, 35	ffvelrnd 6360	. . . . . . . . . 10
37	5, 36	sseldi 3601	. . . . . . . . 9 Word
38		efgredlemb.p	. . . . . . . . . 10
39		elfzuz 12338	. . . . . . . . . 10
40		eluzfz1 12348	. . . . . . . . . 10
41	38, 39, 40	3syl 18	. . . . . . . . 9
42		lencl 13324	. . . . . . . . . . . 12 Word
43	37, 42	syl 17	. . . . . . . . . . 11
44		nn0uz 11722	. . . . . . . . . . 11
45	43, 44	syl6eleq 2711	. . . . . . . . . 10
46		eluzfz2 12349	. . . . . . . . . 10
47	45, 46	syl 17	. . . . . . . . 9
48		ccatswrd 13456	. . . . . . . . 9 Word $/\$ $/\$ $/\$ substr ++ substr substr
49	37, 41, 38, 47, 48	syl13anc 1328	. . . . . . . 8 substr ++ substr substr
50		swrdid 13428	. . . . . . . . 9 Word substr
51	37, 50	syl 17	. . . . . . . 8 substr
52	49, 51	eqtrd 2656	. . . . . . 7 substr ++ substr
53	3, 7, 8, 9, 10, 11	efgsdm 18143	. . . . . . . . . . . . . 14 Word $\$ $/\$ $/\$ ..^
54	53	simp1bi 1076	. . . . . . . . . . . . 13 Word $\$
55	21, 54	syl 17	. . . . . . . . . . . 12 Word $\$
56		eldifi 3732	. . . . . . . . . . . 12 Word $\$ Word
57		wrdf 13310	. . . . . . . . . . . 12 Word ..^
58	55, 56, 57	3syl 18	. . . . . . . . . . 11 ..^
59		fzossfz 12488	. . . . . . . . . . . . 13 ..^
60		efgredlemb.l	. . . . . . . . . . . . . 14
61	24	simprd 479	. . . . . . . . . . . . . . 15
62		fzo0end 12560	. . . . . . . . . . . . . . 15 ..^
63	61, 62	syl 17	. . . . . . . . . . . . . 14 ..^
64	60, 63	syl5eqel 2705	. . . . . . . . . . . . 13 ..^
65	59, 64	sseldi 3601	. . . . . . . . . . . 12
66		lencl 13324	. . . . . . . . . . . . . . 15 Word
67	55, 56, 66	3syl 18	. . . . . . . . . . . . . 14
68	67	nn0zd 11480	. . . . . . . . . . . . 13
69		fzoval 12471	. . . . . . . . . . . . 13 ..^
70	68, 69	syl 17	. . . . . . . . . . . 12 ..^
71	65, 70	eleqtrrd 2704	. . . . . . . . . . 11 ..^
72	58, 71	ffvelrnd 6360	. . . . . . . . . 10
73	5, 72	sseldi 3601	. . . . . . . . 9 Word
74		efgredlemb.q	. . . . . . . . . 10
75		elfzuz 12338	. . . . . . . . . 10
76		eluzfz1 12348	. . . . . . . . . 10
77	74, 75, 76	3syl 18	. . . . . . . . 9
78		lencl 13324	. . . . . . . . . . . 12 Word
79	73, 78	syl 17	. . . . . . . . . . 11
80	79, 44	syl6eleq 2711	. . . . . . . . . 10
81		eluzfz2 12349	. . . . . . . . . 10
82	80, 81	syl 17	. . . . . . . . 9
83		ccatswrd 13456	. . . . . . . . 9 Word $/\$ $/\$ $/\$ substr ++ substr substr
84	73, 77, 74, 82, 83	syl13anc 1328	. . . . . . . 8 substr ++ substr substr
85		swrdid 13428	. . . . . . . . 9 Word substr
86	73, 85	syl 17	. . . . . . . 8 substr
87	84, 86	eqtrd 2656	. . . . . . 7 substr ++ substr
88	52, 87	eqeq12d 2637	. . . . . 6 substr ++ substr substr ++ substr
89	2, 88	mtbird 315	. . . . 5 substr ++ substr substr ++ substr
90		efgredlemb.6	. . . . . . . . . . . . 13
91		efgredlemb.u	. . . . . . . . . . . . . 14
92	3, 7, 8, 9	efgtval 18136	. . . . . . . . . . . . . 14 $/\$ $/\$ splice
93	36, 38, 91, 92	syl3anc 1326	. . . . . . . . . . . . 13 splice
94	8	efgmf 18126	. . . . . . . . . . . . . . . . 17
95	94	ffvelrni 6358	. . . . . . . . . . . . . . . 16
96	91, 95	syl 17	. . . . . . . . . . . . . . 15
97	91, 96	s2cld 13616	. . . . . . . . . . . . . 14 Word
98		splval 13502	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ Word splice substr ++ ++ substr
99	36, 38, 38, 97, 98	syl13anc 1328	. . . . . . . . . . . . 13 splice substr ++ ++ substr
100	90, 93, 99	3eqtrd 2660	. . . . . . . . . . . 12 substr ++ ++ substr
101		efgredlemb.7	. . . . . . . . . . . . 13
102		efgredlemb.v	. . . . . . . . . . . . . 14
103	3, 7, 8, 9	efgtval 18136	. . . . . . . . . . . . . 14 $/\$ $/\$ splice
104	72, 74, 102, 103	syl3anc 1326	. . . . . . . . . . . . 13 splice
105	94	ffvelrni 6358	. . . . . . . . . . . . . . . 16
106	102, 105	syl 17	. . . . . . . . . . . . . . 15
107	102, 106	s2cld 13616	. . . . . . . . . . . . . 14 Word
108		splval 13502	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ Word splice substr ++ ++ substr
109	72, 74, 74, 107, 108	syl13anc 1328	. . . . . . . . . . . . 13 splice substr ++ ++ substr
110	101, 104, 109	3eqtrd 2660	. . . . . . . . . . . 12 substr ++ ++ substr
111	22, 100, 110	3eqtr3d 2664	. . . . . . . . . . 11 substr ++ ++ substr substr ++ ++ substr
112	111	adantr 481	. . . . . . . . . 10 $/\$ substr ++ ++ substr substr ++ ++ substr
113		swrdcl 13419	. . . . . . . . . . . . . 14 Word substr Word
114	37, 113	syl 17	. . . . . . . . . . . . 13 substr Word
115	114	adantr 481	. . . . . . . . . . . 12 $/\$ substr Word
116	97	adantr 481	. . . . . . . . . . . 12 $/\$ Word
117		ccatcl 13359	. . . . . . . . . . . 12 substr Word $/\$ Word substr ++ Word
118	115, 116, 117	syl2anc 693	. . . . . . . . . . 11 $/\$ substr ++ Word
119		swrdcl 13419	. . . . . . . . . . . . 13 Word substr Word
120	37, 119	syl 17	. . . . . . . . . . . 12 substr Word
121	120	adantr 481	. . . . . . . . . . 11 $/\$ substr Word
122		swrdcl 13419	. . . . . . . . . . . . . 14 Word substr Word
123	73, 122	syl 17	. . . . . . . . . . . . 13 substr Word
124	123	adantr 481	. . . . . . . . . . . 12 $/\$ substr Word
125	107	adantr 481	. . . . . . . . . . . 12 $/\$ Word
126		ccatcl 13359	. . . . . . . . . . . 12 substr Word $/\$ Word substr ++ Word
127	124, 125, 126	syl2anc 693	. . . . . . . . . . 11 $/\$ substr ++ Word
128		swrdcl 13419	. . . . . . . . . . . . 13 Word substr Word
129	73, 128	syl 17	. . . . . . . . . . . 12 substr Word
130	129	adantr 481	. . . . . . . . . . 11 $/\$ substr Word
131		swrd0len 13422	. . . . . . . . . . . . . . . 16 Word $/\$ substr
132	37, 38, 131	syl2anc 693	. . . . . . . . . . . . . . 15 substr
133		swrd0len 13422	. . . . . . . . . . . . . . . 16 Word $/\$ substr
134	73, 74, 133	syl2anc 693	. . . . . . . . . . . . . . 15 substr
135	132, 134	eqeq12d 2637	. . . . . . . . . . . . . 14 substr substr
136	135	biimpar 502	. . . . . . . . . . . . 13 $/\$ substr substr
137		s2len 13634	. . . . . . . . . . . . . . 15
138		s2len 13634	. . . . . . . . . . . . . . 15
139	137, 138	eqtr4i 2647	. . . . . . . . . . . . . 14
140	139	a1i 11	. . . . . . . . . . . . 13 $/\$
141	136, 140	oveq12d 6668	. . . . . . . . . . . 12 $/\$ substr substr
142		ccatlen 13360	. . . . . . . . . . . . 13 substr Word $/\$ Word substr ++ substr
143	115, 116, 142	syl2anc 693	. . . . . . . . . . . 12 $/\$ substr ++ substr
144		ccatlen 13360	. . . . . . . . . . . . 13 substr Word $/\$ Word substr ++ substr
145	124, 125, 144	syl2anc 693	. . . . . . . . . . . 12 $/\$ substr ++ substr
146	141, 143, 145	3eqtr4d 2666	. . . . . . . . . . 11 $/\$ substr ++ substr ++
147		ccatopth 13470	. . . . . . . . . . 11 substr ++ Word $/\$ substr Word $/\$ substr ++ Word $/\$ substr Word $/\$ substr ++ substr ++ substr ++ ++ substr substr ++ ++ substr substr ++ substr ++ $/\$ substr substr
148	118, 121, 127, 130, 146, 147	syl221anc 1337	. . . . . . . . . 10 $/\$ substr ++ ++ substr substr ++ ++ substr substr ++ substr ++ $/\$ substr substr
149	112, 148	mpbid 222	. . . . . . . . 9 $/\$ substr ++ substr ++ $/\$ substr substr
150	149	simpld 475	. . . . . . . 8 $/\$ substr ++ substr ++
151		ccatopth 13470	. . . . . . . . 9 substr Word $/\$ Word $/\$ substr Word $/\$ Word $/\$ substr substr substr ++ substr ++ substr substr $/\$
152	115, 116, 124, 125, 136, 151	syl221anc 1337	. . . . . . . 8 $/\$ substr ++ substr ++ substr substr $/\$
153	150, 152	mpbid 222	. . . . . . 7 $/\$ substr substr $/\$
154	153	simpld 475	. . . . . 6 $/\$ substr substr
155	149	simprd 479	. . . . . 6 $/\$ substr substr
156	154, 155	oveq12d 6668	. . . . 5 $/\$ substr ++ substr substr ++ substr
157	89, 156	mtand 691	. . . 4
158	157	pm2.21d 118	. . 3
159		uzp1 11721	. . . 4 $\/$
160	91	s1cld 13383	. . . . . . . . . . . . . . . . 17 Word
161		ccatcl 13359	. . . . . . . . . . . . . . . . 17 substr Word $/\$ Word substr ++ Word
162	114, 160, 161	syl2anc 693	. . . . . . . . . . . . . . . 16 substr ++ Word
163	96	s1cld 13383	. . . . . . . . . . . . . . . 16 Word
164		ccatass 13371	. . . . . . . . . . . . . . . 16 substr ++ Word $/\$ Word $/\$ substr Word substr ++ ++ ++ substr substr ++ ++ ++ substr
165	162, 163, 120, 164	syl3anc 1326	. . . . . . . . . . . . . . 15 substr ++ ++ ++ substr substr ++ ++ ++ substr
166		ccatass 13371	. . . . . . . . . . . . . . . . . . 19 substr Word $/\$ Word $/\$ Word substr ++ ++ substr ++ ++
167	114, 160, 163, 166	syl3anc 1326	. . . . . . . . . . . . . . . . . 18 substr ++ ++ substr ++ ++
168		df-s2 13593	. . . . . . . . . . . . . . . . . . 19 ++
169	168	oveq2i 6661	. . . . . . . . . . . . . . . . . 18 substr ++ substr ++ ++
170	167, 169	syl6eqr 2674	. . . . . . . . . . . . . . . . 17 substr ++ ++ substr ++
171	170	oveq1d 6665	. . . . . . . . . . . . . . . 16 substr ++ ++ ++ substr substr ++ ++ substr
172	102	s1cld 13383	. . . . . . . . . . . . . . . . . . 19 Word
173	106	s1cld 13383	. . . . . . . . . . . . . . . . . . 19 Word
174		ccatass 13371	. . . . . . . . . . . . . . . . . . 19 substr Word $/\$ Word $/\$ Word substr ++ ++ substr ++ ++
175	123, 172, 173, 174	syl3anc 1326	. . . . . . . . . . . . . . . . . 18 substr ++ ++ substr ++ ++
176		df-s2 13593	. . . . . . . . . . . . . . . . . . 19 ++
177	176	oveq2i 6661	. . . . . . . . . . . . . . . . . 18 substr ++ substr ++ ++
178	175, 177	syl6eqr 2674	. . . . . . . . . . . . . . . . 17 substr ++ ++ substr ++
179	178	oveq1d 6665	. . . . . . . . . . . . . . . 16 substr ++ ++ ++ substr substr ++ ++ substr
180	111, 171, 179	3eqtr4d 2666	. . . . . . . . . . . . . . 15 substr ++ ++ ++ substr substr ++ ++ ++ substr
181	165, 180	eqtr3d 2658	. . . . . . . . . . . . . 14 substr ++ ++ ++ substr substr ++ ++ ++ substr
182	181	adantr 481	. . . . . . . . . . . . 13 $/\$ substr ++ ++ ++ substr substr ++ ++ ++ substr
183	162	adantr 481	. . . . . . . . . . . . . 14 $/\$ substr ++ Word
184	163	adantr 481	. . . . . . . . . . . . . . 15 $/\$ Word
185	120	adantr 481	. . . . . . . . . . . . . . 15 $/\$ substr Word
186		ccatcl 13359	. . . . . . . . . . . . . . 15 Word $/\$ substr Word ++ substr Word
187	184, 185, 186	syl2anc 693	. . . . . . . . . . . . . 14 $/\$ ++ substr Word
188		ccatcl 13359	. . . . . . . . . . . . . . . . 17 substr Word $/\$ Word substr ++ Word
189	123, 172, 188	syl2anc 693	. . . . . . . . . . . . . . . 16 substr ++ Word
190	189	adantr 481	. . . . . . . . . . . . . . 15 $/\$ substr ++ Word
191	173	adantr 481	. . . . . . . . . . . . . . 15 $/\$ Word
192		ccatcl 13359	. . . . . . . . . . . . . . 15 substr ++ Word $/\$ Word substr ++ ++ Word
193	190, 191, 192	syl2anc 693	. . . . . . . . . . . . . 14 $/\$ substr ++ ++ Word
194	129	adantr 481	. . . . . . . . . . . . . 14 $/\$ substr Word
195		ccatlen 13360	. . . . . . . . . . . . . . . . . . . 20 substr Word $/\$ Word substr ++ substr
196	123, 172, 195	syl2anc 693	. . . . . . . . . . . . . . . . . . 19 substr ++ substr
197		s1len 13385	. . . . . . . . . . . . . . . . . . . . 21
198	197	a1i 11	. . . . . . . . . . . . . . . . . . . 20
199	134, 198	oveq12d 6668	. . . . . . . . . . . . . . . . . . 19 substr
200	196, 199	eqtrd 2656	. . . . . . . . . . . . . . . . . 18 substr ++
201	132, 200	eqeq12d 2637	. . . . . . . . . . . . . . . . 17 substr substr ++
202	201	biimpar 502	. . . . . . . . . . . . . . . 16 $/\$ substr substr ++
203		s1len 13385	. . . . . . . . . . . . . . . . . 18
204		s1len 13385	. . . . . . . . . . . . . . . . . 18
205	203, 204	eqtr4i 2647	. . . . . . . . . . . . . . . . 17
206	205	a1i 11	. . . . . . . . . . . . . . . 16 $/\$
207	202, 206	oveq12d 6668	. . . . . . . . . . . . . . 15 $/\$ substr substr ++
208	114	adantr 481	. . . . . . . . . . . . . . . 16 $/\$ substr Word
209	160	adantr 481	. . . . . . . . . . . . . . . 16 $/\$ Word
210		ccatlen 13360	. . . . . . . . . . . . . . . 16 substr Word $/\$ Word substr ++ substr
211	208, 209, 210	syl2anc 693	. . . . . . . . . . . . . . 15 $/\$ substr ++ substr
212		ccatlen 13360	. . . . . . . . . . . . . . . 16 substr ++ Word $/\$ Word substr ++ ++ substr ++
213	190, 191, 212	syl2anc 693	. . . . . . . . . . . . . . 15 $/\$ substr ++ ++ substr ++
214	207, 211, 213	3eqtr4d 2666	. . . . . . . . . . . . . 14 $/\$ substr ++ substr ++ ++
215		ccatopth 13470	. . . . . . . . . . . . . 14 substr ++ Word $/\$ ++ substr Word $/\$ substr ++ ++ Word $/\$ substr Word $/\$ substr ++ substr ++ ++ substr ++ ++ ++ substr substr ++ ++ ++ substr substr ++ substr ++ ++ $/\$ ++ substr substr
216	183, 187, 193, 194, 214, 215	syl221anc 1337	. . . . . . . . . . . . 13 $/\$ substr ++ ++ ++ substr substr ++ ++ ++ substr substr ++ substr ++ ++ $/\$ ++ substr substr
217	182, 216	mpbid 222	. . . . . . . . . . . 12 $/\$ substr ++ substr ++ ++ $/\$ ++ substr substr
218	217	simpld 475	. . . . . . . . . . 11 $/\$ substr ++ substr ++ ++
219		ccatopth 13470	. . . . . . . . . . . 12 substr Word $/\$ Word $/\$ substr ++ Word $/\$ Word $/\$ substr substr ++ substr ++ substr ++ ++ substr substr ++ $/\$
220	208, 209, 190, 191, 202, 219	syl221anc 1337	. . . . . . . . . . 11 $/\$ substr ++ substr ++ ++ substr substr ++ $/\$
221	218, 220	mpbid 222	. . . . . . . . . 10 $/\$ substr substr ++ $/\$
222	221	simpld 475	. . . . . . . . 9 $/\$ substr substr ++
223	222	oveq1d 6665	. . . . . . . 8 $/\$ substr ++ substr substr ++ ++ substr
224	123	adantr 481	. . . . . . . . 9 $/\$ substr Word
225	172	adantr 481	. . . . . . . . 9 $/\$ Word
226		ccatass 13371	. . . . . . . . 9 substr Word $/\$ Word $/\$ substr Word substr ++ ++ substr substr ++ ++ substr
227	224, 225, 185, 226	syl3anc 1326	. . . . . . . 8 $/\$ substr ++ ++ substr substr ++ ++ substr
228	221	simprd 479	. . . . . . . . . . . . . . 15 $/\$
229		s111 13395	. . . . . . . . . . . . . . . . 17 $/\$
230	91, 106, 229	syl2anc 693	. . . . . . . . . . . . . . . 16
231	230	adantr 481	. . . . . . . . . . . . . . 15 $/\$
232	228, 231	mpbid 222	. . . . . . . . . . . . . 14 $/\$
233	232	fveq2d 6195	. . . . . . . . . . . . 13 $/\$
234	8	efgmnvl 18127	. . . . . . . . . . . . . . 15
235	102, 234	syl 17	. . . . . . . . . . . . . 14
236	235	adantr 481	. . . . . . . . . . . . 13 $/\$
237	233, 236	eqtrd 2656	. . . . . . . . . . . 12 $/\$
238	237	s1eqd 13381	. . . . . . . . . . 11 $/\$
239	238	oveq1d 6665	. . . . . . . . . 10 $/\$ ++ substr ++ substr
240	217	simprd 479	. . . . . . . . . 10 $/\$ ++ substr substr
241	239, 240	eqtr3d 2658	. . . . . . . . 9 $/\$ ++ substr substr
242	241	oveq2d 6666	. . . . . . . 8 $/\$ substr ++ ++ substr substr ++ substr
243	223, 227, 242	3eqtrd 2660	. . . . . . 7 $/\$ substr ++ substr substr ++ substr
244	89, 243	mtand 691	. . . . . 6
245	244	pm2.21d 118	. . . . 5
246		elfzelz 12342	. . . . . . . . . . . 12
247	74, 246	syl 17	. . . . . . . . . . 11
248	247	zcnd 11483	. . . . . . . . . 10
249		1cnd 10056	. . . . . . . . . 10
250	248, 249, 249	addassd 10062	. . . . . . . . 9
251		df-2 11079	. . . . . . . . . 10
252	251	oveq2i 6661	. . . . . . . . 9
253	250, 252	syl6eqr 2674	. . . . . . . 8
254	253	fveq2d 6195	. . . . . . 7
255	254	eleq2d 2687	. . . . . 6
256	3, 7, 8, 9, 10, 11	efgsfo 18152	. . . . . . . . . 10
257		swrdcl 13419	. . . . . . . . . . . . 13 Word substr Word
258	37, 257	syl 17	. . . . . . . . . . . 12 substr Word
259		ccatcl 13359	. . . . . . . . . . . 12 substr Word $/\$ substr Word substr ++ substr Word
260	123, 258, 259	syl2anc 693	. . . . . . . . . . 11 substr ++ substr Word
261	3	efgrcl 18128	. . . . . . . . . . . . 13 $/\$ Word
262	36, 261	syl 17	. . . . . . . . . . . 12 $/\$ Word
263	262	simprd 479	. . . . . . . . . . 11 Word
264	260, 263	eleqtrrd 2704	. . . . . . . . . 10 substr ++ substr
265		foelrn 6378	. . . . . . . . . 10 $/\$ substr ++ substr substr ++ substr
266	256, 264, 265	sylancr 695	. . . . . . . . 9 substr ++ substr
267	266	adantr 481	. . . . . . . 8 $/\$ substr ++ substr
268	20	ad2antrr 762	. . . . . . . . 9 $/\$ $/\$ $/\$ substr ++ substr
269	6	ad2antrr 762	. . . . . . . . 9 $/\$ $/\$ $/\$ substr ++ substr
270	21	ad2antrr 762	. . . . . . . . 9 $/\$ $/\$ $/\$ substr ++ substr
271	22	ad2antrr 762	. . . . . . . . 9 $/\$ $/\$ $/\$ substr ++ substr
272	23	ad2antrr 762	. . . . . . . . 9 $/\$ $/\$ $/\$ substr ++ substr
273	38	ad2antrr 762	. . . . . . . . 9 $/\$ $/\$ $/\$ substr ++ substr
274	74	ad2antrr 762	. . . . . . . . 9 $/\$ $/\$ $/\$ substr ++ substr
275	91	ad2antrr 762	. . . . . . . . 9 $/\$ $/\$ $/\$ substr ++ substr
276	102	ad2antrr 762	. . . . . . . . 9 $/\$ $/\$ $/\$ substr ++ substr
277	90	ad2antrr 762	. . . . . . . . 9 $/\$ $/\$ $/\$ substr ++ substr
278	101	ad2antrr 762	. . . . . . . . 9 $/\$ $/\$ $/\$ substr ++ substr
279	2	ad2antrr 762	. . . . . . . . 9 $/\$ $/\$ $/\$ substr ++ substr
280		simplr 792	. . . . . . . . 9 $/\$ $/\$ $/\$ substr ++ substr
281		simprl 794	. . . . . . . . 9 $/\$ $/\$ $/\$ substr ++ substr
282		simprr 796	. . . . . . . . . 10 $/\$ $/\$ $/\$ substr ++ substr substr ++ substr
283	282	eqcomd 2628	. . . . . . . . 9 $/\$ $/\$ $/\$ substr ++ substr substr ++ substr
284	3, 7, 8, 9, 10, 11, 268, 269, 270, 271, 272, 19, 60, 273, 274, 275, 276, 277, 278, 279, 280, 281, 283	efgredlemd 18157	. . . . . . . 8 $/\$ $/\$ $/\$ substr ++ substr
285	267, 284	rexlimddv 3035	. . . . . . 7 $/\$
286	285	ex 450	. . . . . 6
287	255, 286	sylbid 230	. . . . 5
288	245, 287	jaod 395	. . . 4 $\/$
289	159, 288	syl5 34	. . 3
290	158, 289	jaod 395	. 2 $\/$
291	1, 290	syl5 34	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 196 $\/$ wo 383 $/\$ wa 384

wceq 1483

wcel 1990

wral 2912

wrex 2913

crab 2916

cvv 3200 $\$ cdif 3571

c0 3915

csn 4177

cop 4183

cotp 4185

ciun 4520 class class class wbr 4653

cmpt 4729

cid 5023

cxp 5112

cdm 5114

crn 5115

wf 5884

wfo 5886

cfv 5888 (class class class)co 6650

cmpt2 6652

c1o 7553

c2o 7554

cc0 9936

c1 9937

caddc 9939

clt 10074

cmin 10266

cn 11020

c2 11070

cn0 11292

cz 11377

cuz 11687

cfz 12326 ..^cfzo 12465

chash 13117 Word cword 13291 ++ cconcat 13293

cs1 13294 substr csubstr 13295 splice csplice 13296

cs2 13586 ~_FG cefg 18119

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-ot 4186 df-uni 4437 df-int 4476 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-2o 7561 df-oadd 7564 df-er 7742 df-map 7859 df-pm 7860 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-card 8765 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-nn 11021 df-2 11079 df-n0 11293 df-z 11378 df-uz 11688 df-rp 11833 df-fz 12327 df-fzo 12466 df-hash 13118 df-word 13299 df-concat 13301 df-s1 13302 df-substr 13303 df-splice 13304 df-s2 13593

This theorem is referenced by: efgredlemb 18159

W3C validator