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	$⊢ Ⅎ k φ$
	sge0gtfsumgt.a	$⊢ φ \to A \in V$
	sge0gtfsumgt.b	$⊢ (φ \land k \in A) \to B \in [0, +∞)$
	sge0gtfsumgt.c	$⊢ φ \to C \in ℝ$
	sge0gtfsumgt.l	$⊢ φ \to C < sum^((k \in A ⟼ B))$
Assertion	sge0gtfsumgt	$⊢ φ \to \exists y \in (𝒫 A \cap Fin) C < \sum_{k \in y} B$

Proof

Step	Hyp	Ref	Expression
1		sge0gtfsumgt.k	$⊢ Ⅎ k φ$
2		sge0gtfsumgt.a	$⊢ φ \to A \in V$
3		sge0gtfsumgt.b	$⊢ (φ \land k \in A) \to B \in [0, +∞)$
4		sge0gtfsumgt.c	$⊢ φ \to C \in ℝ$
5		sge0gtfsumgt.l	$⊢ φ \to C < sum^((k \in A ⟼ B))$
6		nfcv	$⊢ \underline{Ⅎ} k sum^$
7		nfmpt1	$⊢ \underline{Ⅎ} k (k \in A ⟼ B)$
8	6 7	nffv	$⊢ \underline{Ⅎ} k sum^((k \in A ⟼ B))$
9		nfcv	$⊢ \underline{Ⅎ} k ℝ$
10	8 9	nfel	$⊢ Ⅎ k sum^((k \in A ⟼ B)) \in ℝ$
11	1 10	nfan	$⊢ Ⅎ k (φ \land sum^((k \in A ⟼ B)) \in ℝ)$
12	2	adantr	$⊢ (φ \land sum^((k \in A ⟼ B)) \in ℝ) \to A \in V$
13		icossicc	$⊢ [0, +∞) \subseteq [0, +∞]$
14	13 3	sselid	$⊢ (φ \land k \in A) \to B \in [0, +∞]$
15	14	adantlr	$⊢ ((φ \land sum^((k \in A ⟼ B)) \in ℝ) \land k \in A) \to B \in [0, +∞]$
16	5	adantr	$⊢ (φ \land sum^((k \in A ⟼ B)) \in ℝ) \to C < sum^((k \in A ⟼ B))$
17	4	adantr	$⊢ (φ \land sum^((k \in A ⟼ B)) \in ℝ) \to C \in ℝ$
18		simpr	$⊢ (φ \land sum^((k \in A ⟼ B)) \in ℝ) \to sum^((k \in A ⟼ B)) \in ℝ$
19		difrp	$⊢ (C \in ℝ \land sum^((k \in A ⟼ B)) \in ℝ) \to (C < sum^((k \in A ⟼ B)) \leftrightarrow sum^((k \in A ⟼ B)) - C \in ℝ^{+})$
20	17 18 19	syl2anc	$⊢ (φ \land sum^((k \in A ⟼ B)) \in ℝ) \to (C < sum^((k \in A ⟼ B)) \leftrightarrow sum^((k \in A ⟼ B)) - C \in ℝ^{+})$
21	16 20	mpbid	$⊢ (φ \land sum^((k \in A ⟼ B)) \in ℝ) \to sum^((k \in A ⟼ B)) - C \in ℝ^{+}$
22	11 12 15 21 18	sge0ltfirpmpt2	$⊢ (φ \land sum^((k \in A ⟼ B)) \in ℝ) \to \exists y \in (𝒫 A \cap Fin) sum^((k \in A ⟼ B)) < \sum_{k \in y} B + sum^((k \in A ⟼ B)) - C$
23		simpr	$⊢ (((φ \land sum^((k \in A ⟼ B)) \in ℝ) \land y \in (𝒫 A \cap Fin)) \land sum^((k \in A ⟼ B)) < \sum_{k \in y} B + sum^((k \in A ⟼ B)) - C) \to sum^((k \in A ⟼ B)) < \sum_{k \in y} B + sum^((k \in A ⟼ B)) - C$
24		nfv	$⊢ Ⅎ k y \in (𝒫 A \cap Fin)$
25	1 24	nfan	$⊢ Ⅎ k (φ \land y \in (𝒫 A \cap Fin))$
26		elinel2	$⊢ y \in (𝒫 A \cap Fin) \to y \in Fin$
27	26	adantl	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to y \in Fin$
28		simpll	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land k \in y) \to φ$
29		elpwinss	$⊢ y \in (𝒫 A \cap Fin) \to y \subseteq A$
30	29	adantr	$⊢ (y \in (𝒫 A \cap Fin) \land k \in y) \to y \subseteq A$
31		simpr	$⊢ (y \in (𝒫 A \cap Fin) \land k \in y) \to k \in y$
32	30 31	sseldd	$⊢ (y \in (𝒫 A \cap Fin) \land k \in y) \to k \in A$
33	32	adantll	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land k \in y) \to k \in A$
34		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
35	34 3	sselid	$⊢ (φ \land k \in A) \to B \in ℝ$
36	28 33 35	syl2anc	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land k \in y) \to B \in ℝ$
37	25 27 36	fsumreclf	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to \sum_{k \in y} B \in ℝ$
38	37	recnd	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to \sum_{k \in y} B \in ℂ$
39	38	ad4ant13	$⊢ (((φ \land sum^((k \in A ⟼ B)) \in ℝ) \land y \in (𝒫 A \cap Fin)) \land sum^((k \in A ⟼ B)) < \sum_{k \in y} B + sum^((k \in A ⟼ B)) - C) \to \sum_{k \in y} B \in ℂ$
40	18	ad2antrr	$⊢ (((φ \land sum^((k \in A ⟼ B)) \in ℝ) \land y \in (𝒫 A \cap Fin)) \land sum^((k \in A ⟼ B)) < \sum_{k \in y} B + sum^((k \in A ⟼ B)) - C) \to sum^((k \in A ⟼ B)) \in ℝ$
41	40	recnd	$⊢ (((φ \land sum^((k \in A ⟼ B)) \in ℝ) \land y \in (𝒫 A \cap Fin)) \land sum^((k \in A ⟼ B)) < \sum_{k \in y} B + sum^((k \in A ⟼ B)) - C) \to sum^((k \in A ⟼ B)) \in ℂ$
42	17	ad2antrr	$⊢ (((φ \land sum^((k \in A ⟼ B)) \in ℝ) \land y \in (𝒫 A \cap Fin)) \land sum^((k \in A ⟼ B)) < \sum_{k \in y} B + sum^((k \in A ⟼ B)) - C) \to C \in ℝ$
43	42	recnd	$⊢ (((φ \land sum^((k \in A ⟼ B)) \in ℝ) \land y \in (𝒫 A \cap Fin)) \land sum^((k \in A ⟼ B)) < \sum_{k \in y} B + sum^((k \in A ⟼ B)) - C) \to C \in ℂ$
44	41 43	subcld	$⊢ (((φ \land sum^((k \in A ⟼ B)) \in ℝ) \land y \in (𝒫 A \cap Fin)) \land sum^((k \in A ⟼ B)) < \sum_{k \in y} B + sum^((k \in A ⟼ B)) - C) \to sum^((k \in A ⟼ B)) - C \in ℂ$
45	39 44	addcomd	$⊢ (((φ \land sum^((k \in A ⟼ B)) \in ℝ) \land y \in (𝒫 A \cap Fin)) \land sum^((k \in A ⟼ B)) < \sum_{k \in y} B + sum^((k \in A ⟼ B)) - C) \to \sum_{k \in y} B + sum^((k \in A ⟼ B)) - C = sum^((k \in A ⟼ B)) - C + \sum_{k \in y} B$
46	23 45	breqtrd	$⊢ (((φ \land sum^((k \in A ⟼ B)) \in ℝ) \land y \in (𝒫 A \cap Fin)) \land sum^((k \in A ⟼ B)) < \sum_{k \in y} B + sum^((k \in A ⟼ B)) - C) \to sum^((k \in A ⟼ B)) < sum^((k \in A ⟼ B)) - C + \sum_{k \in y} B$
47	40 42	resubcld	$⊢ (((φ \land sum^((k \in A ⟼ B)) \in ℝ) \land y \in (𝒫 A \cap Fin)) \land sum^((k \in A ⟼ B)) < \sum_{k \in y} B + sum^((k \in A ⟼ B)) - C) \to sum^((k \in A ⟼ B)) - C \in ℝ$
48	37	ad4ant13	$⊢ (((φ \land sum^((k \in A ⟼ B)) \in ℝ) \land y \in (𝒫 A \cap Fin)) \land sum^((k \in A ⟼ B)) < \sum_{k \in y} B + sum^((k \in A ⟼ B)) - C) \to \sum_{k \in y} B \in ℝ$
49	40 47 48	ltsubadd2d	$⊢ (((φ \land sum^((k \in A ⟼ B)) \in ℝ) \land y \in (𝒫 A \cap Fin)) \land sum^((k \in A ⟼ B)) < \sum_{k \in y} B + sum^((k \in A ⟼ B)) - C) \to (sum^((k \in A ⟼ B)) - (sum^((k \in A ⟼ B)) - C) < \sum_{k \in y} B \leftrightarrow sum^((k \in A ⟼ B)) < sum^((k \in A ⟼ B)) - C + \sum_{k \in y} B)$
50	46 49	mpbird	$⊢ (((φ \land sum^((k \in A ⟼ B)) \in ℝ) \land y \in (𝒫 A \cap Fin)) \land sum^((k \in A ⟼ B)) < \sum_{k \in y} B + sum^((k \in A ⟼ B)) - C) \to sum^((k \in A ⟼ B)) - (sum^((k \in A ⟼ B)) - C) < \sum_{k \in y} B$
51	41 43	nncand	$⊢ (((φ \land sum^((k \in A ⟼ B)) \in ℝ) \land y \in (𝒫 A \cap Fin)) \land sum^((k \in A ⟼ B)) < \sum_{k \in y} B + sum^((k \in A ⟼ B)) - C) \to sum^((k \in A ⟼ B)) - (sum^((k \in A ⟼ B)) - C) = C$
52	51	breq1d	$⊢ (((φ \land sum^((k \in A ⟼ B)) \in ℝ) \land y \in (𝒫 A \cap Fin)) \land sum^((k \in A ⟼ B)) < \sum_{k \in y} B + sum^((k \in A ⟼ B)) - C) \to (sum^((k \in A ⟼ B)) - (sum^((k \in A ⟼ B)) - C) < \sum_{k \in y} B \leftrightarrow C < \sum_{k \in y} B)$
53	50 52	mpbid	$⊢ (((φ \land sum^((k \in A ⟼ B)) \in ℝ) \land y \in (𝒫 A \cap Fin)) \land sum^((k \in A ⟼ B)) < \sum_{k \in y} B + sum^((k \in A ⟼ B)) - C) \to C < \sum_{k \in y} B$
54	53	ex	$⊢ ((φ \land sum^((k \in A ⟼ B)) \in ℝ) \land y \in (𝒫 A \cap Fin)) \to (sum^((k \in A ⟼ B)) < \sum_{k \in y} B + sum^((k \in A ⟼ B)) - C \to C < \sum_{k \in y} B)$
55	54	reximdva	$⊢ (φ \land sum^((k \in A ⟼ B)) \in ℝ) \to (\exists y \in (𝒫 A \cap Fin) sum^((k \in A ⟼ B)) < \sum_{k \in y} B + sum^((k \in A ⟼ B)) - C \to \exists y \in (𝒫 A \cap Fin) C < \sum_{k \in y} B)$
56	22 55	mpd	$⊢ (φ \land sum^((k \in A ⟼ B)) \in ℝ) \to \exists y \in (𝒫 A \cap Fin) C < \sum_{k \in y} B$
57		simpl	$⊢ (φ \land \neg sum^((k \in A ⟼ B)) \in ℝ) \to φ$
58		simpr	$⊢ (φ \land \neg sum^((k \in A ⟼ B)) \in ℝ) \to \neg sum^((k \in A ⟼ B)) \in ℝ$
59		eqid	$⊢ (k \in A ⟼ B) = (k \in A ⟼ B)$
60	1 3 59	fmptdf	$⊢ φ \to (k \in A ⟼ B) : A ⟶ [0, +∞)$
61	13	a1i	$⊢ φ \to [0, +∞) \subseteq [0, +∞]$
62	60 61	fssd	$⊢ φ \to (k \in A ⟼ B) : A ⟶ [0, +∞]$
63	2 62	sge0repnf	$⊢ φ \to (sum^((k \in A ⟼ B)) \in ℝ \leftrightarrow \neg sum^((k \in A ⟼ B)) = +∞)$
64	63	adantr	$⊢ (φ \land \neg sum^((k \in A ⟼ B)) \in ℝ) \to (sum^((k \in A ⟼ B)) \in ℝ \leftrightarrow \neg sum^((k \in A ⟼ B)) = +∞)$
65	58 64	mtbid	$⊢ (φ \land \neg sum^((k \in A ⟼ B)) \in ℝ) \to \neg \neg sum^((k \in A ⟼ B)) = +∞$
66		notnotb	$⊢ sum^((k \in A ⟼ B)) = +∞ \leftrightarrow \neg \neg sum^((k \in A ⟼ B)) = +∞$
67	65 66	sylibr	$⊢ (φ \land \neg sum^((k \in A ⟼ B)) \in ℝ) \to sum^((k \in A ⟼ B)) = +∞$
68	8	nfeq1	$⊢ Ⅎ k sum^((k \in A ⟼ B)) = +∞$
69	1 68	nfan	$⊢ Ⅎ k (φ \land sum^((k \in A ⟼ B)) = +∞)$
70	2	adantr	$⊢ (φ \land sum^((k \in A ⟼ B)) = +∞) \to A \in V$
71	3	adantlr	$⊢ ((φ \land sum^((k \in A ⟼ B)) = +∞) \land k \in A) \to B \in [0, +∞)$
72		simpr	$⊢ (φ \land sum^((k \in A ⟼ B)) = +∞) \to sum^((k \in A ⟼ B)) = +∞$
73	4	adantr	$⊢ (φ \land sum^((k \in A ⟼ B)) = +∞) \to C \in ℝ$
74	69 70 71 72 73	sge0pnffsumgt	$⊢ (φ \land sum^((k \in A ⟼ B)) = +∞) \to \exists y \in (𝒫 A \cap Fin) C < \sum_{k \in y} B$
75	57 67 74	syl2anc	$⊢ (φ \land \neg sum^((k \in A ⟼ B)) \in ℝ) \to \exists y \in (𝒫 A \cap Fin) C < \sum_{k \in y} B$
76	56 75	pm2.61dan	$⊢ φ \to \exists y \in (𝒫 A \cap Fin) C < \sum_{k \in y} B$

Metamath Proof Explorer

Theorem sge0gtfsumgt

Proof