Metamath Proof Explorer

Theorem esumcvgre

Description: All terms of a converging extended sum shall be finite. (Contributed by Thierry Arnoux, 23-Sep-2019)

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

Proof

Step Hyp Ref Expression
1 esumcvgre.0 
 |-  F/ k ph
2 esumcvgre.1 
 |-  ( ph -> A e. V )
3 esumcvgre.2 
 |-  ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )
4 esumcvgre.3 
 |-  ( ph -> sum* k e. A B e. RR )
5 nfre1 
 |-  F/ k E. k e. A B = +oo
6 1 5 nfan 
 |-  F/ k ( ph /\ E. k e. A B = +oo )
7 2 adantr 
 |-  ( ( ph /\ E. k e. A B = +oo ) -> A e. V )
8 3 adantlr 
 |-  ( ( ( ph /\ E. k e. A B = +oo ) /\ k e. A ) -> B e. ( 0 [,] +oo ) )
9 simpr 
 |-  ( ( ph /\ E. k e. A B = +oo ) -> E. k e. A B = +oo )
10 6 7 8 9 esumpinfval 
 |-  ( ( ph /\ E. k e. A B = +oo ) -> sum* k e. A B = +oo )
11 ltpnf 
 |-  ( sum* k e. A B e. RR -> sum* k e. A B < +oo )
12 4 11 syl 
 |-  ( ph -> sum* k e. A B < +oo )
13 4 12 gtned 
 |-  ( ph -> +oo =/= sum* k e. A B )
14 13 adantr 
 |-  ( ( ph /\ E. k e. A B = +oo ) -> +oo =/= sum* k e. A B )
15 necom 
 |-  ( +oo =/= sum* k e. A B <-> sum* k e. A B =/= +oo )
16 15 imbi2i 
 |-  ( ( ( ph /\ E. k e. A B = +oo ) -> +oo =/= sum* k e. A B ) <-> ( ( ph /\ E. k e. A B = +oo ) -> sum* k e. A B =/= +oo ) )
17 14 16 mpbi 
 |-  ( ( ph /\ E. k e. A B = +oo ) -> sum* k e. A B =/= +oo )
18 17 neneqd 
 |-  ( ( ph /\ E. k e. A B = +oo ) -> -. sum* k e. A B = +oo )
19 10 18 pm2.65da 
 |-  ( ph -> -. E. k e. A B = +oo )
20 ralnex 
 |-  ( A. k e. A -. B = +oo <-> -. E. k e. A B = +oo )
21 19 20 sylibr 
 |-  ( ph -> A. k e. A -. B = +oo )
22 21 r19.21bi 
 |-  ( ( ph /\ k e. A ) -> -. B = +oo )
23 eliccxr 
 |-  ( B e. ( 0 [,] +oo ) -> B e. RR* )
24 xrge0neqmnf 
 |-  ( B e. ( 0 [,] +oo ) -> B =/= -oo )
25 xrnemnf 
 |-  ( ( B e. RR* /\ B =/= -oo ) <-> ( B e. RR \/ B = +oo ) )
26 25 biimpi 
 |-  ( ( B e. RR* /\ B =/= -oo ) -> ( B e. RR \/ B = +oo ) )
27 23 24 26 syl2anc 
 |-  ( B e. ( 0 [,] +oo ) -> ( B e. RR \/ B = +oo ) )
28 3 27 syl 
 |-  ( ( ph /\ k e. A ) -> ( B e. RR \/ B = +oo ) )
29 28 orcomd 
 |-  ( ( ph /\ k e. A ) -> ( B = +oo \/ B e. RR ) )
30 29 orcanai 
 |-  ( ( ( ph /\ k e. A ) /\ -. B = +oo ) -> B e. RR )
31 22 30 mpdan 
 |-  ( ( ph /\ k e. A ) -> B e. RR )