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

Theorem swrdccatin2 12712
Description: The subword of a concatenation of two words within the second of the concatenated words. (Contributed by Alexander van der Vekens, 28-Mar-2018.) (Revised by Alexander van der Vekens, 27-May-2018.)
Hypothesis
Ref Expression
swrdccatin12.l
Assertion
Ref Expression
swrdccatin2

Proof of Theorem swrdccatin2
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 swrdccatin12.l . . . . . . . 8
2 oveq1 6303 . . . . . . . . . 10
32eleq2d 2527 . . . . . . . . 9
4 id 22 . . . . . . . . . . 11
5 oveq1 6303 . . . . . . . . . . 11
64, 5oveq12d 6314 . . . . . . . . . 10
76eleq2d 2527 . . . . . . . . 9
83, 7anbi12d 710 . . . . . . . 8
91, 8ax-mp 5 . . . . . . 7
10 lencl 12562 . . . . . . . . 9
11 elnn0uz 11147 . . . . . . . . . . . . 13
1211biimpi 194 . . . . . . . . . . . 12
13 fzss1 11751 . . . . . . . . . . . 12
1412, 13syl 16 . . . . . . . . . . 11
1514sseld 3502 . . . . . . . . . 10
16 fzss1 11751 . . . . . . . . . . . 12
1712, 16syl 16 . . . . . . . . . . 11
1817sseld 3502 . . . . . . . . . 10
1915, 18anim12d 563 . . . . . . . . 9
2010, 19syl 16 . . . . . . . 8
2120adantr 465 . . . . . . 7
229, 21syl5bi 217 . . . . . 6
2322imp 429 . . . . 5
24 swrdccatfn 12707 . . . . 5
2523, 24syldan 470 . . . 4
26 elfz2 11708 . . . . . . . . . 10
27 zcn 10894 . . . . . . . . . . . . 13
28 zcn 10894 . . . . . . . . . . . . 13
29 zcn 10894 . . . . . . . . . . . . 13
3027, 28, 293anim123i 1181 . . . . . . . . . . . 12
31303comr 1204 . . . . . . . . . . 11
3231adantr 465 . . . . . . . . . 10
3326, 32sylbi 195 . . . . . . . . 9
3433adantr 465 . . . . . . . 8
35 nnncan2 9879 . . . . . . . 8
3634, 35syl 16 . . . . . . 7
3736adantl 466 . . . . . 6
3837oveq2d 6312 . . . . 5
3938fneq2d 5677 . . . 4
4025, 39mpbird 232 . . 3
41 simpr 461 . . . . 5
4241adantr 465 . . . 4
43 elfzmlbm 11813 . . . . 5
4443ad2antrl 727 . . . 4
45 lencl 12562 . . . . . . . . . 10
4645nn0zd 10992 . . . . . . . . 9
4746adantl 466 . . . . . . . 8
48 elfzmlbp 11815 . . . . . . . . 9
4948ex 434 . . . . . . . 8
5047, 49syl 16 . . . . . . 7
5150com12 31 . . . . . 6
5251adantl 466 . . . . 5
5352impcom 430 . . . 4
54 swrdvalfn 12663 . . . 4
5542, 44, 53, 54syl3anc 1228 . . 3
56 simpl 457 . . . . . . . 8
5756adantr 465 . . . . . . 7
58 elfzoelz 11829 . . . . . . . . 9
59 elfzelz 11717 . . . . . . . . . . 11
60 zaddcl 10929 . . . . . . . . . . . 12
6160expcom 435 . . . . . . . . . . 11
6259, 61syl 16 . . . . . . . . . 10
6362ad2antrl 727 . . . . . . . . 9
6458, 63syl5com 30 . . . . . . . 8
6564impcom 430 . . . . . . 7
66 df-3an 975 . . . . . . 7
6757, 65, 66sylanbrc 664 . . . . . 6
68 ccatsymb 12600 . . . . . 6
6967, 68syl 16 . . . . 5
70 elfzonn0 11867 . . . . . . . 8
71 zre 10893 . . . . . . . . . . . . . . . . . . 19
72 zre 10893 . . . . . . . . . . . . . . . . . . 19
7371, 72anim12i 566 . . . . . . . . . . . . . . . . . 18
74 elnn0z 10902 . . . . . . . . . . . . . . . . . . 19
75 zre 10893 . . . . . . . . . . . . . . . . . . . 20
76 0red 9618 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
7776anim1i 568 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
7877ancoms 453 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
7978adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26
80 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
8180anim2i 569 . . . . . . . . . . . . . . . . . . . . . . . . . 26
82 le2add 10059 . . . . . . . . . . . . . . . . . . . . . . . . . 26
8379, 81, 82syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . 25
84 recn 9603 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
8584addid2d 9802 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
8685ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . . 26
8786breq1d 4462 . . . . . . . . . . . . . . . . . . . . . . . . 25
8883, 87sylibd 214 . . . . . . . . . . . . . . . . . . . . . . . 24
89 simpl 457 . . . . . . . . . . . . . . . . . . . . . . . . . 26
9089adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . 25
91 readdcl 9596 . . . . . . . . . . . . . . . . . . . . . . . . . 26
9281, 91syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25
9390, 92lenltd 9752 . . . . . . . . . . . . . . . . . . . . . . . 24
9488, 93sylibd 214 . . . . . . . . . . . . . . . . . . . . . . 23
9594expd 436 . . . . . . . . . . . . . . . . . . . . . 22
9695com12 31 . . . . . . . . . . . . . . . . . . . . 21
9796expd 436 . . . . . . . . . . . . . . . . . . . 20
9875, 97mpan9 469 . . . . . . . . . . . . . . . . . . 19
9974, 98sylbi 195 . . . . . . . . . . . . . . . . . 18
10073, 99mpan9 469 . . . . . . . . . . . . . . . . 17
1011eqcomi 2470 . . . . . . . . . . . . . . . . . . 19
102101breq2i 4460 . . . . . . . . . . . . . . . . . 18
103102notbii 296 . . . . . . . . . . . . . . . . 17
104100, 103syl6ibr 227 . . . . . . . . . . . . . . . 16
105104ex 434 . . . . . . . . . . . . . . 15
106105com23 78 . . . . . . . . . . . . . 14
1071063adant2 1015 . . . . . . . . . . . . 13
108107com12 31 . . . . . . . . . . . 12
109108adantr 465 . . . . . . . . . . 11
110109impcom 430 . . . . . . . . . 10
11126, 110sylbi 195 . . . . . . . . 9
112111ad2antrl 727 . . . . . . . 8
11370, 112syl5com 30 . . . . . . 7
114113impcom 430 . . . . . 6
115114iffalsed 3952 . . . . 5
116 zcn 10894 . . . . . . . . . . . . . . . . 17
117116adantl 466 . . . . . . . . . . . . . . . 16
11828adantl 466 . . . . . . . . . . . . . . . . 17
119118adantr 465 . . . . . . . . . . . . . . . 16
12029ad2antrr 725 . . . . . . . . . . . . . . . 16
121117, 119, 120addsubassd 9974 . . . . . . . . . . . . . . 15
122 oveq2 6304 . . . . . . . . . . . . . . . 16
123122eqeq1d 2459 . . . . . . . . . . . . . . 15
124121, 123syl5ib 219 . . . . . . . . . . . . . 14
1251, 124ax-mp 5 . . . . . . . . . . . . 13
126125ex 434 . . . . . . . . . . . 12
1271263adant2 1015 . . . . . . . . . . 11
128127adantr 465 . . . . . . . . . 10
12926, 128sylbi 195 . . . . . . . . 9
130129ad2antrl 727 . . . . . . . 8
13158, 130syl5com 30 . . . . . . 7
132131impcom 430 . . . . . 6
133132fveq2d 5875 . . . . 5
13469, 115, 1333eqtrd 2502 . . . 4
135 ccatcl 12593 . . . . . 6
136135ad2antrr 725 . . . . 5
1371, 12syl5eqel 2549 . . . . . . . . . . . 12
138 fzss1 11751 . . . . . . . . . . . 12
13910, 137, 1383syl 20 . . . . . . . . . . 11
140139sseld 3502 . . . . . . . . . 10
141140adantr 465 . . . . . . . . 9
142141com12 31 . . . . . . . 8
143142adantr 465 . . . . . . 7
144143impcom 430 . . . . . 6
145144adantr 465 . . . . 5
1461, 7ax-mp 5 . . . . . . . . 9
14710, 12syl 16 . . . . . . . . . . . . . . 15
148147adantr 465 . . . . . . . . . . . . . 14
149148, 16syl 16 . . . . . . . . . . . . 13
150149sseld 3502 . . . . . . . . . . . 12
151150impcom 430 . . . . . . . . . . 11
152 ccatlen 12594 . . . . . . . . . . . . . 14
153152oveq2d 6312 . . . . . . . . . . . . 13
154153eleq2d 2527 . . . . . . . . . . . 12
155154adantl 466 . . . . . . . . . . 11
156151, 155mpbird 232 . . . . . . . . . 10
157156ex 434 . . . . . . . . 9
158146, 157sylbi 195 . . . . . . . 8
159158adantl 466 . . . . . . 7
160159impcom 430 . . . . . 6
161160adantr 465 . . . . 5
162 fzmmmeqm 11746 . . . . . . . . . 10
163162oveq2d 6312 . . . . . . . . 9
164163eleq2d 2527 . . . . . . . 8
165164biimpd 207 . . . . . . 7
166165ad2antrl 727 . . . . . 6
167166imp 429 . . . . 5
168 swrdfv 12651 . . . . 5
169136, 145, 161, 167, 168syl31anc 1231 . . . 4
17046, 49syl 16 . . . . . . . . . 10
171170adantl 466 . . . . . . . . 9
172171com12 31 . . . . . . . 8
173172adantl 466 . . . . . . 7
174173impcom 430 . . . . . 6
17542, 44, 1743jca 1176 . . . . 5
176 swrdfv 12651 . . . . 5
177175, 176sylan 471 . . . 4
178134, 169, 1773eqtr4d 2508 . . 3
17940, 55, 178eqfnfvd 5984 . 2