sge0p1

Description: The addition of the next term in a finite sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	sge0p1.1	$⊢ φ \to N \in ℤ_{\geq M}$
	sge0p1.2	$⊢ (φ \land k \in (M \dots N + 1)) \to A \in [0, +∞]$
	sge0p1.3	$⊢ k = N + 1 \to A = B$
Assertion	sge0p1	$⊢ φ \to sum^((k \in (M \dots N + 1) ⟼ A)) = sum^((k \in (M \dots N) ⟼ A)) +_{𝑒} B$

Proof

Step	Hyp	Ref	Expression
1		sge0p1.1	$⊢ φ \to N \in ℤ_{\geq M}$
2		sge0p1.2	$⊢ (φ \land k \in (M \dots N + 1)) \to A \in [0, +∞]$
3		sge0p1.3	$⊢ k = N + 1 \to A = B$
4		fzsuc	$⊢ N \in ℤ_{\geq M} \to (M \dots N + 1) = (M \dots N) \cup \{N + 1\}$
5	1 4	syl	$⊢ φ \to (M \dots N + 1) = (M \dots N) \cup \{N + 1\}$
6	5	mpteq1d	$⊢ φ \to (k \in (M \dots N + 1) ⟼ A) = (k \in ((M \dots N) \cup \{N + 1\}) ⟼ A)$
7	6	fveq2d	$⊢ φ \to sum^((k \in (M \dots N + 1) ⟼ A)) = sum^((k \in ((M \dots N) \cup \{N + 1\}) ⟼ A))$
8		nfv	$⊢ Ⅎ k φ$
9		ovex	$⊢ (M \dots N) \in V$
10	9	a1i	$⊢ φ \to (M \dots N) \in V$
11		snex	$⊢ \{N + 1\} \in V$
12	11	a1i	$⊢ φ \to \{N + 1\} \in V$
13		fzp1disj	$⊢ (M \dots N) \cap \{N + 1\} = \emptyset$
14	13	a1i	$⊢ φ \to (M \dots N) \cap \{N + 1\} = \emptyset$
15		0xr	$⊢ 0 \in ℝ^{*}$
16	15	a1i	$⊢ (φ \land k \in (M \dots N)) \to 0 \in ℝ^{*}$
17		pnfxr	$⊢ +∞ \in ℝ^{*}$
18	17	a1i	$⊢ (φ \land k \in (M \dots N)) \to +∞ \in ℝ^{*}$
19		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
20		simpl	$⊢ (φ \land k \in (M \dots N)) \to φ$
21		fzelp1	$⊢ k \in (M \dots N) \to k \in (M \dots N + 1)$
22	21	adantl	$⊢ (φ \land k \in (M \dots N)) \to k \in (M \dots N + 1)$
23	20 22 2	syl2anc	$⊢ (φ \land k \in (M \dots N)) \to A \in [0, +∞]$
24	19 23	sselid	$⊢ (φ \land k \in (M \dots N)) \to A \in ℝ^{*}$
25		iccgelb	$⊢ (0 \in ℝ^{} \land +∞ \in ℝ^{} \land A \in [0, +∞]) \to 0 \leq A$
26	16 18 23 25	syl3anc	$⊢ (φ \land k \in (M \dots N)) \to 0 \leq A$
27		iccleub	$⊢ (0 \in ℝ^{} \land +∞ \in ℝ^{} \land A \in [0, +∞]) \to A \leq +∞$
28	16 18 23 27	syl3anc	$⊢ (φ \land k \in (M \dots N)) \to A \leq +∞$
29	16 18 24 26 28	eliccxrd	$⊢ (φ \land k \in (M \dots N)) \to A \in [0, +∞]$
30		simpl	$⊢ (φ \land k \in \{N + 1\}) \to φ$
31		elsni	$⊢ k \in \{N + 1\} \to k = N + 1$
32	31	adantl	$⊢ (φ \land k \in \{N + 1\}) \to k = N + 1$
33		simpr	$⊢ (φ \land k = N + 1) \to k = N + 1$
34		peano2uz	$⊢ N \in ℤ_{\geq M} \to N + 1 \in ℤ_{\geq M}$
35		eluzfz2	$⊢ N + 1 \in ℤ_{\geq M} \to N + 1 \in (M \dots N + 1)$
36	1 34 35	3syl	$⊢ φ \to N + 1 \in (M \dots N + 1)$
37	36	adantr	$⊢ (φ \land k = N + 1) \to N + 1 \in (M \dots N + 1)$
38	33 37	eqeltrd	$⊢ (φ \land k = N + 1) \to k \in (M \dots N + 1)$
39	30 32 38	syl2anc	$⊢ (φ \land k \in \{N + 1\}) \to k \in (M \dots N + 1)$
40	30 39 2	syl2anc	$⊢ (φ \land k \in \{N + 1\}) \to A \in [0, +∞]$
41	8 10 12 14 29 40	sge0splitmpt	$⊢ φ \to sum^((k \in ((M \dots N) \cup \{N + 1\}) ⟼ A)) = sum^((k \in (M \dots N) ⟼ A)) +_{𝑒} sum^((k \in \{N + 1\} ⟼ A))$
42		ovex	$⊢ N + 1 \in V$
43	42	a1i	$⊢ φ \to N + 1 \in V$
44		id	$⊢ φ \to φ$
45		eleq1	$⊢ k = N + 1 \to (k \in (M \dots N + 1) \leftrightarrow N + 1 \in (M \dots N + 1))$
46	45	anbi2d	$⊢ k = N + 1 \to ((φ \land k \in (M \dots N + 1)) \leftrightarrow (φ \land N + 1 \in (M \dots N + 1)))$
47	3	eleq1d	$⊢ k = N + 1 \to (A \in [0, +∞] \leftrightarrow B \in [0, +∞])$
48	46 47	imbi12d	$⊢ k = N + 1 \to (((φ \land k \in (M \dots N + 1)) \to A \in [0, +∞]) \leftrightarrow ((φ \land N + 1 \in (M \dots N + 1)) \to B \in [0, +∞]))$
49	48 2	vtoclg	$⊢ N + 1 \in V \to ((φ \land N + 1 \in (M \dots N + 1)) \to B \in [0, +∞])$
50	42 49	ax-mp	$⊢ (φ \land N + 1 \in (M \dots N + 1)) \to B \in [0, +∞]$
51	44 36 50	syl2anc	$⊢ φ \to B \in [0, +∞]$
52	43 51 3	sge0snmpt	$⊢ φ \to sum^((k \in \{N + 1\} ⟼ A)) = B$
53	52	oveq2d	$⊢ φ \to sum^((k \in (M \dots N) ⟼ A)) +_{𝑒} sum^((k \in \{N + 1\} ⟼ A)) = sum^((k \in (M \dots N) ⟼ A)) +_{𝑒} B$
54	7 41 53	3eqtrd	$⊢ φ \to sum^((k \in (M \dots N + 1) ⟼ A)) = sum^((k \in (M \dots N) ⟼ A)) +_{𝑒} B$

Metamath Proof Explorer

Theorem sge0p1

Proof