Description: Split a group sum into two parts. (Contributed by Mario Carneiro, 25-Apr-2016) (Revised by AV, 5-Jun-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | gsumzsplit.b | |
|
gsumzsplit.0 | |
||
gsumzsplit.p | |
||
gsumzsplit.z | |
||
gsumzsplit.g | |
||
gsumzsplit.a | |
||
gsumzsplit.f | |
||
gsumzsplit.c | |
||
gsumzsplit.w | |
||
gsumzsplit.i | |
||
gsumzsplit.u | |
||
Assertion | gsumzsplit | |