fsumnncl

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

	Ref	Expression
Hypotheses	fsumnncl.an0	$⊢ φ \to A \neq \emptyset$
	fsumnncl.afi	$⊢ φ \to A \in Fin$
	fsumnncl.b	$⊢ (φ \land k \in A) \to B \in ℕ$
Assertion	fsumnncl	$⊢ φ \to \sum_{k \in A} B \in ℕ$

Proof

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

Metamath Proof Explorer

Theorem fsumnncl

Proof