Description: A sum of a singleton is the term. The deduction version of sumsn . (Contributed by Glauco Siliprandi, 20-Apr-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | sumsnd.1 | |
|
sumsnd.2 | |
||
sumsnd.3 | |
||
sumsnd.4 | |
||
sumsnd.5 | |
||
Assertion | sumsnd | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sumsnd.1 | |
|
2 | sumsnd.2 | |
|
3 | sumsnd.3 | |
|
4 | sumsnd.4 | |
|
5 | sumsnd.5 | |
|
6 | nfcv | |
|
7 | nfcsb1v | |
|
8 | csbeq1a | |
|
9 | 6 7 8 | cbvsumi | |
10 | csbeq1 | |
|
11 | 1nn | |
|
12 | 11 | a1i | |
13 | f1osng | |
|
14 | 11 4 13 | sylancr | |
15 | 1z | |
|
16 | fzsn | |
|
17 | f1oeq2 | |
|
18 | 15 16 17 | mp2b | |
19 | 14 18 | sylibr | |
20 | elsni | |
|
21 | 20 | adantl | |
22 | 21 | csbeq1d | |
23 | 2 1 4 3 | csbiedf | |
24 | 23 | adantr | |
25 | 5 | adantr | |
26 | 24 25 | eqeltrd | |
27 | 22 26 | eqeltrd | |
28 | 23 | adantr | |
29 | elfz1eq | |
|
30 | 29 | fveq2d | |
31 | fvsng | |
|
32 | 11 4 31 | sylancr | |
33 | 30 32 | sylan9eqr | |
34 | 33 | csbeq1d | |
35 | 29 | fveq2d | |
36 | fvsng | |
|
37 | 11 5 36 | sylancr | |
38 | 35 37 | sylan9eqr | |
39 | 28 34 38 | 3eqtr4rd | |
40 | 10 12 19 27 39 | fsum | |
41 | 9 40 | eqtrid | |
42 | 15 37 | seq1i | |
43 | 41 42 | eqtrd | |