Theorem esumpad2

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

	Ref	Expression
Hypotheses	esumpad.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	esumpad.2	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
	esumpad.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
	esumpad.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → 𝐶 = 0 )
Assertion	esumpad2	⊢ ( 𝜑 → Σ* 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 = Σ* 𝑘 ∈ 𝐴 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		esumpad.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		esumpad.2	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3		esumpad.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
4		esumpad.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → 𝐶 = 0 )
5		nfv	⊢ Ⅎ 𝑘 𝜑
6		difssd	⊢ ( 𝜑 → ( 𝐴 ∖ 𝐵 ) ⊆ 𝐴 )
7	5 1 3 6	esummono	⊢ ( 𝜑 → Σ* 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 ≤ Σ* 𝑘 ∈ 𝐴 𝐶 )
8		unexg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ∪ 𝐵 ) ∈ V )
9	1 2 8	syl2anc	⊢ ( 𝜑 → ( 𝐴 ∪ 𝐵 ) ∈ V )
10		elun	⊢ ( 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) ↔ ( 𝑘 ∈ 𝐴 ∨ 𝑘 ∈ 𝐵 ) )
11		0e0iccpnf	⊢ 0 ∈ ( 0 [,] +∞ )
12	4 11	eqeltrdi	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
13	3 12	jaodan	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∨ 𝑘 ∈ 𝐵 ) ) → 𝐶 ∈ ( 0 [,] +∞ ) )
14	10 13	sylan2b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) ) → 𝐶 ∈ ( 0 [,] +∞ ) )
15		ssun1	⊢ 𝐴 ⊆ ( 𝐴 ∪ 𝐵 )
16	15	a1i	⊢ ( 𝜑 → 𝐴 ⊆ ( 𝐴 ∪ 𝐵 ) )
17	5 9 14 16	esummono	⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐶 ≤ Σ* 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) 𝐶 )
18		undif1	⊢ ( ( 𝐴 ∖ 𝐵 ) ∪ 𝐵 ) = ( 𝐴 ∪ 𝐵 )
19		esumeq1	⊢ ( ( ( 𝐴 ∖ 𝐵 ) ∪ 𝐵 ) = ( 𝐴 ∪ 𝐵 ) → Σ* 𝑘 ∈ ( ( 𝐴 ∖ 𝐵 ) ∪ 𝐵 ) 𝐶 = Σ* 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) 𝐶 )
20	18 19	ax-mp	⊢ Σ* 𝑘 ∈ ( ( 𝐴 ∖ 𝐵 ) ∪ 𝐵 ) 𝐶 = Σ* 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) 𝐶
21	1	difexd	⊢ ( 𝜑 → ( 𝐴 ∖ 𝐵 ) ∈ V )
22	6	sselda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) ) → 𝑘 ∈ 𝐴 )
23	22 3	syldan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) ) → 𝐶 ∈ ( 0 [,] +∞ ) )
24	21 2 23 4	esumpad	⊢ ( 𝜑 → Σ* 𝑘 ∈ ( ( 𝐴 ∖ 𝐵 ) ∪ 𝐵 ) 𝐶 = Σ* 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 )
25	20 24	eqtr3id	⊢ ( 𝜑 → Σ* 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) 𝐶 = Σ* 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 )
26	17 25	breqtrd	⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐶 ≤ Σ* 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 )
27	7 26	jca	⊢ ( 𝜑 → ( Σ* 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 ≤ Σ* 𝑘 ∈ 𝐴 𝐶 ∧ Σ* 𝑘 ∈ 𝐴 𝐶 ≤ Σ* 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 ) )
28		iccssxr	⊢ ( 0 [,] +∞ ) ⊆ ℝ*
29	23	ralrimiva	⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 ∈ ( 0 [,] +∞ ) )
30		nfcv	⊢ Ⅎ 𝑘 ( 𝐴 ∖ 𝐵 )
31	30	esumcl	⊢ ( ( ( 𝐴 ∖ 𝐵 ) ∈ V ∧ ∀ 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 ∈ ( 0 [,] +∞ ) ) → Σ* 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 ∈ ( 0 [,] +∞ ) )
32	21 29 31	syl2anc	⊢ ( 𝜑 → Σ* 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 ∈ ( 0 [,] +∞ ) )
33	28 32	sselid	⊢ ( 𝜑 → Σ* 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 ∈ ℝ* )
34	3	ralrimiva	⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 𝐶 ∈ ( 0 [,] +∞ ) )
35		nfcv	⊢ Ⅎ 𝑘 𝐴
36	35	esumcl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ∈ ( 0 [,] +∞ ) ) → Σ* 𝑘 ∈ 𝐴 𝐶 ∈ ( 0 [,] +∞ ) )
37	1 34 36	syl2anc	⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐶 ∈ ( 0 [,] +∞ ) )
38	28 37	sselid	⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐶 ∈ ℝ* )
39		xrletri3	⊢ ( ( Σ* 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 ∈ ℝ* ∧ Σ* 𝑘 ∈ 𝐴 𝐶 ∈ ℝ* ) → ( Σ* 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 = Σ* 𝑘 ∈ 𝐴 𝐶 ↔ ( Σ* 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 ≤ Σ* 𝑘 ∈ 𝐴 𝐶 ∧ Σ* 𝑘 ∈ 𝐴 𝐶 ≤ Σ* 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 ) ) )
40	33 38 39	syl2anc	⊢ ( 𝜑 → ( Σ* 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 = Σ* 𝑘 ∈ 𝐴 𝐶 ↔ ( Σ* 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 ≤ Σ* 𝑘 ∈ 𝐴 𝐶 ∧ Σ* 𝑘 ∈ 𝐴 𝐶 ≤ Σ* 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 ) ) )
41	27 40	mpbird	⊢ ( 𝜑 → Σ* 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 = Σ* 𝑘 ∈ 𝐴 𝐶 )