Description: Lemma for numclwwlk1lem2foa . (Contributed by AV, 29-May-2021) (Revised by AV, 1-Nov-2022)
Ref | Expression | ||
---|---|---|---|
Assertion | numclwwlk1lem2foalem | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl | |
|
2 | s1cl | |
|
3 | s1cl | |
|
4 | 1 2 3 | 3anim123i | |
5 | 4 | 3expb | |
6 | ccatass | |
|
7 | 5 6 | syl | |
8 | 7 | oveq1d | |
9 | 1 | adantr | |
10 | ccat2s1cl | |
|
11 | 10 | adantl | |
12 | simpr | |
|
13 | 12 | eqcomd | |
14 | 13 | adantr | |
15 | pfxccatid | |
|
16 | 9 11 14 15 | syl3anc | |
17 | 8 16 | eqtrd | |
18 | 17 | 3adant3 | |
19 | 1e2m1 | |
|
20 | 19 | oveq2i | |
21 | eluzelcn | |
|
22 | 2cnd | |
|
23 | 1cnd | |
|
24 | 21 22 23 | subsubd | |
25 | 20 24 | eqtrid | |
26 | 25 | 3ad2ant3 | |
27 | 26 | fveq2d | |
28 | ccatw2s1p2 | |
|
29 | 28 | 3adant3 | |
30 | 27 29 | eqtrd | |
31 | simpl | |
|
32 | ccatw2s1p1 | |
|
33 | 1 12 31 32 | syl2an3an | |
34 | 33 | 3adant3 | |
35 | 18 30 34 | 3jca | |