Theorem sge0lempt

Description: If all of the terms of sums compare, so do the sums. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	sge0lempt.xph	⊢ Ⅎ 𝑥 𝜑
	sge0lempt.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	sge0lempt.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
	sge0lempt.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
	sge0lempt.le	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ≤ 𝐶 )
Assertion	sge0lempt	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ≤ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		sge0lempt.xph	⊢ Ⅎ 𝑥 𝜑
2		sge0lempt.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		sge0lempt.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
4		sge0lempt.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
5		sge0lempt.le	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ≤ 𝐶 )
6		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
7	1 3 6	fmptdf	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
8		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
9	1 4 8	fmptdf	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
10		nfv	⊢ Ⅎ 𝑥 𝑦 ∈ 𝐴
11	1 10	nfan	⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑦 ∈ 𝐴 )
12		nfcv	⊢ Ⅎ 𝑥 𝑦
13	12	nfcsb1	⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐵
14		nfcv	⊢ Ⅎ 𝑥 ≤
15	12	nfcsb1	⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐶
16	13 14 15	nfbr	⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ≤ ⦋ 𝑦 / 𝑥 ⦌ 𝐶
17	11 16	nfim	⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ≤ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 )
18		eleq1w	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
19	18	anbi2d	⊢ ( 𝑥 = 𝑦 → ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ) )
20		csbeq1a	⊢ ( 𝑥 = 𝑦 → 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
21		csbeq1a	⊢ ( 𝑥 = 𝑦 → 𝐶 = ⦋ 𝑦 / 𝑥 ⦌ 𝐶 )
22	20 21	breq12d	⊢ ( 𝑥 = 𝑦 → ( 𝐵 ≤ 𝐶 ↔ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ≤ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) )
23	19 22	imbi12d	⊢ ( 𝑥 = 𝑦 → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ≤ 𝐶 ) ↔ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ≤ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ) )
24	17 23 5	chvarfv	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ≤ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 )
25		simpr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ 𝐴 )
26	13	nfel1	⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ ( 0 [,] +∞ )
27	11 26	nfim	⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ ( 0 [,] +∞ ) )
28	20	eleq1d	⊢ ( 𝑥 = 𝑦 → ( 𝐵 ∈ ( 0 [,] +∞ ) ↔ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ ( 0 [,] +∞ ) ) )
29	19 28	imbi12d	⊢ ( 𝑥 = 𝑦 → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) ) ↔ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ ( 0 [,] +∞ ) ) ) )
30	27 29 3	chvarfv	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ ( 0 [,] +∞ ) )
31	12 13 20 6	fvmptf	⊢ ( ( 𝑦 ∈ 𝐴 ∧ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ ( 0 [,] +∞ ) ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
32	25 30 31	syl2anc	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
33		nfcv	⊢ Ⅎ 𝑥 ( 0 [,] +∞ )
34	15 33	nfel	⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ∈ ( 0 [,] +∞ )
35	11 34	nfim	⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ∈ ( 0 [,] +∞ ) )
36	21	eleq1d	⊢ ( 𝑥 = 𝑦 → ( 𝐶 ∈ ( 0 [,] +∞ ) ↔ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ∈ ( 0 [,] +∞ ) ) )
37	19 36	imbi12d	⊢ ( 𝑥 = 𝑦 → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ( 0 [,] +∞ ) ) ↔ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ∈ ( 0 [,] +∞ ) ) ) )
38	35 37 4	chvarfv	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ∈ ( 0 [,] +∞ ) )
39	12 15 21 8	fvmptf	⊢ ( ( 𝑦 ∈ 𝐴 ∧ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ∈ ( 0 [,] +∞ ) ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) = ⦋ 𝑦 / 𝑥 ⦌ 𝐶 )
40	25 38 39	syl2anc	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) = ⦋ 𝑦 / 𝑥 ⦌ 𝐶 )
41	32 40	breq12d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) ≤ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) ↔ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ≤ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) )
42	24 41	mpbird	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) ≤ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) )
43	2 7 9 42	sge0le	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ≤ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ) )