isumrpcl

Description: The infinite sum of positive reals is positive. (Contributed by Paul Chapman, 9-Feb-2008) (Revised by Mario Carneiro, 24-Apr-2014)

	Ref	Expression
Hypotheses	isumrpcl.1	$⊢ Z = ℤ_{\geq M}$
	isumrpcl.2	$⊢ W = ℤ_{\geq N}$
	isumrpcl.3	$⊢ φ \to N \in Z$
	isumrpcl.4	$⊢ (φ \land k \in Z) \to F (k) = A$
	isumrpcl.5	$⊢ (φ \land k \in Z) \to A \in ℝ^{+}$
	isumrpcl.6	$⊢ φ \to seq M (+ F) \in dom ⇝$
Assertion	isumrpcl	$⊢ φ \to \sum_{k \in W} A \in ℝ^{+}$

Proof

Step	Hyp	Ref	Expression
1		isumrpcl.1	$⊢ Z = ℤ_{\geq M}$
2		isumrpcl.2	$⊢ W = ℤ_{\geq N}$
3		isumrpcl.3	$⊢ φ \to N \in Z$
4		isumrpcl.4	$⊢ (φ \land k \in Z) \to F (k) = A$
5		isumrpcl.5	$⊢ (φ \land k \in Z) \to A \in ℝ^{+}$
6		isumrpcl.6	$⊢ φ \to seq M (+ F) \in dom ⇝$
7	3 1	eleqtrdi	$⊢ φ \to N \in ℤ_{\geq M}$
8		eluzelz	$⊢ N \in ℤ_{\geq M} \to N \in ℤ$
9	7 8	syl	$⊢ φ \to N \in ℤ$
10		uzss	$⊢ N \in ℤ_{\geq M} \to ℤ_{\geq N} \subseteq ℤ_{\geq M}$
11	7 10	syl	$⊢ φ \to ℤ_{\geq N} \subseteq ℤ_{\geq M}$
12	11 2 1	3sstr4g	$⊢ φ \to W \subseteq Z$
13	12	sselda	$⊢ (φ \land k \in W) \to k \in Z$
14	13 4	syldan	$⊢ (φ \land k \in W) \to F (k) = A$
15	5	rpred	$⊢ (φ \land k \in Z) \to A \in ℝ$
16	13 15	syldan	$⊢ (φ \land k \in W) \to A \in ℝ$
17	4 5	eqeltrd	$⊢ (φ \land k \in Z) \to F (k) \in ℝ^{+}$
18	17	rpcnd	$⊢ (φ \land k \in Z) \to F (k) \in ℂ$
19	1 3 18	iserex	$⊢ φ \to (seq M (+ F) \in dom ⇝ \leftrightarrow seq N (+ F) \in dom ⇝)$
20	6 19	mpbid	$⊢ φ \to seq N (+ F) \in dom ⇝$
21	2 9 14 16 20	isumrecl	$⊢ φ \to \sum_{k \in W} A \in ℝ$
22		fveq2	$⊢ k = N \to F (k) = F (N)$
23	22	eleq1d	$⊢ k = N \to (F (k) \in ℝ^{+} \leftrightarrow F (N) \in ℝ^{+})$
24	17	ralrimiva	$⊢ φ \to \forall k \in Z F (k) \in ℝ^{+}$
25	23 24 3	rspcdva	$⊢ φ \to F (N) \in ℝ^{+}$
26		seq1	$⊢ N \in ℤ \to seq N (+ F) (N) = F (N)$
27	9 26	syl	$⊢ φ \to seq N (+ F) (N) = F (N)$
28		uzid	$⊢ N \in ℤ \to N \in ℤ_{\geq N}$
29	9 28	syl	$⊢ φ \to N \in ℤ_{\geq N}$
30	29 2	eleqtrrdi	$⊢ φ \to N \in W$
31	16	recnd	$⊢ (φ \land k \in W) \to A \in ℂ$
32	2 9 14 31 20	isumclim2	$⊢ φ \to seq N (+ F) ⇝ \sum_{k \in W} A$
33	12	sseld	$⊢ φ \to (m \in W \to m \in Z)$
34		fveq2	$⊢ k = m \to F (k) = F (m)$
35	34	eleq1d	$⊢ k = m \to (F (k) \in ℝ^{+} \leftrightarrow F (m) \in ℝ^{+})$
36	35	rspcv	$⊢ m \in Z \to (\forall k \in Z F (k) \in ℝ^{+} \to F (m) \in ℝ^{+})$
37	33 24 36	syl6ci	$⊢ φ \to (m \in W \to F (m) \in ℝ^{+})$
38	37	imp	$⊢ (φ \land m \in W) \to F (m) \in ℝ^{+}$
39	38	rpred	$⊢ (φ \land m \in W) \to F (m) \in ℝ$
40	38	rpge0d	$⊢ (φ \land m \in W) \to 0 \leq F (m)$
41	2 30 32 39 40	climserle	$⊢ φ \to seq N (+ F) (N) \leq \sum_{k \in W} A$
42	27 41	eqbrtrrd	$⊢ φ \to F (N) \leq \sum_{k \in W} A$
43	21 25 42	rpgecld	$⊢ φ \to \sum_{k \in W} A \in ℝ^{+}$

Metamath Proof Explorer

Theorem isumrpcl

Proof