Description: Group multiple (exponentiation) operation at zero. (Contributed by Mario Carneiro, 11-Dec-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | mulg0.b | |
|
mulg0.o | |
||
mulg0.t | |
||
Assertion | mulg0 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mulg0.b | |
|
2 | mulg0.o | |
|
3 | mulg0.t | |
|
4 | 0z | |
|
5 | eqid | |
|
6 | eqid | |
|
7 | eqid | |
|
8 | 1 5 2 6 3 7 | mulgval | |
9 | eqid | |
|
10 | 9 | iftruei | |
11 | 8 10 | eqtrdi | |
12 | 4 11 | mpan | |