Theorem knoppcnlem3

Description: Lemma for knoppcn . (Contributed by Asger C. Ipsen, 4-Apr-2021) (Revised by Asger C. Ipsen, 5-Jul-2021)

	Ref	Expression
Hypotheses	knoppcnlem3.t	$$⊢T=\left(x\in ℝ⟼\left|⌊x+\left(\frac{1}{2}\right)⌋-x\right|\right)$$
	knoppcnlem3.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)$$
	knoppcnlem3.n	$$⊢\phi \to N\in \mathbb{N}$$
	knoppcnlem3.1	$$⊢\phi \to C\in ℝ$$
	knoppcnlem3.2	$$⊢\phi \to A\in ℝ$$
	knoppcnlem3.3	$$⊢\phi \to M\in {\mathbb{N}}_0$$
Assertion	knoppcnlem3	$$⊢\phi \to F\left(A\right)\left(M\right)\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		knoppcnlem3.t	$$⊢T=\left(x\in ℝ⟼\left|⌊x+\left(\frac{1}{2}\right)⌋-x\right|\right)$$
2		knoppcnlem3.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		knoppcnlem3.n	$$⊢\phi \to N\in \mathbb{N}$$
4		knoppcnlem3.1	$$⊢\phi \to C\in ℝ$$
5		knoppcnlem3.2	$$⊢\phi \to A\in ℝ$$
6		knoppcnlem3.3	$$⊢\phi \to M\in {\mathbb{N}}_0$$
7	2 5 6	knoppcnlem1	$$⊢\phi \to F\left(A\right)\left(M\right)=C^{M}T\left({2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A\right)$$
8	1 3 4 5 6	knoppcnlem2	$$⊢\phi \to C^{M}T\left({2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A\right)\in ℝ$$
9	7 8	eqeltrd	$$⊢\phi \to F\left(A\right)\left(M\right)\in ℝ$$