Description: A sum of nonnegative extended reals is smaller than a given extended real if and only if every finite subsum is smaller than it. (Contributed by Glauco Siliprandi, 17-Aug-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | sge0lefi.1 | |
|
sge0lefi.2 | |
||
sge0lefi.3 | |
||
Assertion | sge0lefi | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sge0lefi.1 | |
|
2 | sge0lefi.2 | |
|
3 | sge0lefi.3 | |
|
4 | simpr | |
|
5 | 2 | adantr | |
6 | elpwinss | |
|
7 | 6 | adantl | |
8 | 5 7 | fssresd | |
9 | 4 8 | sge0xrcl | |
10 | 9 | adantlr | |
11 | 1 2 | sge0xrcl | |
12 | 11 | ad2antrr | |
13 | 3 | ad2antrr | |
14 | 1 | adantr | |
15 | 14 5 | sge0less | |
16 | 15 | adantlr | |
17 | simplr | |
|
18 | 10 12 13 16 17 | xrletrd | |
19 | 18 | ralrimiva | |
20 | 19 | ex | |
21 | 1 2 | sge0sup | |
22 | 21 | adantr | |
23 | vex | |
|
24 | eqid | |
|
25 | 24 | elrnmpt | |
26 | 23 25 | ax-mp | |
27 | 26 | biimpi | |
28 | 27 | adantl | |
29 | nfv | |
|
30 | nfra1 | |
|
31 | 29 30 | nfan | |
32 | nfcv | |
|
33 | nfmpt1 | |
|
34 | 33 | nfrn | |
35 | 32 34 | nfel | |
36 | 31 35 | nfan | |
37 | nfv | |
|
38 | simp3 | |
|
39 | rspa | |
|
40 | 39 | 3adant3 | |
41 | 38 40 | eqbrtrd | |
42 | 41 | 3adant1l | |
43 | 42 | 3exp | |
44 | 43 | adantr | |
45 | 36 37 44 | rexlimd | |
46 | 28 45 | mpd | |
47 | 46 | ralrimiva | |
48 | 9 | ralrimiva | |
49 | 24 | rnmptss | |
50 | 48 49 | syl | |
51 | 50 | adantr | |
52 | 3 | adantr | |
53 | supxrleub | |
|
54 | 51 52 53 | syl2anc | |
55 | 47 54 | mpbird | |
56 | 22 55 | eqbrtrd | |
57 | 56 | ex | |
58 | 20 57 | impbid | |