Metamath Proof Explorer


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 k φ
sge0uzfsumgt.h φ K
sge0uzfsumgt.z Z = K
sge0uzfsumgt.b φ k Z B 0 +∞
sge0uzfsumgt.c φ C
sge0uzfsumgt.l φ C < sum^ k Z B
Assertion sge0uzfsumgt φ m Z C < k = K m B

Proof

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