Description: Obsolete version of ccat2s1p2 as of 20-Jan-2024. Extract the second of two concatenated singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018) (Proof modification is discouraged.) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | ccat2s1p2OLD | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | s1cl | |
|
2 | 1 | adantr | |
3 | s1cl | |
|
4 | 3 | adantl | |
5 | 1z | |
|
6 | 2z | |
|
7 | 1lt2 | |
|
8 | fzolb | |
|
9 | 5 6 7 8 | mpbir3an | |
10 | s1len | |
|
11 | s1len | |
|
12 | 10 11 | oveq12i | |
13 | 1p1e2 | |
|
14 | 12 13 | eqtri | |
15 | 10 14 | oveq12i | |
16 | 9 15 | eleqtrri | |
17 | 16 | a1i | |
18 | ccatval2 | |
|
19 | 2 4 17 18 | syl3anc | |
20 | 10 | oveq2i | |
21 | 1m1e0 | |
|
22 | 20 21 | eqtri | |
23 | 22 | a1i | |
24 | 23 | fveq2d | |
25 | s1fv | |
|
26 | 24 25 | eqtrd | |
27 | 26 | adantl | |
28 | 19 27 | eqtrd | |