esumle

Description: If all of the terms of an extended sums compare, so do the sums. (Contributed by Thierry Arnoux, 8-Jun-2017)

	Ref	Expression
Hypotheses	esumadd.0	$⊢ φ \to A \in V$
	esumadd.1	$⊢ (φ \land k \in A) \to B \in [0, +∞]$
	esumadd.2	$⊢ (φ \land k \in A) \to C \in [0, +∞]$
	esumle.3	$⊢ (φ \land k \in A) \to B \leq C$
Assertion	esumle	$⊢ φ \to \underset{k \in A}{\sum^{}} B \leq \underset{k \in A}{\sum^{}} C$

Proof

Step	Hyp	Ref	Expression
1		esumadd.0	$⊢ φ \to A \in V$
2		esumadd.1	$⊢ (φ \land k \in A) \to B \in [0, +∞]$
3		esumadd.2	$⊢ (φ \land k \in A) \to C \in [0, +∞]$
4		esumle.3	$⊢ (φ \land k \in A) \to B \leq C$
5		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
6	2	ralrimiva	$⊢ φ \to \forall k \in A B \in [0, +∞]$
7		nfcv	$⊢ \underline{Ⅎ} k A$
8	7	esumcl	$⊢ (A \in V \land \forall k \in A B \in [0, +∞]) \to \underset{k \in A}{\sum^{*}} B \in [0, +∞]$
9	1 6 8	syl2anc	$⊢ φ \to \underset{k \in A}{\sum^{*}} B \in [0, +∞]$
10	5 9	sselid	$⊢ φ \to \underset{k \in A}{\sum^{}} B \in ℝ^{}$
11	5 3	sselid	$⊢ (φ \land k \in A) \to C \in ℝ^{*}$
12	5 2	sselid	$⊢ (φ \land k \in A) \to B \in ℝ^{*}$
13	12	xnegcld	$⊢ (φ \land k \in A) \to - B \in ℝ^{*}$
14	11 13	xaddcld	$⊢ (φ \land k \in A) \to C +_{𝑒} (- B) \in ℝ^{*}$
15		xsubge0	$⊢ (C \in ℝ^{} \land B \in ℝ^{}) \to (0 \leq C +_{𝑒} (- B) \leftrightarrow B \leq C)$
16	11 12 15	syl2anc	$⊢ (φ \land k \in A) \to (0 \leq C +_{𝑒} (- B) \leftrightarrow B \leq C)$
17	4 16	mpbird	$⊢ (φ \land k \in A) \to 0 \leq C +_{𝑒} (- B)$
18		pnfge	$⊢ C +_{𝑒} (- B) \in ℝ^{*} \to C +_{𝑒} (- B) \leq +∞$
19	14 18	syl	$⊢ (φ \land k \in A) \to C +_{𝑒} (- B) \leq +∞$
20		0xr	$⊢ 0 \in ℝ^{*}$
21		pnfxr	$⊢ +∞ \in ℝ^{*}$
22		elicc1	$⊢ (0 \in ℝ^{} \land +∞ \in ℝ^{}) \to (C +_{𝑒} (- B) \in [0, +∞] \leftrightarrow (C +_{𝑒} (- B) \in ℝ^{*} \land 0 \leq C +_{𝑒} (- B) \land C +_{𝑒} (- B) \leq +∞))$
23	20 21 22	mp2an	$⊢ C +_{𝑒} (- B) \in [0, +∞] \leftrightarrow (C +_{𝑒} (- B) \in ℝ^{*} \land 0 \leq C +_{𝑒} (- B) \land C +_{𝑒} (- B) \leq +∞)$
24	14 17 19 23	syl3anbrc	$⊢ (φ \land k \in A) \to C +_{𝑒} (- B) \in [0, +∞]$
25	24	ralrimiva	$⊢ φ \to \forall k \in A C +_{𝑒} (- B) \in [0, +∞]$
26	7	esumcl	$⊢ (A \in V \land \forall k \in A C +_{𝑒} (- B) \in [0, +∞]) \to \underset{k \in A}{\sum^{*}} (C +_{𝑒} (- B)) \in [0, +∞]$
27	1 25 26	syl2anc	$⊢ φ \to \underset{k \in A}{\sum^{*}} (C +_{𝑒} (- B)) \in [0, +∞]$
28	5 27	sselid	$⊢ φ \to \underset{k \in A}{\sum^{}} (C +_{𝑒} (- B)) \in ℝ^{}$
29	20	a1i	$⊢ φ \to 0 \in ℝ^{*}$
30	21	a1i	$⊢ φ \to +∞ \in ℝ^{*}$
31		elicc4	$⊢ (0 \in ℝ^{} \land +∞ \in ℝ^{} \land \underset{k \in A}{\sum^{}} (C +_{𝑒} (- B)) \in ℝ^{}) \to (\underset{k \in A}{\sum^{}} (C +_{𝑒} (- B)) \in [0, +∞] \leftrightarrow (0 \leq \underset{k \in A}{\sum^{}} (C +_{𝑒} (- B)) \land \underset{k \in A}{\sum^{*}} (C +_{𝑒} (- B)) \leq +∞))$
32	29 30 28 31	syl3anc	$⊢ φ \to (\underset{k \in A}{\sum^{}} (C +_{𝑒} (- B)) \in [0, +∞] \leftrightarrow (0 \leq \underset{k \in A}{\sum^{}} (C +_{𝑒} (- B)) \land \underset{k \in A}{\sum^{*}} (C +_{𝑒} (- B)) \leq +∞))$
33	27 32	mpbid	$⊢ φ \to (0 \leq \underset{k \in A}{\sum^{}} (C +_{𝑒} (- B)) \land \underset{k \in A}{\sum^{}} (C +_{𝑒} (- B)) \leq +∞)$
34	33	simpld	$⊢ φ \to 0 \leq \underset{k \in A}{\sum^{*}} (C +_{𝑒} (- B))$
35		xraddge02	$⊢ (\underset{k \in A}{\sum^{}} B \in ℝ^{} \land \underset{k \in A}{\sum^{}} (C +_{𝑒} (- B)) \in ℝ^{}) \to (0 \leq \underset{k \in A}{\sum^{}} (C +_{𝑒} (- B)) \to \underset{k \in A}{\sum^{}} B \leq \underset{k \in A}{\sum^{}} B +_{𝑒} \underset{k \in A}{\sum^{}} (C +_{𝑒} (- B)))$
36	35	imp	$⊢ ((\underset{k \in A}{\sum^{}} B \in ℝ^{} \land \underset{k \in A}{\sum^{}} (C +_{𝑒} (- B)) \in ℝ^{}) \land 0 \leq \underset{k \in A}{\sum^{}} (C +_{𝑒} (- B))) \to \underset{k \in A}{\sum^{}} B \leq \underset{k \in A}{\sum^{}} B +_{𝑒} \underset{k \in A}{\sum^{}} (C +_{𝑒} (- B))$
37	10 28 34 36	syl21anc	$⊢ φ \to \underset{k \in A}{\sum^{}} B \leq \underset{k \in A}{\sum^{}} B +_{𝑒} \underset{k \in A}{\sum^{*}} (C +_{𝑒} (- B))$
38		xaddcom	$⊢ (\underset{k \in A}{\sum^{}} B \in ℝ^{} \land \underset{k \in A}{\sum^{}} (C +_{𝑒} (- B)) \in ℝ^{}) \to \underset{k \in A}{\sum^{}} B +_{𝑒} \underset{k \in A}{\sum^{}} (C +_{𝑒} (- B)) = \underset{k \in A}{\sum^{}} (C +_{𝑒} (- B)) +_{𝑒} \underset{k \in A}{\sum^{}} B$
39	10 28 38	syl2anc	$⊢ φ \to \underset{k \in A}{\sum^{}} B +_{𝑒} \underset{k \in A}{\sum^{}} (C +_{𝑒} (- B)) = \underset{k \in A}{\sum^{}} (C +_{𝑒} (- B)) +_{𝑒} \underset{k \in A}{\sum^{}} B$
40	37 39	breqtrd	$⊢ φ \to \underset{k \in A}{\sum^{}} B \leq \underset{k \in A}{\sum^{}} (C +_{𝑒} (- B)) +_{𝑒} \underset{k \in A}{\sum^{*}} B$
41	1 24 2	esumadd	$⊢ φ \to \underset{k \in A}{\sum^{}} ((C +_{𝑒} (- B)) +_{𝑒} B) = \underset{k \in A}{\sum^{}} (C +_{𝑒} (- B)) +_{𝑒} \underset{k \in A}{\sum^{*}} B$
42		xrge0npcan	$⊢ (C \in [0, +∞] \land B \in [0, +∞] \land B \leq C) \to (C +_{𝑒} (- B)) +_{𝑒} B = C$
43	3 2 4 42	syl3anc	$⊢ (φ \land k \in A) \to (C +_{𝑒} (- B)) +_{𝑒} B = C$
44	43	esumeq2dv	$⊢ φ \to \underset{k \in A}{\sum^{}} ((C +_{𝑒} (- B)) +_{𝑒} B) = \underset{k \in A}{\sum^{}} C$
45	41 44	eqtr3d	$⊢ φ \to \underset{k \in A}{\sum^{}} (C +_{𝑒} (- B)) +_{𝑒} \underset{k \in A}{\sum^{}} B = \underset{k \in A}{\sum^{*}} C$
46	40 45	breqtrd	$⊢ φ \to \underset{k \in A}{\sum^{}} B \leq \underset{k \in A}{\sum^{}} C$

Metamath Proof Explorer

Theorem esumle

Proof