Metamath Proof Explorer

Theorem sge0p1

Description: The addition of the next term in a finite sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0p1.1 
|- ( ph -> N e. ( ZZ>= ` M ) )
sge0p1.2 
|- ( ( ph /\ k e. ( M ... ( N + 1 ) ) ) -> A e. ( 0 [,] +oo ) )
sge0p1.3 
|- ( k = ( N + 1 ) -> A = B )
Assertion sge0p1 
|- ( ph -> ( sum^ ` ( k e. ( M ... ( N + 1 ) ) |-> A ) ) = ( ( sum^ ` ( k e. ( M ... N ) |-> A ) ) +e B ) )

Proof

Step Hyp Ref Expression
1 sge0p1.1 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
2 sge0p1.2 
 |-  ( ( ph /\ k e. ( M ... ( N + 1 ) ) ) -> A e. ( 0 [,] +oo ) )
3 sge0p1.3 
 |-  ( k = ( N + 1 ) -> A = B )
4 fzsuc 
 |-  ( N e. ( ZZ>= ` M ) -> ( M ... ( N + 1 ) ) = ( ( M ... N ) u. { ( N + 1 ) } ) )
5 1 4 syl 
 |-  ( ph -> ( M ... ( N + 1 ) ) = ( ( M ... N ) u. { ( N + 1 ) } ) )
6 5 mpteq1d 
 |-  ( ph -> ( k e. ( M ... ( N + 1 ) ) |-> A ) = ( k e. ( ( M ... N ) u. { ( N + 1 ) } ) |-> A ) )
7 6 fveq2d 
 |-  ( ph -> ( sum^ ` ( k e. ( M ... ( N + 1 ) ) |-> A ) ) = ( sum^ ` ( k e. ( ( M ... N ) u. { ( N + 1 ) } ) |-> A ) ) )
8 nfv 
 |-  F/ k ph
9 ovex 
 |-  ( M ... N ) e. _V
10 9 a1i 
 |-  ( ph -> ( M ... N ) e. _V )
11 snex 
 |-  { ( N + 1 ) } e. _V
12 11 a1i 
 |-  ( ph -> { ( N + 1 ) } e. _V )
13 fzp1disj 
 |-  ( ( M ... N ) i^i { ( N + 1 ) } ) = (/)
14 13 a1i 
 |-  ( ph -> ( ( M ... N ) i^i { ( N + 1 ) } ) = (/) )
15 0xr 
 |-  0 e. RR*
16 15 a1i 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> 0 e. RR* )
17 pnfxr 
 |-  +oo e. RR*
18 17 a1i 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> +oo e. RR* )
19 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
20 simpl 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> ph )
21 fzelp1 
 |-  ( k e. ( M ... N ) -> k e. ( M ... ( N + 1 ) ) )
22 21 adantl 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> k e. ( M ... ( N + 1 ) ) )
23 20 22 2 syl2anc 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> A e. ( 0 [,] +oo ) )
24 19 23 sselid 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> A e. RR* )
25 iccgelb 
 |-  ( ( 0 e. RR* /\ +oo e. RR* /\ A e. ( 0 [,] +oo ) ) -> 0 <_ A )
26 16 18 23 25 syl3anc 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> 0 <_ A )
27 iccleub 
 |-  ( ( 0 e. RR* /\ +oo e. RR* /\ A e. ( 0 [,] +oo ) ) -> A <_ +oo )
28 16 18 23 27 syl3anc 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> A <_ +oo )
29 16 18 24 26 28 eliccxrd 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> A e. ( 0 [,] +oo ) )
30 simpl 
 |-  ( ( ph /\ k e. { ( N + 1 ) } ) -> ph )
31 elsni 
 |-  ( k e. { ( N + 1 ) } -> k = ( N + 1 ) )
32 31 adantl 
 |-  ( ( ph /\ k e. { ( N + 1 ) } ) -> k = ( N + 1 ) )
33 simpr 
 |-  ( ( ph /\ k = ( N + 1 ) ) -> k = ( N + 1 ) )
