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	⊢ ( ( 𝜑 ∧ 𝑘 = 𝐴 ) → 𝐶 = 𝐷 )
	esumpr.2	⊢ ( ( 𝜑 ∧ 𝑘 = 𝐵 ) → 𝐶 = 𝐸 )
	esumpr.3	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	esumpr.4	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
	esumpr.5	⊢ ( 𝜑 → 𝐷 ∈ ( 0 [,] +∞ ) )
	esumpr.6	⊢ ( 𝜑 → 𝐸 ∈ ( 0 [,] +∞ ) )
	esumpr2.1	⊢ ( 𝜑 → ( 𝐴 = 𝐵 → ( 𝐷 = 0 ∨ 𝐷 = +∞ ) ) )
Assertion	esumpr2	⊢ ( 𝜑 → Σ* 𝑘 ∈ { 𝐴 , 𝐵 } 𝐶 = ( 𝐷 +e 𝐸 ) )

Proof

Step	Hyp	Ref	Expression
1		esumpr.1	⊢ ( ( 𝜑 ∧ 𝑘 = 𝐴 ) → 𝐶 = 𝐷 )
2		esumpr.2	⊢ ( ( 𝜑 ∧ 𝑘 = 𝐵 ) → 𝐶 = 𝐸 )
3		esumpr.3	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
4		esumpr.4	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
5		esumpr.5	⊢ ( 𝜑 → 𝐷 ∈ ( 0 [,] +∞ ) )
6		esumpr.6	⊢ ( 𝜑 → 𝐸 ∈ ( 0 [,] +∞ ) )
7		esumpr2.1	⊢ ( 𝜑 → ( 𝐴 = 𝐵 → ( 𝐷 = 0 ∨ 𝐷 = +∞ ) ) )
8		simpr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝐴 = 𝐵 )
9		dfsn2	⊢ { 𝐴 } = { 𝐴 , 𝐴 }
10		preq2	⊢ ( 𝐴 = 𝐵 → { 𝐴 , 𝐴 } = { 𝐴 , 𝐵 } )
11	9 10	eqtr2id	⊢ ( 𝐴 = 𝐵 → { 𝐴 , 𝐵 } = { 𝐴 } )
12		esumeq1	⊢ ( { 𝐴 , 𝐵 } = { 𝐴 } → Σ* 𝑘 ∈ { 𝐴 , 𝐵 } 𝐶 = Σ* 𝑘 ∈ { 𝐴 } 𝐶 )
13	8 11 12	3syl	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → Σ* 𝑘 ∈ { 𝐴 , 𝐵 } 𝐶 = Σ* 𝑘 ∈ { 𝐴 } 𝐶 )
14	1 3 5	esumsn	⊢ ( 𝜑 → Σ* 𝑘 ∈ { 𝐴 } 𝐶 = 𝐷 )
15	14	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → Σ* 𝑘 ∈ { 𝐴 } 𝐶 = 𝐷 )
16	13 15	eqtrd	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → Σ* 𝑘 ∈ { 𝐴 , 𝐵 } 𝐶 = 𝐷 )
17		oveq2	⊢ ( 𝐷 = 0 → ( 𝐷 +e 𝐷 ) = ( 𝐷 +e 0 ) )
18		0xr	⊢ 0 ∈ ℝ*
19		eleq1	⊢ ( 𝐷 = 0 → ( 𝐷 ∈ ℝ* ↔ 0 ∈ ℝ* ) )
20	18 19	mpbiri	⊢ ( 𝐷 = 0 → 𝐷 ∈ ℝ* )
21		xaddrid	⊢ ( 𝐷 ∈ ℝ* → ( 𝐷 +e 0 ) = 𝐷 )
22	20 21	syl	⊢ ( 𝐷 = 0 → ( 𝐷 +e 0 ) = 𝐷 )
23	17 22	eqtrd	⊢ ( 𝐷 = 0 → ( 𝐷 +e 𝐷 ) = 𝐷 )
24		pnfxr	⊢ +∞ ∈ ℝ*
25		eleq1	⊢ ( 𝐷 = +∞ → ( 𝐷 ∈ ℝ* ↔ +∞ ∈ ℝ* ) )
26	24 25	mpbiri	⊢ ( 𝐷 = +∞ → 𝐷 ∈ ℝ* )
27		pnfnemnf	⊢ +∞ ≠ -∞
28		neeq1	⊢ ( 𝐷 = +∞ → ( 𝐷 ≠ -∞ ↔ +∞ ≠ -∞ ) )
29	27 28	mpbiri	⊢ ( 𝐷 = +∞ → 𝐷 ≠ -∞ )
30		xaddpnf1	⊢ ( ( 𝐷 ∈ ℝ* ∧ 𝐷 ≠ -∞ ) → ( 𝐷 +e +∞ ) = +∞ )
31	26 29 30	syl2anc	⊢ ( 𝐷 = +∞ → ( 𝐷 +e +∞ ) = +∞ )
32		oveq2	⊢ ( 𝐷 = +∞ → ( 𝐷 +e 𝐷 ) = ( 𝐷 +e +∞ ) )
33		id	⊢ ( 𝐷 = +∞ → 𝐷 = +∞ )
34	31 32 33	3eqtr4d	⊢ ( 𝐷 = +∞ → ( 𝐷 +e 𝐷 ) = 𝐷 )
35	23 34	jaoi	⊢ ( ( 𝐷 = 0 ∨ 𝐷 = +∞ ) → ( 𝐷 +e 𝐷 ) = 𝐷 )
36	7 35	syl6	⊢ ( 𝜑 → ( 𝐴 = 𝐵 → ( 𝐷 +e 𝐷 ) = 𝐷 ) )
37	36	imp	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → ( 𝐷 +e 𝐷 ) = 𝐷 )
38		simpll	⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐵 ) ∧ 𝑘 = 𝐵 ) → 𝜑 )
39		eqeq2	⊢ ( 𝐴 = 𝐵 → ( 𝑘 = 𝐴 ↔ 𝑘 = 𝐵 ) )
40	39	biimprd	⊢ ( 𝐴 = 𝐵 → ( 𝑘 = 𝐵 → 𝑘 = 𝐴 ) )
41	8 40	syl	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → ( 𝑘 = 𝐵 → 𝑘 = 𝐴 ) )
42	41	imp	⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐵 ) ∧ 𝑘 = 𝐵 ) → 𝑘 = 𝐴 )
43	38 42 1	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐵 ) ∧ 𝑘 = 𝐵 ) → 𝐶 = 𝐷 )
44	4	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝐵 ∈ 𝑊 )
45	5	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝐷 ∈ ( 0 [,] +∞ ) )
46	43 44 45	esumsn	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → Σ* 𝑘 ∈ { 𝐵 } 𝐶 = 𝐷 )
47	2 4 6	esumsn	⊢ ( 𝜑 → Σ* 𝑘 ∈ { 𝐵 } 𝐶 = 𝐸 )
48	47	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → Σ* 𝑘 ∈ { 𝐵 } 𝐶 = 𝐸 )
49	46 48	eqtr3d	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝐷 = 𝐸 )
50	49	oveq2d	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → ( 𝐷 +e 𝐷 ) = ( 𝐷 +e 𝐸 ) )
51	16 37 50	3eqtr2d	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → Σ* 𝑘 ∈ { 𝐴 , 𝐵 } 𝐶 = ( 𝐷 +e 𝐸 ) )
52	1	adantlr	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑘 = 𝐴 ) → 𝐶 = 𝐷 )
53	2	adantlr	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑘 = 𝐵 ) → 𝐶 = 𝐸 )
54	3	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝐴 ∈ 𝑉 )
55	4	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝐵 ∈ 𝑊 )
56	5	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝐷 ∈ ( 0 [,] +∞ ) )
57	6	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝐸 ∈ ( 0 [,] +∞ ) )
58		simpr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝐴 ≠ 𝐵 )
59	52 53 54 55 56 57 58	esumpr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → Σ* 𝑘 ∈ { 𝐴 , 𝐵 } 𝐶 = ( 𝐷 +e 𝐸 ) )
60	51 59	pm2.61dane	⊢ ( 𝜑 → Σ* 𝑘 ∈ { 𝐴 , 𝐵 } 𝐶 = ( 𝐷 +e 𝐸 ) )