Theorem knoppcnlem2

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

	Ref	Expression
Hypotheses	knoppcnlem2.t	$$⊢T=\left(x\in ℝ⟼\left|⌊x+\left(\frac{1}{2}\right)⌋-x\right|\right)$$
	knoppcnlem2.n	$$⊢\phi \to N\in \mathbb{N}$$
	knoppcnlem2.1	$$⊢\phi \to C\in ℝ$$
	knoppcnlem2.2	$$⊢\phi \to A\in ℝ$$
	knoppcnlem2.3	$$⊢\phi \to M\in {\mathbb{N}}_0$$
Assertion	knoppcnlem2	$$⊢\phi \to C^{M}T\left({2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A\right)\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		knoppcnlem2.t	$$⊢T=\left(x\in ℝ⟼\left|⌊x+\left(\frac{1}{2}\right)⌋-x\right|\right)$$
2		knoppcnlem2.n	$$⊢\phi \to N\in \mathbb{N}$$
3		knoppcnlem2.1	$$⊢\phi \to C\in ℝ$$
4		knoppcnlem2.2	$$⊢\phi \to A\in ℝ$$
5		knoppcnlem2.3	$$⊢\phi \to M\in {\mathbb{N}}_0$$
6	3 5	reexpcld	$$⊢\phi \to C^M\in ℝ$$
7		2re	$$⊢2\in ℝ$$
8	7	a1i	$$⊢\phi \to 2\in ℝ$$
9		nnre	$$⊢N\in \mathbb{N}\to N\in ℝ$$
10	2 9	syl	$$⊢\phi \to N\in ℝ$$
11	8 10	remulcld	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℝ$$
12	11 5	reexpcld	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^M\in ℝ$$
13	12 4	remulcld	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A\in ℝ$$
14	1 13	dnicld2	$$⊢\phi \to T\left({2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A\right)\in ℝ$$
15	6 14	remulcld	$$⊢\phi \to C^{M}T\left({2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A\right)\in ℝ$$