Description: Group sum of a singleton, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by Thierry Arnoux, 28-Mar-2018) (Proof shortened by AV, 11-Dec-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | gsumsnf.c | |
|
gsumsnf.b | |
||
gsumsnf.s | |
||
Assertion | gsumsnf | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | gsumsnf.c | |
|
2 | gsumsnf.b | |
|
3 | gsumsnf.s | |
|
4 | simp1 | |
|
5 | simp2 | |
|
6 | simp3 | |
|
7 | 3 | adantl | |
8 | nfv | |
|
9 | nfv | |
|
10 | 1 | nfel1 | |
11 | 8 9 10 | nf3an | |
12 | 2 4 5 6 7 11 1 | gsumsnfd | |