Theorem dvfsumrlimf

Description: Lemma for dvfsumrlim . (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	⊢ ( 𝑥 = 𝑘 → 𝐵 = 𝐶 )
	dvfsumrlimf.g	⊢ 𝐺 = ( 𝑥 ∈ 𝑆 ↦ ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) 𝐶 − 𝐴 ) )
Assertion	dvfsumrlimf	⊢ ( 𝜑 → 𝐺 : 𝑆 ⟶ ℝ )

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		dvfsumrlimf.g	⊢ 𝐺 = ( 𝑥 ∈ 𝑆 ↦ ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) 𝐶 − 𝐴 ) )
13		fzfid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
14	9	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑍 𝐵 ∈ ℝ )
15	14	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ∀ 𝑥 ∈ 𝑍 𝐵 ∈ ℝ )
16		elfzuz	⊢ ( 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
17	16 2	eleqtrrdi	⊢ ( 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) → 𝑘 ∈ 𝑍 )
18	11	eleq1d	⊢ ( 𝑥 = 𝑘 → ( 𝐵 ∈ ℝ ↔ 𝐶 ∈ ℝ ) )
19	18	rspccva	⊢ ( ( ∀ 𝑥 ∈ 𝑍 𝐵 ∈ ℝ ∧ 𝑘 ∈ 𝑍 ) → 𝐶 ∈ ℝ )
20	15 17 19	syl2an	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝐶 ∈ ℝ )
21	13 20	fsumrecl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) 𝐶 ∈ ℝ )
22	21 7	resubcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) 𝐶 − 𝐴 ) ∈ ℝ )
23	22 12	fmptd	⊢ ( 𝜑 → 𝐺 : 𝑆 ⟶ ℝ )