Metamath Proof Explorer

Theorem esumpinfsum

Description: The value of the extended sum of infinitely many terms greater than one. (Contributed by Thierry Arnoux, 29-Jun-2017)

Ref Expression
Hypotheses esumpinfsum.p 
|- F/ k ph
esumpinfsum.a 
|- F/_ k A
esumpinfsum.1 
|- ( ph -> A e. V )
esumpinfsum.2 
|- ( ph -> -. A e. Fin )
esumpinfsum.3 
|- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )
esumpinfsum.4 
|- ( ( ph /\ k e. A ) -> M <_ B )
esumpinfsum.5 
|- ( ph -> M e. RR* )
esumpinfsum.6 
|- ( ph -> 0 < M )
Assertion esumpinfsum 
|- ( ph -> sum* k e. A B = +oo )

Proof

Step Hyp Ref Expression
1 esumpinfsum.p 
 |-  F/ k ph
2 esumpinfsum.a 
 |-  F/_ k A
3 esumpinfsum.1 
 |-  ( ph -> A e. V )
4 esumpinfsum.2 
 |-  ( ph -> -. A e. Fin )
5 esumpinfsum.3 
 |-  ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )
6 esumpinfsum.4 
 |-  ( ( ph /\ k e. A ) -> M <_ B )
7 esumpinfsum.5 
 |-  ( ph -> M e. RR* )
8 esumpinfsum.6 
 |-  ( ph -> 0 < M )
9 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
10 5 ex 
 |-  ( ph -> ( k e. A -> B e. ( 0 [,] +oo ) ) )
11 1 10 ralrimi 
 |-  ( ph -> A. k e. A B e. ( 0 [,] +oo ) )
12 2 esumcl 
 |-  ( ( A e. V /\ A. k e. A B e. ( 0 [,] +oo ) ) -> sum* k e. A B e. ( 0 [,] +oo ) )
13 3 11 12 syl2anc 
 |-  ( ph -> sum* k e. A B e. ( 0 [,] +oo ) )
14 9 13 sselid 
 |-  ( ph -> sum* k e. A B e. RR* )
15 0xr 
 |-  0 e. RR*
16 xrltle 
 |-  ( ( 0 e. RR* /\ M e. RR* ) -> ( 0 < M -> 0 <_ M ) )
17 15 7 16 sylancr 
 |-  ( ph -> ( 0 < M -> 0 <_ M ) )
18 8 17 mpd 
 |-  ( ph -> 0 <_ M )
19 pnfge 
 |-  ( M e. RR* -> M <_ +oo )
20 7 19 syl 
 |-  ( ph -> M <_ +oo )
21 pnfxr 
 |-  +oo e. RR*
22 elicc1 
 |-  ( ( 0 e. RR* /\ +oo e. RR* ) -> ( M e. ( 0 [,] +oo ) <-> ( M e. RR* /\ 0 <_ M /\ M <_ +oo ) ) )
23 15 21 22 mp2an 
 |-  ( M e. ( 0 [,] +oo ) <-> ( M e. RR* /\ 0 <_ M /\ M <_ +oo ) )
24 7 18 20 23 syl3anbrc 
 |-  ( ph -> M e. ( 0 [,] +oo ) )
25 nfcv 
 |-  F/_ k M
26 2 25 esumcst 
 |-  ( ( A e. V /\ M e. ( 0 [,] +oo ) ) -> sum* k e. A M = ( ( # ` A ) *e M ) )
27 3 24 26 syl2anc 
 |-  ( ph -> sum* k e. A M = ( ( # ` A ) *e M ) )
28 hashinf 
 |-  ( ( A e. V /\ -. A e. Fin ) -> ( # ` A ) = +oo )
29 3 4 28 syl2anc 
 |-  ( ph -> ( # ` A ) = +oo )
30 29 oveq1d 
 |-  ( ph -> ( ( # ` A ) *e M ) = ( +oo *e M ) )
31 xmulpnf2 
 |-  ( ( M e. RR* /\ 0 < M ) -> ( +oo *e M ) = +oo )
32 7 8 31 syl2anc 
 |-  ( ph -> ( +oo *e M ) = +oo )
33 27 30 32 3eqtrd 
 |-  ( ph -> sum* k e. A M = +oo )
34 24 adantr 
 |-  ( ( ph /\ k e. A ) -> M e. ( 0 [,] +oo ) )
35 1 2 3 34 5 6 esumlef 
 |-  ( ph -> sum* k e. A M <_ sum* k e. A B )
36 33 35 eqbrtrrd 
 |-  ( ph -> +oo <_ sum* k e. A B )
37 xgepnf 
 |-  ( sum* k e. A B e. RR* -> ( +oo <_ sum* k e. A B <-> sum* k e. A B = +oo ) )
38 37 biimpd 
 |-  ( sum* k e. A B e. RR* -> ( +oo <_ sum* k e. A B -> sum* k e. A B = +oo ) )
39 14 36 38 sylc 
 |-  ( ph -> sum* k e. A B = +oo )