esumlef

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	esumaddf.0	$⊢ Ⅎ k φ$
	esumaddf.a	$⊢ \underline{Ⅎ} k A$
	esumaddf.1	$⊢ φ \to A \in V$
	esumaddf.2	$⊢ (φ \land k \in A) \to B \in [0, +∞]$
	esumaddf.3	$⊢ (φ \land k \in A) \to C \in [0, +∞]$
	esumlef.3	$⊢ (φ \land k \in A) \to B \leq C$
Assertion	esumlef	$⊢ φ \to \underset{k \in A}{\sum^{}} B \leq \underset{k \in A}{\sum^{}} C$

Proof

Step	Hyp	Ref	Expression
1		esumaddf.0	$⊢ Ⅎ k φ$
2		esumaddf.a	$⊢ \underline{Ⅎ} k A$
3		esumaddf.1	$⊢ φ \to A \in V$
4		esumaddf.2	$⊢ (φ \land k \in A) \to B \in [0, +∞]$
5		esumaddf.3	$⊢ (φ \land k \in A) \to C \in [0, +∞]$
6		esumlef.3	$⊢ (φ \land k \in A) \to B \leq C$
7		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
8	4	ex	$⊢ φ \to (k \in A \to B \in [0, +∞])$
9	1 8	ralrimi	$⊢ φ \to \forall k \in A B \in [0, +∞]$
10	2	esumcl	$⊢ (A \in V \land \forall k \in A B \in [0, +∞]) \to \underset{k \in A}{\sum^{*}} B \in [0, +∞]$
11	3 9 10	syl2anc	$⊢ φ \to \underset{k \in A}{\sum^{*}} B \in [0, +∞]$
12	7 11	sseldi	$⊢ φ \to \underset{k \in A}{\sum^{}} B \in ℝ^{}$
13	7 5	sseldi	$⊢ (φ \land k \in A) \to C \in ℝ^{*}$
14	7 4	sseldi	$⊢ (φ \land k \in A) \to B \in ℝ^{*}$
15	14	xnegcld	$⊢ (φ \land k \in A) \to - B \in ℝ^{*}$
16	13 15	xaddcld	$⊢ (φ \land k \in A) \to C +_{𝑒} (- B) \in ℝ^{*}$
17		xsubge0	$⊢ (C \in ℝ^{} \land B \in ℝ^{}) \to (0 \leq C +_{𝑒} (- B) \leftrightarrow B \leq C)$
18	13 14 17	syl2anc	$⊢ (φ \land k \in A) \to (0 \leq C +_{𝑒} (- B) \leftrightarrow B \leq C)$
19	6 18	mpbird	$⊢ (φ \land k \in A) \to 0 \leq C +_{𝑒} (- B)$
20		pnfge	$⊢ C +_{𝑒} (- B) \in ℝ^{*} \to C +_{𝑒} (- B) \leq +∞$
21	16 20	syl	$⊢ (φ \land k \in A) \to C +_{𝑒} (- B) \leq +∞$
22		0xr	$⊢ 0 \in ℝ^{*}$
23		pnfxr	$⊢ +∞ \in ℝ^{*}$
24		elicc1	$⊢ (0 \in ℝ^{} \land +∞ \in ℝ^{}) \to (C +_{𝑒} (- B) \in [0, +∞] \leftrightarrow (C +_{𝑒} (- B) \in ℝ^{*} \land 0 \leq C +_{𝑒} (- B) \land C +_{𝑒} (- B) \leq +∞))$
25	22 23 24	mp2an	$⊢ C +_{𝑒} (- B) \in [0, +∞] \leftrightarrow (C +_{𝑒} (- B) \in ℝ^{*} \land 0 \leq C +_{𝑒} (- B) \land C +_{𝑒} (- B) \leq +∞)$
26	16 19 21 25	syl3anbrc	$⊢ (φ \land k \in A) \to C +_{𝑒} (- B) \in [0, +∞]$
27	26	ex	$⊢ φ \to (k \in A \to C +_{𝑒} (- B) \in [0, +∞])$
28	1 27	ralrimi	$⊢ φ \to \forall k \in A C +_{𝑒} (- B) \in [0, +∞]$
29	2	esumcl	$⊢ (A \in V \land \forall k \in A C +_{𝑒} (- B) \in [0, +∞]) \to \underset{k \in A}{\sum^{*}} (C +_{𝑒} (- B)) \in [0, +∞]$
30	3 28 29	syl2anc	$⊢ φ \to \underset{k \in A}{\sum^{*}} (C +_{𝑒} (- B)) \in [0, +∞]$
31	7 30	sseldi	$⊢ φ \to \underset{k \in A}{\sum^{}} (C +_{𝑒} (- B)) \in ℝ^{}$
32	22	a1i	$⊢ φ \to 0 \in ℝ^{*}$
33	23	a1i	$⊢ φ \to +∞ \in ℝ^{*}$
34		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 +∞))$
35	32 33 31 34	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 +∞))$
36	30 35	mpbid	$⊢ φ \to (0 \leq \underset{k \in A}{\sum^{}} (C +_{𝑒} (- B)) \land \underset{k \in A}{\sum^{}} (C +_{𝑒} (- B)) \leq +∞)$
37	36	simpld	$⊢ φ \to 0 \leq \underset{k \in A}{\sum^{*}} (C +_{𝑒} (- B))$
38		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)))$
39	38	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))$
40	12 31 37 39	syl21anc	$⊢ φ \to \underset{k \in A}{\sum^{}} B \leq \underset{k \in A}{\sum^{}} B +_{𝑒} \underset{k \in A}{\sum^{*}} (C +_{𝑒} (- B))$
41		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$
42	12 31 41	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$
43	40 42	breqtrd	$⊢ φ \to \underset{k \in A}{\sum^{}} B \leq \underset{k \in A}{\sum^{}} (C +_{𝑒} (- B)) +_{𝑒} \underset{k \in A}{\sum^{*}} B$
44	1 2 3 26 4	esumaddf	$⊢ φ \to \underset{k \in A}{\sum^{}} ((C +_{𝑒} (- B)) +_{𝑒} B) = \underset{k \in A}{\sum^{}} (C +_{𝑒} (- B)) +_{𝑒} \underset{k \in A}{\sum^{*}} B$
45		xrge0npcan	$⊢ (C \in [0, +∞] \land B \in [0, +∞] \land B \leq C) \to (C +_{𝑒} (- B)) +_{𝑒} B = C$
46	5 4 6 45	syl3anc	$⊢ (φ \land k \in A) \to (C +_{𝑒} (- B)) +_{𝑒} B = C$
47	46	ex	$⊢ φ \to (k \in A \to (C +_{𝑒} (- B)) +_{𝑒} B = C)$
48	1 47	ralrimi	$⊢ φ \to \forall k \in A (C +_{𝑒} (- B)) +_{𝑒} B = C$
49	1 48	esumeq2d	$⊢ φ \to \underset{k \in A}{\sum^{}} ((C +_{𝑒} (- B)) +_{𝑒} B) = \underset{k \in A}{\sum^{}} C$
50	44 49	eqtr3d	$⊢ φ \to \underset{k \in A}{\sum^{}} (C +_{𝑒} (- B)) +_{𝑒} \underset{k \in A}{\sum^{}} B = \underset{k \in A}{\sum^{*}} C$
51	43 50	breqtrd	$⊢ φ \to \underset{k \in A}{\sum^{}} B \leq \underset{k \in A}{\sum^{}} C$

Metamath Proof Explorer

Theorem esumlef

Proof