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 biimpi 
 |-  ( z e. ran ( n e. NN |-> sum* k e. ( 1 ... n ) A ) -> E. n e. NN z = sum* k e. ( 1 ... n ) A )
20 19 adantl 
 |-  ( ( ph /\ z e. ran ( n e. NN |-> sum* k e. ( 1 ... n ) A ) ) -> E. n e. NN z = sum* k e. ( 1 ... n ) A )
21 10 15 20 r19.29af 
 |-  ( ( ph /\ z e. ran ( n e. NN |-> sum* k e. ( 1 ... n ) A ) ) -> z <_ B )
22 21 ralrimiva 
 |-  ( ph -> A. z e. ran ( n e. NN |-> sum* k e. ( 1 ... n ) A ) z <_ B )
23 ovexd 
 |-  ( ( ph /\ n e. NN ) -> ( 1 ... n ) e. _V )
24 simpll 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ph )
25 fz1ssnn 
 |-  ( 1 ... n ) C_ NN
26 25 a1i 
 |-  ( ( ph /\ n e. NN ) -> ( 1 ... n ) C_ NN )
27 26 sselda 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> k e. NN )
28 24 27 2 syl2anc 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> A e. ( 0 [,] +oo ) )
29 28 ralrimiva 
 |-  ( ( ph /\ n e. NN ) -> A. k e. ( 1 ... n ) A e. ( 0 [,] +oo ) )
30 nfcv 
 |-  F/_ k ( 1 ... n )
31 30 esumcl 
 |-  ( ( ( 1 ... n ) e. _V /\ A. k e. ( 1 ... n ) A e. ( 0 [,] +oo ) ) -> sum* k e. ( 1 ... n ) A e. ( 0 [,] +oo ) )
32 23 29 31 syl2anc 
 |-  ( ( ph /\ n e. NN ) -> sum* k e. ( 1 ... n ) A e. ( 0 [,] +oo ) )
33 32 ralrimiva 
 |-  ( ph -> A. n e. NN sum* k e. ( 1 ... n ) A e. ( 0 [,] +oo ) )
34 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 ) )
35 33 34 syl 
 |-  ( ph -> ran ( n e. NN |-> sum* k e. ( 1 ... n ) A ) C_ ( 0 [,] +oo ) )
36 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
37 35 36 sstrdi 
 |-  ( ph -> ran ( n e. NN |-> sum* k e. ( 1 ... n ) A ) C_ RR* )
38 36 1 sseldi 
 |-  ( ph -> B e. RR* )
39 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 ) )
40 37 38 39 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 ) )
41 22 40 mpbird 
 |-  ( ph -> sup ( ran ( n e. NN |-> sum* k e. ( 1 ... n ) A ) , RR* , < ) <_ B )
42 4 41 eqbrtrd 
 |-  ( ph -> sum* k e. NN A <_ B )