Metamath Proof Explorer

Theorem esumpad2

Description: Remove zeroes from an extended sum. (Contributed by Thierry Arnoux, 5-Jun-2020)

Ref Expression
Hypotheses esumpad.1 
|- ( ph -> A e. V )
esumpad.2 
|- ( ph -> B e. W )
esumpad.3 
|- ( ( ph /\ k e. A ) -> C e. ( 0 [,] +oo ) )
esumpad.4 
|- ( ( ph /\ k e. B ) -> C = 0 )
Assertion esumpad2 
|- ( ph -> sum* k e. ( A \ B ) C = sum* k e. A C )

Proof

Step Hyp Ref Expression
1 esumpad.1 
 |-  ( ph -> A e. V )
2 esumpad.2 
 |-  ( ph -> B e. W )
3 esumpad.3 
 |-  ( ( ph /\ k e. A ) -> C e. ( 0 [,] +oo ) )
4 esumpad.4 
 |-  ( ( ph /\ k e. B ) -> C = 0 )
5 nfv 
 |-  F/ k ph
6 difssd 
 |-  ( ph -> ( A \ B ) C_ A )
7 5 1 3 6 esummono 
 |-  ( ph -> sum* k e. ( A \ B ) C <_ sum* k e. A C )
8 unexg 
 |-  ( ( A e. V /\ B e. W ) -> ( A u. B ) e. _V )
9 1 2 8 syl2anc 
 |-  ( ph -> ( A u. B ) e. _V )
10 elun 
 |-  ( k e. ( A u. B ) <-> ( k e. A \/ k e. B ) )
11 0e0iccpnf 
 |-  0 e. ( 0 [,] +oo )
12 4 11 eqeltrdi 
 |-  ( ( ph /\ k e. B ) -> C e. ( 0 [,] +oo ) )
13 3 12 jaodan 
 |-  ( ( ph /\ ( k e. A \/ k e. B ) ) -> C e. ( 0 [,] +oo ) )
14 10 13 sylan2b 
 |-  ( ( ph /\ k e. ( A u. B ) ) -> C e. ( 0 [,] +oo ) )
15 ssun1 
 |-  A C_ ( A u. B )
16 15 a1i 
 |-  ( ph -> A C_ ( A u. B ) )
17 5 9 14 16 esummono 
 |-  ( ph -> sum* k e. A C <_ sum* k e. ( A u. B ) C )
18 undif1 
 |-  ( ( A \ B ) u. B ) = ( A u. B )
19 esumeq1 
 |-  ( ( ( A \ B ) u. B ) = ( A u. B ) -> sum* k e. ( ( A \ B ) u. B ) C = sum* k e. ( A u. B ) C )
20 18 19 ax-mp 
 |-  sum* k e. ( ( A \ B ) u. B ) C = sum* k e. ( A u. B ) C
21 difexg 
 |-  ( A e. V -> ( A \ B ) e. _V )
22 1 21 syl 
 |-  ( ph -> ( A \ B ) e. _V )
23 6 sselda 
 |-  ( ( ph /\ k e. ( A \ B ) ) -> k e. A )
24 23 3 syldan 
 |-  ( ( ph /\ k e. ( A \ B ) ) -> C e. ( 0 [,] +oo ) )
25 22 2 24 4 esumpad 
 |-  ( ph -> sum* k e. ( ( A \ B ) u. B ) C = sum* k e. ( A \ B ) C )
26 20 25 eqtr3id 
 |-  ( ph -> sum* k e. ( A u. B ) C = sum* k e. ( A \ B ) C )
27 17 26 breqtrd 
 |-  ( ph -> sum* k e. A C <_ sum* k e. ( A \ B ) C )
28 7 27 jca 
 |-  ( ph -> ( sum* k e. ( A \ B ) C <_ sum* k e. A C /\ sum* k e. A C <_ sum* k e. ( A \ B ) C ) )
29 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
30 24 ralrimiva 
 |-  ( ph -> A. k e. ( A \ B ) C e. ( 0 [,] +oo ) )
31 nfcv 
 |-  F/_ k ( A \ B )
32 31 esumcl 
 |-  ( ( ( A \ B ) e. _V /\ A. k e. ( A \ B ) C e. ( 0 [,] +oo ) ) -> sum* k e. ( A \ B ) C e. ( 0 [,] +oo ) )
33 22 30 32 syl2anc 
 |-  ( ph -> sum* k e. ( A \ B ) C e. ( 0 [,] +oo ) )
34 29 33 sseldi 
 |-  ( ph -> sum* k e. ( A \ B ) C e. RR* )
35 3 ralrimiva 
 |-  ( ph -> A. k e. A C e. ( 0 [,] +oo ) )
36 nfcv 
 |-  F/_ k A
37 36 esumcl 
 |-  ( ( A e. V /\ A. k e. A C e. ( 0 [,] +oo ) ) -> sum* k e. A C e. ( 0 [,] +oo ) )
38 1 35 37 syl2anc 
 |-  ( ph -> sum* k e. A C e. ( 0 [,] +oo ) )
39 29 38 sseldi 
 |-  ( ph -> sum* k e. A C e. RR* )
40 xrletri3 
 |-  ( ( sum* k e. ( A \ B ) C e. RR* /\ sum* k e. A C e. RR* ) -> ( sum* k e. ( A \ B ) C = sum* k e. A C <-> ( sum* k e. ( A \ B ) C <_ sum* k e. A C /\ sum* k e. A C <_ sum* k e. ( A \ B ) C ) ) )
41 34 39 40 syl2anc 
 |-  ( ph -> ( sum* k e. ( A \ B ) C = sum* k e. A C <-> ( sum* k e. ( A \ B ) C <_ sum* k e. A C /\ sum* k e. A C <_ sum* k e. ( A \ B ) C ) ) )
42 28 41 mpbird 
 |-  ( ph -> sum* k e. ( A \ B ) C = sum* k e. A C )