Theorem 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	⊢ 𝑆 = ( 𝑇 (,) +∞ )
	dvfsum.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	dvfsum.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	dvfsum.d	⊢ ( 𝜑 → 𝐷 ∈ ℝ )
	dvfsum.md	⊢ ( 𝜑 → 𝑀 ≤ ( 𝐷 + 1 ) )
	dvfsum.t	⊢ ( 𝜑 → 𝑇 ∈ ℝ )
	dvfsum.a	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐴 ∈ ℝ )
	dvfsum.b1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐵 ∈ 𝑉 )
	dvfsum.b2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑍 ) → 𝐵 ∈ ℝ )
	dvfsum.b3	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) )
	dvfsum.c	⊢ ( 𝑥 = 𝑘 → 𝐵 = 𝐶 )
	dvfsumrlim.l	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ) ) → 𝐶 ≤ 𝐵 )
	dvfsumrlim.g	⊢ 𝐺 = ( 𝑥 ∈ 𝑆 ↦ ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) 𝐶 − 𝐴 ) )
	dvfsumrlim.k	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) ⇝𝑟 0 )
	dvfsumrlim3.1	⊢ ( 𝑥 = 𝑋 → 𝐵 = 𝐸 )
Assertion	dvfsumrlim3	⊢ ( 𝜑 → ( 𝐺 : 𝑆 ⟶ ℝ ∧ 𝐺 ∈ dom ⇝𝑟 ∧ ( ( 𝐺 ⇝𝑟 𝐿 ∧ 𝑋 ∈ 𝑆 ∧ 𝐷 ≤ 𝑋 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) − 𝐿 ) ) ≤ 𝐸 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dvfsum.s	⊢ 𝑆 = ( 𝑇 (,) +∞ )
2		dvfsum.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3		dvfsum.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
4		dvfsum.d	⊢ ( 𝜑 → 𝐷 ∈ ℝ )
5		dvfsum.md	⊢ ( 𝜑 → 𝑀 ≤ ( 𝐷 + 1 ) )
6		dvfsum.t	⊢ ( 𝜑 → 𝑇 ∈ ℝ )
7		dvfsum.a	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐴 ∈ ℝ )
8		dvfsum.b1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐵 ∈ 𝑉 )
9		dvfsum.b2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑍 ) → 𝐵 ∈ ℝ )
10		dvfsum.b3	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) )
11		dvfsum.c	⊢ ( 𝑥 = 𝑘 → 𝐵 = 𝐶 )
12		dvfsumrlim.l	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ) ) → 𝐶 ≤ 𝐵 )
13		dvfsumrlim.g	⊢ 𝐺 = ( 𝑥 ∈ 𝑆 ↦ ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) 𝐶 − 𝐴 ) )
14		dvfsumrlim.k	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) ⇝𝑟 0 )
15		dvfsumrlim3.1	⊢ ( 𝑥 = 𝑋 → 𝐵 = 𝐸 )
16	1 2 3 4 5 6 7 8 9 10 11 13	dvfsumrlimf	⊢ ( 𝜑 → 𝐺 : 𝑆 ⟶ ℝ )
17	1 2 3 4 5 6 7 8 9 10 11 12 13 14	dvfsumrlim	⊢ ( 𝜑 → 𝐺 ∈ dom ⇝𝑟 )
18	3	adantr	⊢ ( ( 𝜑 ∧ ( 𝐷 ≤ 𝑋 ∧ 𝑋 ∈ 𝑆 ) ) → 𝑀 ∈ ℤ )
19	4	adantr	⊢ ( ( 𝜑 ∧ ( 𝐷 ≤ 𝑋 ∧ 𝑋 ∈ 𝑆 ) ) → 𝐷 ∈ ℝ )
20	5	adantr	⊢ ( ( 𝜑 ∧ ( 𝐷 ≤ 𝑋 ∧ 𝑋 ∈ 𝑆 ) ) → 𝑀 ≤ ( 𝐷 + 1 ) )
21	6	adantr	⊢ ( ( 𝜑 ∧ ( 𝐷 ≤ 𝑋 ∧ 𝑋 ∈ 𝑆 ) ) → 𝑇 ∈ ℝ )
22	7	adantlr	⊢ ( ( ( 𝜑 ∧ ( 𝐷 ≤ 𝑋 ∧ 𝑋 ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝐴 ∈ ℝ )
23	8	adantlr	⊢ ( ( ( 𝜑 ∧ ( 𝐷 ≤ 𝑋 ∧ 𝑋 ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝐵 ∈ 𝑉 )
24	9	adantlr	⊢ ( ( ( 𝜑 ∧ ( 𝐷 ≤ 𝑋 ∧ 𝑋 ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝑍 ) → 𝐵 ∈ ℝ )
25	10	adantr	⊢ ( ( 𝜑 ∧ ( 𝐷 ≤ 𝑋 ∧ 𝑋 ∈ 𝑆 ) ) → ( ℝ D ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) )
26	12	3adant1r	⊢ ( ( ( 𝜑 ∧ ( 𝐷 ≤ 𝑋 ∧ 𝑋 ∈ 𝑆 ) ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ) ) → 𝐶 ≤ 𝐵 )
27	14	adantr	⊢ ( ( 𝜑 ∧ ( 𝐷 ≤ 𝑋 ∧ 𝑋 ∈ 𝑆 ) ) → ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) ⇝𝑟 0 )
28		simprr	⊢ ( ( 𝜑 ∧ ( 𝐷 ≤ 𝑋 ∧ 𝑋 ∈ 𝑆 ) ) → 𝑋 ∈ 𝑆 )
29		simprl	⊢ ( ( 𝜑 ∧ ( 𝐷 ≤ 𝑋 ∧ 𝑋 ∈ 𝑆 ) ) → 𝐷 ≤ 𝑋 )
30	1 2 18 19 20 21 22 23 24 25 11 26 13 27 28 29	dvfsumrlim2	⊢ ( ( ( 𝜑 ∧ ( 𝐷 ≤ 𝑋 ∧ 𝑋 ∈ 𝑆 ) ) ∧ 𝐺 ⇝𝑟 𝐿 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) − 𝐿 ) ) ≤ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 )
31	28	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝐷 ≤ 𝑋 ∧ 𝑋 ∈ 𝑆 ) ) ∧ 𝐺 ⇝𝑟 𝐿 ) → 𝑋 ∈ 𝑆 )
32		nfcvd	⊢ ( 𝑋 ∈ 𝑆 → Ⅎ 𝑥 𝐸 )
33	32 15	csbiegf	⊢ ( 𝑋 ∈ 𝑆 → ⦋ 𝑋 / 𝑥 ⦌ 𝐵 = 𝐸 )
34	31 33	syl	⊢ ( ( ( 𝜑 ∧ ( 𝐷 ≤ 𝑋 ∧ 𝑋 ∈ 𝑆 ) ) ∧ 𝐺 ⇝𝑟 𝐿 ) → ⦋ 𝑋 / 𝑥 ⦌ 𝐵 = 𝐸 )
35	30 34	breqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝐷 ≤ 𝑋 ∧ 𝑋 ∈ 𝑆 ) ) ∧ 𝐺 ⇝𝑟 𝐿 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) − 𝐿 ) ) ≤ 𝐸 )
36	35	exp42	⊢ ( 𝜑 → ( 𝐷 ≤ 𝑋 → ( 𝑋 ∈ 𝑆 → ( 𝐺 ⇝𝑟 𝐿 → ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) − 𝐿 ) ) ≤ 𝐸 ) ) ) )
37	36	com24	⊢ ( 𝜑 → ( 𝐺 ⇝𝑟 𝐿 → ( 𝑋 ∈ 𝑆 → ( 𝐷 ≤ 𝑋 → ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) − 𝐿 ) ) ≤ 𝐸 ) ) ) )
38	37	3impd	⊢ ( 𝜑 → ( ( 𝐺 ⇝𝑟 𝐿 ∧ 𝑋 ∈ 𝑆 ∧ 𝐷 ≤ 𝑋 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) − 𝐿 ) ) ≤ 𝐸 ) )
39	16 17 38	3jca	⊢ ( 𝜑 → ( 𝐺 : 𝑆 ⟶ ℝ ∧ 𝐺 ∈ dom ⇝𝑟 ∧ ( ( 𝐺 ⇝𝑟 𝐿 ∧ 𝑋 ∈ 𝑆 ∧ 𝐷 ≤ 𝑋 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) − 𝐿 ) ) ≤ 𝐸 ) ) )