sge0uzfsumgt

Description: If a real number is smaller than a generalized sum of nonnegative reals, then it is smaller than some finite subsum. (Contributed by Glauco Siliprandi, 21-Nov-2020)

	Ref	Expression
Hypotheses	sge0uzfsumgt.p	$⊢ Ⅎ k φ$
	sge0uzfsumgt.h	$⊢ φ \to K \in ℤ$
	sge0uzfsumgt.z	$⊢ Z = ℤ_{\geq K}$
	sge0uzfsumgt.b	$⊢ (φ \land k \in Z) \to B \in [0, +∞)$
	sge0uzfsumgt.c	$⊢ φ \to C \in ℝ$
	sge0uzfsumgt.l	$⊢ φ \to C < sum^((k \in Z ⟼ B))$
Assertion	sge0uzfsumgt	$⊢ φ \to \exists m \in Z C < \sum_{k = K}^{m} B$

Proof

Step	Hyp	Ref	Expression
1		sge0uzfsumgt.p	$⊢ Ⅎ k φ$
2		sge0uzfsumgt.h	$⊢ φ \to K \in ℤ$
3		sge0uzfsumgt.z	$⊢ Z = ℤ_{\geq K}$
4		sge0uzfsumgt.b	$⊢ (φ \land k \in Z) \to B \in [0, +∞)$
5		sge0uzfsumgt.c	$⊢ φ \to C \in ℝ$
6		sge0uzfsumgt.l	$⊢ φ \to C < sum^((k \in Z ⟼ B))$
7	3	fvexi	$⊢ Z \in V$
8	7	a1i	$⊢ φ \to Z \in V$
9	1 8 4 5 6	sge0gtfsumgt	$⊢ φ \to \exists x \in (𝒫 Z \cap Fin) C < \sum_{k \in x} B$
10	2	3ad2ant1	$⊢ (φ \land x \in (𝒫 Z \cap Fin) \land C < \sum_{k \in x} B) \to K \in ℤ$
11		elpwinss	$⊢ x \in (𝒫 Z \cap Fin) \to x \subseteq Z$
12	11	3ad2ant2	$⊢ (φ \land x \in (𝒫 Z \cap Fin) \land C < \sum_{k \in x} B) \to x \subseteq Z$
13		elinel2	$⊢ x \in (𝒫 Z \cap Fin) \to x \in Fin$
14	13	3ad2ant2	$⊢ (φ \land x \in (𝒫 Z \cap Fin) \land C < \sum_{k \in x} B) \to x \in Fin$
15	10 3 12 14	uzfissfz	$⊢ (φ \land x \in (𝒫 Z \cap Fin) \land C < \sum_{k \in x} B) \to \exists m \in Z x \subseteq (K \dots m)$
16	5	ad2antrr	$⊢ ((φ \land C < \sum_{k \in x} B) \land x \subseteq (K \dots m)) \to C \in ℝ$
17		nfv	$⊢ Ⅎ k x \subseteq (K \dots m)$
18	1 17	nfan	$⊢ Ⅎ k (φ \land x \subseteq (K \dots m))$
19		fzfid	$⊢ (φ \land x \subseteq (K \dots m)) \to (K \dots m) \in Fin$
20		simpr	$⊢ (φ \land x \subseteq (K \dots m)) \to x \subseteq (K \dots m)$
21	19 20	ssfid	$⊢ (φ \land x \subseteq (K \dots m)) \to x \in Fin$
22		simpll	$⊢ ((φ \land x \subseteq (K \dots m)) \land k \in x) \to φ$
23	20	sselda	$⊢ ((φ \land x \subseteq (K \dots m)) \land k \in x) \to k \in (K \dots m)$
24		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
25		fzssuz	$⊢ (K \dots m) \subseteq ℤ_{\geq K}$
26	25 3	sseqtrri	$⊢ (K \dots m) \subseteq Z$
27		id	$⊢ k \in (K \dots m) \to k \in (K \dots m)$
28	26 27	sseldi	$⊢ k \in (K \dots m) \to k \in Z$
29	28 4	sylan2	$⊢ (φ \land k \in (K \dots m)) \to B \in [0, +∞)$
30	24 29	sseldi	$⊢ (φ \land k \in (K \dots m)) \to B \in ℝ$
31	22 23 30	syl2anc	$⊢ ((φ \land x \subseteq (K \dots m)) \land k \in x) \to B \in ℝ$
32	18 21 31	fsumreclf	$⊢ (φ \land x \subseteq (K \dots m)) \to \sum_{k \in x} B \in ℝ$
33	32	adantlr	$⊢ ((φ \land C < \sum_{k \in x} B) \land x \subseteq (K \dots m)) \to \sum_{k \in x} B \in ℝ$
34		fzfid	$⊢ φ \to (K \dots m) \in Fin$
35	1 34 30	fsumreclf	$⊢ φ \to \sum_{k = K}^{m} B \in ℝ$
36	35	ad2antrr	$⊢ ((φ \land C < \sum_{k \in x} B) \land x \subseteq (K \dots m)) \to \sum_{k = K}^{m} B \in ℝ$
37		simplr	$⊢ ((φ \land C < \sum_{k \in x} B) \land x \subseteq (K \dots m)) \to C < \sum_{k \in x} B$
38	30	adantlr	$⊢ ((φ \land x \subseteq (K \dots m)) \land k \in (K \dots m)) \to B \in ℝ$
39		0xr	$⊢ 0 \in ℝ^{*}$
40	39	a1i	$⊢ (φ \land k \in (K \dots m)) \to 0 \in ℝ^{*}$
41		pnfxr	$⊢ +∞ \in ℝ^{*}$
42	41	a1i	$⊢ (φ \land k \in (K \dots m)) \to +∞ \in ℝ^{*}$
43		icogelb	$⊢ (0 \in ℝ^{} \land +∞ \in ℝ^{} \land B \in [0, +∞)) \to 0 \leq B$
44	40 42 29 43	syl3anc	$⊢ (φ \land k \in (K \dots m)) \to 0 \leq B$
45	44	adantlr	$⊢ ((φ \land x \subseteq (K \dots m)) \land k \in (K \dots m)) \to 0 \leq B$
46	18 19 38 45 20	fsumlessf	$⊢ (φ \land x \subseteq (K \dots m)) \to \sum_{k \in x} B \leq \sum_{k = K}^{m} B$
47	46	adantlr	$⊢ ((φ \land C < \sum_{k \in x} B) \land x \subseteq (K \dots m)) \to \sum_{k \in x} B \leq \sum_{k = K}^{m} B$
48	16 33 36 37 47	ltletrd	$⊢ ((φ \land C < \sum_{k \in x} B) \land x \subseteq (K \dots m)) \to C < \sum_{k = K}^{m} B$
49	48	ex	$⊢ (φ \land C < \sum_{k \in x} B) \to (x \subseteq (K \dots m) \to C < \sum_{k = K}^{m} B)$
50	49	adantr	$⊢ ((φ \land C < \sum_{k \in x} B) \land m \in Z) \to (x \subseteq (K \dots m) \to C < \sum_{k = K}^{m} B)$
51	50	3adantl2	$⊢ ((φ \land x \in (𝒫 Z \cap Fin) \land C < \sum_{k \in x} B) \land m \in Z) \to (x \subseteq (K \dots m) \to C < \sum_{k = K}^{m} B)$
52	51	reximdva	$⊢ (φ \land x \in (𝒫 Z \cap Fin) \land C < \sum_{k \in x} B) \to (\exists m \in Z x \subseteq (K \dots m) \to \exists m \in Z C < \sum_{k = K}^{m} B)$
53	15 52	mpd	$⊢ (φ \land x \in (𝒫 Z \cap Fin) \land C < \sum_{k \in x} B) \to \exists m \in Z C < \sum_{k = K}^{m} B$
54	53	3exp	$⊢ φ \to (x \in (𝒫 Z \cap Fin) \to (C < \sum_{k \in x} B \to \exists m \in Z C < \sum_{k = K}^{m} B))$
55	54	rexlimdv	$⊢ φ \to (\exists x \in (𝒫 Z \cap Fin) C < \sum_{k \in x} B \to \exists m \in Z C < \sum_{k = K}^{m} B)$
56	9 55	mpd	$⊢ φ \to \exists m \in Z C < \sum_{k = K}^{m} B$

Metamath Proof Explorer

Theorem sge0uzfsumgt

Proof