Theorem dvfsumrlimf

Description: Lemma for dvfsumrlim . (Contributed by Mario Carneiro, 18-May-2016)

	Ref	Expression
Hypotheses	dvfsum.s	$$⊢S=\left(T,\mathrm{+\infty }\right)$$
	dvfsum.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	dvfsum.m	$$⊢\phi \to M\in \mathbb{Z}$$
	dvfsum.d	$$⊢\phi \to D\in ℝ$$
	dvfsum.md	$$⊢\phi \to M\le D+1$$
	dvfsum.t	$$⊢\phi \to T\in ℝ$$
	dvfsum.a	$$⊢\left(\phi \wedge x\in S\right)\to A\in ℝ$$
	dvfsum.b1	$$⊢\left(\phi \wedge x\in S\right)\to B\in V$$
	dvfsum.b2	$$⊢\left(\phi \wedge x\in Z\right)\to B\in ℝ$$
	dvfsum.b3	$$⊢\phi \to \frac{d\left(x\in S⟼A\right)}{d_{ℝ}x}=\left(x\in S⟼B\right)$$
	dvfsum.c	$$⊢x=k\to B=C$$
	dvfsumrlimf.g	$$⊢G=\left(x\in S⟼\sum _{k=M}^{⌊x⌋}C-A\right)$$
Assertion	dvfsumrlimf	$$⊢\phi \to G:S⟶ℝ$$

Proof

Step	Hyp	Ref	Expression
1		dvfsum.s	$$⊢S=\left(T,\mathrm{+\infty }\right)$$
2		dvfsum.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
3		dvfsum.m	$$⊢\phi \to M\in \mathbb{Z}$$
4		dvfsum.d	$$⊢\phi \to D\in ℝ$$
5		dvfsum.md	$$⊢\phi \to M\le D+1$$
6		dvfsum.t	$$⊢\phi \to T\in ℝ$$
7		dvfsum.a	$$⊢\left(\phi \wedge x\in S\right)\to A\in ℝ$$
8		dvfsum.b1	$$⊢\left(\phi \wedge x\in S\right)\to B\in V$$
9		dvfsum.b2	$$⊢\left(\phi \wedge x\in Z\right)\to B\in ℝ$$
10		dvfsum.b3	$$⊢\phi \to \frac{d\left(x\in S⟼A\right)}{d_{ℝ}x}=\left(x\in S⟼B\right)$$
11		dvfsum.c	$$⊢x=k\to B=C$$
12		dvfsumrlimf.g	$$⊢G=\left(x\in S⟼\sum _{k=M}^{⌊x⌋}C-A\right)$$
13		fzfid	$$⊢\left(\phi \wedge x\in S\right)\to \left(M\dots ⌊x⌋\right)\in \mathrm{Fin}$$
14	9	ralrimiva	$$⊢\phi \to \forall x\in ZB\in ℝ$$
15	14	adantr	$$⊢\left(\phi \wedge x\in S\right)\to \forall x\in ZB\in ℝ$$
16		elfzuz	$$⊢k\in \left(M\dots ⌊x⌋\right)\to k\in {\mathbb{Z}}_{\ge M}$$
17	16 2	eleqtrrdi	$$⊢k\in \left(M\dots ⌊x⌋\right)\to k\in Z$$
18	11	eleq1d	$$⊢x=k\to \left(B\in ℝ\leftrightarrow C\in ℝ\right)$$
19	18	rspccva	$$⊢\left(\forall x\in ZB\in ℝ\wedge k\in Z\right)\to C\in ℝ$$
20	15 17 19	syl2an	$$⊢\left(\left(\phi \wedge x\in S\right)\wedge k\in \left(M\dots ⌊x⌋\right)\right)\to C\in ℝ$$
21	13 20	fsumrecl	$$⊢\left(\phi \wedge x\in S\right)\to \sum _{k=M}^{⌊x⌋}C\in ℝ$$
22	21 7	resubcld	$$⊢\left(\phi \wedge x\in S\right)\to \sum _{k=M}^{⌊x⌋}C-A\in ℝ$$
23	22 12	fmptd	$$⊢\phi \to G:S⟶ℝ$$