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

Theorem ccat2s1p2 12613
 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 12594 . . . 4 Word
21adantr 465 . . 3 Word
3 s1cl 12594 . . . 4 Word
43adantl 466 . . 3 Word
5 1z 10906 . . . . . 6
6 2z 10908 . . . . . 6
7 1lt2 10714 . . . . . 6
8 fzolb 11814 . . . . . 6 ..^
95, 6, 7, 8mpbir3an 1178 . . . . 5 ..^
10 s1len 12597 . . . . . 6
11 s1len 12597 . . . . . . . 8
1210, 11oveq12i 6307 . . . . . . 7
13 1p1e2 10661 . . . . . . 7
1412, 13eqtri 2496 . . . . . 6
1510, 14oveq12i 6307 . . . . 5 ..^ ..^
169, 15eleqtrri 2554 . . . 4 ..^
1716a1i 11 . . 3 ..^
18 ccatval2 12576 . . 3 Word Word ..^ concat
192, 4, 17, 18syl3anc 1228 . 2 concat
2010oveq2i 6306 . . . . . . 7
21 1m1e0 10616 . . . . . . 7
2220, 21eqtri 2496 . . . . . 6
2322a1i 11 . . . . 5
2423fveq2d 5876 . . . 4
25 s1fv 12599 . . . 4
2624, 25eqtrd 2508 . . 3