sge0le

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

	Ref	Expression
Hypotheses	sge0le.x	$⊢ φ \to X \in V$
	sge0le.F	$⊢ φ \to F : X ⟶ [0, +∞]$
	sge0le.g	$⊢ φ \to G : X ⟶ [0, +∞]$
	sge0le.le	$⊢ (φ \land x \in X) \to F (x) \leq G (x)$
Assertion	sge0le	$⊢ φ \to sum^(F) \leq sum^(G)$

Proof

Step	Hyp	Ref	Expression
1		sge0le.x	$⊢ φ \to X \in V$
2		sge0le.F	$⊢ φ \to F : X ⟶ [0, +∞]$
3		sge0le.g	$⊢ φ \to G : X ⟶ [0, +∞]$
4		sge0le.le	$⊢ (φ \land x \in X) \to F (x) \leq G (x)$
5	1 2	sge0xrcl	$⊢ φ \to sum^(F) \in ℝ^{*}$
6		pnfge	$⊢ sum^(F) \in ℝ^{*} \to sum^(F) \leq +∞$
7	5 6	syl	$⊢ φ \to sum^(F) \leq +∞$
8	7	adantr	$⊢ (φ \land sum^(G) = +∞) \to sum^(F) \leq +∞$
9		id	$⊢ sum^(G) = +∞ \to sum^(G) = +∞$
10	9	eqcomd	$⊢ sum^(G) = +∞ \to +∞ = sum^(G)$
11	10	adantl	$⊢ (φ \land sum^(G) = +∞) \to +∞ = sum^(G)$
12	8 11	breqtrd	$⊢ (φ \land sum^(G) = +∞) \to sum^(F) \leq sum^(G)$
13		elinel2	$⊢ y \in (𝒫 X \cap Fin) \to y \in Fin$
14	13	adantl	$⊢ ((φ \land \neg sum^(G) = +∞) \land y \in (𝒫 X \cap Fin)) \to y \in Fin$
15	2	adantr	$⊢ (φ \land \neg sum^(G) = +∞) \to F : X ⟶ [0, +∞]$
16	1	adantr	$⊢ (φ \land +∞ \in ran F) \to X \in V$
17	3	adantr	$⊢ (φ \land +∞ \in ran F) \to G : X ⟶ [0, +∞]$
18		simpr	$⊢ (φ \land +∞ \in ran F) \to +∞ \in ran F$
19	2	ffnd	$⊢ φ \to F Fn X$
20		fvelrnb	$⊢ F Fn X \to (+∞ \in ran F \leftrightarrow \exists x \in X F (x) = +∞)$
21	19 20	syl	$⊢ φ \to (+∞ \in ran F \leftrightarrow \exists x \in X F (x) = +∞)$
22	21	adantr	$⊢ (φ \land +∞ \in ran F) \to (+∞ \in ran F \leftrightarrow \exists x \in X F (x) = +∞)$
23	18 22	mpbid	$⊢ (φ \land +∞ \in ran F) \to \exists x \in X F (x) = +∞$
24		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
25	3	ffvelcdmda	$⊢ (φ \land x \in X) \to G (x) \in [0, +∞]$
26	24 25	sselid	$⊢ (φ \land x \in X) \to G (x) \in ℝ^{*}$
27	26	adantr	$⊢ ((φ \land x \in X) \land F (x) = +∞) \to G (x) \in ℝ^{*}$
28		id	$⊢ F (x) = +∞ \to F (x) = +∞$
29	28	eqcomd	$⊢ F (x) = +∞ \to +∞ = F (x)$
30	29	adantl	$⊢ ((φ \land x \in X) \land F (x) = +∞) \to +∞ = F (x)$
31	4	adantr	$⊢ ((φ \land x \in X) \land F (x) = +∞) \to F (x) \leq G (x)$
32	30 31	eqbrtrd	$⊢ ((φ \land x \in X) \land F (x) = +∞) \to +∞ \leq G (x)$
33	27 32	xrgepnfd	$⊢ ((φ \land x \in X) \land F (x) = +∞) \to G (x) = +∞$
34	33	eqcomd	$⊢ ((φ \land x \in X) \land F (x) = +∞) \to +∞ = G (x)$
35	3	ffnd	$⊢ φ \to G Fn X$
36	35	adantr	$⊢ (φ \land x \in X) \to G Fn X$
37		simpr	$⊢ (φ \land x \in X) \to x \in X$
38		fnfvelrn	$⊢ (G Fn X \land x \in X) \to G (x) \in ran G$
39	36 37 38	syl2anc	$⊢ (φ \land x \in X) \to G (x) \in ran G$
40	39	adantr	$⊢ ((φ \land x \in X) \land F (x) = +∞) \to G (x) \in ran G$
41	34 40	eqeltrd	$⊢ ((φ \land x \in X) \land F (x) = +∞) \to +∞ \in ran G$
42	41	ex	$⊢ (φ \land x \in X) \to (F (x) = +∞ \to +∞ \in ran G)$
43	42	adantlr	$⊢ ((φ \land +∞ \in ran F) \land x \in X) \to (F (x) = +∞ \to +∞ \in ran G)$
44	43	rexlimdva	$⊢ (φ \land +∞ \in ran F) \to (\exists x \in X F (x) = +∞ \to +∞ \in ran G)$
45	23 44	mpd	$⊢ (φ \land +∞ \in ran F) \to +∞ \in ran G$
46	16 17 45	sge0pnfval	$⊢ (φ \land +∞ \in ran F) \to sum^(G) = +∞$
47	46	adantlr	$⊢ ((φ \land \neg sum^(G) = +∞) \land +∞ \in ran F) \to sum^(G) = +∞$
48		simplr	$⊢ ((φ \land \neg sum^(G) = +∞) \land +∞ \in ran F) \to \neg sum^(G) = +∞$
49	47 48	pm2.65da	$⊢ (φ \land \neg sum^(G) = +∞) \to \neg +∞ \in ran F$
50	15 49	fge0iccico	$⊢ (φ \land \neg sum^(G) = +∞) \to F : X ⟶ [0, +∞)$
51	50	adantr	$⊢ ((φ \land \neg sum^(G) = +∞) \land y \in (𝒫 X \cap Fin)) \to F : X ⟶ [0, +∞)$
52		elpwinss	$⊢ y \in (𝒫 X \cap Fin) \to y \subseteq X$
53	52	adantl	$⊢ ((φ \land \neg sum^(G) = +∞) \land y \in (𝒫 X \cap Fin)) \to y \subseteq X$
54	51 53	fssresd	$⊢ ((φ \land \neg sum^(G) = +∞) \land y \in (𝒫 X \cap Fin)) \to ({F ↾}_{y}) : y ⟶ [0, +∞)$
55	14 54	sge0fsum	$⊢ ((φ \land \neg sum^(G) = +∞) \land y \in (𝒫 X \cap Fin)) \to sum^({F ↾}_{y}) = \sum_{x \in y} ({F ↾}_{y}) (x)$
56		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
57	54	ffvelcdmda	$⊢ (((φ \land \neg sum^(G) = +∞) \land y \in (𝒫 X \cap Fin)) \land x \in y) \to ({F ↾}_{y}) (x) \in [0, +∞)$
58	56 57	sselid	$⊢ (((φ \land \neg sum^(G) = +∞) \land y \in (𝒫 X \cap Fin)) \land x \in y) \to ({F ↾}_{y}) (x) \in ℝ$
59	14 58	fsumrecl	$⊢ ((φ \land \neg sum^(G) = +∞) \land y \in (𝒫 X \cap Fin)) \to \sum_{x \in y} ({F ↾}_{y}) (x) \in ℝ$
60	55 59	eqeltrd	$⊢ ((φ \land \neg sum^(G) = +∞) \land y \in (𝒫 X \cap Fin)) \to sum^({F ↾}_{y}) \in ℝ$
61	3	adantr	$⊢ (φ \land \neg sum^(G) = +∞) \to G : X ⟶ [0, +∞]$
62	1	adantr	$⊢ (φ \land \neg sum^(G) = +∞) \to X \in V$
63		simpr	$⊢ (φ \land \neg sum^(G) = +∞) \to \neg sum^(G) = +∞$
64	62 61	sge0repnf	$⊢ (φ \land \neg sum^(G) = +∞) \to (sum^(G) \in ℝ \leftrightarrow \neg sum^(G) = +∞)$
65	63 64	mpbird	$⊢ (φ \land \neg sum^(G) = +∞) \to sum^(G) \in ℝ$
66	62 61 65	sge0rern	$⊢ (φ \land \neg sum^(G) = +∞) \to \neg +∞ \in ran G$
67	61 66	fge0iccico	$⊢ (φ \land \neg sum^(G) = +∞) \to G : X ⟶ [0, +∞)$
68	67	adantr	$⊢ ((φ \land \neg sum^(G) = +∞) \land y \in (𝒫 X \cap Fin)) \to G : X ⟶ [0, +∞)$
69	68 53	fssresd	$⊢ ((φ \land \neg sum^(G) = +∞) \land y \in (𝒫 X \cap Fin)) \to ({G ↾}_{y}) : y ⟶ [0, +∞)$
70	14 69	sge0fsum	$⊢ ((φ \land \neg sum^(G) = +∞) \land y \in (𝒫 X \cap Fin)) \to sum^({G ↾}_{y}) = \sum_{x \in y} ({G ↾}_{y}) (x)$
71	69	ffvelcdmda	$⊢ (((φ \land \neg sum^(G) = +∞) \land y \in (𝒫 X \cap Fin)) \land x \in y) \to ({G ↾}_{y}) (x) \in [0, +∞)$
72	56 71	sselid	$⊢ (((φ \land \neg sum^(G) = +∞) \land y \in (𝒫 X \cap Fin)) \land x \in y) \to ({G ↾}_{y}) (x) \in ℝ$
73	14 72	fsumrecl	$⊢ ((φ \land \neg sum^(G) = +∞) \land y \in (𝒫 X \cap Fin)) \to \sum_{x \in y} ({G ↾}_{y}) (x) \in ℝ$
74	70 73	eqeltrd	$⊢ ((φ \land \neg sum^(G) = +∞) \land y \in (𝒫 X \cap Fin)) \to sum^({G ↾}_{y}) \in ℝ$
75	65	adantr	$⊢ ((φ \land \neg sum^(G) = +∞) \land y \in (𝒫 X \cap Fin)) \to sum^(G) \in ℝ$
76		simplll	$⊢ (((φ \land \neg sum^(G) = +∞) \land y \in (𝒫 X \cap Fin)) \land x \in y) \to φ$
77	53	sselda	$⊢ (((φ \land \neg sum^(G) = +∞) \land y \in (𝒫 X \cap Fin)) \land x \in y) \to x \in X$
78	76 77 4	syl2anc	$⊢ (((φ \land \neg sum^(G) = +∞) \land y \in (𝒫 X \cap Fin)) \land x \in y) \to F (x) \leq G (x)$
79		fvres	$⊢ x \in y \to ({F ↾}_{y}) (x) = F (x)$
80	79	adantl	$⊢ (((φ \land \neg sum^(G) = +∞) \land y \in (𝒫 X \cap Fin)) \land x \in y) \to ({F ↾}_{y}) (x) = F (x)$
81		fvres	$⊢ x \in y \to ({G ↾}_{y}) (x) = G (x)$
82	81	adantl	$⊢ (((φ \land \neg sum^(G) = +∞) \land y \in (𝒫 X \cap Fin)) \land x \in y) \to ({G ↾}_{y}) (x) = G (x)$
83	80 82	breq12d	$⊢ (((φ \land \neg sum^(G) = +∞) \land y \in (𝒫 X \cap Fin)) \land x \in y) \to (({F ↾}_{y}) (x) \leq ({G ↾}_{y}) (x) \leftrightarrow F (x) \leq G (x))$
84	78 83	mpbird	$⊢ (((φ \land \neg sum^(G) = +∞) \land y \in (𝒫 X \cap Fin)) \land x \in y) \to ({F ↾}_{y}) (x) \leq ({G ↾}_{y}) (x)$
85	14 58 72 84	fsumle	$⊢ ((φ \land \neg sum^(G) = +∞) \land y \in (𝒫 X \cap Fin)) \to \sum_{x \in y} ({F ↾}_{y}) (x) \leq \sum_{x \in y} ({G ↾}_{y}) (x)$
86	55 70	breq12d	$⊢ ((φ \land \neg sum^(G) = +∞) \land y \in (𝒫 X \cap Fin)) \to (sum^({F ↾}_{y}) \leq sum^({G ↾}_{y}) \leftrightarrow \sum_{x \in y} ({F ↾}_{y}) (x) \leq \sum_{x \in y} ({G ↾}_{y}) (x))$
87	85 86	mpbird	$⊢ ((φ \land \neg sum^(G) = +∞) \land y \in (𝒫 X \cap Fin)) \to sum^({F ↾}_{y}) \leq sum^({G ↾}_{y})$
88	1	adantr	$⊢ (φ \land y \in (𝒫 X \cap Fin)) \to X \in V$
89	3	adantr	$⊢ (φ \land y \in (𝒫 X \cap Fin)) \to G : X ⟶ [0, +∞]$
90	88 89	sge0less	$⊢ (φ \land y \in (𝒫 X \cap Fin)) \to sum^({G ↾}_{y}) \leq sum^(G)$
91	90	adantlr	$⊢ ((φ \land \neg sum^(G) = +∞) \land y \in (𝒫 X \cap Fin)) \to sum^({G ↾}_{y}) \leq sum^(G)$
92	60 74 75 87 91	letrd	$⊢ ((φ \land \neg sum^(G) = +∞) \land y \in (𝒫 X \cap Fin)) \to sum^({F ↾}_{y}) \leq sum^(G)$
93	92	ralrimiva	$⊢ (φ \land \neg sum^(G) = +∞) \to \forall y \in (𝒫 X \cap Fin) sum^({F ↾}_{y}) \leq sum^(G)$
94	62 61	sge0xrcl	$⊢ (φ \land \neg sum^(G) = +∞) \to sum^(G) \in ℝ^{*}$
95	62 15 94	sge0lefi	$⊢ (φ \land \neg sum^(G) = +∞) \to (sum^(F) \leq sum^(G) \leftrightarrow \forall y \in (𝒫 X \cap Fin) sum^({F ↾}_{y}) \leq sum^(G))$
96	93 95	mpbird	$⊢ (φ \land \neg sum^(G) = +∞) \to sum^(F) \leq sum^(G)$
97	12 96	pm2.61dan	$⊢ φ \to sum^(F) \leq sum^(G)$

Metamath Proof Explorer

Theorem sge0le

Proof