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