Metamath Proof Explorer

Theorem sge0ltfirpmpt2

Description: If the extended sum of nonnegative reals is not +oo , then it can be approximated from below by finite subsums. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0ltfirpmpt2.xph 
|- F/ x ph
sge0ltfirpmpt2.a 
|- ( ph -> A e. V )
sge0ltfirpmpt2.b 
|- ( ( ph /\ x e. A ) -> B e. ( 0 [,] +oo ) )
sge0ltfirpmpt2.rp 
|- ( ph -> Y e. RR+ )
sge0ltfirpmpt2.re 
|- ( ph -> ( sum^ ` ( x e. A |-> B ) ) e. RR )
Assertion sge0ltfirpmpt2 
|- ( ph -> E. y e. ( ~P A i^i Fin ) ( sum^ ` ( x e. A |-> B ) ) < ( sum_ x e. y B + Y ) )

Proof

Step Hyp Ref Expression
1 sge0ltfirpmpt2.xph 
 |-  F/ x ph
2 sge0ltfirpmpt2.a 
 |-  ( ph -> A e. V )
3 sge0ltfirpmpt2.b 
 |-  ( ( ph /\ x e. A ) -> B e. ( 0 [,] +oo ) )
4 sge0ltfirpmpt2.rp 
 |-  ( ph -> Y e. RR+ )
5 sge0ltfirpmpt2.re 
 |-  ( ph -> ( sum^ ` ( x e. A |-> B ) ) e. RR )
6 eqid 
 |-  ( x e. A |-> B ) = ( x e. A |-> B )
7 1 3 6 fmptdf 
 |-  ( ph -> ( x e. A |-> B ) : A --> ( 0 [,] +oo ) )
8 2 7 4 5 sge0ltfirp 
 |-  ( ph -> E. y e. ( ~P A i^i Fin ) ( sum^ ` ( x e. A |-> B ) ) < ( ( sum^ ` ( ( x e. A |-> B ) |` y ) ) + Y ) )
9 simpr 
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ ( sum^ ` ( x e. A |-> B ) ) < ( ( sum^ ` ( ( x e. A |-> B ) |` y ) ) + Y ) ) -> ( sum^ ` ( x e. A |-> B ) ) < ( ( sum^ ` ( ( x e. A |-> B ) |` y ) ) + Y ) )
10 elpwinss 
 |-  ( y e. ( ~P A i^i Fin ) -> y C_ A )
11 10 resmptd 
 |-  ( y e. ( ~P A i^i Fin ) -> ( ( x e. A |-> B ) |` y ) = ( x e. y |-> B ) )
12 11 fveq2d 
 |-  ( y e. ( ~P A i^i Fin ) -> ( sum^ ` ( ( x e. A |-> B ) |` y ) ) = ( sum^ ` ( x e. y |-> B ) ) )
13 12 adantl 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> ( sum^ ` ( ( x e. A |-> B ) |` y ) ) = ( sum^ ` ( x e. y |-> B ) ) )
14 elinel2 
 |-  ( y e. ( ~P A i^i Fin ) -> y e. Fin )
15 14 adantl 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> y e. Fin )
16 nfv 
 |-  F/ x y e. ( ~P A i^i Fin )
17 1 16 nfan 
 |-  F/ x ( ph /\ y e. ( ~P A i^i Fin ) )
18 simpll 
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ x e. y ) -> ph )
19 10 sselda 
 |-  ( ( y e. ( ~P A i^i Fin ) /\ x e. y ) -> x e. A )
20 19 adantll 
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ x e. y ) -> x e. A )
21 1 2 3 5 sge0rernmpt 
 |-  ( ( ph /\ x e. A ) -> B e. ( 0 [,) +oo ) )
22 18 20 21 syl2anc 
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ x e. y ) -> B e. ( 0 [,) +oo ) )
23 eqid 
 |-  ( x e. y |-> B ) = ( x e. y |-> B )
24 17 22 23 fmptdf 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> ( x e. y |-> B ) : y --> ( 0 [,) +oo ) )
25 15 24 sge0fsum 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> ( sum^ ` ( x e. y |-> B ) ) = sum_ k e. y ( ( x e. y |-> B ) ` k ) )
26 simpr 
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ k e. y ) -> k e. y )
27 simpll 
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ k e. y ) -> ph )
28 10 sselda 
 |-  ( ( y e. ( ~P A i^i Fin ) /\ k e. y ) -> k e. A )
29 28 adantll 
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ k e. y ) -> k e. A )
30 nfv 
 |-  F/ x k e. A
31 1 30 nfan 
 |-  F/ x ( ph /\ k e. A )
32 nfcsb1v 
 |-  F/_ x [_ k / x ]_ B
33 32 nfel1 
 |-  F/ x [_ k / x ]_ B e. ( 0 [,) +oo )
34 31 33 nfim 
 |-  F/ x ( ( ph /\ k e. A ) -> [_ k / x ]_ B e. ( 0 [,) +oo ) )
35 eleq1w 
 |-  ( x = k -> ( x e. A <-> k e. A ) )
36 35 anbi2d 
 |-  ( x = k -> ( ( ph /\ x e. A ) <-> ( ph /\ k e. A ) ) )
37 csbeq1a 
 |-  ( x = k -> B = [_ k / x ]_ B )
38 37 eleq1d 
 |-  ( x = k -> ( B e. ( 0 [,) +oo ) <-> [_ k / x ]_ B e. ( 0 [,) +oo ) ) )
39 36 38 imbi12d 
 |-  ( x = k -> ( ( ( ph /\ x e. A ) -> B e. ( 0 [,) +oo ) ) <-> ( ( ph /\ k e. A ) -> [_ k / x ]_ B e. ( 0 [,) +oo ) ) ) )
40 34 39 21 chvarfv 
 |-  ( ( ph /\ k e. A ) -> [_ k / x ]_ B e. ( 0 [,) +oo ) )
41 27 29 40 syl2anc 
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ k e. y ) -> [_ k / x ]_ B e. ( 0 [,) +oo ) )
42 nfcv 
 |-  F/_ k B
43 42 32 37 cbvmpt 
 |-  ( x e. y |-> B ) = ( k e. y |-> [_ k / x ]_ B )
44 43 fvmpt2 
 |-  ( ( k e. y /\ [_ k / x ]_ B e. ( 0 [,) +oo ) ) -> ( ( x e. y |-> B ) ` k ) = [_ k / x ]_ B )
