Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ccat2s1p2 Structured version   Unicode version

Theorem ccat2s1p2 30437
 Description: Extract the second of two concatenated singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018.)
Assertion
Ref Expression
ccat2s1p2 concat

Proof of Theorem ccat2s1p2
StepHypRef Expression
1 s1cl 12415 . . . 4 Word
21adantr 465 . . 3 Word
3 s1cl 12415 . . . 4 Word
43adantl 466 . . 3 Word
5 1z 10791 . . . . . 6
6 2z 10793 . . . . . 6
7 1lt2 10603 . . . . . 6
8 fzolb 11679 . . . . . 6 ..^
95, 6, 7, 8mpbir3an 1170 . . . . 5 ..^
10 s1len 12418 . . . . . 6
11 s1len 12418 . . . . . . . 8
1210, 11oveq12i 6215 . . . . . . 7
13 1p1e2 10550 . . . . . . 7
1412, 13eqtri 2483 . . . . . 6
1510, 14oveq12i 6215 . . . . 5 ..^ ..^
169, 15eleqtrri 2541 . . . 4 ..^
1716a1i 11 . . 3 ..^
18 ccatval2 12399 . . 3 Word Word ..^ concat
192, 4, 17, 18syl3anc 1219 . 2 concat
2010oveq2i 6214 . . . . . . 7
21 1m1e0 10505 . . . . . . 7
2220, 21eqtri 2483 . . . . . 6
2322a1i 11 . . . . 5
2423fveq2d 5806 . . . 4
25 s1fv 12420 . . . 4
2624, 25eqtrd 2495 . . 3