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 ⊢ S = T +∞
dvfsum.z ⊢ Z = ℤ ≥ M
dvfsum.m ⊢ φ → M ∈ ℤ
dvfsum.d ⊢ φ → D ∈ ℝ
dvfsum.md ⊢ φ → M ≤ D + 1
dvfsum.t ⊢ φ → T ∈ ℝ
dvfsum.a ⊢ φ ∧ x ∈ S → A ∈ ℝ
dvfsum.b1 ⊢ φ ∧ x ∈ S → B ∈ V
dvfsum.b2 ⊢ φ ∧ x ∈ Z → B ∈ ℝ
dvfsum.b3 ⊢ φ → dx ∈ S A d ℝ x = x ∈ S ⟼ B
dvfsum.c ⊢ x = k → B = C
dvfsumrlimf.g ⊢ G = x ∈ S ⟼ ∑ k = M x C − A
Assertion dvfsumrlimf ⊢ φ → G : S ⟶ ℝ

Proof

Step Hyp Ref Expression
1 dvfsum.s ⊢ S = T +∞
2 dvfsum.z ⊢ Z = ℤ ≥ M
3 dvfsum.m ⊢ φ → M ∈ ℤ
4 dvfsum.d ⊢ φ → D ∈ ℝ
5 dvfsum.md ⊢ φ → M ≤ D + 1
6 dvfsum.t ⊢ φ → T ∈ ℝ
7 dvfsum.a ⊢ φ ∧ x ∈ S → A ∈ ℝ
8 dvfsum.b1 ⊢ φ ∧ x ∈ S → B ∈ V
9 dvfsum.b2 ⊢ φ ∧ x ∈ Z → B ∈ ℝ
10 dvfsum.b3 ⊢ φ → dx ∈ S A d ℝ x = x ∈ S ⟼ B
11 dvfsum.c ⊢ x = k → B = C
12 dvfsumrlimf.g ⊢ G = x ∈ S ⟼ ∑ k = M x C − A
13 fzfid ⊢ φ ∧ x ∈ S → M … x ∈ Fin
14 9 ralrimiva ⊢ φ → ∀ x ∈ Z B ∈ ℝ
15 14 adantr ⊢ φ ∧ x ∈ S → ∀ x ∈ Z B ∈ ℝ
16 elfzuz ⊢ k ∈ M … x → k ∈ ℤ ≥ M
17 16 2 eleqtrrdi ⊢ k ∈ M … x → k ∈ Z
18 11 eleq1d ⊢ x = k → B ∈ ℝ ↔ C ∈ ℝ
19 18 rspccva ⊢ ∀ x ∈ Z B ∈ ℝ ∧ k ∈ Z → C ∈ ℝ
20 15 17 19 syl2an ⊢ φ ∧ x ∈ S ∧ k ∈ M … x → C ∈ ℝ
21 13 20 fsumrecl ⊢ φ ∧ x ∈ S → ∑ k = M x C ∈ ℝ
22 21 7 resubcld ⊢ φ ∧ x ∈ S → ∑ k = M x C − A ∈ ℝ
23 22 12 fmptd ⊢ φ → G : S ⟶ ℝ