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	⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
	knoppcnlem2.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	knoppcnlem2.1	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
	knoppcnlem2.2	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	knoppcnlem2.3	⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
Assertion	knoppcnlem2	⊢ ( 𝜑 → ( ( 𝐶 ↑ 𝑀 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) ) ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		knoppcnlem2.t	⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
2		knoppcnlem2.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
3		knoppcnlem2.1	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
4		knoppcnlem2.2	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
5		knoppcnlem2.3	⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
6	3 5	reexpcld	⊢ ( 𝜑 → ( 𝐶 ↑ 𝑀 ) ∈ ℝ )
7		2re	⊢ 2 ∈ ℝ
8	7	a1i	⊢ ( 𝜑 → 2 ∈ ℝ )
9		nnre	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
10	2 9	syl	⊢ ( 𝜑 → 𝑁 ∈ ℝ )
11	8 10	remulcld	⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℝ )
12	11 5	reexpcld	⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ↑ 𝑀 ) ∈ ℝ )
13	12 4	remulcld	⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) ∈ ℝ )
14	1 13	dnicld2	⊢ ( 𝜑 → ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) ) ∈ ℝ )
15	6 14	remulcld	⊢ ( 𝜑 → ( ( 𝐶 ↑ 𝑀 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) ) ) ∈ ℝ )