esumgect

Description: "Send n to +oo " in an inequality with an extended sum. (Contributed by Thierry Arnoux, 24-May-2020)

	Ref	Expression
Hypotheses	esumsup.1	$⊢ φ \to B \in [0, +∞]$
	esumsup.2	$⊢ (φ \land k \in ℕ) \to A \in [0, +∞]$
	esumgect.1	$⊢ (φ \land n \in ℕ) \to {\sum^{*}}_{k = 1}^{n} A \leq B$
Assertion	esumgect	$⊢ φ \to \underset{k \in ℕ}{\sum^{*}} A \leq B$

Proof

Step	Hyp	Ref	Expression
1		esumsup.1	$⊢ φ \to B \in [0, +∞]$
2		esumsup.2	$⊢ (φ \land k \in ℕ) \to A \in [0, +∞]$
3		esumgect.1	$⊢ (φ \land n \in ℕ) \to {\sum^{*}}_{k = 1}^{n} A \leq B$
4	1 2	esumsup	$⊢ φ \to \underset{k \in ℕ}{\sum^{}} A = sup (ran (n \in ℕ ⟼ {\sum^{}}_{k = 1}^{n} A) ℝ^{*} <)$
5		nfv	$⊢ Ⅎ n φ$
6		nfcv	$⊢ \underline{Ⅎ} n z$
7		nfmpt1	$⊢ \underline{Ⅎ} n (n \in ℕ ⟼ {\sum^{*}}_{k = 1}^{n} A)$
8	7	nfrn	$⊢ \underline{Ⅎ} n ran (n \in ℕ ⟼ {\sum^{*}}_{k = 1}^{n} A)$
9	6 8	nfel	$⊢ Ⅎ n z \in ran (n \in ℕ ⟼ {\sum^{*}}_{k = 1}^{n} A)$
10	5 9	nfan	$⊢ Ⅎ n (φ \land z \in ran (n \in ℕ ⟼ {\sum^{*}}_{k = 1}^{n} A))$
11		simpr	$⊢ (((φ \land z \in ran (n \in ℕ ⟼ {\sum^{}}_{k = 1}^{n} A)) \land n \in ℕ) \land z = {\sum^{}}_{k = 1}^{n} A) \to z = {\sum^{*}}_{k = 1}^{n} A$
12		simplll	$⊢ (((φ \land z \in ran (n \in ℕ ⟼ {\sum^{}}_{k = 1}^{n} A)) \land n \in ℕ) \land z = {\sum^{}}_{k = 1}^{n} A) \to φ$
13		simplr	$⊢ (((φ \land z \in ran (n \in ℕ ⟼ {\sum^{}}_{k = 1}^{n} A)) \land n \in ℕ) \land z = {\sum^{}}_{k = 1}^{n} A) \to n \in ℕ$
14	12 13 3	syl2anc	$⊢ (((φ \land z \in ran (n \in ℕ ⟼ {\sum^{}}_{k = 1}^{n} A)) \land n \in ℕ) \land z = {\sum^{}}_{k = 1}^{n} A) \to {\sum^{*}}_{k = 1}^{n} A \leq B$
15	11 14	eqbrtrd	$⊢ (((φ \land z \in ran (n \in ℕ ⟼ {\sum^{}}_{k = 1}^{n} A)) \land n \in ℕ) \land z = {\sum^{}}_{k = 1}^{n} A) \to z \leq B$
16		eqid	$⊢ (n \in ℕ ⟼ {\sum^{}}_{k = 1}^{n} A) = (n \in ℕ ⟼ {\sum^{}}_{k = 1}^{n} A)$
17		esumex	$⊢ {\sum^{*}}_{k = 1}^{n} A \in V$
18	16 17	elrnmpti	$⊢ z \in ran (n \in ℕ ⟼ {\sum^{}}_{k = 1}^{n} A) \leftrightarrow \exists n \in ℕ z = {\sum^{}}_{k = 1}^{n} A$
19	18	biimpi	$⊢ z \in ran (n \in ℕ ⟼ {\sum^{}}_{k = 1}^{n} A) \to \exists n \in ℕ z = {\sum^{}}_{k = 1}^{n} A$
20	19	adantl	$⊢ (φ \land z \in ran (n \in ℕ ⟼ {\sum^{}}_{k = 1}^{n} A)) \to \exists n \in ℕ z = {\sum^{}}_{k = 1}^{n} A$
21	10 15 20	r19.29af	$⊢ (φ \land z \in ran (n \in ℕ ⟼ {\sum^{*}}_{k = 1}^{n} A)) \to z \leq B$
22	21	ralrimiva	$⊢ φ \to \forall z \in ran (n \in ℕ ⟼ {\sum^{*}}_{k = 1}^{n} A) z \leq B$
23		ovexd	$⊢ (φ \land n \in ℕ) \to (1 \dots n) \in V$
24		simpll	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to φ$
25		fz1ssnn	$⊢ (1 \dots n) \subseteq ℕ$
26	25	a1i	$⊢ (φ \land n \in ℕ) \to (1 \dots n) \subseteq ℕ$
27	26	sselda	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to k \in ℕ$
28	24 27 2	syl2anc	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to A \in [0, +∞]$
29	28	ralrimiva	$⊢ (φ \land n \in ℕ) \to \forall k \in (1 \dots n) A \in [0, +∞]$
30		nfcv	$⊢ \underline{Ⅎ} k (1 \dots n)$
31	30	esumcl	$⊢ ((1 \dots n) \in V \land \forall k \in (1 \dots n) A \in [0, +∞]) \to {\sum^{*}}_{k = 1}^{n} A \in [0, +∞]$
32	23 29 31	syl2anc	$⊢ (φ \land n \in ℕ) \to {\sum^{*}}_{k = 1}^{n} A \in [0, +∞]$
33	32	ralrimiva	$⊢ φ \to \forall n \in ℕ {\sum^{*}}_{k = 1}^{n} A \in [0, +∞]$
34	16	rnmptss	$⊢ \forall n \in ℕ {\sum^{}}_{k = 1}^{n} A \in [0, +∞] \to ran (n \in ℕ ⟼ {\sum^{}}_{k = 1}^{n} A) \subseteq [0, +∞]$
35	33 34	syl	$⊢ φ \to ran (n \in ℕ ⟼ {\sum^{*}}_{k = 1}^{n} A) \subseteq [0, +∞]$
36		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
37	35 36	sstrdi	$⊢ φ \to ran (n \in ℕ ⟼ {\sum^{}}_{k = 1}^{n} A) \subseteq ℝ^{}$
38	36 1	sseldi	$⊢ φ \to B \in ℝ^{*}$
39		supxrleub	$⊢ (ran (n \in ℕ ⟼ {\sum^{}}_{k = 1}^{n} A) \subseteq ℝ^{} \land B \in ℝ^{}) \to (sup (ran (n \in ℕ ⟼ {\sum^{}}_{k = 1}^{n} A) ℝ^{} <) \leq B \leftrightarrow \forall z \in ran (n \in ℕ ⟼ {\sum^{}}_{k = 1}^{n} A) z \leq B)$
40	37 38 39	syl2anc	$⊢ φ \to (sup (ran (n \in ℕ ⟼ {\sum^{}}_{k = 1}^{n} A) ℝ^{} <) \leq B \leftrightarrow \forall z \in ran (n \in ℕ ⟼ {\sum^{*}}_{k = 1}^{n} A) z \leq B)$
41	22 40	mpbird	$⊢ φ \to sup (ran (n \in ℕ ⟼ {\sum^{}}_{k = 1}^{n} A) ℝ^{} <) \leq B$
42	4 41	eqbrtrd	$⊢ φ \to \underset{k \in ℕ}{\sum^{*}} A \leq B$

Metamath Proof Explorer

Theorem esumgect

Proof