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

Theorem repswswrd 12941
 Description: A subword of a "repeated symbol word" is again a "repeated symbol word". The assumption N <_ L is required, because otherwise ( L < N ): repeatS substr , but for M < N repeatS ! The proof is relatively long because the border cases ( , ..^ ..^ must have been considered. (Contributed by AV, 6-Nov-2018.)
Assertion
Ref Expression
repswswrd repeatS substr repeatS

Proof of Theorem repswswrd
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 repsw 12932 . . . . . 6 repeatS Word
2 nn0z 10984 . . . . . . 7
3 nn0z 10984 . . . . . . 7
42, 3anim12i 576 . . . . . 6
51, 4anim12i 576 . . . . 5 repeatS Word
6 3anass 1011 . . . . 5 repeatS Word repeatS Word
75, 6sylibr 217 . . . 4 repeatS Word
873adant3 1050 . . 3 repeatS Word
9 swrdval 12827 . . 3 repeatS Word repeatS substr ..^ repeatS ..^ repeatS
108, 9syl 17 . 2 repeatS substr ..^ repeatS ..^ repeatS
11 repsf 12930 . . . . . 6 repeatS ..^
12113ad2ant1 1051 . . . . 5 repeatS ..^
13 fdm 5745 . . . . 5 repeatS ..^ repeatS ..^
1412, 13syl 17 . . . 4 repeatS ..^
1514sseq2d 3446 . . 3 ..^ repeatS ..^ ..^
1615ifbid 3894 . 2 ..^ repeatS ..^ repeatS ..^ ..^ ..^ repeatS
17 fzon 11966 . . . . . . . . . . 11 ..^
184, 17syl 17 . . . . . . . . . 10 ..^
1918adantl 473 . . . . . . . . 9 ..^
2019biimpac 494 . . . . . . . 8 ..^
21 0ss 3766 . . . . . . . 8 ..^
2220, 21syl6eqss 3468 . . . . . . 7 ..^ ..^
23 iftrue 3878 . . . . . . 7 ..^ ..^ ..^ ..^ ..^ repeatS ..^ repeatS
2422, 23syl 17 . . . . . 6 ..^ ..^ ..^ repeatS ..^ repeatS
25 nn0re 10902 . . . . . . . . . . . 12
26 nn0re 10902 . . . . . . . . . . . 12
2725, 26anim12ci 577 . . . . . . . . . . 11
2827adantl 473 . . . . . . . . . 10
29 suble0 10149 . . . . . . . . . 10
3028, 29syl 17 . . . . . . . . 9
3130biimparc 495 . . . . . . . 8
32 0z 10972 . . . . . . . . 9
33 zsubcl 11003 . . . . . . . . . . . 12
343, 2, 33syl2anr 486 . . . . . . . . . . 11
3534adantl 473 . . . . . . . . . 10
3635adantl 473 . . . . . . . . 9
37 fzon 11966 . . . . . . . . 9 ..^
3832, 36, 37sylancr 676 . . . . . . . 8 ..^
3931, 38mpbid 215 . . . . . . 7 ..^
4039mpteq1d 4477 . . . . . 6 ..^ repeatS repeatS
41 oveq2 6316 . . . . . . . . . . . . 13
4241oveq2d 6324 . . . . . . . . . . . 12 repeatS repeatS
43 nn0cn 10903 . . . . . . . . . . . . . . . . 17
4443adantl 473 . . . . . . . . . . . . . . . 16
4544subidd 9993 . . . . . . . . . . . . . . 15
4645adantl 473 . . . . . . . . . . . . . 14
4746oveq2d 6324 . . . . . . . . . . . . 13 repeatS repeatS
48 repsw0 12934 . . . . . . . . . . . . . 14 repeatS
4948ad2antrr 740 . . . . . . . . . . . . 13 repeatS
5047, 49eqtrd 2505 . . . . . . . . . . . 12 repeatS
5142, 50sylan9eqr 2527 . . . . . . . . . . 11 repeatS
5251ex 441 . . . . . . . . . 10 repeatS
5352adantl 473 . . . . . . . . 9 repeatS
5453com12 31 . . . . . . . 8 repeatS
55 elnn0z 10974 . . . . . . . . . . . . . . 15
56 subge0 10148 . . . . . . . . . . . . . . . . . . . . . 22
5726, 25, 56syl2anr 486 . . . . . . . . . . . . . . . . . . . . 21
5825, 26anim12i 576 . . . . . . . . . . . . . . . . . . . . . . . 24
59 letri3 9737 . . . . . . . . . . . . . . . . . . . . . . . 24
6058, 59syl 17 . . . . . . . . . . . . . . . . . . . . . . 23
6160biimprd 231 . . . . . . . . . . . . . . . . . . . . . 22
6261expd 443 . . . . . . . . . . . . . . . . . . . . 21
6357, 62sylbid 223 . . . . . . . . . . . . . . . . . . . 20
6463com23 80 . . . . . . . . . . . . . . . . . . 19
6564adantl 473 . . . . . . . . . . . . . . . . . 18
6665impcom 437 . . . . . . . . . . . . . . . . 17
6766com12 31 . . . . . . . . . . . . . . . 16
6867adantl 473 . . . . . . . . . . . . . . 15
6955, 68sylbi 200 . . . . . . . . . . . . . 14
7069com12 31 . . . . . . . . . . . . 13
7170con3d 140 . . . . . . . . . . . 12
7271impcom 437 . . . . . . . . . . 11
73 df-nel 2644 . . . . . . . . . . 11
7472, 73sylibr 217 . . . . . . . . . 10
75 repsundef 12928 . . . . . . . . . 10 repeatS
7674, 75syl 17 . . . . . . . . 9 repeatS
7776ex 441 . . . . . . . 8 repeatS
7854, 77pm2.61i 169 . . . . . . 7 repeatS
79 mpt0 5715 . . . . . . 7 repeatS
8078, 79syl6reqr 2524 . . . . . 6 repeatS repeatS
8124, 40, 803eqtrd 2509 . . . . 5 ..^ ..^ ..^ repeatS repeatS
8281expcom 442 . . . 4 ..^ ..^ ..^ repeatS repeatS
83823adant3 1050 . . 3 ..^ ..^ ..^ repeatS repeatS
84 ltnle 9731 . . . . . . 7
8558, 84syl 17 . . . . . 6
8685bicomd 206 . . . . 5
87863ad2ant2 1052 . . . 4
8823adantr 472 . . . . . . 7 ..^ ..^ ..^ ..^ ..^ repeatS ..^ repeatS
8943ad2ant2 1052 . . . . . . . . . . 11
9089adantr 472 . . . . . . . . . 10
91 0zd 10973 . . . . . . . . . . . . 13
92 nn0z 10984 . . . . . . . . . . . . 13
9391, 92anim12i 576 . . . . . . . . . . . 12
94933ad2ant1 1051 . . . . . . . . . . 11
9594adantr 472 . . . . . . . . . 10
96 simpr 468 . . . . . . . . . 10
97 ssfzo12bi 12035 . . . . . . . . . 10 ..^ ..^
9890, 95, 96, 97syl3anc 1292 . . . . . . . . 9 ..^ ..^
99 simpl1l 1081 . . . . . . . . . . . . . 14
10099ad2antrr 740 . . . . . . . . . . . . 13 ..^
101 simpl1r 1082 . . . . . . . . . . . . . 14
102101ad2antrr 740 . . . . . . . . . . . . 13 ..^
103 elfzonn0 11988 . . . . . . . . . . . . . . . 16 ..^
104 nn0addcl 10929 . . . . . . . . . . . . . . . . . . . 20
105104expcom 442 . . . . . . . . . . . . . . . . . . 19
106105adantr 472 . . . . . . . . . . . . . . . . . 18
1071063ad2ant2 1052 . . . . . . . . . . . . . . . . 17
108107ad2antrr 740 . . . . . . . . . . . . . . . 16
109103, 108syl5com 30 . . . . . . . . . . . . . . 15 ..^
110109impcom 437 . . . . . . . . . . . . . 14 ..^
11192adantl 473 . . . . . . . . . . . . . . . . . 18
1121113ad2ant1 1051 . . . . . . . . . . . . . . . . 17
113112adantr 472 . . . . . . . . . . . . . . . 16
114 nn0re 10902 . . . . . . . . . . . . . . . . . . . . . . . 24
115114adantl 473 . . . . . . . . . . . . . . . . . . . . . . 23
116115, 58anim12ci 577 . . . . . . . . . . . . . . . . . . . . . 22
117 df-3an 1009 . . . . . . . . . . . . . . . . . . . . . 22
118116, 117sylibr 217 . . . . . . . . . . . . . . . . . . . . 21
119 ltletr 9743 . . . . . . . . . . . . . . . . . . . . 21
120118, 119syl 17 . . . . . . . . . . . . . . . . . . . 20
121 elnn0z 10974 . . . . . . . . . . . . . . . . . . . . . . 23
122 0red 9662 . . . . . . . . . . . . . . . . . . . . . . . . . 26
123 zre 10965 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
124123adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . 26
125115adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . 26
126 lelttr 9742 . . . . . . . . . . . . . . . . . . . . . . . . . 26
127122, 124, 125, 126syl3anc 1292 . . . . . . . . . . . . . . . . . . . . . . . . 25
128127expd 443 . . . . . . . . . . . . . . . . . . . . . . . 24
129128impancom 447 . . . . . . . . . . . . . . . . . . . . . . 23
130121, 129sylbi 200 . . . . . . . . . . . . . . . . . . . . . 22
131130adantr 472 . . . . . . . . . . . . . . . . . . . . 21
132131impcom 437 . . . . . . . . . . . . . . . . . . . 20
133120, 132syld 44 . . . . . . . . . . . . . . . . . . 19
134133expcomd 445 . . . . . . . . . . . . . . . . . 18
1351343impia 1228 . . . . . . . . . . . . . . . . 17
136135imp 436 . . . . . . . . . . . . . . . 16
137 elnnz 10971 . . . . . . . . . . . . . . . 16
138113, 136, 137sylanbrc 677 . . . . . . . . . . . . . . 15
139138ad2antrr 740 . . . . . . . . . . . . . 14 ..^
140 elfzo0 11984 . . . . . . . . . . . . . . . 16 ..^
141 nn0readdcl 10955 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
142141expcom 442 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
143142ad2antrl 742 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
144143impcom 437 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
14526adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
146145adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
147146adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
148114ad2antrl 742 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
149144, 147, 1483jca 1210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
150149ex 441 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
151150adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
152151impcom 437 . . . . . . . . . . . . . . . . . . . . . . . . . 26
153152adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . 25
154 nn0re 10902 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
155154adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
15625ad2antrl 742 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
157156adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
158155, 157, 147ltaddsubd 10234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
159 idd 24 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
160159ex 441 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
161160com23 80 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
162158, 161sylbird 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
163162impancom 447 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
164163impcom 437 . . . . . . . . . . . . . . . . . . . . . . . . . 26
165164impac 633 . . . . . . . . . . . . . . . . . . . . . . . . 25
166 ltletr 9743 . . . . . . . . . . . . . . . . . . . . . . . . 25
167153, 165, 166sylc 61 . . . . . . . . . . . . . . . . . . . . . . . 24
168167exp31 615 . . . . . . . . . . . . . . . . . . . . . . 23
169168com23 80 . . . . . . . . . . . . . . . . . . . . . 22
170169ex 441 . . . . . . . . . . . . . . . . . . . . 21
171170adantl 473 . . . . . . . . . . . . . . . . . . . 20
1721713imp 1224 . . . . . . . . . . . . . . . . . . 19
173172ad2antrr 740 . . . . . . . . . . . . . . . . . 18
174173com12 31 . . . . . . . . . . . . . . . . 17
1751743adant2 1049 . . . . . . . . . . . . . . . 16
176140, 175sylbi 200 . . . . . . . . . . . . . . 15 ..^
177176impcom 437 . . . . . . . . . . . . . 14 ..^
178 elfzo0 11984 . . . . . . . . . . . . . 14 ..^
179110, 139, 177, 178syl3anbrc 1214 . . . . . . . . . . . . 13 ..^ ..^
180 repswsymb 12931 . . . . . . . . . . . . 13 ..^ repeatS
181100, 102, 179, 180syl3anc 1292 . . . . . . . . . . . 12 ..^ repeatS
182181mpteq2dva 4482 . . . . . . . . . . 11 ..^ repeatS ..^
183343ad2ant2 1052 . . . . . . . . . . . . . . . 16
184183adantr 472 . . . . . . . . . . . . . . 15
185583ad2ant2 1052 . . . . . . . . . . . . . . . . . 18
186 ltle 9740 . . . . . . . . . . . . . . . . . 18
187185, 186syl 17 . . . . . . . . . . . . . . . . 17
188273ad2ant2 1052 . . . . . . . . . . . . . . . . . 18
189188, 56syl 17 . . . . . . . . . . . . . . . . 17
190187, 189sylibrd 242 . . . . . . . . . . . . . . . 16
191190imp 436 . . . . . . . . . . . . . . 15
192184, 191, 55sylanbrc 677 . . . . . . . . . . . . . 14
19399, 192jca 541 . . . . . . . . . . . . 13
194193adantr 472 . . . . . . . . . . . 12
195 reps 12927 . . . . . . . . . . . . 13 repeatS ..^
196195eqcomd 2477 . . . . . . . . . . . 12 ..^ repeatS
197194, 196syl 17 . . . . . . . . . . 11 ..^ repeatS
198182, 197eqtrd 2505 . . . . . . . . . 10 ..^ repeatS repeatS
199198ex 441 . . . . . . . . 9 ..^ repeatS repeatS
20098, 199sylbid 223 . . . . . . . 8 ..^ ..^ ..^ repeatS repeatS
201200impcom 437 . . . . . . 7 ..^ ..^ ..^ repeatS repeatS
20288, 201eqtrd 2505 . . . . . 6 ..^ ..^ ..^ ..^ ..^ repeatS repeatS
203 iffalse 3881 . . . . . . . 8 ..^ ..^ ..^ ..^ ..^ repeatS
204203adantr 472 . . . . . . 7 ..^ ..^ ..^ ..^ ..^ repeatS
20598notbid 301 . . . . . . . . 9 ..^ ..^
206 ianor 496 . . . . . . . . . . 11
207 nn0ge0 10919 . . . . . . . . . . . . . . . . 17
208 pm2.24 112 . . . . . . . . . . . . . . . . 17 repeatS
209207, 208syl 17 . . . . . . . . . . . . . . . 16 repeatS
210209adantr 472 . . . . . . . . . . . . . . 15 repeatS
2112103ad2ant2 1052 . . . . . . . . . . . . . 14 repeatS
212211adantr 472 . . . . . . . . . . . . 13 repeatS
213212com12 31 . . . . . . . . . . . 12 repeatS
214 pm2.24 112 . . . . . . . . . . . . . . 15 repeatS
2152143ad2ant3 1053 . . . . . . . . . . . . . 14 repeatS
216215adantr 472 . . . . . . . . . . . . 13 repeatS
217216com12 31 . . . . . . . . . . . 12 repeatS
218213, 217jaoi 386 . . . . . . . . . . 11 repeatS
219206, 218sylbi 200 . . . . . . . . . 10 repeatS
220219com12 31 . . . . . . . . 9 repeatS
221205, 220sylbid 223 . . . . . . . 8 ..^ ..^ repeatS
222221impcom 437 . . . . . . 7 ..^ ..^ repeatS
223204, 222eqtr4d 2508 . . . . . 6 ..^ ..^ ..^ ..^ ..^ repeatS repeatS
224202, 223pm2.61ian 807 . . . . 5 ..^ ..^ ..^ repeatS repeatS
225224ex 441 . . . 4 ..^ ..^ ..^ repeatS repeatS
22687, 225sylbid 223 . . 3 ..^ ..^ ..^ repeatS repeatS
22783, 226pm2.61d 163 . 2 ..^ ..^ ..^ repeatS repeatS
22810, 16, 2273eqtrd 2509 1 repeatS substr repeatS
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 189   wo 375   wa 376   w3a 1007   wceq 1452   wcel 1904   wnel 2642   wss 3390  c0 3722  cif 3872  cop 3965   class class class wbr 4395   cmpt 4454   cdm 4839  wf 5585  cfv 5589  (class class class)co 6308  cc 9555  cr 9556  cc0 9557   caddc 9560   clt 9693   cle 9694   cmin 9880  cn 10631  cn0 10893  cz 10961  ..^cfzo 11942  Word cword 12703   substr csubstr 12707   repeatS creps 12710 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-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-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-er 7381  df-en 7588  df-dom 7589  df-sdom 7590  df-fin 7591  df-card 8391  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-n0 10894  df-z 10962  df-uz 11183  df-fz 11811  df-fzo 11943  df-hash 12554  df-word 12711  df-substr 12715  df-reps 12718 This theorem is referenced by:  repswcshw  12968
 Copyright terms: Public domain W3C validator