34 peano2uz 
 |-  ( N e. ( ZZ>= ` M ) -> ( N + 1 ) e. ( ZZ>= ` M ) )
35 eluzfz2 
 |-  ( ( N + 1 ) e. ( ZZ>= ` M ) -> ( N + 1 ) e. ( M ... ( N + 1 ) ) )
36 1 34 35 3syl 
 |-  ( ph -> ( N + 1 ) e. ( M ... ( N + 1 ) ) )
37 36 adantr 
 |-  ( ( ph /\ k = ( N + 1 ) ) -> ( N + 1 ) e. ( M ... ( N + 1 ) ) )
38 33 37 eqeltrd 
 |-  ( ( ph /\ k = ( N + 1 ) ) -> k e. ( M ... ( N + 1 ) ) )
39 30 32 38 syl2anc 
 |-  ( ( ph /\ k e. { ( N + 1 ) } ) -> k e. ( M ... ( N + 1 ) ) )
40 30 39 2 syl2anc 
 |-  ( ( ph /\ k e. { ( N + 1 ) } ) -> A e. ( 0 [,] +oo ) )
41 8 10 12 14 29 40 sge0splitmpt 
 |-  ( ph -> ( sum^ ` ( k e. ( ( M ... N ) u. { ( N + 1 ) } ) |-> A ) ) = ( ( sum^ ` ( k e. ( M ... N ) |-> A ) ) +e ( sum^ ` ( k e. { ( N + 1 ) } |-> A ) ) ) )
42 ovex 
 |-  ( N + 1 ) e. _V
43 42 a1i 
 |-  ( ph -> ( N + 1 ) e. _V )
44 id 
 |-  ( ph -> ph )
45 eleq1 
 |-  ( k = ( N + 1 ) -> ( k e. ( M ... ( N + 1 ) ) <-> ( N + 1 ) e. ( M ... ( N + 1 ) ) ) )
46 45 anbi2d 
 |-  ( k = ( N + 1 ) -> ( ( ph /\ k e. ( M ... ( N + 1 ) ) ) <-> ( ph /\ ( N + 1 ) e. ( M ... ( N + 1 ) ) ) ) )
47 3 eleq1d 
 |-  ( k = ( N + 1 ) -> ( A e. ( 0 [,] +oo ) <-> B e. ( 0 [,] +oo ) ) )
48 46 47 imbi12d 
 |-  ( k = ( N + 1 ) -> ( ( ( ph /\ k e. ( M ... ( N + 1 ) ) ) -> A e. ( 0 [,] +oo ) ) <-> ( ( ph /\ ( N + 1 ) e. ( M ... ( N + 1 ) ) ) -> B e. ( 0 [,] +oo ) ) ) )
49 48 2 vtoclg 
 |-  ( ( N + 1 ) e. _V -> ( ( ph /\ ( N + 1 ) e. ( M ... ( N + 1 ) ) ) -> B e. ( 0 [,] +oo ) ) )
50 42 49 ax-mp 
 |-  ( ( ph /\ ( N + 1 ) e. ( M ... ( N + 1 ) ) ) -> B e. ( 0 [,] +oo ) )
51 44 36 50 syl2anc 
 |-  ( ph -> B e. ( 0 [,] +oo ) )
52 43 51 3 sge0snmpt 
 |-  ( ph -> ( sum^ ` ( k e. { ( N + 1 ) } |-> A ) ) = B )
53 52 oveq2d 
 |-  ( ph -> ( ( sum^ ` ( k e. ( M ... N ) |-> A ) ) +e ( sum^ ` ( k e. { ( N + 1 ) } |-> A ) ) ) = ( ( sum^ ` ( k e. ( M ... N ) |-> A ) ) +e B ) )
54 7 41 53 3eqtrd 
 |-  ( ph -> ( sum^ ` ( k e. ( M ... ( N + 1 ) ) |-> A ) ) = ( ( sum^ ` ( k e. ( M ... N ) |-> A ) ) +e B ) )