Step |
Hyp |
Ref |
Expression |
1 |
|
sge0ltfirp.x |
|- ( ph -> X e. V ) |
2 |
|
sge0ltfirp.f |
|- ( ph -> F : X --> ( 0 [,] +oo ) ) |
3 |
|
sge0ltfirp.y |
|- ( ph -> Y e. RR+ ) |
4 |
|
sge0ltfirp.re |
|- ( ph -> ( sum^ ` F ) e. RR ) |
5 |
1 2 4
|
sge0rern |
|- ( ph -> -. +oo e. ran F ) |
6 |
2 5
|
fge0iccico |
|- ( ph -> F : X --> ( 0 [,) +oo ) ) |
7 |
6
|
sge0rnre |
|- ( ph -> ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) C_ RR ) |
8 |
|
sge0rnn0 |
|- ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) =/= (/) |
9 |
8
|
a1i |
|- ( ph -> ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) =/= (/) ) |
10 |
1 2 4
|
sge0rnbnd |
|- ( ph -> E. z e. RR A. w e. ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) w <_ z ) |
11 |
7 9 10 3
|
suprltrp |
|- ( ph -> E. w e. ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < w ) |
12 |
|
nfv |
|- F/ w ph |
13 |
|
nfv |
|- F/ w E. x e. ( ~P X i^i Fin ) ( sum^ ` F ) < ( ( sum^ ` ( F |` x ) ) + Y ) |
14 |
|
simp1 |
|- ( ( ph /\ w e. ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) /\ ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < w ) -> ph ) |
15 |
|
vex |
|- w e. _V |
16 |
|
eqid |
|- ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) = ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) |
17 |
16
|
elrnmpt |
|- ( w e. _V -> ( w e. ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) <-> E. x e. ( ~P X i^i Fin ) w = sum_ y e. x ( F ` y ) ) ) |
18 |
15 17
|
ax-mp |
|- ( w e. ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) <-> E. x e. ( ~P X i^i Fin ) w = sum_ y e. x ( F ` y ) ) |
19 |
18
|
biimpi |
|- ( w e. ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) -> E. x e. ( ~P X i^i Fin ) w = sum_ y e. x ( F ` y ) ) |
20 |
19
|
adantr |
|- ( ( w e. ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) /\ ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < w ) -> E. x e. ( ~P X i^i Fin ) w = sum_ y e. x ( F ` y ) ) |
21 |
|
nfmpt1 |
|- F/_ x ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) |
22 |
21
|
nfrn |
|- F/_ x ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) |
23 |
|
nfcv |
|- F/_ x RR |
24 |
|
nfcv |
|- F/_ x < |
25 |
22 23 24
|
nfsup |
|- F/_ x sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) |
26 |
|
nfcv |
|- F/_ x - |
27 |
|
nfcv |
|- F/_ x Y |
28 |
25 26 27
|
nfov |
|- F/_ x ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) |
29 |
|
nfcv |
|- F/_ x w |
30 |
28 24 29
|
nfbr |
|- F/ x ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < w |
31 |
|
simpl |
|- ( ( ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < w /\ w = sum_ y e. x ( F ` y ) ) -> ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < w ) |
32 |
|
simpr |
|- ( ( ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < w /\ w = sum_ y e. x ( F ` y ) ) -> w = sum_ y e. x ( F ` y ) ) |
33 |
31 32
|
breqtrd |
|- ( ( ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < w /\ w = sum_ y e. x ( F ` y ) ) -> ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < sum_ y e. x ( F ` y ) ) |
34 |
33
|
ex |
|- ( ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < w -> ( w = sum_ y e. x ( F ` y ) -> ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < sum_ y e. x ( F ` y ) ) ) |
35 |
34
|
a1d |
|- ( ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < w -> ( x e. ( ~P X i^i Fin ) -> ( w = sum_ y e. x ( F ` y ) -> ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < sum_ y e. x ( F ` y ) ) ) ) |
36 |
30 35
|
reximdai |
|- ( ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < w -> ( E. x e. ( ~P X i^i Fin ) w = sum_ y e. x ( F ` y ) -> E. x e. ( ~P X i^i Fin ) ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < sum_ y e. x ( F ` y ) ) ) |
37 |
36
|
adantl |
|- ( ( w e. ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) /\ ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < w ) -> ( E. x e. ( ~P X i^i Fin ) w = sum_ y e. x ( F ` y ) -> E. x e. ( ~P X i^i Fin ) ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < sum_ y e. x ( F ` y ) ) ) |
38 |
20 37
|
mpd |
|- ( ( w e. ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) /\ ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < w ) -> E. x e. ( ~P X i^i Fin ) ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < sum_ y e. x ( F ` y ) ) |
39 |
38
|
3adant1 |
|- ( ( ph /\ w e. ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) /\ ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < w ) -> E. x e. ( ~P X i^i Fin ) ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < sum_ y e. x ( F ` y ) ) |
40 |
|
simpl |
|- ( ( ( ph /\ x e. ( ~P X i^i Fin ) ) /\ ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < sum_ y e. x ( F ` y ) ) -> ( ph /\ x e. ( ~P X i^i Fin ) ) ) |
41 |
1 2 4
|
sge0supre |
|- ( ph -> ( sum^ ` F ) = sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) ) |
42 |
41
|
oveq1d |
|- ( ph -> ( ( sum^ ` F ) - Y ) = ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) ) |
43 |
42
|
adantr |
|- ( ( ph /\ ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < sum_ y e. x ( F ` y ) ) -> ( ( sum^ ` F ) - Y ) = ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) ) |
44 |
|
simpr |
|- ( ( ph /\ ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < sum_ y e. x ( F ` y ) ) -> ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < sum_ y e. x ( F ` y ) ) |
45 |
43 44
|
eqbrtrd |
|- ( ( ph /\ ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < sum_ y e. x ( F ` y ) ) -> ( ( sum^ ` F ) - Y ) < sum_ y e. x ( F ` y ) ) |
46 |
45
|
adantlr |
|- ( ( ( ph /\ x e. ( ~P X i^i Fin ) ) /\ ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < sum_ y e. x ( F ` y ) ) -> ( ( sum^ ` F ) - Y ) < sum_ y e. x ( F ` y ) ) |
47 |
|
simpr |
|- ( ( ( ph /\ x e. ( ~P X i^i Fin ) ) /\ ( ( sum^ ` F ) - Y ) < sum_ y e. x ( F ` y ) ) -> ( ( sum^ ` F ) - Y ) < sum_ y e. x ( F ` y ) ) |
48 |
4
|
adantr |
|- ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> ( sum^ ` F ) e. RR ) |
49 |
3
|
rpred |
|- ( ph -> Y e. RR ) |
50 |
49
|
adantr |
|- ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> Y e. RR ) |
51 |
|
elinel2 |
|- ( x e. ( ~P X i^i Fin ) -> x e. Fin ) |
52 |
51
|
adantl |
|- ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> x e. Fin ) |
53 |
|
rge0ssre |
|- ( 0 [,) +oo ) C_ RR |
54 |
6
|
adantr |
|- ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> F : X --> ( 0 [,) +oo ) ) |
55 |
54
|
adantr |
|- ( ( ( ph /\ x e. ( ~P X i^i Fin ) ) /\ y e. x ) -> F : X --> ( 0 [,) +oo ) ) |
56 |
|
elpwinss |
|- ( x e. ( ~P X i^i Fin ) -> x C_ X ) |
57 |
56
|
adantl |
|- ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> x C_ X ) |
58 |
57
|
sselda |
|- ( ( ( ph /\ x e. ( ~P X i^i Fin ) ) /\ y e. x ) -> y e. X ) |
59 |
55 58
|
ffvelrnd |
|- ( ( ( ph /\ x e. ( ~P X i^i Fin ) ) /\ y e. x ) -> ( F ` y ) e. ( 0 [,) +oo ) ) |
60 |
53 59
|
sseldi |
|- ( ( ( ph /\ x e. ( ~P X i^i Fin ) ) /\ y e. x ) -> ( F ` y ) e. RR ) |
61 |
52 60
|
fsumrecl |
|- ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> sum_ y e. x ( F ` y ) e. RR ) |
62 |
48 50 61
|
ltsubaddd |
|- ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> ( ( ( sum^ ` F ) - Y ) < sum_ y e. x ( F ` y ) <-> ( sum^ ` F ) < ( sum_ y e. x ( F ` y ) + Y ) ) ) |
63 |
62
|
adantr |
|- ( ( ( ph /\ x e. ( ~P X i^i Fin ) ) /\ ( ( sum^ ` F ) - Y ) < sum_ y e. x ( F ` y ) ) -> ( ( ( sum^ ` F ) - Y ) < sum_ y e. x ( F ` y ) <-> ( sum^ ` F ) < ( sum_ y e. x ( F ` y ) + Y ) ) ) |
64 |
47 63
|
mpbid |
|- ( ( ( ph /\ x e. ( ~P X i^i Fin ) ) /\ ( ( sum^ ` F ) - Y ) < sum_ y e. x ( F ` y ) ) -> ( sum^ ` F ) < ( sum_ y e. x ( F ` y ) + Y ) ) |
65 |
54 57
|
fssresd |
|- ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> ( F |` x ) : x --> ( 0 [,) +oo ) ) |
66 |
52 65
|
sge0fsum |
|- ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> ( sum^ ` ( F |` x ) ) = sum_ y e. x ( ( F |` x ) ` y ) ) |
67 |
|
fvres |
|- ( y e. x -> ( ( F |` x ) ` y ) = ( F ` y ) ) |
68 |
67
|
sumeq2i |
|- sum_ y e. x ( ( F |` x ) ` y ) = sum_ y e. x ( F ` y ) |
69 |
68
|
a1i |
|- ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> sum_ y e. x ( ( F |` x ) ` y ) = sum_ y e. x ( F ` y ) ) |
70 |
66 69
|
eqtr2d |
|- ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> sum_ y e. x ( F ` y ) = ( sum^ ` ( F |` x ) ) ) |
71 |
70
|
oveq1d |
|- ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> ( sum_ y e. x ( F ` y ) + Y ) = ( ( sum^ ` ( F |` x ) ) + Y ) ) |
72 |
71
|
adantr |
|- ( ( ( ph /\ x e. ( ~P X i^i Fin ) ) /\ ( ( sum^ ` F ) - Y ) < sum_ y e. x ( F ` y ) ) -> ( sum_ y e. x ( F ` y ) + Y ) = ( ( sum^ ` ( F |` x ) ) + Y ) ) |
73 |
64 72
|
breqtrd |
|- ( ( ( ph /\ x e. ( ~P X i^i Fin ) ) /\ ( ( sum^ ` F ) - Y ) < sum_ y e. x ( F ` y ) ) -> ( sum^ ` F ) < ( ( sum^ ` ( F |` x ) ) + Y ) ) |
74 |
40 46 73
|
syl2anc |
|- ( ( ( ph /\ x e. ( ~P X i^i Fin ) ) /\ ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < sum_ y e. x ( F ` y ) ) -> ( sum^ ` F ) < ( ( sum^ ` ( F |` x ) ) + Y ) ) |
75 |
74
|
ex |
|- ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> ( ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < sum_ y e. x ( F ` y ) -> ( sum^ ` F ) < ( ( sum^ ` ( F |` x ) ) + Y ) ) ) |
76 |
75
|
reximdva |
|- ( ph -> ( E. x e. ( ~P X i^i Fin ) ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < sum_ y e. x ( F ` y ) -> E. x e. ( ~P X i^i Fin ) ( sum^ ` F ) < ( ( sum^ ` ( F |` x ) ) + Y ) ) ) |
77 |
76
|
imp |
|- ( ( ph /\ E. x e. ( ~P X i^i Fin ) ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < sum_ y e. x ( F ` y ) ) -> E. x e. ( ~P X i^i Fin ) ( sum^ ` F ) < ( ( sum^ ` ( F |` x ) ) + Y ) ) |
78 |
14 39 77
|
syl2anc |
|- ( ( ph /\ w e. ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) /\ ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < w ) -> E. x e. ( ~P X i^i Fin ) ( sum^ ` F ) < ( ( sum^ ` ( F |` x ) ) + Y ) ) |
79 |
78
|
3exp |
|- ( ph -> ( w e. ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) -> ( ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < w -> E. x e. ( ~P X i^i Fin ) ( sum^ ` F ) < ( ( sum^ ` ( F |` x ) ) + Y ) ) ) ) |
80 |
12 13 79
|
rexlimd |
|- ( ph -> ( E. w e. ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) ( sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) - Y ) < w -> E. x e. ( ~P X i^i Fin ) ( sum^ ` F ) < ( ( sum^ ` ( F |` x ) ) + Y ) ) ) |
81 |
11 80
|
mpd |
|- ( ph -> E. x e. ( ~P X i^i Fin ) ( sum^ ` F ) < ( ( sum^ ` ( F |` x ) ) + Y ) ) |