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

Theorem swrdspsleq 12673
Description: Two words have a common subword (starting at the same position with the same length) iff they have the same symbols at each position. (Contributed by Alexander van der Vekens, 7-Aug-2018.)
Assertion
Ref Expression
swrdspsleq
Distinct variable groups:   ,M   ,N   ,   ,   ,

Proof of Theorem swrdspsleq
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 simpl 457 . . . . . . . . . 10
21adantr 465 . . . . . . . . 9
3 nn0z 10912 . . . . . . . . . . 11
43adantr 465 . . . . . . . . . 10
54adantl 466 . . . . . . . . 9
6 nn0z 10912 . . . . . . . . . . 11
76adantl 466 . . . . . . . . . 10
87adantl 466 . . . . . . . . 9
9 swrdlend 12656 . . . . . . . . 9
102, 5, 8, 9syl3anc 1228 . . . . . . . 8
1110imp 429 . . . . . . 7
12 simpr 461 . . . . . . . . . 10
1312adantr 465 . . . . . . . . 9
14 swrdlend 12656 . . . . . . . . 9
1513, 5, 8, 14syl3anc 1228 . . . . . . . 8
1615imp 429 . . . . . . 7
1711, 16eqtr4d 2501 . . . . . 6
1817ex 434 . . . . 5
19183adant3 1016 . . . 4
2019impcom 430 . . 3
21 ral0 3934 . . . . . . 7
22 fzon 11847 . . . . . . . . . 10
233, 6, 22syl2an 477 . . . . . . . . 9
2423biimpa 484 . . . . . . . 8
2524raleqdv 3060 . . . . . . 7
2621, 25mpbiri 233 . . . . . 6
2726ex 434 . . . . 5
28273ad2ant2 1018 . . . 4
2928impcom 430 . . 3
3020, 292thd 240 . 2
31 swrdcl 12646 . . . . . 6
32 swrdcl 12646 . . . . . 6
33 eqwrd 12582 . . . . . 6
3431, 32, 33syl2an 477 . . . . 5
35343ad2ant1 1017 . . . 4
3635adantl 466 . . 3
3713ad2ant1 1017 . . . . . . 7
3837adantl 466 . . . . . 6
39 nn0re 10829 . . . . . . . . . 10
40 nn0re 10829 . . . . . . . . . 10
41 ltnle 9685 . . . . . . . . . 10
4239, 40, 41syl2an 477 . . . . . . . . 9
43 fzossfz 11846 . . . . . . . . . . 11
4463anim2i 1183 . . . . . . . . . . . . 13
45 elfzo0z 11865 . . . . . . . . . . . . 13
4644, 45sylibr 212 . . . . . . . . . . . 12
47463expa 1196 . . . . . . . . . . 11
4843, 47sseldi 3501 . . . . . . . . . 10
4948ex 434 . . . . . . . . 9
5042, 49sylbird 235 . . . . . . . 8
51503ad2ant2 1018 . . . . . . 7
5251impcom 430 . . . . . 6
53 simpr 461 . . . . . . . . . 10
54 lencl 12562 . . . . . . . . . . 11
5554adantr 465 . . . . . . . . . 10
56 simpl 457 . . . . . . . . . 10
5753, 55, 563anim123i 1181 . . . . . . . . 9
58573com12 1200 . . . . . . . 8
59 elfz2nn0 11798 . . . . . . . 8
6058, 59sylibr 212 . . . . . . 7
6160adantl 466 . . . . . 6
62 swrdlen 12650 . . . . . 6
6338, 52, 61, 62syl3anc 1228 . . . . 5
64123ad2ant1 1017 . . . . . . 7
6564adantl 466 . . . . . 6
66443expa 1196 . . . . . . . . . . . 12
6766, 45sylibr 212 . . . . . . . . . . 11
6843, 67sseldi 3501 . . . . . . . . . 10
6968ex 434 . . . . . . . . 9
7042, 69sylbird 235 . . . . . . . 8
71703ad2ant2 1018 . . . . . . 7
7271impcom 430 . . . . . 6
73 lencl 12562 . . . . . . . . . . 11
7473adantl 466 . . . . . . . . . 10
75 simpr 461 . . . . . . . . . 10
7653, 74, 753anim123i 1181 . . . . . . . . 9
77763com12 1200 . . . . . . . 8
78 elfz2nn0 11798 . . . . . . . 8
7977, 78sylibr 212 . . . . . . 7
8079adantl 466 . . . . . 6
81 swrdlen 12650 . . . . . 6
8265, 72, 80, 81syl3anc 1228 . . . . 5
8363, 82eqtr4d 2501 . . . 4
8483biantrurd 508 . . 3
85 0zd 10901 . . . . 5
86 lencl 12562 . . . . . . . . . 10
8731, 86syl 16 . . . . . . . . 9
8887nn0zd 10992 . . . . . . . 8
8988adantr 465 . . . . . . 7
90893ad2ant1 1017 . . . . . 6
9190adantl 466 . . . . 5
9243ad2ant2 1018 . . . . . 6
9392adantl 466 . . . . 5
94 fzoshftral 11923 . . . . 5
9585, 91, 93, 94syl3anc 1228 . . . 4
96 nn0cn 10830 . . . . . . . . . 10
9796addid2d 9802 . . . . . . . . 9
9897adantr 465 . . . . . . . 8
99983ad2ant2 1018 . . . . . . 7
10099adantl 466 . . . . . 6
10163oveq1d 6311 . . . . . . 7
102 nn0cn 10830 . . . . . . . . . . 11
10396, 102anim12ci 567 . . . . . . . . . 10
104 npcan 9852 . . . . . . . . . 10
105103, 104syl 16 . . . . . . . . 9
1061053ad2ant2 1018 . . . . . . . 8
107106adantl 466 . . . . . . 7
108101, 107eqtrd 2498 . . . . . 6
109100, 108oveq12d 6314 . . . . 5
110 ovex 6324 . . . . . . 7
111 sbceqg 3825 . . . . . . . 8
112 csbfv2g 5908 . . . . . . . . . 10
113 csbvarg 3848 . . . . . . . . . . 11
114113fveq2d 5875 . . . . . . . . . 10
115112, 114eqtrd 2498 . . . . . . . . 9
116 csbfv2g 5908 . . . . . . . . . 10
117113fveq2d 5875 . . . . . . . . . 10
118116, 117eqtrd 2498 . . . . . . . . 9
119115, 118eqeq12d 2479 . . . . . . . 8
120111, 119bitrd 253 . . . . . . 7
121110, 120mp1i 12 . . . . . 6
12258adantl 466 . . . . . . . . . . . . . 14
123122, 59sylibr 212 . . . . . . . . . . . . 13
12438, 52, 123, 62syl3anc 1228 . . . . . . . . . . . 12
125124oveq1d 6311 . . . . . . . . . . 11
126125, 107eqtrd 2498 . . . . . . . . . 10
127100, 126oveq12d 6314 . . . . . . . . 9
128127eleq2d 2527 . . . . . . . 8
12938, 52, 1233jca 1176 . . . . . . . . . . . 12
130129adantr 465 . . . . . . . . . . 11
13177adantl 466 . . . . . . . . . . . . . 14
132131, 78sylibr 212 . . . . . . . . . . . . 13
13365, 52, 1323jca 1176 . . . . . . . . . . . 12
134133adantr 465 . . . . . . . . . . 11
135130, 134jca 532 . . . . . . . . . 10
136 pncan3 9851 . . . . . . . . . . . . . . . . . . . . 21
13796, 102, 136syl2an 477 . . . . . . . . . . . . . . . . . . . 20
138137eqcomd 2465 . . . . . . . . . . . . . . . . . . 19
139138oveq2d 6312 . . . . . . . . . . . . . . . . . 18
140139eleq2d 2527 . . . . . . . . . . . . . . . . 17
141140biimpa 484 . . . . . . . . . . . . . . . 16
1423, 6anim12ci 567 . . . . . . . . . . . . . . . . . 18
143 zsubcl 10931 . . . . . . . . . . . . . . . . . 18
144142, 143syl 16 . . . . . . . . . . . . . . . . 17
145144adantr 465 . . . . . . . . . . . . . . . 16
146141, 145jca 532 . . . . . . . . . . . . . . 15