Description: Lemma for zlmbas and zlmplusg . (Contributed by Mario Carneiro, 2-Oct-2015) (Revised by AV, 3-Nov-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | zlmbas.w | |
|
zlmlem.2 | |
||
zlmlem.3 | |
||
zlmlem.4 | |
||
Assertion | zlmlem | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | zlmbas.w | |
|
2 | zlmlem.2 | |
|
3 | zlmlem.3 | |
|
4 | zlmlem.4 | |
|
5 | 2 3 | setsnid | |
6 | 2 4 | setsnid | |
7 | 5 6 | eqtri | |
8 | eqid | |
|
9 | 1 8 | zlmval | |
10 | 9 | fveq2d | |
11 | 7 10 | eqtr4id | |
12 | 2 | str0 | |
13 | 12 | eqcomi | |
14 | 13 1 | fveqprc | |
15 | 11 14 | pm2.61i | |