Metamath Proof Explorer

Theorem esumpinfval

Description: The value of the extended sum of nonnegative terms, with at least one infinite term. (Contributed by Thierry Arnoux, 19-Jun-2017)

Ref Expression
Hypotheses esumpinfval.0 
|- F/ k ph
esumpinfval.1 
|- ( ph -> A e. V )
esumpinfval.2 
|- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )
esumpinfval.3 
|- ( ph -> E. k e. A B = +oo )
Assertion esumpinfval 
|- ( ph -> sum* k e. A B = +oo )

Proof

Step Hyp Ref Expression
1 esumpinfval.0 
 |-  F/ k ph
2 esumpinfval.1 
 |-  ( ph -> A e. V )
3 esumpinfval.2 
 |-  ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )
4 esumpinfval.3 
 |-  ( ph -> E. k e. A B = +oo )
5 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
6 3 ex 
 |-  ( ph -> ( k e. A -> B e. ( 0 [,] +oo ) ) )
7 1 6 ralrimi 
 |-  ( ph -> A. k e. A B e. ( 0 [,] +oo ) )
8 nfcv 
 |-  F/_ k A
9 8 esumcl 
 |-  ( ( A e. V /\ A. k e. A B e. ( 0 [,] +oo ) ) -> sum* k e. A B e. ( 0 [,] +oo ) )
10 2 7 9 syl2anc 
 |-  ( ph -> sum* k e. A B e. ( 0 [,] +oo ) )
11 5 10 sseldi 
 |-  ( ph -> sum* k e. A B e. RR* )
12 nfrab1 
 |-  F/_ k { k e. A | B = +oo }
13 ssrab2 
 |-  { k e. A | B = +oo } C_ A
14 13 a1i 
 |-  ( ph -> { k e. A | B = +oo } C_ A )
15 0xr 
 |-  0 e. RR*
16 pnfxr 
 |-  +oo e. RR*
17 0lepnf 
 |-  0 <_ +oo
18 ubicc2 
 |-  ( ( 0 e. RR* /\ +oo e. RR* /\ 0 <_ +oo ) -> +oo e. ( 0 [,] +oo ) )
19 15 16 17 18 mp3an 
 |-  +oo e. ( 0 [,] +oo )
20 19 a1i 
 |-  ( ( ( ph /\ k e. A ) /\ B = +oo ) -> +oo e. ( 0 [,] +oo ) )
21 0e0iccpnf 
 |-  0 e. ( 0 [,] +oo )
22 21 a1i 
 |-  ( ( ( ph /\ k e. A ) /\ -. B = +oo ) -> 0 e. ( 0 [,] +oo ) )
23 20 22 ifclda 
 |-  ( ( ph /\ k e. A ) -> if ( B = +oo , +oo , 0 ) e. ( 0 [,] +oo ) )
24 eldif 
 |-  ( k e. ( A \ { k e. A | B = +oo } ) <-> ( k e. A /\ -. k e. { k e. A | B = +oo } ) )
25 rabid 
 |-  ( k e. { k e. A | B = +oo } <-> ( k e. A /\ B = +oo ) )
26 25 simplbi2 
 |-  ( k e. A -> ( B = +oo -> k e. { k e. A | B = +oo } ) )
27 26 con3dimp 
 |-  ( ( k e. A /\ -. k e. { k e. A | B = +oo } ) -> -. B = +oo )
28 24 27 sylbi 
 |-  ( k e. ( A \ { k e. A | B = +oo } ) -> -. B = +oo )
29 28 adantl 
 |-  ( ( ph /\ k e. ( A \ { k e. A | B = +oo } ) ) -> -. B = +oo )
30 29 iffalsed 
 |-  ( ( ph /\ k e. ( A \ { k e. A | B = +oo } ) ) -> if ( B = +oo , +oo , 0 ) = 0 )
31 1 12 8 14 2 23 30 esumss 
 |-  ( ph -> sum* k e. { k e. A | B = +oo } if ( B = +oo , +oo , 0 ) = sum* k e. A if ( B = +oo , +oo , 0 ) )
32 eqidd 
 |-  ( ph -> { k e. A | B = +oo } = { k e. A | B = +oo } )
33 25 simprbi 
 |-  ( k e. { k e. A | B = +oo } -> B = +oo )
34 33 iftrued 
 |-  ( k e. { k e. A | B = +oo } -> if ( B = +oo , +oo , 0 ) = +oo )
35 34 adantl 
 |-  ( ( ph /\ k e. { k e. A | B = +oo } ) -> if ( B = +oo , +oo , 0 ) = +oo )
