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	bilani	$⊢ (φ \land z \in ran (n \in ℕ ⟼ {\sum^{}}_{k = 1}^{n} A)) \to \exists n \in ℕ z = {\sum^{}}_{k = 1}^{n} A$
20	10 15 19	r19.29af	$⊢ (φ \land z \in ran (n \in ℕ ⟼ {\sum^{*}}_{k = 1}^{n} A)) \to z \leq B$
21	20	ralrimiva	$⊢ φ \to \forall z \in ran (n \in ℕ ⟼ {\sum^{*}}_{k = 1}^{n} A) z \leq B$
22		ovexd	$⊢ (φ \land n \in ℕ) \to (1 \dots n) \in V$
23		simpll	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to φ$
24		fz1ssnn	$⊢ (1 \dots n) \subseteq ℕ$
25	24	a1i	$⊢ (φ \land n \in ℕ) \to (1 \dots n) \subseteq ℕ$
26	25	sselda	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to k \in ℕ$
27	23 26 2	syl2anc	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to A \in [0, +∞]$
28	27	ralrimiva	$⊢ (φ \land n \in ℕ) \to \forall k \in (1 \dots n) A \in [0, +∞]$
29		nfcv	$⊢ \underline{Ⅎ} k (1 \dots n)$
30	29	esumcl	$⊢ ((1 \dots n) \in V \land \forall k \in (1 \dots n) A \in [0, +∞]) \to {\sum^{*}}_{k = 1}^{n} A \in [0, +∞]$
31	22 28 30	syl2anc	$⊢ (φ \land n \in ℕ) \to {\sum^{*}}_{k = 1}^{n} A \in [0, +∞]$
32	31	ralrimiva	$⊢ φ \to \forall n \in ℕ {\sum^{*}}_{k = 1}^{n} A \in [0, +∞]$
33	16	rnmptss	$⊢ \forall n \in ℕ {\sum^{}}_{k = 1}^{n} A \in [0, +∞] \to ran (n \in ℕ ⟼ {\sum^{}}_{k = 1}^{n} A) \subseteq [0, +∞]$
34	32 33	syl	$⊢ φ \to ran (n \in ℕ ⟼ {\sum^{*}}_{k = 1}^{n} A) \subseteq [0, +∞]$
35		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
36	34 35	sstrdi	$⊢ φ \to ran (n \in ℕ ⟼ {\sum^{}}_{k = 1}^{n} A) \subseteq ℝ^{}$
37	35 1	sselid	$⊢ φ \to B \in ℝ^{*}$
38		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)$
39	36 37 38	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)$
40	21 39	mpbird	$⊢ φ \to sup (ran (n \in ℕ ⟼ {\sum^{}}_{k = 1}^{n} A) ℝ^{} <) \leq B$
41	4 40	eqbrtrd	$⊢ φ \to \underset{k \in ℕ}{\sum^{*}} A \leq B$

Metamath Proof Explorer

Theorem esumgect

Proof