Metamath Proof Explorer

Theorem esumgect

Description: "Send n to +oo " in an inequality with an extended sum. (Contributed by Thierry Arnoux, 24-May-2020)

Ref Expression
Hypotheses esumsup.1 
|- ( ph -> B e. ( 0 [,] +oo ) )
esumsup.2 
|- ( ( ph /\ k e. NN ) -> A e. ( 0 [,] +oo ) )
esumgect.1 
|- ( ( ph /\ n e. NN ) -> sum* k e. ( 1 ... n ) A <_ B )
Assertion esumgect 
|- ( ph -> sum* k e. NN A <_ B )

Proof

Step Hyp Ref Expression
1 esumsup.1 
 |-  ( ph -> B e. ( 0 [,] +oo ) )
2 esumsup.2 
 |-  ( ( ph /\ k e. NN ) -> A e. ( 0 [,] +oo ) )
3 esumgect.1 
 |-  ( ( ph /\ n e. NN ) -> sum* k e. ( 1 ... n ) A <_ B )
4 1 2 esumsup 
 |-  ( ph -> sum* k e. NN A = sup ( ran ( n e. NN |-> sum* k e. ( 1 ... n ) A ) , RR* , < ) )
5 nfv 
 |-  F/ n ph
6 nfcv 
 |-  F/_ n z
7 nfmpt1 
 |-  F/_ n ( n e. NN |-> sum* k e. ( 1 ... n ) A )
8 7 nfrn 
 |-  F/_ n ran ( n e. NN |-> sum* k e. ( 1 ... n ) A )
9 6 8 nfel 
 |-  F/ n z e. ran ( n e. NN |-> sum* k e. ( 1 ... n ) A )
10 5 9 nfan 
 |-  F/ n ( ph /\ z e. ran ( n e. NN |-> sum* k e. ( 1 ... n ) A ) )
11 simpr 
 |-  ( ( ( ( ph /\ z e. ran ( n e. NN |-> sum* k e. ( 1 ... n ) A ) ) /\ n e. NN ) /\ z = sum* k e. ( 1 ... n ) A ) -> z = sum* k e. ( 1 ... n ) A )
12 simplll 
 |-  ( ( ( ( ph /\ z e. ran ( n e. NN |-> sum* k e. ( 1 ... n ) A ) ) /\ n e. NN ) /\ z = sum* k e. ( 1 ... n ) A ) -> ph )
13 simplr 
 |-  ( ( ( ( ph /\ z e. ran ( n e. NN |-> sum* k e. ( 1 ... n ) A ) ) /\ n e. NN ) /\ z = sum* k e. ( 1 ... n ) A ) -> n e. NN )
14 12 13 3 syl2anc 
 |-  ( ( ( ( ph /\ z e. ran ( n e. NN |-> sum* k e. ( 1 ... n ) A ) ) /\ n e. NN ) /\ z = sum* k e. ( 1 ... n ) A ) -> sum* k e. ( 1 ... n ) A <_ B )
15 11 14 eqbrtrd 
 |-  ( ( ( ( ph /\ z e. ran ( n e. NN |-> sum* k e. ( 1 ... n ) A ) ) /\ n e. NN ) /\ z = sum* k e. ( 1 ... n ) A ) -> z <_ B )
16 eqid 
 |-  ( n e. NN |-> sum* k e. ( 1 ... n ) A ) = ( n e. NN |-> sum* k e. ( 1 ... n ) A )
17 esumex 
 |-  sum* k e. ( 1 ... n ) A e. _V
18 16 17 elrnmpti 
 |-  ( z e. ran ( n e. NN |-> sum* k e. ( 1 ... n ) A ) <-> E. n e. NN z = sum* k e. ( 1 ... n ) A )
19 18 bilani 
 |-  ( ( ph /\ z e. ran ( n e. NN |-> sum* k e. ( 1 ... n ) A ) ) -> E. n e. NN z = sum* k e. ( 1 ... n ) A )
20 10 15 19 r19.29af 
 |-  ( ( ph /\ z e. ran ( n e. NN |-> sum* k e. ( 1 ... n ) A ) ) -> z <_ B )
21 20 ralrimiva 
 |-  ( ph -> A. z e. ran ( n e. NN |-> sum* k e. ( 1 ... n ) A ) z <_ B )
22 ovexd 
 |-  ( ( ph /\ n e. NN ) -> ( 1 ... n ) e. _V )
23 simpll 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ph )
24 fz1ssnn 
 |-  ( 1 ... n ) C_ NN
25 24 a1i 
 |-  ( ( ph /\ n e. NN ) -> ( 1 ... n ) C_ NN )
26 25 sselda 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> k e. NN )
27 23 26 2 syl2anc 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> A e. ( 0 [,] +oo ) )
28 27 ralrimiva 
 |-  ( ( ph /\ n e. NN ) -> A. k e. ( 1 ... n ) A e. ( 0 [,] +oo ) )
29 nfcv 
 |-  F/_ k ( 1 ... n )
30 29 esumcl 
 |-  ( ( ( 1 ... n ) e. _V /\ A. k e. ( 1 ... n ) A e. ( 0 [,] +oo ) ) -> sum* k e. ( 1 ... n ) A e. ( 0 [,] +oo ) )
31 22 28 30 syl2anc 
 |-  ( ( ph /\ n e. NN ) -> sum* k e. ( 1 ... n ) A e. ( 0 [,] +oo ) )
32 31 ralrimiva 
 |-  ( ph -> A. n e. NN sum* k e. ( 1 ... n ) A e. ( 0 [,] +oo ) )
33 16 rnmptss 
 |-  ( A. n e. NN sum* k e. ( 1 ... n ) A e. ( 0 [,] +oo ) -> ran ( n e. NN |-> sum* k e. ( 1 ... n ) A ) C_ ( 0 [,] +oo ) )
34 32 33 syl 
 |-  ( ph -> ran ( n e. NN |-> sum* k e. ( 1 ... n ) A ) C_ ( 0 [,] +oo ) )
35 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
36 34 35 sstrdi 
 |-  ( ph -> ran ( n e. NN |-> sum* k e. ( 1 ... n ) A ) C_ RR* )
37 35 1 sselid 
 |-  ( ph -> B e. RR* )
38 supxrleub 
 |-  ( ( ran ( n e. NN |-> sum* k e. ( 1 ... n ) A ) C_ RR* /\ B e. RR* ) -> ( sup ( ran ( n e. NN |-> sum* k e. ( 1 ... n ) A ) , RR* , < ) <_ B <-> A. z e. ran ( n e. NN |-> sum* k e. ( 1 ... n ) A ) z <_ B ) )
39 36 37 38 syl2anc 
 |-  ( ph -> ( sup ( ran ( n e. NN |-> sum* k e. ( 1 ... n ) A ) , RR* , < ) <_ B <-> A. z e. ran ( n e. NN |-> sum* k e. ( 1 ... n ) A ) z <_ B ) )
40 21 39 mpbird 
 |-  ( ph -> sup ( ran ( n e. NN |-> sum* k e. ( 1 ... n ) A ) , RR* , < ) <_ B )
41 4 40 eqbrtrd 
 |-  ( ph -> sum* k e. NN A <_ B )