Description: The integral of the constant zero function is zero. (Contributed by Thierry Arnoux, 13-Mar-2018)
Ref | Expression | ||
---|---|---|---|
Hypotheses | sitgval.b | |
|
sitgval.j | |
||
sitgval.s | |
||
sitgval.0 | |
||
sitgval.x | |
||
sitgval.h | |
||
sitgval.1 | |
||
sitgval.2 | |
||
sitg0.1 | |
||
sitg0.2 | |
||
Assertion | sitg0 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sitgval.b | |
|
2 | sitgval.j | |
|
3 | sitgval.s | |
|
4 | sitgval.0 | |
|
5 | sitgval.x | |
|
6 | sitgval.h | |
|
7 | sitgval.1 | |
|
8 | sitgval.2 | |
|
9 | sitg0.1 | |
|
10 | sitg0.2 | |
|
11 | 1 2 3 4 5 6 7 8 9 10 | sibf0 | |
12 | 1 2 3 4 5 6 7 8 11 | sitgfval | |
13 | rnxpss | |
|
14 | ssdif0 | |
|
15 | 13 14 | mpbi | |
16 | mpteq1 | |
|
17 | 15 16 | ax-mp | |
18 | mpt0 | |
|
19 | 17 18 | eqtri | |
20 | 19 | oveq2i | |
21 | 4 | gsum0 | |
22 | 20 21 | eqtri | |
23 | 12 22 | eqtrdi | |