![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > fsumcl | Structured version Unicode version |
Description: Closure of a finite sum
of complex numbers ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
fsumcl.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
fsumcl.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
fsumcl |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssid 3484 |
. . 3
![]() ![]() ![]() ![]() | |
2 | 1 | a1i 11 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | addcl 9476 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | adantl 466 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | fsumcl.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | fsumcl.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 0cnd 9491 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
8 | 2, 4, 5, 6, 7 | fsumcllem 13328 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Copyright terms: Public domain | W3C validator |