Description: sum^ splits into two parts, when it's a real number. This is a special case of sge0split . (Contributed by Glauco Siliprandi, 17-Aug-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | sge0resplit.a | |
|
sge0resplit.b | |
||
sge0resplit.u | |
||
sge0resplit.in0 | |
||
sge0resplit.f | |
||
sge0resplit.re | |
||
Assertion | sge0resplit | |