Theorem 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	⊢ Ⅎ 𝑘 𝜑
	sge0uzfsumgt.h	⊢ ( 𝜑 → 𝐾 ∈ ℤ )
	sge0uzfsumgt.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝐾 )
	sge0uzfsumgt.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 ∈ ( 0 [,) +∞ ) )
	sge0uzfsumgt.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
	sge0uzfsumgt.l	⊢ ( 𝜑 → 𝐶 < ( Σ^ ‘ ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ) )
Assertion	sge0uzfsumgt	⊢ ( 𝜑 → ∃ 𝑚 ∈ 𝑍 𝐶 < Σ 𝑘 ∈ ( 𝐾 ... 𝑚 ) 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		sge0uzfsumgt.p	⊢ Ⅎ 𝑘 𝜑
2		sge0uzfsumgt.h	⊢ ( 𝜑 → 𝐾 ∈ ℤ )
3		sge0uzfsumgt.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝐾 )
4		sge0uzfsumgt.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 ∈ ( 0 [,) +∞ ) )
5		sge0uzfsumgt.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
6		sge0uzfsumgt.l	⊢ ( 𝜑 → 𝐶 < ( Σ^ ‘ ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ) )
7	3	fvexi	⊢ 𝑍 ∈ V
8	7	a1i	⊢ ( 𝜑 → 𝑍 ∈ V )
9	1 8 4 5 6	sge0gtfsumgt	⊢ ( 𝜑 → ∃ 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) 𝐶 < Σ 𝑘 ∈ 𝑥 𝐵 )
10	2	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ∧ 𝐶 < Σ 𝑘 ∈ 𝑥 𝐵 ) → 𝐾 ∈ ℤ )
11		elpwinss	⊢ ( 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) → 𝑥 ⊆ 𝑍 )
12	11	3ad2ant2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ∧ 𝐶 < Σ 𝑘 ∈ 𝑥 𝐵 ) → 𝑥 ⊆ 𝑍 )
13		elinel2	⊢ ( 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) → 𝑥 ∈ Fin )
14	13	3ad2ant2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ∧ 𝐶 < Σ 𝑘 ∈ 𝑥 𝐵 ) → 𝑥 ∈ Fin )
15	10 3 12 14	uzfissfz	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ∧ 𝐶 < Σ 𝑘 ∈ 𝑥 𝐵 ) → ∃ 𝑚 ∈ 𝑍 𝑥 ⊆ ( 𝐾 ... 𝑚 ) )
16	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐶 < Σ 𝑘 ∈ 𝑥 𝐵 ) ∧ 𝑥 ⊆ ( 𝐾 ... 𝑚 ) ) → 𝐶 ∈ ℝ )
17		nfv	⊢ Ⅎ 𝑘 𝑥 ⊆ ( 𝐾 ... 𝑚 )
18	1 17	nfan	⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑥 ⊆ ( 𝐾 ... 𝑚 ) )
19		fzfid	⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ( 𝐾 ... 𝑚 ) ) → ( 𝐾 ... 𝑚 ) ∈ Fin )
20		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ( 𝐾 ... 𝑚 ) ) → 𝑥 ⊆ ( 𝐾 ... 𝑚 ) )
21	19 20	ssfid	⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ( 𝐾 ... 𝑚 ) ) → 𝑥 ∈ Fin )
22		simpll	⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ ( 𝐾 ... 𝑚 ) ) ∧ 𝑘 ∈ 𝑥 ) → 𝜑 )
23	20	sselda	⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ ( 𝐾 ... 𝑚 ) ) ∧ 𝑘 ∈ 𝑥 ) → 𝑘 ∈ ( 𝐾 ... 𝑚 ) )
24		rge0ssre	⊢ ( 0 [,) +∞ ) ⊆ ℝ
25		fzssuz	⊢ ( 𝐾 ... 𝑚 ) ⊆ ( ℤ≥ ‘ 𝐾 )
26	25 3	sseqtrri	⊢ ( 𝐾 ... 𝑚 ) ⊆ 𝑍
27		id	⊢ ( 𝑘 ∈ ( 𝐾 ... 𝑚 ) → 𝑘 ∈ ( 𝐾 ... 𝑚 ) )
28	26 27	sselid	⊢ ( 𝑘 ∈ ( 𝐾 ... 𝑚 ) → 𝑘 ∈ 𝑍 )
29	28 4	sylan2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐾 ... 𝑚 ) ) → 𝐵 ∈ ( 0 [,) +∞ ) )
30	24 29	sselid	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐾 ... 𝑚 ) ) → 𝐵 ∈ ℝ )
31	22 23 30	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ ( 𝐾 ... 𝑚 ) ) ∧ 𝑘 ∈ 𝑥 ) → 𝐵 ∈ ℝ )
32	18 21 31	fsumreclf	⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ( 𝐾 ... 𝑚 ) ) → Σ 𝑘 ∈ 𝑥 𝐵 ∈ ℝ )
33	32	adantlr	⊢ ( ( ( 𝜑 ∧ 𝐶 < Σ 𝑘 ∈ 𝑥 𝐵 ) ∧ 𝑥 ⊆ ( 𝐾 ... 𝑚 ) ) → Σ 𝑘 ∈ 𝑥 𝐵 ∈ ℝ )
34		fzfid	⊢ ( 𝜑 → ( 𝐾 ... 𝑚 ) ∈ Fin )
35	1 34 30	fsumreclf	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝐾 ... 𝑚 ) 𝐵 ∈ ℝ )
36	35	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐶 < Σ 𝑘 ∈ 𝑥 𝐵 ) ∧ 𝑥 ⊆ ( 𝐾 ... 𝑚 ) ) → Σ 𝑘 ∈ ( 𝐾 ... 𝑚 ) 𝐵 ∈ ℝ )
37		simplr	⊢ ( ( ( 𝜑 ∧ 𝐶 < Σ 𝑘 ∈ 𝑥 𝐵 ) ∧ 𝑥 ⊆ ( 𝐾 ... 𝑚 ) ) → 𝐶 < Σ 𝑘 ∈ 𝑥 𝐵 )
38	30	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ ( 𝐾 ... 𝑚 ) ) ∧ 𝑘 ∈ ( 𝐾 ... 𝑚 ) ) → 𝐵 ∈ ℝ )
39		0xr	⊢ 0 ∈ ℝ*
40	39	a1i	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐾 ... 𝑚 ) ) → 0 ∈ ℝ* )
41		pnfxr	⊢ +∞ ∈ ℝ*
42	41	a1i	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐾 ... 𝑚 ) ) → +∞ ∈ ℝ* )
43		icogelb	⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → 0 ≤ 𝐵 )
44	40 42 29 43	syl3anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐾 ... 𝑚 ) ) → 0 ≤ 𝐵 )
45	44	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ ( 𝐾 ... 𝑚 ) ) ∧ 𝑘 ∈ ( 𝐾 ... 𝑚 ) ) → 0 ≤ 𝐵 )
46	18 19 38 45 20	fsumlessf	⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ( 𝐾 ... 𝑚 ) ) → Σ 𝑘 ∈ 𝑥 𝐵 ≤ Σ 𝑘 ∈ ( 𝐾 ... 𝑚 ) 𝐵 )
47	46	adantlr	⊢ ( ( ( 𝜑 ∧ 𝐶 < Σ 𝑘 ∈ 𝑥 𝐵 ) ∧ 𝑥 ⊆ ( 𝐾 ... 𝑚 ) ) → Σ 𝑘 ∈ 𝑥 𝐵 ≤ Σ 𝑘 ∈ ( 𝐾 ... 𝑚 ) 𝐵 )
48	16 33 36 37 47	ltletrd	⊢ ( ( ( 𝜑 ∧ 𝐶 < Σ 𝑘 ∈ 𝑥 𝐵 ) ∧ 𝑥 ⊆ ( 𝐾 ... 𝑚 ) ) → 𝐶 < Σ 𝑘 ∈ ( 𝐾 ... 𝑚 ) 𝐵 )
49	48	ex	⊢ ( ( 𝜑 ∧ 𝐶 < Σ 𝑘 ∈ 𝑥 𝐵 ) → ( 𝑥 ⊆ ( 𝐾 ... 𝑚 ) → 𝐶 < Σ 𝑘 ∈ ( 𝐾 ... 𝑚 ) 𝐵 ) )
50	49	adantr	⊢ ( ( ( 𝜑 ∧ 𝐶 < Σ 𝑘 ∈ 𝑥 𝐵 ) ∧ 𝑚 ∈ 𝑍 ) → ( 𝑥 ⊆ ( 𝐾 ... 𝑚 ) → 𝐶 < Σ 𝑘 ∈ ( 𝐾 ... 𝑚 ) 𝐵 ) )
51	50	3adantl2	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ∧ 𝐶 < Σ 𝑘 ∈ 𝑥 𝐵 ) ∧ 𝑚 ∈ 𝑍 ) → ( 𝑥 ⊆ ( 𝐾 ... 𝑚 ) → 𝐶 < Σ 𝑘 ∈ ( 𝐾 ... 𝑚 ) 𝐵 ) )
52	51	reximdva	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ∧ 𝐶 < Σ 𝑘 ∈ 𝑥 𝐵 ) → ( ∃ 𝑚 ∈ 𝑍 𝑥 ⊆ ( 𝐾 ... 𝑚 ) → ∃ 𝑚 ∈ 𝑍 𝐶 < Σ 𝑘 ∈ ( 𝐾 ... 𝑚 ) 𝐵 ) )
53	15 52	mpd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ∧ 𝐶 < Σ 𝑘 ∈ 𝑥 𝐵 ) → ∃ 𝑚 ∈ 𝑍 𝐶 < Σ 𝑘 ∈ ( 𝐾 ... 𝑚 ) 𝐵 )
54	53	3exp	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) → ( 𝐶 < Σ 𝑘 ∈ 𝑥 𝐵 → ∃ 𝑚 ∈ 𝑍 𝐶 < Σ 𝑘 ∈ ( 𝐾 ... 𝑚 ) 𝐵 ) ) )
55	54	rexlimdv	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) 𝐶 < Σ 𝑘 ∈ 𝑥 𝐵 → ∃ 𝑚 ∈ 𝑍 𝐶 < Σ 𝑘 ∈ ( 𝐾 ... 𝑚 ) 𝐵 ) )
56	9 55	mpd	⊢ ( 𝜑 → ∃ 𝑚 ∈ 𝑍 𝐶 < Σ 𝑘 ∈ ( 𝐾 ... 𝑚 ) 𝐵 )