dvfsumrlimge0

	Ref	Expression
Hypotheses	dvfsum.s	$⊢ S = (T, +∞)$
	dvfsum.z	$⊢ Z = ℤ_{\geq M}$
	dvfsum.m	$⊢ φ \to M \in ℤ$
	dvfsum.d	$⊢ φ \to D \in ℝ$
	dvfsum.md	$⊢ φ \to M \leq D + 1$
	dvfsum.t	$⊢ φ \to T \in ℝ$
	dvfsum.a	$⊢ (φ \land x \in S) \to A \in ℝ$
	dvfsum.b1	$⊢ (φ \land x \in S) \to B \in V$
	dvfsum.b2	$⊢ (φ \land x \in Z) \to B \in ℝ$
	dvfsum.b3	$⊢ φ \to \frac{d (x \in S⟼ A)}{d_{ℝ} x} = (x \in S ⟼ B)$
	dvfsum.c	$⊢ x = k \to B = C$
	dvfsumrlim.l	$⊢ (φ \land (x \in S \land k \in S) \land (D \leq x \land x \leq k)) \to C \leq B$
	dvfsumrlim.g	$⊢ G = (x \in S ⟼ \sum_{k = M}^{⌊x⌋} C - A)$
	dvfsumrlim.k	$⊢ φ \to (x \in S ⟼ B) \underset{ℝ}{⇝} 0$
Assertion	dvfsumrlimge0	$⊢ (φ \land (x \in S \land D \leq x)) \to 0 \leq B$

Proof

