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	$$⊢\left(\phi \wedge k=A\right)\to C=D$$
	esumpr.2	$$⊢\left(\phi \wedge k=B\right)\to C=E$$
	esumpr.3	$$⊢\phi \to A\in V$$
	esumpr.4	$$⊢\phi \to B\in W$$
	esumpr.5	$$⊢\phi \to D\in \left[0,\mathrm{+\infty }\right]$$
	esumpr.6	$$⊢\phi \to E\in \left[0,\mathrm{+\infty }\right]$$
	esumpr2.1	$$⊢\phi \to \left(A=B\to \left(D=0\vee D=\mathrm{+\infty }\right)\right)$$
Assertion	esumpr2	$$⊢\phi \to \underset{k\in \left\{A,B\right\}}{{\sum }^{*}}C=D{+}_{𝑒}E$$

Proof

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