Metamath Proof Explorer

Theorem esumpr2

Description: Extended sum over a pair, with a relaxed condition compared to esumpr . (Contributed by Thierry Arnoux, 2-Jan-2017)

Ref Expression
Hypotheses esumpr.1 
|- ( ( ph /\ k = A ) -> C = D )
esumpr.2 
|- ( ( ph /\ k = B ) -> C = E )
esumpr.3 
|- ( ph -> A e. V )
esumpr.4 
|- ( ph -> B e. W )
esumpr.5 
|- ( ph -> D e. ( 0 [,] +oo ) )
esumpr.6 
|- ( ph -> E e. ( 0 [,] +oo ) )
esumpr2.1 
|- ( ph -> ( A = B -> ( D = 0 \/ D = +oo ) ) )
Assertion esumpr2 
|- ( ph -> sum* k e. { A , B } C = ( D +e E ) )

Proof

Step Hyp Ref Expression
1 esumpr.1 
 |-  ( ( ph /\ k = A ) -> C = D )
2 esumpr.2 
 |-  ( ( ph /\ k = B ) -> C = E )
3 esumpr.3 
 |-  ( ph -> A e. V )
4 esumpr.4 
 |-  ( ph -> B e. W )
5 esumpr.5 
 |-  ( ph -> D e. ( 0 [,] +oo ) )
6 esumpr.6 
 |-  ( ph -> E e. ( 0 [,] +oo ) )
7 esumpr2.1 
 |-  ( ph -> ( A = B -> ( D = 0 \/ D = +oo ) ) )
8 simpr 
 |-  ( ( ph /\ A = B ) -> A = B )
9 dfsn2 
 |-  { A } = { A , A }
10 preq2 
 |-  ( A = B -> { A , A } = { A , B } )
11 9 10 eqtr2id 
 |-  ( A = B -> { A , B } = { A } )
12 esumeq1 
 |-  ( { A , B } = { A } -> sum* k e. { A , B } C = sum* k e. { A } C )
13 8 11 12 3syl 
 |-  ( ( ph /\ A = B ) -> sum* k e. { A , B } C = sum* k e. { A } C )
14 1 3 5 esumsn 
 |-  ( ph -> sum* k e. { A } C = D )
15 14 adantr 
 |-  ( ( ph /\ A = B ) -> sum* k e. { A } C = D )
16 13 15 eqtrd 
 |-  ( ( ph /\ A = B ) -> sum* k e. { A , B } C = D )
17 oveq2 
 |-  ( D = 0 -> ( D +e D ) = ( D +e 0 ) )
18 0xr 
 |-  0 e. RR*
19 eleq1 
 |-  ( D = 0 -> ( D e. RR* <-> 0 e. RR* ) )
20 18 19 mpbiri 
 |-  ( D = 0 -> D e. RR* )
21 xaddid1 
 |-  ( D e. RR* -> ( D +e 0 ) = D )
22 20 21 syl 
 |-  ( D = 0 -> ( D +e 0 ) = D )
23 17 22 eqtrd 
 |-  ( D = 0 -> ( D +e D ) = D )
24 pnfxr 
 |-  +oo e. RR*
25 eleq1 
 |-  ( D = +oo -> ( D e. RR* <-> +oo e. RR* ) )
26 24 25 mpbiri 
 |-  ( D = +oo -> D e. RR* )
27 pnfnemnf 
 |-  +oo =/= -oo
28 neeq1 
 |-  ( D = +oo -> ( D =/= -oo <-> +oo =/= -oo ) )
29 27 28 mpbiri 
 |-  ( D = +oo -> D =/= -oo )
30 xaddpnf1 
 |-  ( ( D e. RR* /\ D =/= -oo ) -> ( D +e +oo ) = +oo )
31 26 29 30 syl2anc 
 |-  ( D = +oo -> ( D +e +oo ) = +oo )
32 oveq2 
 |-  ( D = +oo -> ( D +e D ) = ( D +e +oo ) )
33 id 
 |-  ( D = +oo -> D = +oo )
34 31 32 33 3eqtr4d 
 |-  ( D = +oo -> ( D +e D ) = D )
35 23 34 jaoi 
 |-  ( ( D = 0 \/ D = +oo ) -> ( D +e D ) = D )
36 7 35 syl6 
 |-  ( ph -> ( A = B -> ( D +e D ) = D ) )
37 36 imp 
 |-  ( ( ph /\ A = B ) -> ( D +e D ) = D )
38 simpll 
 |-  ( ( ( ph /\ A = B ) /\ k = B ) -> ph )
39 eqeq2 
 |-  ( A = B -> ( k = A <-> k = B ) )
40 39 biimprd 
 |-  ( A = B -> ( k = B -> k = A ) )
41 8 40 syl 
 |-  ( ( ph /\ A = B ) -> ( k = B -> k = A ) )
42 41 imp 
 |-  ( ( ( ph /\ A = B ) /\ k = B ) -> k = A )
43 38 42 1 syl2anc 
 |-  ( ( ( ph /\ A = B ) /\ k = B ) -> C = D )
44 4 adantr 
 |-  ( ( ph /\ A = B ) -> B e. W )
45 5 adantr 
 |-  ( ( ph /\ A = B ) -> D e. ( 0 [,] +oo ) )
46 43 44 45 esumsn 
 |-  ( ( ph /\ A = B ) -> sum* k e. { B } C = D )
47 2 4 6 esumsn 
 |-  ( ph -> sum* k e. { B } C = E )
48 47 adantr 
 |-  ( ( ph /\ A = B ) -> sum* k e. { B } C = E )
49 46 48 eqtr3d 
 |-  ( ( ph /\ A = B ) -> D = E )
50 49 oveq2d 
 |-  ( ( ph /\ A = B ) -> ( D +e D ) = ( D +e E ) )
51 16 37 50 3eqtr2d 
 |-  ( ( ph /\ A = B ) -> sum* k e. { A , B } C = ( D +e E ) )
52 1 adantlr 
 |-  ( ( ( ph /\ A =/= B ) /\ k = A ) -> C = D )
53 2 adantlr 
 |-  ( ( ( ph /\ A =/= B ) /\ k = B ) -> C = E )
54 3 adantr 
 |-  ( ( ph /\ A =/= B ) -> A e. V )
55 4 adantr 
 |-  ( ( ph /\ A =/= B ) -> B e. W )
56 5 adantr 
 |-  ( ( ph /\ A =/= B ) -> D e. ( 0 [,] +oo ) )
57 6 adantr 
 |-  ( ( ph /\ A =/= B ) -> E e. ( 0 [,] +oo ) )
58 simpr 
 |-  ( ( ph /\ A =/= B ) -> A =/= B )
59 52 53 54 55 56 57 58 esumpr 
 |-  ( ( ph /\ A =/= B ) -> sum* k e. { A , B } C = ( D +e E ) )
60 51 59 pm2.61dane 
 |-  ( ph -> sum* k e. { A , B } C = ( D +e E ) )