esumpmono

Description: The partial sums in an extended sum form a monotonic sequence. (Contributed by Thierry Arnoux, 31-Aug-2017)

	Ref	Expression
Hypotheses	esumpmono.1	$⊢ φ \to M \in ℕ$
	esumpmono.2	$⊢ φ \to N \in ℤ_{\geq M}$
	esumpmono.3	$⊢ (φ \land k \in ℕ) \to A \in [0, +∞)$
Assertion	esumpmono	$⊢ φ \to {\sum^{}}_{k = 1}^{M} A \leq {\sum^{}}_{k = 1}^{N} A$

Proof

Step	Hyp	Ref	Expression
1		esumpmono.1	$⊢ φ \to M \in ℕ$
2		esumpmono.2	$⊢ φ \to N \in ℤ_{\geq M}$
3		esumpmono.3	$⊢ (φ \land k \in ℕ) \to A \in [0, +∞)$
4		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
5		ovexd	$⊢ φ \to (1 \dots M) \in V$
6		elfznn	$⊢ k \in (1 \dots M) \to k \in ℕ$
7		icossicc	$⊢ [0, +∞) \subseteq [0, +∞]$
8	7 3	sselid	$⊢ (φ \land k \in ℕ) \to A \in [0, +∞]$
9	6 8	sylan2	$⊢ (φ \land k \in (1 \dots M)) \to A \in [0, +∞]$
10	9	ralrimiva	$⊢ φ \to \forall k \in (1 \dots M) A \in [0, +∞]$
11		nfcv	$⊢ \underline{Ⅎ} k (1 \dots M)$
12	11	esumcl	$⊢ ((1 \dots M) \in V \land \forall k \in (1 \dots M) A \in [0, +∞]) \to {\sum^{*}}_{k = 1}^{M} A \in [0, +∞]$
13	5 10 12	syl2anc	$⊢ φ \to {\sum^{*}}_{k = 1}^{M} A \in [0, +∞]$
14	4 13	sselid	$⊢ φ \to {\sum^{}}_{k = 1}^{M} A \in ℝ^{}$
15	14	xrleidd	$⊢ φ \to {\sum^{}}_{k = 1}^{M} A \leq {\sum^{}}_{k = 1}^{M} A$
16		ovexd	$⊢ φ \to (M + 1 \dots N) \in V$
17	1	adantr	$⊢ (φ \land k \in (M + 1 \dots N)) \to M \in ℕ$
18		peano2nn	$⊢ M \in ℕ \to M + 1 \in ℕ$
19		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
20	18 19	eleqtrdi	$⊢ M \in ℕ \to M + 1 \in ℤ_{\geq 1}$
21		fzss1	$⊢ M + 1 \in ℤ_{\geq 1} \to (M + 1 \dots N) \subseteq (1 \dots N)$
22	17 20 21	3syl	$⊢ (φ \land k \in (M + 1 \dots N)) \to (M + 1 \dots N) \subseteq (1 \dots N)$
23		simpr	$⊢ (φ \land k \in (M + 1 \dots N)) \to k \in (M + 1 \dots N)$
24	22 23	sseldd	$⊢ (φ \land k \in (M + 1 \dots N)) \to k \in (1 \dots N)$
25		elfznn	$⊢ k \in (1 \dots N) \to k \in ℕ$
26	24 25	syl	$⊢ (φ \land k \in (M + 1 \dots N)) \to k \in ℕ$
27	26 8	syldan	$⊢ (φ \land k \in (M + 1 \dots N)) \to A \in [0, +∞]$
28	27	ralrimiva	$⊢ φ \to \forall k \in (M + 1 \dots N) A \in [0, +∞]$
29		nfcv	$⊢ \underline{Ⅎ} k (M + 1 \dots N)$
30	29	esumcl	$⊢ ((M + 1 \dots N) \in V \land \forall k \in (M + 1 \dots N) A \in [0, +∞]) \to {\sum^{*}}_{k = M + 1}^{N} A \in [0, +∞]$
31	16 28 30	syl2anc	$⊢ φ \to {\sum^{*}}_{k = M + 1}^{N} A \in [0, +∞]$
32		elxrge0	$⊢ {\sum^{}}_{k = M + 1}^{N} A \in [0, +∞] \leftrightarrow ({\sum^{}}_{k = M + 1}^{N} A \in ℝ^{} \land 0 \leq {\sum^{}}_{k = M + 1}^{N} A)$
33	32	simprbi	$⊢ {\sum^{}}_{k = M + 1}^{N} A \in [0, +∞] \to 0 \leq {\sum^{}}_{k = M + 1}^{N} A$
34	31 33	syl	$⊢ φ \to 0 \leq {\sum^{*}}_{k = M + 1}^{N} A$
35		0xr	$⊢ 0 \in ℝ^{*}$
36	35	a1i	$⊢ φ \to 0 \in ℝ^{*}$
37	4 31	sselid	$⊢ φ \to {\sum^{}}_{k = M + 1}^{N} A \in ℝ^{}$
38		xle2add	$⊢ (({\sum^{}}_{k = 1}^{M} A \in ℝ^{} \land 0 \in ℝ^{}) \land ({\sum^{}}_{k = 1}^{M} A \in ℝ^{} \land {\sum^{}}_{k = M + 1}^{N} A \in ℝ^{})) \to (({\sum^{}}_{k = 1}^{M} A \leq {\sum^{}}_{k = 1}^{M} A \land 0 \leq {\sum^{}}_{k = M + 1}^{N} A) \to {\sum^{}}_{k = 1}^{M} A +_{𝑒} 0 \leq {\sum^{}}_{k = 1}^{M} A +_{𝑒} {\sum^{*}}_{k = M + 1}^{N} A)$
39	14 36 14 37 38	syl22anc	$⊢ φ \to (({\sum^{}}_{k = 1}^{M} A \leq {\sum^{}}_{k = 1}^{M} A \land 0 \leq {\sum^{}}_{k = M + 1}^{N} A) \to {\sum^{}}_{k = 1}^{M} A +_{𝑒} 0 \leq {\sum^{}}_{k = 1}^{M} A +_{𝑒} {\sum^{}}_{k = M + 1}^{N} A)$
40	15 34 39	mp2and	$⊢ φ \to {\sum^{}}_{k = 1}^{M} A +_{𝑒} 0 \leq {\sum^{}}_{k = 1}^{M} A +_{𝑒} {\sum^{*}}_{k = M + 1}^{N} A$
41		xaddid1	$⊢ {\sum^{}}_{k = 1}^{M} A \in ℝ^{} \to {\sum^{}}_{k = 1}^{M} A +_{𝑒} 0 = {\sum^{}}_{k = 1}^{M} A$
42	14 41	syl	$⊢ φ \to {\sum^{}}_{k = 1}^{M} A +_{𝑒} 0 = {\sum^{}}_{k = 1}^{M} A$
43	42	eqcomd	$⊢ φ \to {\sum^{}}_{k = 1}^{M} A = {\sum^{}}_{k = 1}^{M} A +_{𝑒} 0$
44	1 19	eleqtrdi	$⊢ φ \to M \in ℤ_{\geq 1}$
45		eluzfz	$⊢ (M \in ℤ_{\geq 1} \land N \in ℤ_{\geq M}) \to M \in (1 \dots N)$
46	44 2 45	syl2anc	$⊢ φ \to M \in (1 \dots N)$
47		fzsplit	$⊢ M \in (1 \dots N) \to (1 \dots N) = (1 \dots M) \cup (M + 1 \dots N)$
48		esumeq1	$⊢ (1 \dots N) = (1 \dots M) \cup (M + 1 \dots N) \to {\sum^{}}_{k = 1}^{N} A = \underset{k \in (1 \dots M) \cup (M + 1 \dots N)}{\sum^{}} A$
49	46 47 48	3syl	$⊢ φ \to {\sum^{}}_{k = 1}^{N} A = \underset{k \in (1 \dots M) \cup (M + 1 \dots N)}{\sum^{}} A$
50		nfv	$⊢ Ⅎ k φ$
51		nnre	$⊢ M \in ℕ \to M \in ℝ$
52	51	ltp1d	$⊢ M \in ℕ \to M < M + 1$
53		fzdisj	$⊢ M < M + 1 \to (1 \dots M) \cap (M + 1 \dots N) = \emptyset$
54	1 52 53	3syl	$⊢ φ \to (1 \dots M) \cap (M + 1 \dots N) = \emptyset$
55	50 11 29 5 16 54 9 27	esumsplit	$⊢ φ \to \underset{k \in (1 \dots M) \cup (M + 1 \dots N)}{\sum^{}} A = {\sum^{}}_{k = 1}^{M} A +_{𝑒} {\sum^{*}}_{k = M + 1}^{N} A$
56	49 55	eqtrd	$⊢ φ \to {\sum^{}}_{k = 1}^{N} A = {\sum^{}}_{k = 1}^{M} A +_{𝑒} {\sum^{*}}_{k = M + 1}^{N} A$
57	40 43 56	3brtr4d	$⊢ φ \to {\sum^{}}_{k = 1}^{M} A \leq {\sum^{}}_{k = 1}^{N} A$

Metamath Proof Explorer

Theorem esumpmono

Proof