Theorem sge0gtfsumgt

Description: If the generalized sum of nonnegative reals is larger than a given number, then that number can be dominated by a finite subsum. (Contributed by Glauco Siliprandi, 21-Nov-2020)

	Ref	Expression
Hypotheses	sge0gtfsumgt.k	⊢ Ⅎ 𝑘 𝜑
	sge0gtfsumgt.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	sge0gtfsumgt.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,) +∞ ) )
	sge0gtfsumgt.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
	sge0gtfsumgt.l	⊢ ( 𝜑 → 𝐶 < ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) )
Assertion	sge0gtfsumgt	⊢ ( 𝜑 → ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝐶 < Σ 𝑘 ∈ 𝑦 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		sge0gtfsumgt.k	⊢ Ⅎ 𝑘 𝜑
2		sge0gtfsumgt.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		sge0gtfsumgt.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,) +∞ ) )
4		sge0gtfsumgt.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
5		sge0gtfsumgt.l	⊢ ( 𝜑 → 𝐶 < ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) )
6		nfcv	⊢ Ⅎ 𝑘 Σ^
7		nfmpt1	⊢ Ⅎ 𝑘 ( 𝑘 ∈ 𝐴 ↦ 𝐵 )
8	6 7	nffv	⊢ Ⅎ 𝑘 ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) )
9		nfcv	⊢ Ⅎ 𝑘 ℝ
10	8 9	nfel	⊢ Ⅎ 𝑘 ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ
11	1 10	nfan	⊢ Ⅎ 𝑘 ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ )
12	2	adantr	⊢ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ ) → 𝐴 ∈ 𝑉 )
13		icossicc	⊢ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ )
14	13 3	sseldi	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
15	14	adantlr	⊢ ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ ) ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
16	5	adantr	⊢ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ ) → 𝐶 < ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) )
17	4	adantr	⊢ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ ) → 𝐶 ∈ ℝ )
18		simpr	⊢ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ ) → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ )
19		difrp	⊢ ( ( 𝐶 ∈ ℝ ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ ) → ( 𝐶 < ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ↔ ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) − 𝐶 ) ∈ ℝ+ ) )
20	17 18 19	syl2anc	⊢ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ ) → ( 𝐶 < ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ↔ ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) − 𝐶 ) ∈ ℝ+ ) )
21	16 20	mpbid	⊢ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ ) → ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) − 𝐶 ) ∈ ℝ+ )
22	11 12 15 21 18	sge0ltfirpmpt2	⊢ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ ) → ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑦 𝐵 + ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) − 𝐶 ) ) )
23		simpr	⊢ ( ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑦 𝐵 + ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) − 𝐶 ) ) ) → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑦 𝐵 + ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) − 𝐶 ) ) )
24		nfv	⊢ Ⅎ 𝑘 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin )
25	1 24	nfan	⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) )
26		elinel2	⊢ ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑦 ∈ Fin )
27	26	adantl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑦 ∈ Fin )
28		simpll	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑦 ) → 𝜑 )
29		elpwinss	⊢ ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑦 ⊆ 𝐴 )
30	29	adantr	⊢ ( ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑘 ∈ 𝑦 ) → 𝑦 ⊆ 𝐴 )
31		simpr	⊢ ( ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑘 ∈ 𝑦 ) → 𝑘 ∈ 𝑦 )
32	30 31	sseldd	⊢ ( ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑘 ∈ 𝑦 ) → 𝑘 ∈ 𝐴 )
33	32	adantll	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑦 ) → 𝑘 ∈ 𝐴 )
34		rge0ssre	⊢ ( 0 [,) +∞ ) ⊆ ℝ
35	34 3	sseldi	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
36	28 33 35	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑦 ) → 𝐵 ∈ ℝ )
37	25 27 36	fsumreclf	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Σ 𝑘 ∈ 𝑦 𝐵 ∈ ℝ )
38	37	recnd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Σ 𝑘 ∈ 𝑦 𝐵 ∈ ℂ )
39	38	ad4ant13	⊢ ( ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑦 𝐵 + ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) − 𝐶 ) ) ) → Σ 𝑘 ∈ 𝑦 𝐵 ∈ ℂ )
40	18	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑦 𝐵 + ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) − 𝐶 ) ) ) → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ )
41	40	recnd	⊢ ( ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑦 𝐵 + ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) − 𝐶 ) ) ) → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℂ )
42	17	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑦 𝐵 + ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) − 𝐶 ) ) ) → 𝐶 ∈ ℝ )
43	42	recnd	⊢ ( ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑦 𝐵 + ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) − 𝐶 ) ) ) → 𝐶 ∈ ℂ )
44	41 43	subcld	⊢ ( ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑦 𝐵 + ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) − 𝐶 ) ) ) → ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) − 𝐶 ) ∈ ℂ )
45	39 44	addcomd	⊢ ( ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑦 𝐵 + ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) − 𝐶 ) ) ) → ( Σ 𝑘 ∈ 𝑦 𝐵 + ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) − 𝐶 ) ) = ( ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) − 𝐶 ) + Σ 𝑘 ∈ 𝑦 𝐵 ) )
46	23 45	breqtrd	⊢ ( ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑦 𝐵 + ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) − 𝐶 ) ) ) → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) − 𝐶 ) + Σ 𝑘 ∈ 𝑦 𝐵 ) )
47	40 42	resubcld	⊢ ( ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑦 𝐵 + ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) − 𝐶 ) ) ) → ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) − 𝐶 ) ∈ ℝ )
48	37	ad4ant13	⊢ ( ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑦 𝐵 + ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) − 𝐶 ) ) ) → Σ 𝑘 ∈ 𝑦 𝐵 ∈ ℝ )
49	40 47 48	ltsubadd2d	⊢ ( ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑦 𝐵 + ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) − 𝐶 ) ) ) → ( ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) − ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) − 𝐶 ) ) < Σ 𝑘 ∈ 𝑦 𝐵 ↔ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) − 𝐶 ) + Σ 𝑘 ∈ 𝑦 𝐵 ) ) )
50	46 49	mpbird	⊢ ( ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑦 𝐵 + ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) − 𝐶 ) ) ) → ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) − ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) − 𝐶 ) ) < Σ 𝑘 ∈ 𝑦 𝐵 )
51	41 43	nncand	⊢ ( ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑦 𝐵 + ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) − 𝐶 ) ) ) → ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) − ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) − 𝐶 ) ) = 𝐶 )
52	51	breq1d	⊢ ( ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑦 𝐵 + ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) − 𝐶 ) ) ) → ( ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) − ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) − 𝐶 ) ) < Σ 𝑘 ∈ 𝑦 𝐵 ↔ 𝐶 < Σ 𝑘 ∈ 𝑦 𝐵 ) )
53	50 52	mpbid	⊢ ( ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑦 𝐵 + ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) − 𝐶 ) ) ) → 𝐶 < Σ 𝑘 ∈ 𝑦 𝐵 )
54	53	ex	⊢ ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑦 𝐵 + ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) − 𝐶 ) ) → 𝐶 < Σ 𝑘 ∈ 𝑦 𝐵 ) )
55	54	reximdva	⊢ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ ) → ( ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) < ( Σ 𝑘 ∈ 𝑦 𝐵 + ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) − 𝐶 ) ) → ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝐶 < Σ 𝑘 ∈ 𝑦 𝐵 ) )
56	22 55	mpd	⊢ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ ) → ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝐶 < Σ 𝑘 ∈ 𝑦 𝐵 )
57		simpl	⊢ ( ( 𝜑 ∧ ¬ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ ) → 𝜑 )
58		simpr	⊢ ( ( 𝜑 ∧ ¬ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ ) → ¬ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ )
59		eqid	⊢ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑘 ∈ 𝐴 ↦ 𝐵 )
60	1 3 59	fmptdf	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ( 0 [,) +∞ ) )
61	13	a1i	⊢ ( 𝜑 → ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ ) )
62	60 61	fssd	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
63	2 62	sge0repnf	⊢ ( 𝜑 → ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ ↔ ¬ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = +∞ ) )
64	63	adantr	⊢ ( ( 𝜑 ∧ ¬ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ ) → ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ ↔ ¬ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = +∞ ) )
65	58 64	mtbid	⊢ ( ( 𝜑 ∧ ¬ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ ) → ¬ ¬ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = +∞ )
66		notnotb	⊢ ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = +∞ ↔ ¬ ¬ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = +∞ )
67	65 66	sylibr	⊢ ( ( 𝜑 ∧ ¬ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ ) → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = +∞ )
68	8	nfeq1	⊢ Ⅎ 𝑘 ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = +∞
69	1 68	nfan	⊢ Ⅎ 𝑘 ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = +∞ )
70	2	adantr	⊢ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = +∞ ) → 𝐴 ∈ 𝑉 )
71	3	adantlr	⊢ ( ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = +∞ ) ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,) +∞ ) )
72		simpr	⊢ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = +∞ ) → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = +∞ )
73	4	adantr	⊢ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = +∞ ) → 𝐶 ∈ ℝ )
74	69 70 71 72 73	sge0pnffsumgt	⊢ ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = +∞ ) → ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝐶 < Σ 𝑘 ∈ 𝑦 𝐵 )
75	57 67 74	syl2anc	⊢ ( ( 𝜑 ∧ ¬ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ ) → ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝐶 < Σ 𝑘 ∈ 𝑦 𝐵 )
76	56 75	pm2.61dan	⊢ ( 𝜑 → ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝐶 < Σ 𝑘 ∈ 𝑦 𝐵 )