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

Theorem swrdccatin12 12716
Description: The subword of a concatenation of two words within both of the concatenated words. (Contributed by Alexander van der Vekens, 5-Apr-2018.) (Revised by Alexander van der Vekens, 27-May-2018.)
Hypothesis
Ref Expression
swrdccatin12.l
Assertion
Ref Expression
swrdccatin12

Proof of Theorem swrdccatin12
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 ccatcl 12593 . . . . 5
21adantr 465 . . . 4
3 elfz0fzfz0 11808 . . . . 5
43adantl 466 . . . 4
5 elfzuz2 11720 . . . . . . . . 9
65adantl 466 . . . . . . . 8
7 fzss1 11751 . . . . . . . 8
86, 7syl 16 . . . . . . 7
9 ccatlen 12594 . . . . . . . . . 10
10 swrdccatin12.l . . . . . . . . . . . 12
1110eqcomi 2470 . . . . . . . . . . 11
1211oveq1i 6306 . . . . . . . . . 10
139, 12syl6eq 2514 . . . . . . . . 9
1413adantr 465 . . . . . . . 8
1514oveq2d 6312 . . . . . . 7
168, 15sseqtr4d 3540 . . . . . 6
1716sseld 3502 . . . . 5
1817impr 619 . . . 4
19 swrdvalfn 12663 . . . 4
202, 4, 18, 19syl3anc 1228 . . 3
21 swrdcl 12646 . . . . . . 7
22 swrdcl 12646 . . . . . . 7
2321, 22anim12i 566 . . . . . 6
2423adantr 465 . . . . 5
25 ccatvalfn 12599 . . . . 5
2624, 25syl 16 . . . 4
27 simpll 753 . . . . . . . . 9
28 simprl 756 . . . . . . . . 9
29 lencl 12562 . . . . . . . . . . . 12
30 elnn0uz 11147 . . . . . . . . . . . . . 14
31 eluzfz2 11723 . . . . . . . . . . . . . 14
3230, 31sylbi 195 . . . . . . . . . . . . 13
3310, 32syl5eqel 2549 . . . . . . . . . . . 12
3429, 33syl 16 . . . . . . . . . . 11
3534adantr 465 . . . . . . . . . 10
3635adantr 465 . . . . . . . . 9
37 swrdlen 12650 . . . . . . . . 9
3827, 28, 36, 37syl3anc 1228 . . . . . . . 8
39 simpr 461 . . . . . . . . . 10
4039adantr 465 . . . . . . . . 9
41 lencl 12562 . . . . . . . . . . . . 13
4241nn0zd 10992 . . . . . . . . . . . 12
4342adantl 466 . . . . . . . . . . 11
44 simpr 461 . . . . . . . . . . 11
4543, 44anim12i 566 . . . . . . . . . 10
46 elfzmlbp 11815 . . . . . . . . . 10
4745, 46syl 16 . . . . . . . . 9
48 swrd0len 12649 . . . . . . . . 9
4940, 47, 48syl2anc 661 . . . . . . . 8
5038, 49oveq12d 6314 . . . . . . 7
51 elfz2nn0 11798 . . . . . . . . . . 11
52 elfzelz 11717 . . . . . . . . . . . . . 14
53 nn0cn 10830 . . . . . . . . . . . . . . . . . 18
5453adantl 466 . . . . . . . . . . . . . . . . 17
5554adantl 466 . . . . . . . . . . . . . . . 16
56 nn0cn 10830 . . . . . . . . . . . . . . . . 17
5756ad2antrl 727 . . . . . . . . . . . . . . . 16
58 zcn 10894 . . . . . . . . . . . . . . . . 17
5958adantr 465 . . . . . . . . . . . . . . . 16
6055, 57, 593jca 1176 . . . . . . . . . . . . . . 15
6160ex 434 . . . . . . . . . . . . . 14
6252, 61syl 16 . . . . . . . . . . . . 13
6362com12 31 . . . . . . . . . . . 12
64633adant3 1016 . . . . . . . . . . 11
6551, 64sylbi 195 . . . . . . . . . 10
6665imp 429 . . . . . . . . 9
6766adantl 466 . . . . . . . 8
68 npncan3 9880 . . . . . . . 8
6967, 68syl 16 . . . . . . 7
7050, 69eqtr2d 2499 . . . . . 6
7170oveq2d 6312 . . . . 5
7271fneq2d 5677 . . . 4
7326, 72mpbird 232 . . 3
74 simprl 756 . . . . . 6
75 simpr 461 . . . . . . . 8
7675anim2i 569 . . . . . . 7
7776ancomd 451 . . . . . 6
7810swrdccatin12lem3 12715 . . . . . 6
7974, 77, 78sylc 60 . . . . 5
8024ad2antrl 727 . . . . . . 7
81 simpl 457 . . . . . . . 8
82 nn0fz0 11803 . . . . . . . . . . . . . . . 16
8329, 82sylib 196 . . . . . . . . . . . . . . 15
8410, 83syl5eqel 2549 . . . . . . . . . . . . . 14
8584adantr 465 . . . . . . . . . . . . 13
8685adantr 465 . . . . . . . . . . . 12
8727, 28, 863jca 1176 . . . . . . . . . . 11
8887ad2antrl 727 . . . . . . . . . 10
8988, 37syl 16 . . . . . . . . 9
9089oveq2d 6312 . . . . . . . 8
9181, 90eleqtrrd 2548 . . . . . . 7
92 df-3an 975 . . . . . . 7
9380, 91, 92sylanbrc 664 . . . . . 6
94 ccatval1 12595 . . . . . 6
9593, 94syl 16 . . . . 5
9679, 95eqtr4d 2501 . . . 4
97 simprl 756 . . . . . 6
9875anim2i 569 . . . . . . 7
9998ancomd 451 . . . . . 6
10010swrdccatin12lem2 12714 . . . . . 6
10197, 99, 100sylc 60 . . . . 5
10224ad2antrl 727 . . . . . . 7
103 elfzuz 11713 . . . . . . . . . . . . 13
104 eluzelz 11119 . . . . . . . . . . . . . 14
105 simpll 753 . . . . . . . . . . . . . . . . . . 19
106 simpr 461 . . . . . . . . . . . . . . . . . . . 20
107106adantr 465 . . . . . . . . . . . . . . . . . . 19
108 simpr 461 . . . . . . . . . . . . . . . . . . 19
109105, 107, 1083jca 1176 . . . . . . . . . . . . . . . . . 18
110109ex 434 . . . . . . . . . . . . . . . . 17
111110ancoms 453 . . . . . . . . . . . . . . . 16
1121113adant3 1016 . . . . . . . . . . . . . . 15
11351, 112sylbi 195 . . . . . . . . . . . . . 14
114104, 113syl5com 30 . . . . . . . . . . . . 13
115103, 114syl 16 . . . . . . . . . . . 12
116115impcom 430 . . . . . . . . . . 11
117116adantl 466 . . . . . . . . . 10
118117ad2antrl 727 . . . . . . . . 9
119 swrdccatin12lem1 12709 . . . . . . . . 9
120118, 99, 119sylc 60 . . . . . . . 8
12127, 28, 86, 37syl3anc 1228 . . . . . . . . . 10
12239adantl 466 . . . . . . . . . . . . . . . 16
12343adantl 466 . . . . . . . . . . . . . . . . 17
124 simpl 457 . . . . . . . . . . . . . . . . 17
125123, 124, 46syl2anc 661 . . . . . . . . . . . . . . . 16
126122, 125jca 532 . . . . . . . . . . . . . . 15
127126ex 434 . . . . . . . . . . . . . 14
128127adantl 466 . . . . . . . . . . . . 13
129128impcom 430 . . . . . . . . . . . 12
130129, 48syl 16 . . . . . . . . . . 11
131121, 130oveq12d 6314 . . . . . . . . . 10
132121, 131oveq12d 6314 . . . . . . . . 9
133132ad2antrl 727 . . . . . . . 8
134120, 133eleqtrrd 2548 . . . . . . 7
135 df-3an 975 . . . . . . 7
136102, 134, 135sylanbrc 664 . . . . . 6
137 ccatval2 12596 . . . . . 6
138136, 137syl 16 . . . . 5