45 26 41 44 syl2anc 
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ k e. y ) -> ( ( x e. y |-> B ) ` k ) = [_ k / x ]_ B )
46 45 sumeq2dv 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> sum_ k e. y ( ( x e. y |-> B ) ` k ) = sum_ k e. y [_ k / x ]_ B )
47 eqcom 
 |-  ( x = k <-> k = x )
48 47 imbi1i 
 |-  ( ( x = k -> B = [_ k / x ]_ B ) <-> ( k = x -> B = [_ k / x ]_ B ) )
49 eqcom 
 |-  ( B = [_ k / x ]_ B <-> [_ k / x ]_ B = B )
50 49 imbi2i 
 |-  ( ( k = x -> B = [_ k / x ]_ B ) <-> ( k = x -> [_ k / x ]_ B = B ) )
51 48 50 bitri 
 |-  ( ( x = k -> B = [_ k / x ]_ B ) <-> ( k = x -> [_ k / x ]_ B = B ) )
52 37 51 mpbi 
 |-  ( k = x -> [_ k / x ]_ B = B )
53 nfcv 
 |-  F/_ x y
54 nfcv 
 |-  F/_ k y
55 52 53 54 32 42 cbvsum 
 |-  sum_ k e. y [_ k / x ]_ B = sum_ x e. y B
56 55 a1i 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> sum_ k e. y [_ k / x ]_ B = sum_ x e. y B )
57 46 56 eqtrd 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> sum_ k e. y ( ( x e. y |-> B ) ` k ) = sum_ x e. y B )
58 13 25 57 3eqtrd 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> ( sum^ ` ( ( x e. A |-> B ) |` y ) ) = sum_ x e. y B )
59 58 oveq1d 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> ( ( sum^ ` ( ( x e. A |-> B ) |` y ) ) + Y ) = ( sum_ x e. y B + Y ) )
60 59 adantr 
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ ( sum^ ` ( x e. A |-> B ) ) < ( ( sum^ ` ( ( x e. A |-> B ) |` y ) ) + Y ) ) -> ( ( sum^ ` ( ( x e. A |-> B ) |` y ) ) + Y ) = ( sum_ x e. y B + Y ) )
61 9 60 breqtrd 
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ ( sum^ ` ( x e. A |-> B ) ) < ( ( sum^ ` ( ( x e. A |-> B ) |` y ) ) + Y ) ) -> ( sum^ ` ( x e. A |-> B ) ) < ( sum_ x e. y B + Y ) )
62 61 ex 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> ( ( sum^ ` ( x e. A |-> B ) ) < ( ( sum^ ` ( ( x e. A |-> B ) |` y ) ) + Y ) -> ( sum^ ` ( x e. A |-> B ) ) < ( sum_ x e. y B + Y ) ) )
63 62 reximdva 
 |-  ( ph -> ( E. y e. ( ~P A i^i Fin ) ( sum^ ` ( x e. A |-> B ) ) < ( ( sum^ ` ( ( x e. A |-> B ) |` y ) ) + Y ) -> E. y e. ( ~P A i^i Fin ) ( sum^ ` ( x e. A |-> B ) ) < ( sum_ x e. y B + Y ) ) )
64 8 63 mpd 
 |-  ( ph -> E. y e. ( ~P A i^i Fin ) ( sum^ ` ( x e. A |-> B ) ) < ( sum_ x e. y B + Y ) )