36 1 32 35 esumeq12dvaf 
 |-  ( ph -> sum* k e. { k e. A | B = +oo } if ( B = +oo , +oo , 0 ) = sum* k e. { k e. A | B = +oo } +oo )
37 2 14 ssexd 
 |-  ( ph -> { k e. A | B = +oo } e. _V )
38 nfcv 
 |-  F/_ k +oo
39 12 38 esumcst 
 |-  ( ( { k e. A | B = +oo } e. _V /\ +oo e. ( 0 [,] +oo ) ) -> sum* k e. { k e. A | B = +oo } +oo = ( ( # ` { k e. A | B = +oo } ) *e +oo ) )
40 37 19 39 sylancl 
 |-  ( ph -> sum* k e. { k e. A | B = +oo } +oo = ( ( # ` { k e. A | B = +oo } ) *e +oo ) )
41 hashxrcl 
 |-  ( { k e. A | B = +oo } e. _V -> ( # ` { k e. A | B = +oo } ) e. RR* )
42 37 41 syl 
 |-  ( ph -> ( # ` { k e. A | B = +oo } ) e. RR* )
43 rabn0 
 |-  ( { k e. A | B = +oo } =/= (/) <-> E. k e. A B = +oo )
44 4 43 sylibr 
 |-  ( ph -> { k e. A | B = +oo } =/= (/) )
45 hashgt0 
 |-  ( ( { k e. A | B = +oo } e. _V /\ { k e. A | B = +oo } =/= (/) ) -> 0 < ( # ` { k e. A | B = +oo } ) )
46 37 44 45 syl2anc 
 |-  ( ph -> 0 < ( # ` { k e. A | B = +oo } ) )
47 xmulpnf1 
 |-  ( ( ( # ` { k e. A | B = +oo } ) e. RR* /\ 0 < ( # ` { k e. A | B = +oo } ) ) -> ( ( # ` { k e. A | B = +oo } ) *e +oo ) = +oo )
48 42 46 47 syl2anc 
 |-  ( ph -> ( ( # ` { k e. A | B = +oo } ) *e +oo ) = +oo )
49 36 40 48 3eqtrd 
 |-  ( ph -> sum* k e. { k e. A | B = +oo } if ( B = +oo , +oo , 0 ) = +oo )
50 31 49 eqtr3d 
 |-  ( ph -> sum* k e. A if ( B = +oo , +oo , 0 ) = +oo )
51 breq1 
 |-  ( +oo = if ( B = +oo , +oo , 0 ) -> ( +oo <_ B <-> if ( B = +oo , +oo , 0 ) <_ B ) )
52 breq1 
 |-  ( 0 = if ( B = +oo , +oo , 0 ) -> ( 0 <_ B <-> if ( B = +oo , +oo , 0 ) <_ B ) )
53 pnfge 
 |-  ( +oo e. RR* -> +oo <_ +oo )
54 16 53 ax-mp 
 |-  +oo <_ +oo
55 breq2 
 |-  ( B = +oo -> ( +oo <_ B <-> +oo <_ +oo ) )
56 54 55 mpbiri 
 |-  ( B = +oo -> +oo <_ B )
57 56 adantl 
 |-  ( ( ( ph /\ k e. A ) /\ B = +oo ) -> +oo <_ B )
58 3 adantr 
 |-  ( ( ( ph /\ k e. A ) /\ -. B = +oo ) -> B e. ( 0 [,] +oo ) )
59 iccgelb 
 |-  ( ( 0 e. RR* /\ +oo e. RR* /\ B e. ( 0 [,] +oo ) ) -> 0 <_ B )
60 15 16 59 mp3an12 
 |-  ( B e. ( 0 [,] +oo ) -> 0 <_ B )
61 58 60 syl 
 |-  ( ( ( ph /\ k e. A ) /\ -. B = +oo ) -> 0 <_ B )
62 51 52 57 61 ifbothda 
 |-  ( ( ph /\ k e. A ) -> if ( B = +oo , +oo , 0 ) <_ B )
63 1 8 2 23 3 62 esumlef 
 |-  ( ph -> sum* k e. A if ( B = +oo , +oo , 0 ) <_ sum* k e. A B )
64 50 63 eqbrtrrd 
 |-  ( ph -> +oo <_ sum* k e. A B )
65 xgepnf 
 |-  ( sum* k e. A B e. RR* -> ( +oo <_ sum* k e. A B <-> sum* k e. A B = +oo ) )
66 65 biimpd 
 |-  ( sum* k e. A B e. RR* -> ( +oo <_ sum* k e. A B -> sum* k e. A B = +oo ) )
67 11 64 66 sylc 
 |-  ( ph -> sum* k e. A B = +oo )