Metamath Proof Explorer


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 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) ) ) ∈ ℝ )