Theorem sge0ltfirpmpt2

Description: If the extended sum of nonnegative reals is not +oo , then it can be approximated from below by finite subsums. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	sge0ltfirpmpt2.xph	⊢ Ⅎ 𝑥 𝜑
	sge0ltfirpmpt2.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	sge0ltfirpmpt2.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
	sge0ltfirpmpt2.rp	⊢ ( 𝜑 → 𝑌 ∈ ℝ+ )
	sge0ltfirpmpt2.re	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ )
Assertion	sge0ltfirpmpt2	⊢ ( 𝜑 → ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑥 ∈ 𝑦 𝐵 + 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		sge0ltfirpmpt2.xph	⊢ Ⅎ 𝑥 𝜑
2		sge0ltfirpmpt2.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		sge0ltfirpmpt2.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
4		sge0ltfirpmpt2.rp	⊢ ( 𝜑 → 𝑌 ∈ ℝ+ )
5		sge0ltfirpmpt2.re	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ )
6		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
7	1 3 6	fmptdf	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
8	2 7 4 5	sge0ltfirp	⊢ ( 𝜑 → ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < ( ( Σ^ ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑦 ) ) + 𝑌 ) )
9		simpr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < ( ( Σ^ ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑦 ) ) + 𝑌 ) ) → ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < ( ( Σ^ ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑦 ) ) + 𝑌 ) )
10		elpwinss	⊢ ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑦 ⊆ 𝐴 )
11	10	resmptd	⊢ ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑦 ) = ( 𝑥 ∈ 𝑦 ↦ 𝐵 ) )
12	11	fveq2d	⊢ ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) → ( Σ^ ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑦 ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝑦 ↦ 𝐵 ) ) )
13	12	adantl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( Σ^ ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑦 ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝑦 ↦ 𝐵 ) ) )
14		elinel2	⊢ ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑦 ∈ Fin )
15	14	adantl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑦 ∈ Fin )
16		nfv	⊢ Ⅎ 𝑥 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin )
17	1 16	nfan	⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) )
18		simpll	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑦 ) → 𝜑 )
19	10	sselda	⊢ ( ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑥 ∈ 𝑦 ) → 𝑥 ∈ 𝐴 )
20	19	adantll	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑦 ) → 𝑥 ∈ 𝐴 )
21	1 2 3 5	sge0rernmpt	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,) +∞ ) )
22	18 20 21	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑦 ) → 𝐵 ∈ ( 0 [,) +∞ ) )
23		eqid	⊢ ( 𝑥 ∈ 𝑦 ↦ 𝐵 ) = ( 𝑥 ∈ 𝑦 ↦ 𝐵 )
24	17 22 23	fmptdf	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝑥 ∈ 𝑦 ↦ 𝐵 ) : 𝑦 ⟶ ( 0 [,) +∞ ) )
25	15 24	sge0fsum	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( Σ^ ‘ ( 𝑥 ∈ 𝑦 ↦ 𝐵 ) ) = Σ 𝑘 ∈ 𝑦 ( ( 𝑥 ∈ 𝑦 ↦ 𝐵 ) ‘ 𝑘 ) )
26		simpr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑦 ) → 𝑘 ∈ 𝑦 )
27		simpll	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑦 ) → 𝜑 )
28	10	sselda	⊢ ( ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑘 ∈ 𝑦 ) → 𝑘 ∈ 𝐴 )
29	28	adantll	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑦 ) → 𝑘 ∈ 𝐴 )
30		nfv	⊢ Ⅎ 𝑥 𝑘 ∈ 𝐴
31	1 30	nfan	⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑘 ∈ 𝐴 )
32		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑘 / 𝑥 ⦌ 𝐵
33	32	nfel1	⊢ Ⅎ 𝑥 ⦋ 𝑘 / 𝑥 ⦌ 𝐵 ∈ ( 0 [,) +∞ )
34	31 33	nfim	⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ⦋ 𝑘 / 𝑥 ⦌ 𝐵 ∈ ( 0 [,) +∞ ) )
35		eleq1w	⊢ ( 𝑥 = 𝑘 → ( 𝑥 ∈ 𝐴 ↔ 𝑘 ∈ 𝐴 ) )
36	35	anbi2d	⊢ ( 𝑥 = 𝑘 → ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ) )
37		csbeq1a	⊢ ( 𝑥 = 𝑘 → 𝐵 = ⦋ 𝑘 / 𝑥 ⦌ 𝐵 )
38	37	eleq1d	⊢ ( 𝑥 = 𝑘 → ( 𝐵 ∈ ( 0 [,) +∞ ) ↔ ⦋ 𝑘 / 𝑥 ⦌ 𝐵 ∈ ( 0 [,) +∞ ) ) )
39	36 38	imbi12d	⊢ ( 𝑥 = 𝑘 → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,) +∞ ) ) ↔ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ⦋ 𝑘 / 𝑥 ⦌ 𝐵 ∈ ( 0 [,) +∞ ) ) ) )
40	34 39 21	chvarfv	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ⦋ 𝑘 / 𝑥 ⦌ 𝐵 ∈ ( 0 [,) +∞ ) )
41	27 29 40	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑦 ) → ⦋ 𝑘 / 𝑥 ⦌ 𝐵 ∈ ( 0 [,) +∞ ) )
42		nfcv	⊢ Ⅎ 𝑘 𝐵
43	42 32 37	cbvmpt	⊢ ( 𝑥 ∈ 𝑦 ↦ 𝐵 ) = ( 𝑘 ∈ 𝑦 ↦ ⦋ 𝑘 / 𝑥 ⦌ 𝐵 )
44	43	fvmpt2	⊢ ( ( 𝑘 ∈ 𝑦 ∧ ⦋ 𝑘 / 𝑥 ⦌ 𝐵 ∈ ( 0 [,) +∞ ) ) → ( ( 𝑥 ∈ 𝑦 ↦ 𝐵 ) ‘ 𝑘 ) = ⦋ 𝑘 / 𝑥 ⦌ 𝐵 )
45	26 41 44	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑦 ) → ( ( 𝑥 ∈ 𝑦 ↦ 𝐵 ) ‘ 𝑘 ) = ⦋ 𝑘 / 𝑥 ⦌ 𝐵 )
46	45	sumeq2dv	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Σ 𝑘 ∈ 𝑦 ( ( 𝑥 ∈ 𝑦 ↦ 𝐵 ) ‘ 𝑘 ) = Σ 𝑘 ∈ 𝑦 ⦋ 𝑘 / 𝑥 ⦌ 𝐵 )
47		eqcom	⊢ ( 𝑥 = 𝑘 ↔ 𝑘 = 𝑥 )
48	47	imbi1i	⊢ ( ( 𝑥 = 𝑘 → 𝐵 = ⦋ 𝑘 / 𝑥 ⦌ 𝐵 ) ↔ ( 𝑘 = 𝑥 → 𝐵 = ⦋ 𝑘 / 𝑥 ⦌ 𝐵 ) )
49		eqcom	⊢ ( 𝐵 = ⦋ 𝑘 / 𝑥 ⦌ 𝐵 ↔ ⦋ 𝑘 / 𝑥 ⦌ 𝐵 = 𝐵 )
50	49	imbi2i	⊢ ( ( 𝑘 = 𝑥 → 𝐵 = ⦋ 𝑘 / 𝑥 ⦌ 𝐵 ) ↔ ( 𝑘 = 𝑥 → ⦋ 𝑘 / 𝑥 ⦌ 𝐵 = 𝐵 ) )
51	48 50	bitri	⊢ ( ( 𝑥 = 𝑘 → 𝐵 = ⦋ 𝑘 / 𝑥 ⦌ 𝐵 ) ↔ ( 𝑘 = 𝑥 → ⦋ 𝑘 / 𝑥 ⦌ 𝐵 = 𝐵 ) )
52	37 51	mpbi	⊢ ( 𝑘 = 𝑥 → ⦋ 𝑘 / 𝑥 ⦌ 𝐵 = 𝐵 )
53		nfcv	⊢ Ⅎ 𝑥 𝑦
54		nfcv	⊢ Ⅎ 𝑘 𝑦
55	52 53 54 32 42	cbvsum	⊢ Σ 𝑘 ∈ 𝑦 ⦋ 𝑘 / 𝑥 ⦌ 𝐵 = Σ 𝑥 ∈ 𝑦 𝐵
56	55	a1i	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Σ 𝑘 ∈ 𝑦 ⦋ 𝑘 / 𝑥 ⦌ 𝐵 = Σ 𝑥 ∈ 𝑦 𝐵 )
57	46 56	eqtrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Σ 𝑘 ∈ 𝑦 ( ( 𝑥 ∈ 𝑦 ↦ 𝐵 ) ‘ 𝑘 ) = Σ 𝑥 ∈ 𝑦 𝐵 )
58	13 25 57	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( Σ^ ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑦 ) ) = Σ 𝑥 ∈ 𝑦 𝐵 )
59	58	oveq1d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( Σ^ ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑦 ) ) + 𝑌 ) = ( Σ 𝑥 ∈ 𝑦 𝐵 + 𝑌 ) )
60	59	adantr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < ( ( Σ^ ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑦 ) ) + 𝑌 ) ) → ( ( Σ^ ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑦 ) ) + 𝑌 ) = ( Σ 𝑥 ∈ 𝑦 𝐵 + 𝑌 ) )
61	9 60	breqtrd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < ( ( Σ^ ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑦 ) ) + 𝑌 ) ) → ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑥 ∈ 𝑦 𝐵 + 𝑌 ) )
62	61	ex	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < ( ( Σ^ ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑦 ) ) + 𝑌 ) → ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑥 ∈ 𝑦 𝐵 + 𝑌 ) ) )
63	62	reximdva	⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < ( ( Σ^ ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑦 ) ) + 𝑌 ) → ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑥 ∈ 𝑦 𝐵 + 𝑌 ) ) )
64	8 63	mpd	⊢ ( 𝜑 → ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑥 ∈ 𝑦 𝐵 + 𝑌 ) )