Step	Hyp	Ref	Expression
1		dvfsum.s	$⊢ S = (T, +∞)$
2		dvfsum.z	$⊢ Z = ℤ_{\geq M}$
3		dvfsum.m	$⊢ φ \to M \in ℤ$
4		dvfsum.d	$⊢ φ \to D \in ℝ$
5		dvfsum.md	$⊢ φ \to M \leq D + 1$
6		dvfsum.t	$⊢ φ \to T \in ℝ$
7		dvfsum.a	$⊢ (φ \land x \in S) \to A \in ℝ$
8		dvfsum.b1	$⊢ (φ \land x \in S) \to B \in V$
9		dvfsum.b2	$⊢ (φ \land x \in Z) \to B \in ℝ$
10		dvfsum.b3	$⊢ φ \to \frac{d (x \in S⟼ A)}{d_{ℝ} x} = (x \in S ⟼ B)$
11		dvfsum.c	$⊢ x = k \to B = C$
12		dvfsumrlim.l	$⊢ (φ \land (x \in S \land k \in S) \land (D \leq x \land x \leq k)) \to C \leq B$
13		dvfsumrlim.g	$⊢ G = (x \in S ⟼ \sum_{k = M}^{⌊x⌋} C - A)$
14		dvfsumrlim.k	$⊢ φ \to (x \in S ⟼ B) \underset{ℝ}{⇝} 0$
15		ioossre	$⊢ (T, +∞) \subseteq ℝ$
16	1 15	eqsstri	$⊢ S \subseteq ℝ$
17		simprl	$⊢ (φ \land (x \in S \land D \leq x)) \to x \in S$
18	16 17	sselid	$⊢ (φ \land (x \in S \land D \leq x)) \to x \in ℝ$
19	18	rexrd	$⊢ (φ \land (x \in S \land D \leq x)) \to x \in ℝ^{*}$
20	18	renepnfd	$⊢ (φ \land (x \in S \land D \leq x)) \to x \neq +∞$
21		icopnfsup	$⊢ (x \in ℝ^{} \land x \neq +∞) \to sup ([x, +∞) ℝ^{} <) = +∞$
22	19 20 21	syl2anc	$⊢ (φ \land (x \in S \land D \leq x)) \to sup ([x, +∞) ℝ^{*} <) = +∞$
23	6	rexrd	$⊢ φ \to T \in ℝ^{*}$
24	17 1	eleqtrdi	$⊢ (φ \land (x \in S \land D \leq x)) \to x \in (T, +∞)$
25	23	adantr	$⊢ (φ \land (x \in S \land D \leq x)) \to T \in ℝ^{*}$
26		elioopnf	$⊢ T \in ℝ^{*} \to (x \in (T, +∞) \leftrightarrow (x \in ℝ \land T < x))$
27	25 26	syl	$⊢ (φ \land (x \in S \land D \leq x)) \to (x \in (T, +∞) \leftrightarrow (x \in ℝ \land T < x))$
28	24 27	mpbid	$⊢ (φ \land (x \in S \land D \leq x)) \to (x \in ℝ \land T < x)$
29	28	simprd	$⊢ (φ \land (x \in S \land D \leq x)) \to T < x$
30		df-ioo	$⊢ (.) = (u \in ℝ^{}, v \in ℝ^{} ⟼ \{w \in ℝ^{*} \| (u < w \land w < v)\})$
31		df-ico	$⊢ [.) = (u \in ℝ^{}, v \in ℝ^{} ⟼ \{w \in ℝ^{*} \| (u \leq w \land w < v)\})$
32		xrltletr	$⊢ (T \in ℝ^{} \land x \in ℝ^{} \land z \in ℝ^{*}) \to ((T < x \land x \leq z) \to T < z)$
33	30 31 32	ixxss1	$⊢ (T \in ℝ^{*} \land T < x) \to [x, +∞) \subseteq (T, +∞)$
34	23 29 33	syl2an2r	$⊢ (φ \land (x \in S \land D \leq x)) \to [x, +∞) \subseteq (T, +∞)$
35	34 1	sseqtrrdi	$⊢ (φ \land (x \in S \land D \leq x)) \to [x, +∞) \subseteq S$
36	11	cbvmptv	$⊢ (x \in S ⟼ B) = (k \in S ⟼ C)$
37	14	adantr	$⊢ (φ \land (x \in S \land D \leq x)) \to (x \in S ⟼ B) \underset{ℝ}{⇝} 0$
38	36 37	eqbrtrrid	$⊢ (φ \land (x \in S \land D \leq x)) \to (k \in S ⟼ C) \underset{ℝ}{⇝} 0$
39	35 38	rlimres2	$⊢ (φ \land (x \in S \land D \leq x)) \to (k \in [x, +∞) ⟼ C) \underset{ℝ}{⇝} 0$
40	16	a1i	$⊢ φ \to S \subseteq ℝ$
41	40 7 8 10	dvmptrecl	$⊢ (φ \land x \in S) \to B \in ℝ$
42	41	adantrr	$⊢ (φ \land (x \in S \land D \leq x)) \to B \in ℝ$
43	42	recnd	$⊢ (φ \land (x \in S \land D \leq x)) \to B \in ℂ$
44		rlimconst	$⊢ (S \subseteq ℝ \land B \in ℂ) \to (k \in S ⟼ B) \underset{ℝ}{⇝} B$
45	40 43 44	syl2an2r	$⊢ (φ \land (x \in S \land D \leq x)) \to (k \in S ⟼ B) \underset{ℝ}{⇝} B$
46	35 45	rlimres2	$⊢ (φ \land (x \in S \land D \leq x)) \to (k \in [x, +∞) ⟼ B) \underset{ℝ}{⇝} B$
47	41	ralrimiva	$⊢ φ \to \forall x \in S B \in ℝ$
48	47	adantr	$⊢ (φ \land (x \in S \land D \leq x)) \to \forall x \in S B \in ℝ$
49	35	sselda	$⊢ ((φ \land (x \in S \land D \leq x)) \land k \in [x, +∞)) \to k \in S$
50	11	eleq1d	$⊢ x = k \to (B \in ℝ \leftrightarrow C \in ℝ)$
51	50	rspccva	$⊢ (\forall x \in S B \in ℝ \land k \in S) \to C \in ℝ$
52	48 49 51	syl2an2r	$⊢ ((φ \land (x \in S \land D \leq x)) \land k \in [x, +∞)) \to C \in ℝ$
53	42	adantr	$⊢ ((φ \land (x \in S \land D \leq x)) \land k \in [x, +∞)) \to B \in ℝ$
54		simpll	$⊢ ((φ \land (x \in S \land D \leq x)) \land k \in [x, +∞)) \to φ$
55		simplrl	$⊢ ((φ \land (x \in S \land D \leq x)) \land k \in [x, +∞)) \to x \in S$
56		simplrr	$⊢ ((φ \land (x \in S \land D \leq x)) \land k \in [x, +∞)) \to D \leq x$
57		elicopnf	$⊢ x \in ℝ \to (k \in [x, +∞) \leftrightarrow (k \in ℝ \land x \leq k))$
58	18 57	syl	$⊢ (φ \land (x \in S \land D \leq x)) \to (k \in [x, +∞) \leftrightarrow (k \in ℝ \land x \leq k))$
59	58	simplbda	$⊢ ((φ \land (x \in S \land D \leq x)) \land k \in [x, +∞)) \to x \leq k$
60	54 55 49 56 59 12	syl122anc	$⊢ ((φ \land (x \in S \land D \leq x)) \land k \in [x, +∞)) \to C \leq B$
61	22 39 46 52 53 60	rlimle	$⊢ (φ \land (x \in S \land D \leq x)) \to 0 \leq B$

Metamath Proof Explorer

Theorem dvfsumrlimge0

Proof