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	⊢ 𝑍 = ( ℤ_≥ ‘ 𝑀 )
	isumrpcl.2	⊢ 𝑊 = ( ℤ_≥ ‘ 𝑁 )
	isumrpcl.3	⊢ ( 𝜑 → 𝑁 ∈ 𝑍 )
	isumrpcl.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
	isumrpcl.5	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℝ⁺ )
	isumrpcl.6	⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
Assertion	isumrpcl	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝑊 𝐴 ∈ ℝ⁺ )

Proof

Step	Hyp	Ref	Expression
1		isumrpcl.1	⊢ 𝑍 = ( ℤ_≥ ‘ 𝑀 )
2		isumrpcl.2	⊢ 𝑊 = ( ℤ_≥ ‘ 𝑁 )
3		isumrpcl.3	⊢ ( 𝜑 → 𝑁 ∈ 𝑍 )
4		isumrpcl.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
5		isumrpcl.5	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℝ⁺ )
6		isumrpcl.6	⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
7	3 1	eleqtrdi	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ_≥ ‘ 𝑀 ) )
8		eluzelz	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 𝑀 ) → 𝑁 ∈ ℤ )
9	7 8	syl	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
10		uzss	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 𝑀 ) → ( ℤ_≥ ‘ 𝑁 ) ⊆ ( ℤ_≥ ‘ 𝑀 ) )
11	7 10	syl	⊢ ( 𝜑 → ( ℤ_≥ ‘ 𝑁 ) ⊆ ( ℤ_≥ ‘ 𝑀 ) )
12	11 2 1	3sstr4g	⊢ ( 𝜑 → 𝑊 ⊆ 𝑍 )
13	12	sselda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → 𝑘 ∈ 𝑍 )
14	13 4	syldan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
15	5	rpred	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℝ )
16	13 15	syldan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → 𝐴 ∈ ℝ )
17	4 5	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ⁺ )
18	17	rpcnd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
19	1 3 18	iserex	⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ ↔ seq 𝑁 ( + , 𝐹 ) ∈ dom ⇝ ) )
20	6 19	mpbid	⊢ ( 𝜑 → seq 𝑁 ( + , 𝐹 ) ∈ dom ⇝ )
21	2 9 14 16 20	isumrecl	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝑊 𝐴 ∈ ℝ )
22		fveq2	⊢ ( 𝑘 = 𝑁 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑁 ) )
23	22	eleq1d	⊢ ( 𝑘 = 𝑁 → ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ⁺ ↔ ( 𝐹 ‘ 𝑁 ) ∈ ℝ⁺ ) )
24	17	ralrimiva	⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝑍 ( 𝐹 ‘ 𝑘 ) ∈ ℝ⁺ )
25	23 24 3	rspcdva	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑁 ) ∈ ℝ⁺ )
26		seq1	⊢ ( 𝑁 ∈ ℤ → ( seq 𝑁 ( + , 𝐹 ) ‘ 𝑁 ) = ( 𝐹 ‘ 𝑁 ) )
27	9 26	syl	⊢ ( 𝜑 → ( seq 𝑁 ( + , 𝐹 ) ‘ 𝑁 ) = ( 𝐹 ‘ 𝑁 ) )
28		uzid	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ( ℤ_≥ ‘ 𝑁 ) )
29	9 28	syl	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ_≥ ‘ 𝑁 ) )
30	29 2	eleqtrrdi	⊢ ( 𝜑 → 𝑁 ∈ 𝑊 )
31	16	recnd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → 𝐴 ∈ ℂ )
32	2 9 14 31 20	isumclim2	⊢ ( 𝜑 → seq 𝑁 ( + , 𝐹 ) ⇝ Σ 𝑘 ∈ 𝑊 𝐴 )
33	12	sseld	⊢ ( 𝜑 → ( 𝑚 ∈ 𝑊 → 𝑚 ∈ 𝑍 ) )
34		fveq2	⊢ ( 𝑘 = 𝑚 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑚 ) )
35	34	eleq1d	⊢ ( 𝑘 = 𝑚 → ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ⁺ ↔ ( 𝐹 ‘ 𝑚 ) ∈ ℝ⁺ ) )
36	35	rspcv	⊢ ( 𝑚 ∈ 𝑍 → ( ∀ 𝑘 ∈ 𝑍 ( 𝐹 ‘ 𝑘 ) ∈ ℝ⁺ → ( 𝐹 ‘ 𝑚 ) ∈ ℝ⁺ ) )
37	33 24 36	syl6ci	⊢ ( 𝜑 → ( 𝑚 ∈ 𝑊 → ( 𝐹 ‘ 𝑚 ) ∈ ℝ⁺ ) )
38	37	imp	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑊 ) → ( 𝐹 ‘ 𝑚 ) ∈ ℝ⁺ )
39	38	rpred	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑊 ) → ( 𝐹 ‘ 𝑚 ) ∈ ℝ )
40	38	rpge0d	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑊 ) → 0 ≤ ( 𝐹 ‘ 𝑚 ) )
41	2 30 32 39 40	climserle	⊢ ( 𝜑 → ( seq 𝑁 ( + , 𝐹 ) ‘ 𝑁 ) ≤ Σ 𝑘 ∈ 𝑊 𝐴 )
42	27 41	eqbrtrrd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑁 ) ≤ Σ 𝑘 ∈ 𝑊 𝐴 )
43	21 25 42	rpgecld	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝑊 𝐴 ∈ ℝ⁺ )

Metamath Proof Explorer

Theorem isumrpcl

Proof