This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → 𝐺 : 𝑆 ⟶ ℝ )