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 1 difexd 
 |-  ( ph -> ( A \ B ) e. _V )
22 6 sselda 
 |-  ( ( ph /\ k e. ( A \ B ) ) -> k e. A )
23 22 3 syldan 
 |-  ( ( ph /\ k e. ( A \ B ) ) -> C e. ( 0 [,] +oo ) )
24 21 2 23 4 esumpad 
 |-  ( ph -> sum* k e. ( ( A \ B ) u. B ) C = sum* k e. ( A \ B ) C )
25 20 24 eqtr3id 
 |-  ( ph -> sum* k e. ( A u. B ) C = sum* k e. ( A \ B ) C )
26 17 25 breqtrd 
 |-  ( ph -> sum* k e. A C <_ sum* k e. ( A \ B ) C )
27 7 26 jca 
 |-  ( ph -> ( sum* k e. ( A \ B ) C <_ sum* k e. A C /\ sum* k e. A C <_ sum* k e. ( A \ B ) C ) )
28 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
29 23 ralrimiva 
 |-  ( ph -> A. k e. ( A \ B ) C e. ( 0 [,] +oo ) )
30 nfcv 
 |-  F/_ k ( A \ B )
31 30 esumcl 
 |-  ( ( ( A \ B ) e. _V /\ A. k e. ( A \ B ) C e. ( 0 [,] +oo ) ) -> sum* k e. ( A \ B ) C e. ( 0 [,] +oo ) )
32 21 29 31 syl2anc 
 |-  ( ph -> sum* k e. ( A \ B ) C e. ( 0 [,] +oo ) )
33 28 32 sselid 
 |-  ( ph -> sum* k e. ( A \ B ) C e. RR* )
34 3 ralrimiva 
 |-  ( ph -> A. k e. A C e. ( 0 [,] +oo ) )
35 nfcv 
 |-  F/_ k A
36 35 esumcl 
 |-  ( ( A e. V /\ A. k e. A C e. ( 0 [,] +oo ) ) -> sum* k e. A C e. ( 0 [,] +oo ) )
37 1 34 36 syl2anc 
 |-  ( ph -> sum* k e. A C e. ( 0 [,] +oo ) )
38 28 37 sselid 
 |-  ( ph -> sum* k e. A C e. RR* )
39 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 ) ) )
40 33 38 39 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 ) ) )
41 27 40 mpbird 
 |-  ( ph -> sum* k e. ( A \ B ) C = sum* k e. A C )