# Metamath Proof Explorer

## Theorem fsumnncl

Description: Closure of a nonempty, finite sum of positive integers. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses fsumnncl.an0 ${⊢}{\phi }\to {A}\ne \varnothing$
fsumnncl.afi ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
fsumnncl.b ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in ℕ$
Assertion fsumnncl ${⊢}{\phi }\to \sum _{{k}\in {A}}{B}\in ℕ$

### Proof

Step Hyp Ref Expression
1 fsumnncl.an0 ${⊢}{\phi }\to {A}\ne \varnothing$
2 fsumnncl.afi ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
3 fsumnncl.b ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in ℕ$
4 3 nnnn0d ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in {ℕ}_{0}$
5 2 4 fsumnn0cl ${⊢}{\phi }\to \sum _{{k}\in {A}}{B}\in {ℕ}_{0}$
6 n0 ${⊢}{A}\ne \varnothing ↔\exists {j}\phantom{\rule{.4em}{0ex}}{j}\in {A}$
7 1 6 sylib ${⊢}{\phi }\to \exists {j}\phantom{\rule{.4em}{0ex}}{j}\in {A}$
8 0red ${⊢}\left({\phi }\wedge {j}\in {A}\right)\to 0\in ℝ$
9 nfv ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {j}\in {A}\right)$
10 nfcsb1v
11 10 nfel1
12 9 11 nfim
13 eleq1w ${⊢}{k}={j}\to \left({k}\in {A}↔{j}\in {A}\right)$
14 13 anbi2d ${⊢}{k}={j}\to \left(\left({\phi }\wedge {k}\in {A}\right)↔\left({\phi }\wedge {j}\in {A}\right)\right)$
15 csbeq1a
16 15 eleq1d
17 14 16 imbi12d
18 12 17 3 chvarfv
19 18 nnred
21 diffi ${⊢}{A}\in \mathrm{Fin}\to {A}\setminus \left\{{j}\right\}\in \mathrm{Fin}$
22 2 21 syl ${⊢}{\phi }\to {A}\setminus \left\{{j}\right\}\in \mathrm{Fin}$
23 eldifi ${⊢}{k}\in \left({A}\setminus \left\{{j}\right\}\right)\to {k}\in {A}$
24 23 adantl ${⊢}\left({\phi }\wedge {k}\in \left({A}\setminus \left\{{j}\right\}\right)\right)\to {k}\in {A}$
25 24 4 syldan ${⊢}\left({\phi }\wedge {k}\in \left({A}\setminus \left\{{j}\right\}\right)\right)\to {B}\in {ℕ}_{0}$
26 22 25 fsumnn0cl ${⊢}{\phi }\to \sum _{{k}\in {A}\setminus \left\{{j}\right\}}{B}\in {ℕ}_{0}$
27 26 nn0red ${⊢}{\phi }\to \sum _{{k}\in {A}\setminus \left\{{j}\right\}}{B}\in ℝ$
28 27 adantr ${⊢}\left({\phi }\wedge {j}\in {A}\right)\to \sum _{{k}\in {A}\setminus \left\{{j}\right\}}{B}\in ℝ$
30 18 nnrpd
32 26 nn0ge0d ${⊢}{\phi }\to 0\le \sum _{{k}\in {A}\setminus \left\{{j}\right\}}{B}$
33 32 adantr ${⊢}\left({\phi }\wedge {j}\in {A}\right)\to 0\le \sum _{{k}\in {A}\setminus \left\{{j}\right\}}{B}$
34 8 28 19 33 leadd1dd
35 8 20 29 31 34 ltletrd
36 difsnid ${⊢}{j}\in {A}\to \left({A}\setminus \left\{{j}\right\}\right)\cup \left\{{j}\right\}={A}$
37 36 adantl ${⊢}\left({\phi }\wedge {j}\in {A}\right)\to \left({A}\setminus \left\{{j}\right\}\right)\cup \left\{{j}\right\}={A}$
38 37 eqcomd ${⊢}\left({\phi }\wedge {j}\in {A}\right)\to {A}=\left({A}\setminus \left\{{j}\right\}\right)\cup \left\{{j}\right\}$
39 38 sumeq1d ${⊢}\left({\phi }\wedge {j}\in {A}\right)\to \sum _{{k}\in {A}}{B}=\sum _{{k}\in \left({A}\setminus \left\{{j}\right\}\right)\cup \left\{{j}\right\}}{B}$
40 22 adantr ${⊢}\left({\phi }\wedge {j}\in {A}\right)\to {A}\setminus \left\{{j}\right\}\in \mathrm{Fin}$
41 simpr ${⊢}\left({\phi }\wedge {j}\in {A}\right)\to {j}\in {A}$
42 neldifsnd ${⊢}\left({\phi }\wedge {j}\in {A}\right)\to ¬{j}\in \left({A}\setminus \left\{{j}\right\}\right)$
43 simpl ${⊢}\left({\phi }\wedge {k}\in \left({A}\setminus \left\{{j}\right\}\right)\right)\to {\phi }$
44 43 24 3 syl2anc ${⊢}\left({\phi }\wedge {k}\in \left({A}\setminus \left\{{j}\right\}\right)\right)\to {B}\in ℕ$
45 44 nncnd ${⊢}\left({\phi }\wedge {k}\in \left({A}\setminus \left\{{j}\right\}\right)\right)\to {B}\in ℂ$
46 45 adantlr ${⊢}\left(\left({\phi }\wedge {j}\in {A}\right)\wedge {k}\in \left({A}\setminus \left\{{j}\right\}\right)\right)\to {B}\in ℂ$
47 nnsscn ${⊢}ℕ\subseteq ℂ$
48 47 a1i ${⊢}\left({\phi }\wedge {j}\in {A}\right)\to ℕ\subseteq ℂ$
49 48 18 sseldd
50 9 10 40 41 42 46 15 49 fsumsplitsn
51 39 50 eqtr2d
52 35 51 breqtrd ${⊢}\left({\phi }\wedge {j}\in {A}\right)\to 0<\sum _{{k}\in {A}}{B}$
53 52 ex ${⊢}{\phi }\to \left({j}\in {A}\to 0<\sum _{{k}\in {A}}{B}\right)$
54 53 exlimdv ${⊢}{\phi }\to \left(\exists {j}\phantom{\rule{.4em}{0ex}}{j}\in {A}\to 0<\sum _{{k}\in {A}}{B}\right)$
55 7 54 mpd ${⊢}{\phi }\to 0<\sum _{{k}\in {A}}{B}$
56 5 55 jca ${⊢}{\phi }\to \left(\sum _{{k}\in {A}}{B}\in {ℕ}_{0}\wedge 0<\sum _{{k}\in {A}}{B}\right)$
57 elnnnn0b ${⊢}\sum _{{k}\in {A}}{B}\in ℕ↔\left(\sum _{{k}\in {A}}{B}\in {ℕ}_{0}\wedge 0<\sum _{{k}\in {A}}{B}\right)$
58 56 57 sylibr ${⊢}{\phi }\to \sum _{{k}\in {A}}{B}\in ℕ$