Theorem esummono

Description: Extended sum is monotonic. (Contributed by Thierry Arnoux, 19-Oct-2017)

	Ref	Expression
Hypotheses	esummono.f	⊢ Ⅎ 𝑘 𝜑
	esummono.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
	esummono.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
	esummono.a	⊢ ( 𝜑 → 𝐴 ⊆ 𝐶 )
Assertion	esummono	⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐵 ≤ Σ* 𝑘 ∈ 𝐶 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		esummono.f	⊢ Ⅎ 𝑘 𝜑
2		esummono.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
3		esummono.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
4		esummono.a	⊢ ( 𝜑 → 𝐴 ⊆ 𝐶 )
5		difexg	⊢ ( 𝐶 ∈ 𝑉 → ( 𝐶 ∖ 𝐴 ) ∈ V )
6	2 5	syl	⊢ ( 𝜑 → ( 𝐶 ∖ 𝐴 ) ∈ V )
7		simpr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐶 ∖ 𝐴 ) ) → 𝑘 ∈ ( 𝐶 ∖ 𝐴 ) )
8	7	eldifad	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐶 ∖ 𝐴 ) ) → 𝑘 ∈ 𝐶 )
9	8 3	syldan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐶 ∖ 𝐴 ) ) → 𝐵 ∈ ( 0 [,] +∞ ) )
10	9	ex	⊢ ( 𝜑 → ( 𝑘 ∈ ( 𝐶 ∖ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) ) )
11	1 10	ralrimi	⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 𝐶 ∖ 𝐴 ) 𝐵 ∈ ( 0 [,] +∞ ) )
12		nfcv	⊢ Ⅎ 𝑘 ( 𝐶 ∖ 𝐴 )
13	12	esumcl	⊢ ( ( ( 𝐶 ∖ 𝐴 ) ∈ V ∧ ∀ 𝑘 ∈ ( 𝐶 ∖ 𝐴 ) 𝐵 ∈ ( 0 [,] +∞ ) ) → Σ* 𝑘 ∈ ( 𝐶 ∖ 𝐴 ) 𝐵 ∈ ( 0 [,] +∞ ) )
14	6 11 13	syl2anc	⊢ ( 𝜑 → Σ* 𝑘 ∈ ( 𝐶 ∖ 𝐴 ) 𝐵 ∈ ( 0 [,] +∞ ) )
15		elxrge0	⊢ ( Σ* 𝑘 ∈ ( 𝐶 ∖ 𝐴 ) 𝐵 ∈ ( 0 [,] +∞ ) ↔ ( Σ* 𝑘 ∈ ( 𝐶 ∖ 𝐴 ) 𝐵 ∈ ℝ* ∧ 0 ≤ Σ* 𝑘 ∈ ( 𝐶 ∖ 𝐴 ) 𝐵 ) )
16	15	simprbi	⊢ ( Σ* 𝑘 ∈ ( 𝐶 ∖ 𝐴 ) 𝐵 ∈ ( 0 [,] +∞ ) → 0 ≤ Σ* 𝑘 ∈ ( 𝐶 ∖ 𝐴 ) 𝐵 )
17	14 16	syl	⊢ ( 𝜑 → 0 ≤ Σ* 𝑘 ∈ ( 𝐶 ∖ 𝐴 ) 𝐵 )
18		iccssxr	⊢ ( 0 [,] +∞ ) ⊆ ℝ*
19	2 4	ssexd	⊢ ( 𝜑 → 𝐴 ∈ V )
20	4	sselda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑘 ∈ 𝐶 )
21	20 3	syldan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
22	21	ex	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 → 𝐵 ∈ ( 0 [,] +∞ ) ) )
23	1 22	ralrimi	⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,] +∞ ) )
24		nfcv	⊢ Ⅎ 𝑘 𝐴
25	24	esumcl	⊢ ( ( 𝐴 ∈ V ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,] +∞ ) ) → Σ* 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,] +∞ ) )
26	19 23 25	syl2anc	⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,] +∞ ) )
27	18 26	sseldi	⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐵 ∈ ℝ* )
28	18 14	sseldi	⊢ ( 𝜑 → Σ* 𝑘 ∈ ( 𝐶 ∖ 𝐴 ) 𝐵 ∈ ℝ* )
29		xraddge02	⊢ ( ( Σ* 𝑘 ∈ 𝐴 𝐵 ∈ ℝ* ∧ Σ* 𝑘 ∈ ( 𝐶 ∖ 𝐴 ) 𝐵 ∈ ℝ* ) → ( 0 ≤ Σ* 𝑘 ∈ ( 𝐶 ∖ 𝐴 ) 𝐵 → Σ* 𝑘 ∈ 𝐴 𝐵 ≤ ( Σ* 𝑘 ∈ 𝐴 𝐵 +𝑒 Σ* 𝑘 ∈ ( 𝐶 ∖ 𝐴 ) 𝐵 ) ) )
30	27 28 29	syl2anc	⊢ ( 𝜑 → ( 0 ≤ Σ* 𝑘 ∈ ( 𝐶 ∖ 𝐴 ) 𝐵 → Σ* 𝑘 ∈ 𝐴 𝐵 ≤ ( Σ* 𝑘 ∈ 𝐴 𝐵 +𝑒 Σ* 𝑘 ∈ ( 𝐶 ∖ 𝐴 ) 𝐵 ) ) )
31	17 30	mpd	⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐵 ≤ ( Σ* 𝑘 ∈ 𝐴 𝐵 +𝑒 Σ* 𝑘 ∈ ( 𝐶 ∖ 𝐴 ) 𝐵 ) )
32		disjdif	⊢ ( 𝐴 ∩ ( 𝐶 ∖ 𝐴 ) ) = ∅
33	32	a1i	⊢ ( 𝜑 → ( 𝐴 ∩ ( 𝐶 ∖ 𝐴 ) ) = ∅ )
34	1 24 12 19 6 33 21 9	esumsplit	⊢ ( 𝜑 → Σ* 𝑘 ∈ ( 𝐴 ∪ ( 𝐶 ∖ 𝐴 ) ) 𝐵 = ( Σ* 𝑘 ∈ 𝐴 𝐵 +𝑒 Σ* 𝑘 ∈ ( 𝐶 ∖ 𝐴 ) 𝐵 ) )
35		undif	⊢ ( 𝐴 ⊆ 𝐶 ↔ ( 𝐴 ∪ ( 𝐶 ∖ 𝐴 ) ) = 𝐶 )
36	4 35	sylib	⊢ ( 𝜑 → ( 𝐴 ∪ ( 𝐶 ∖ 𝐴 ) ) = 𝐶 )
37	1 36	esumeq1d	⊢ ( 𝜑 → Σ* 𝑘 ∈ ( 𝐴 ∪ ( 𝐶 ∖ 𝐴 ) ) 𝐵 = Σ* 𝑘 ∈ 𝐶 𝐵 )
38	34 37	eqtr3d	⊢ ( 𝜑 → ( Σ* 𝑘 ∈ 𝐴 𝐵 +𝑒 Σ* 𝑘 ∈ ( 𝐶 ∖ 𝐴 ) 𝐵 ) = Σ* 𝑘 ∈ 𝐶 𝐵 )
39	31 38	breqtrd	⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐵 ≤ Σ* 𝑘 ∈ 𝐶 𝐵 )