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

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

Proof of Theorem repswswrd
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 repsw 12747 . . . . . 6
2 nn0z 10912 . . . . . . 7
3 nn0z 10912 . . . . . . 7
42, 3anim12i 566 . . . . . 6
51, 4anim12i 566 . . . . 5
6 3anass 977 . . . . 5
75, 6sylibr 212 . . . 4
873adant3 1016 . . 3
9 swrdval 12644 . . 3
108, 9syl 16 . 2
11 repsf 12745 . . . . . 6
12113ad2ant1 1017 . . . . 5
13 fdm 5740 . . . . 5
1412, 13syl 16 . . . 4
1514sseq2d 3531 . . 3
1615ifbid 3963 . 2
17 fzon 11847 . . . . . . . . . . 11
184, 17syl 16 . . . . . . . . . 10
1918adantl 466 . . . . . . . . 9
2019biimpac 486 . . . . . . . 8
21 0ss 3814 . . . . . . . 8
2220, 21syl6eqss 3553 . . . . . . 7
23 iftrue 3947 . . . . . . 7
2422, 23syl 16 . . . . . 6
25 nn0re 10829 . . . . . . . . . . . 12
26 nn0re 10829 . . . . . . . . . . . 12
2725, 26anim12ci 567 . . . . . . . . . . 11
2827adantl 466 . . . . . . . . . 10
29 suble0 10091 . . . . . . . . . 10
3028, 29syl 16 . . . . . . . . 9
3130biimparc 487 . . . . . . . 8
32 0z 10900 . . . . . . . . 9
33 zsubcl 10931 . . . . . . . . . . . 12
343, 2, 33syl2anr 478 . . . . . . . . . . 11
3534adantl 466 . . . . . . . . . 10
3635adantl 466 . . . . . . . . 9
37 fzon 11847 . . . . . . . . 9
3832, 36, 37sylancr 663 . . . . . . . 8
3931, 38mpbid 210 . . . . . . 7
4039mpteq1d 4533 . . . . . 6
41 oveq2 6304 . . . . . . . . . . . . 13
4241oveq2d 6312 . . . . . . . . . . . 12
43 nn0cn 10830 . . . . . . . . . . . . . . . . 17
4443adantl 466 . . . . . . . . . . . . . . . 16
4544subidd 9942 . . . . . . . . . . . . . . 15
4645adantl 466 . . . . . . . . . . . . . 14
4746oveq2d 6312 . . . . . . . . . . . . 13
48 repsw0 12749 . . . . . . . . . . . . . 14
4948ad2antrr 725 . . . . . . . . . . . . 13
5047, 49eqtrd 2498 . . . . . . . . . . . 12
5142, 50sylan9eqr 2520 . . . . . . . . . . 11
5251ex 434 . . . . . . . . . 10
5352adantl 466 . . . . . . . . 9
5453com12 31 . . . . . . . 8
55 elnn0z 10902 . . . . . . . . . . . . . . 15
56 subge0 10090 . . . . . . . . . . . . . . . . . . . . . 22
5726, 25, 56syl2anr 478 . . . . . . . . . . . . . . . . . . . . 21
5825, 26anim12i 566 . . . . . . . . . . . . . . . . . . . . . . . 24
59 letri3 9691 . . . . . . . . . . . . . . . . . . . . . . . 24
6058, 59syl 16 . . . . . . . . . . . . . . . . . . . . . . 23
6160biimprd 223 . . . . . . . . . . . . . . . . . . . . . 22
6261expd 436 . . . . . . . . . . . . . . . . . . . . 21
6357, 62sylbid 215 . . . . . . . . . . . . . . . . . . . 20
6463com23 78 . . . . . . . . . . . . . . . . . . 19
6564adantl 466 . . . . . . . . . . . . . . . . . 18
6665impcom 430 . . . . . . . . . . . . . . . . 17
6766com12 31 . . . . . . . . . . . . . . . 16
6867adantl 466 . . . . . . . . . . . . . . 15
6955, 68sylbi 195 . . . . . . . . . . . . . 14
7069com12 31 . . . . . . . . . . . . 13
7170con3d 133 . . . . . . . . . . . 12
7271impcom 430 . . . . . . . . . . 11
73 df-nel 2655 . . . . . . . . . . 11
7472, 73sylibr 212 . . . . . . . . . 10
75 repsundef 12743 . . . . . . . . . 10
7674, 75syl 16 . . . . . . . . 9
7776ex 434 . . . . . . . 8
7854, 77pm2.61i 164 . . . . . . 7
79 mpt0 5713 . . . . . . 7
8078, 79syl6reqr 2517 . . . . . 6
8124, 40, 803eqtrd 2502 . . . . 5
8281expcom 435 . . . 4
83823adant3 1016 . . 3
84 ltnle 9685 . . . . . . 7
8558, 84syl 16 . . . . . 6
8685bicomd 201 . . . . 5
87863ad2ant2 1018 . . . 4
8823adantr 465 . . . . . . 7
8943ad2ant2 1018 . . . . . . . . . . 11
9089adantr 465 . . . . . . . . . 10
91 0zd 10901 . . . . . . . . . . . . 13
92 nn0z 10912 . . . . . . . . . . . . 13
9391, 92anim12i 566 . . . . . . . . . . . 12
94933ad2ant1 1017 . . . . . . . . . . 11
9594adantr 465 . . . . . . . . . 10
96 simpr 461 . . . . . . . . . 10
97 ssfzo12bi 11907 . . . . . . . . . 10
9890, 95, 96, 97syl3anc 1228 . . . . . . . . 9
99 simpl1l 1047 . . . . . . . . . . . . . 14
10099ad2antrr 725 . . . . . . . . . . . . 13
101 simpl1r 1048 . . . . . . . . . . . . . 14
102101ad2antrr 725 . . . . . . . . . . . . 13
103 elfzonn0 11867 . . . . . . . . . . . . . . . 16
104 nn0addcl 10856 . . . . . . . . . . . . . . . . . . . 20
105104expcom 435 . . . . . . . . . . . . . . . . . . 19
106105adantr 465 . . . . . . . . . . . . . . . . . 18
1071063ad2ant2 1018 . . . . . . . . . . . . . . . . 17
108107ad2antrr 725 . . . . . . . . . . . . . . . 16
109103, 108syl5com 30 . . . . . . . . . . . . . . 15
110109impcom 430 . . . . . . . . . . . . . 14
11192adantl 466 . . . . . . . . . . . . . . . . . 18
1121113ad2ant1 1017 . . . . . . . . . . . . . . . . 17
113112adantr 465 . . . . . . . . . . . . . . . 16
114 nn0re 10829 . . . . . . . . . . . . . . . . . . . . . . . 24
115114adantl 466 . . . . . . . . . . . . . . . . . . . . . . 23
116115, 58anim12ci 567 . . . . . . . . . . . . . . . . . . . . . 22
117 df-3an 975 . . . . . . . . . . . . . . . . . . . . . 22
118116, 117sylibr 212 . . . . . . . . . . . . . . . . . . . . 21
119 ltletr 9697 . . . . . . . . . . . . . . . . . . . . 21
120118, 119syl 16 . . . . . . . . . . . . . . . . . . . 20
121 elnn0z 10902 . . . . . . . . . . . . . . . . . . . . . . 23
122 0red 9618 . . . . . . . . . . . . . . . . . . . . . . . . . 26
123 zre 10893 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
124123adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . 26
125115adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26
126 lelttr 9696 . . . . . . . . . . . . . . . . . . . . . . . . . 26
127122, 124, 125, 126syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . . . 25
128127expd 436 . . . . . . . . . . . . . . . . . . . . . . . 24
129128impancom 440 . . . . . . . . . . . . . . . . . . . . . . 23
130121, 129sylbi 195 . . . . . . . . . . . . . . . . . . . . . 22
131130adantr 465 . . . . . . . . . . . . . . . . . . . . 21
132131impcom 430 . . . . . . . . . . . . . . . . . . . 20
133120, 132syld 44 . . . . . . . . . . . . . . . . . . 19
134133expcomd 438 . . . . . . . . . . . . . . . . . 18
1351343impia 1193 . . . . . . . . . . . . . . . . 17
136135imp 429 . . . . . . . . . . . . . . . 16
137 elnnz 10899 . . . . . . . . . . . . . . . 16
138113, 136, 137sylanbrc 664 . . . . . . . . . . . . . . 15
139138ad2antrr 725 . . . . . . . . . . . . . 14
140 elfzo0 11863 . . . . . . . . . . . . . . . 16
141 nn0readdcl 10883 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
142141expcom 435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
143142ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
144143impcom 430 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
14526adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
146145adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
147146adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
148114ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
149144, 147, 1483jca 1176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
150149ex 434 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
151150adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
152151impcom 430 . . . . . . . . . . . . . . . . . . . . . . . . . 26
153152adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25
154 nn0re 10829 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
155154adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
15625ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
157156adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
158155, 157, 147ltaddsubd 10177 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
159 idd 24 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
160159ex 434 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
161160com23 78 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
162158, 161sylbird 235 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
163162impancom 440 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
164163impcom 430 . . . . . . . . . . . . . . . . . . . . . . . . . 26
165164impac 621 . . . . . . . . . . . . . . . . . . . . . . . . 25