Theorem knoppndvlem5

Description: Lemma for knoppndv . (Contributed by Asger C. Ipsen, 15-Jun-2021) (Revised by Asger C. Ipsen, 5-Jul-2021)

	Ref	Expression
Hypotheses	knoppndvlem5.t	$$⊢T=\left(x\in ℝ⟼\left|⌊x+\left(\frac{1}{2}\right)⌋-x\right|\right)$$
	knoppndvlem5.f	$$⊢F=\left(y\in ℝ⟼\left(n\in {\mathbb{N}}_0⟼C^{n}T\left({2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{n}y\right)\right)\right)$$
	knoppndvlem5.a	$$⊢\phi \to A\in ℝ$$
	knoppndvlem5.c	$$⊢\phi \to C\in ℝ$$
	knoppndvlem5.n	$$⊢\phi \to N\in \mathbb{N}$$
Assertion	knoppndvlem5	$$⊢\phi \to \sum _{i=0}^{J}F\left(A\right)\left(i\right)\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		knoppndvlem5.t	$$⊢T=\left(x\in ℝ⟼\left|⌊x+\left(\frac{1}{2}\right)⌋-x\right|\right)$$
2		knoppndvlem5.f	$$⊢F=\left(y\in ℝ⟼\left(n\in {\mathbb{N}}_0⟼C^{n}T\left({2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{n}y\right)\right)\right)$$
3		knoppndvlem5.a	$$⊢\phi \to A\in ℝ$$
4		knoppndvlem5.c	$$⊢\phi \to C\in ℝ$$
5		knoppndvlem5.n	$$⊢\phi \to N\in \mathbb{N}$$
6		fzfid	$$⊢\phi \to \left(0\dots J\right)\in \mathrm{Fin}$$
7	5	adantr	$$⊢\left(\phi \wedge i\in \left(0\dots J\right)\right)\to N\in \mathbb{N}$$
8	4	adantr	$$⊢\left(\phi \wedge i\in \left(0\dots J\right)\right)\to C\in ℝ$$
9	3	adantr	$$⊢\left(\phi \wedge i\in \left(0\dots J\right)\right)\to A\in ℝ$$
10		elfznn0	$$⊢i\in \left(0\dots J\right)\to i\in {\mathbb{N}}_0$$
11	10	adantl	$$⊢\left(\phi \wedge i\in \left(0\dots J\right)\right)\to i\in {\mathbb{N}}_0$$
12	1 2 7 8 9 11	knoppcnlem3	$$⊢\left(\phi \wedge i\in \left(0\dots J\right)\right)\to F\left(A\right)\left(i\right)\in ℝ$$
13	6 12	fsumrecl	$$⊢\phi \to \sum _{i=0}^{J}F\left(A\right)\left(i\right)\in ℝ$$