dvfsumrlim3

Description: Conjoin the statements of dvfsumrlim and dvfsumrlim2 . (This is useful as a target for lemmas, because the hypotheses to this theorem are complex, and we don't want to repeat ourselves.) (Contributed by Mario Carneiro, 18-May-2016)

	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$
	dvfsumrlim3.1	$⊢ x = X \to B = E$
Assertion	dvfsumrlim3	$⊢ φ \to (G : S ⟶ ℝ \land G \in dom \underset{ℝ}{⇝} \land ((G \underset{ℝ}{⇝} L \land X \in S \land D \leq X) \to \|G (X) - L\| \leq E))$

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		dvfsumrlim3.1	$⊢ x = X \to B = E$
16	1 2 3 4 5 6 7 8 9 10 11 13	dvfsumrlimf	$⊢ φ \to G : S ⟶ ℝ$
17	1 2 3 4 5 6 7 8 9 10 11 12 13 14	dvfsumrlim	$⊢ φ \to G \in dom \underset{ℝ}{⇝}$
18	3	adantr	$⊢ (φ \land (D \leq X \land X \in S)) \to M \in ℤ$
19	4	adantr	$⊢ (φ \land (D \leq X \land X \in S)) \to D \in ℝ$
20	5	adantr	$⊢ (φ \land (D \leq X \land X \in S)) \to M \leq D + 1$
21	6	adantr	$⊢ (φ \land (D \leq X \land X \in S)) \to T \in ℝ$
22	7	adantlr	$⊢ ((φ \land (D \leq X \land X \in S)) \land x \in S) \to A \in ℝ$
23	8	adantlr	$⊢ ((φ \land (D \leq X \land X \in S)) \land x \in S) \to B \in V$
24	9	adantlr	$⊢ ((φ \land (D \leq X \land X \in S)) \land x \in Z) \to B \in ℝ$
25	10	adantr	$⊢ (φ \land (D \leq X \land X \in S)) \to \frac{d (x \in S⟼ A)}{d_{ℝ} x} = (x \in S ⟼ B)$
26	12	3adant1r	$⊢ ((φ \land (D \leq X \land X \in S)) \land (x \in S \land k \in S) \land (D \leq x \land x \leq k)) \to C \leq B$
27	14	adantr	$⊢ (φ \land (D \leq X \land X \in S)) \to (x \in S ⟼ B) \underset{ℝ}{⇝} 0$
28		simprr	$⊢ (φ \land (D \leq X \land X \in S)) \to X \in S$
29		simprl	$⊢ (φ \land (D \leq X \land X \in S)) \to D \leq X$
30	1 2 18 19 20 21 22 23 24 25 11 26 13 27 28 29	dvfsumrlim2	$⊢ ((φ \land (D \leq X \land X \in S)) \land G \underset{ℝ}{⇝} L) \to \|G (X) - L\| \leq ⦋ X / x ⦌ B$
31	28	adantr	$⊢ ((φ \land (D \leq X \land X \in S)) \land G \underset{ℝ}{⇝} L) \to X \in S$
32		nfcvd	$⊢ X \in S \to \underline{Ⅎ} x E$
33	32 15	csbiegf	$⊢ X \in S \to ⦋ X / x ⦌ B = E$
34	31 33	syl	$⊢ ((φ \land (D \leq X \land X \in S)) \land G \underset{ℝ}{⇝} L) \to ⦋ X / x ⦌ B = E$
35	30 34	breqtrd	$⊢ ((φ \land (D \leq X \land X \in S)) \land G \underset{ℝ}{⇝} L) \to \|G (X) - L\| \leq E$
36	35	exp42	$⊢ φ \to (D \leq X \to (X \in S \to (G \underset{ℝ}{⇝} L \to \|G (X) - L\| \leq E)))$
37	36	com24	$⊢ φ \to (G \underset{ℝ}{⇝} L \to (X \in S \to (D \leq X \to \|G (X) - L\| \leq E)))$
38	37	3impd	$⊢ φ \to ((G \underset{ℝ}{⇝} L \land X \in S \land D \leq X) \to \|G (X) - L\| \leq E)$
39	16 17 38	3jca	$⊢ φ \to (G : S ⟶ ℝ \land G \in dom \underset{ℝ}{⇝} \land ((G \underset{ℝ}{⇝} L \land X \in S \land D \leq X) \to \|G (X) - L\| \leq E))$

Metamath Proof Explorer

Theorem dvfsumrlim3

Proof