Step |
Hyp |
Ref |
Expression |
1 |
|
sge0fsum.x |
|- ( ph -> X e. Fin ) |
2 |
|
sge0fsum.f |
|- ( ph -> F : X --> ( 0 [,) +oo ) ) |
3 |
2
|
fge0icoicc |
|- ( ph -> F : X --> ( 0 [,] +oo ) ) |
4 |
1 3
|
sge0xrcl |
|- ( ph -> ( sum^ ` F ) e. RR* ) |
5 |
|
rge0ssre |
|- ( 0 [,) +oo ) C_ RR |
6 |
2
|
ffvelrnda |
|- ( ( ph /\ x e. X ) -> ( F ` x ) e. ( 0 [,) +oo ) ) |
7 |
5 6
|
sseldi |
|- ( ( ph /\ x e. X ) -> ( F ` x ) e. RR ) |
8 |
1 7
|
fsumrecl |
|- ( ph -> sum_ x e. X ( F ` x ) e. RR ) |
9 |
8
|
rexrd |
|- ( ph -> sum_ x e. X ( F ` x ) e. RR* ) |
10 |
1 2
|
sge0reval |
|- ( ph -> ( sum^ ` F ) = sup ( ran ( y e. ( ~P X i^i Fin ) |-> sum_ x e. y ( F ` x ) ) , RR* , < ) ) |
11 |
|
simpr |
|- ( ( ph /\ w e. ran ( y e. ( ~P X i^i Fin ) |-> sum_ x e. y ( F ` x ) ) ) -> w e. ran ( y e. ( ~P X i^i Fin ) |-> sum_ x e. y ( F ` x ) ) ) |
12 |
|
vex |
|- w e. _V |
13 |
12
|
a1i |
|- ( ( ph /\ w e. ran ( y e. ( ~P X i^i Fin ) |-> sum_ x e. y ( F ` x ) ) ) -> w e. _V ) |
14 |
|
eqid |
|- ( y e. ( ~P X i^i Fin ) |-> sum_ x e. y ( F ` x ) ) = ( y e. ( ~P X i^i Fin ) |-> sum_ x e. y ( F ` x ) ) |
15 |
14
|
elrnmpt |
|- ( w e. _V -> ( w e. ran ( y e. ( ~P X i^i Fin ) |-> sum_ x e. y ( F ` x ) ) <-> E. y e. ( ~P X i^i Fin ) w = sum_ x e. y ( F ` x ) ) ) |
16 |
13 15
|
syl |
|- ( ( ph /\ w e. ran ( y e. ( ~P X i^i Fin ) |-> sum_ x e. y ( F ` x ) ) ) -> ( w e. ran ( y e. ( ~P X i^i Fin ) |-> sum_ x e. y ( F ` x ) ) <-> E. y e. ( ~P X i^i Fin ) w = sum_ x e. y ( F ` x ) ) ) |
17 |
11 16
|
mpbid |
|- ( ( ph /\ w e. ran ( y e. ( ~P X i^i Fin ) |-> sum_ x e. y ( F ` x ) ) ) -> E. y e. ( ~P X i^i Fin ) w = sum_ x e. y ( F ` x ) ) |
18 |
|
simp3 |
|- ( ( ph /\ y e. ( ~P X i^i Fin ) /\ w = sum_ x e. y ( F ` x ) ) -> w = sum_ x e. y ( F ` x ) ) |
19 |
1
|
adantr |
|- ( ( ph /\ y e. ( ~P X i^i Fin ) ) -> X e. Fin ) |
20 |
2
|
fge0npnf |
|- ( ph -> -. +oo e. ran F ) |
21 |
3 20
|
fge0iccre |
|- ( ph -> F : X --> RR ) |
22 |
21
|
adantr |
|- ( ( ph /\ y e. ( ~P X i^i Fin ) ) -> F : X --> RR ) |
23 |
22
|
adantr |
|- ( ( ( ph /\ y e. ( ~P X i^i Fin ) ) /\ x e. X ) -> F : X --> RR ) |
24 |
|
simpr |
|- ( ( ( ph /\ y e. ( ~P X i^i Fin ) ) /\ x e. X ) -> x e. X ) |
25 |
23 24
|
ffvelrnd |
|- ( ( ( ph /\ y e. ( ~P X i^i Fin ) ) /\ x e. X ) -> ( F ` x ) e. RR ) |
26 |
|
0xr |
|- 0 e. RR* |
27 |
26
|
a1i |
|- ( ( ( ph /\ y e. ( ~P X i^i Fin ) ) /\ x e. X ) -> 0 e. RR* ) |
28 |
|
pnfxr |
|- +oo e. RR* |
29 |
28
|
a1i |
|- ( ( ( ph /\ y e. ( ~P X i^i Fin ) ) /\ x e. X ) -> +oo e. RR* ) |
30 |
3
|
adantr |
|- ( ( ph /\ y e. ( ~P X i^i Fin ) ) -> F : X --> ( 0 [,] +oo ) ) |
31 |
30
|
ffvelrnda |
|- ( ( ( ph /\ y e. ( ~P X i^i Fin ) ) /\ x e. X ) -> ( F ` x ) e. ( 0 [,] +oo ) ) |
32 |
|
iccgelb |
|- ( ( 0 e. RR* /\ +oo e. RR* /\ ( F ` x ) e. ( 0 [,] +oo ) ) -> 0 <_ ( F ` x ) ) |
33 |
27 29 31 32
|
syl3anc |
|- ( ( ( ph /\ y e. ( ~P X i^i Fin ) ) /\ x e. X ) -> 0 <_ ( F ` x ) ) |
34 |
|
elinel1 |
|- ( y e. ( ~P X i^i Fin ) -> y e. ~P X ) |
35 |
|
elpwi |
|- ( y e. ~P X -> y C_ X ) |
36 |
34 35
|
syl |
|- ( y e. ( ~P X i^i Fin ) -> y C_ X ) |
37 |
36
|
adantl |
|- ( ( ph /\ y e. ( ~P X i^i Fin ) ) -> y C_ X ) |
38 |
19 25 33 37
|
fsumless |
|- ( ( ph /\ y e. ( ~P X i^i Fin ) ) -> sum_ x e. y ( F ` x ) <_ sum_ x e. X ( F ` x ) ) |
39 |
38
|
3adant3 |
|- ( ( ph /\ y e. ( ~P X i^i Fin ) /\ w = sum_ x e. y ( F ` x ) ) -> sum_ x e. y ( F ` x ) <_ sum_ x e. X ( F ` x ) ) |
40 |
18 39
|
eqbrtrd |
|- ( ( ph /\ y e. ( ~P X i^i Fin ) /\ w = sum_ x e. y ( F ` x ) ) -> w <_ sum_ x e. X ( F ` x ) ) |
41 |
40
|
3exp |
|- ( ph -> ( y e. ( ~P X i^i Fin ) -> ( w = sum_ x e. y ( F ` x ) -> w <_ sum_ x e. X ( F ` x ) ) ) ) |
42 |
41
|
rexlimdv |
|- ( ph -> ( E. y e. ( ~P X i^i Fin ) w = sum_ x e. y ( F ` x ) -> w <_ sum_ x e. X ( F ` x ) ) ) |
43 |
42
|
adantr |
|- ( ( ph /\ w e. ran ( y e. ( ~P X i^i Fin ) |-> sum_ x e. y ( F ` x ) ) ) -> ( E. y e. ( ~P X i^i Fin ) w = sum_ x e. y ( F ` x ) -> w <_ sum_ x e. X ( F ` x ) ) ) |
44 |
17 43
|
mpd |
|- ( ( ph /\ w e. ran ( y e. ( ~P X i^i Fin ) |-> sum_ x e. y ( F ` x ) ) ) -> w <_ sum_ x e. X ( F ` x ) ) |
45 |
44
|
ralrimiva |
|- ( ph -> A. w e. ran ( y e. ( ~P X i^i Fin ) |-> sum_ x e. y ( F ` x ) ) w <_ sum_ x e. X ( F ` x ) ) |
46 |
|
elinel2 |
|- ( y e. ( ~P X i^i Fin ) -> y e. Fin ) |
47 |
46
|
adantl |
|- ( ( ph /\ y e. ( ~P X i^i Fin ) ) -> y e. Fin ) |
48 |
22
|
adantr |
|- ( ( ( ph /\ y e. ( ~P X i^i Fin ) ) /\ x e. y ) -> F : X --> RR ) |
49 |
37
|
sselda |
|- ( ( ( ph /\ y e. ( ~P X i^i Fin ) ) /\ x e. y ) -> x e. X ) |
50 |
48 49
|
ffvelrnd |
|- ( ( ( ph /\ y e. ( ~P X i^i Fin ) ) /\ x e. y ) -> ( F ` x ) e. RR ) |
51 |
47 50
|
fsumrecl |
|- ( ( ph /\ y e. ( ~P X i^i Fin ) ) -> sum_ x e. y ( F ` x ) e. RR ) |
52 |
51
|
rexrd |
|- ( ( ph /\ y e. ( ~P X i^i Fin ) ) -> sum_ x e. y ( F ` x ) e. RR* ) |
53 |
52
|
ralrimiva |
|- ( ph -> A. y e. ( ~P X i^i Fin ) sum_ x e. y ( F ` x ) e. RR* ) |
54 |
14
|
rnmptss |
|- ( A. y e. ( ~P X i^i Fin ) sum_ x e. y ( F ` x ) e. RR* -> ran ( y e. ( ~P X i^i Fin ) |-> sum_ x e. y ( F ` x ) ) C_ RR* ) |
55 |
53 54
|
syl |
|- ( ph -> ran ( y e. ( ~P X i^i Fin ) |-> sum_ x e. y ( F ` x ) ) C_ RR* ) |
56 |
|
supxrleub |
|- ( ( ran ( y e. ( ~P X i^i Fin ) |-> sum_ x e. y ( F ` x ) ) C_ RR* /\ sum_ x e. X ( F ` x ) e. RR* ) -> ( sup ( ran ( y e. ( ~P X i^i Fin ) |-> sum_ x e. y ( F ` x ) ) , RR* , < ) <_ sum_ x e. X ( F ` x ) <-> A. w e. ran ( y e. ( ~P X i^i Fin ) |-> sum_ x e. y ( F ` x ) ) w <_ sum_ x e. X ( F ` x ) ) ) |
57 |
55 9 56
|
syl2anc |
|- ( ph -> ( sup ( ran ( y e. ( ~P X i^i Fin ) |-> sum_ x e. y ( F ` x ) ) , RR* , < ) <_ sum_ x e. X ( F ` x ) <-> A. w e. ran ( y e. ( ~P X i^i Fin ) |-> sum_ x e. y ( F ` x ) ) w <_ sum_ x e. X ( F ` x ) ) ) |
58 |
45 57
|
mpbird |
|- ( ph -> sup ( ran ( y e. ( ~P X i^i Fin ) |-> sum_ x e. y ( F ` x ) ) , RR* , < ) <_ sum_ x e. X ( F ` x ) ) |
59 |
10 58
|
eqbrtrd |
|- ( ph -> ( sum^ ` F ) <_ sum_ x e. X ( F ` x ) ) |
60 |
|
ssid |
|- X C_ X |
61 |
60
|
a1i |
|- ( ph -> X C_ X ) |
62 |
1 2 61 1
|
fsumlesge0 |
|- ( ph -> sum_ x e. X ( F ` x ) <_ ( sum^ ` F ) ) |
63 |
4 9 59 62
|
xrletrid |
|- ( ph -> ( sum^ ` F ) = sum_ x e. X ( F ` x ) ) |