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	⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
	knoppndvlem5.f	⊢ 𝐹 = ( 𝑦 ∈ ℝ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐶 ↑ 𝑛 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑛 ) · 𝑦 ) ) ) ) )
	knoppndvlem5.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	knoppndvlem5.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
	knoppndvlem5.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
Assertion	knoppndvlem5	⊢ ( 𝜑 → Σ 𝑖 ∈ ( 0 ... 𝐽 ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		knoppndvlem5.t	⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
2		knoppndvlem5.f	⊢ 𝐹 = ( 𝑦 ∈ ℝ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐶 ↑ 𝑛 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑛 ) · 𝑦 ) ) ) ) )
3		knoppndvlem5.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
4		knoppndvlem5.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
5		knoppndvlem5.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
6		fzfid	⊢ ( 𝜑 → ( 0 ... 𝐽 ) ∈ Fin )
7	5	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐽 ) ) → 𝑁 ∈ ℕ )
8	4	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐽 ) ) → 𝐶 ∈ ℝ )
9	3	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐽 ) ) → 𝐴 ∈ ℝ )
10		elfznn0	⊢ ( 𝑖 ∈ ( 0 ... 𝐽 ) → 𝑖 ∈ ℕ0 )
11	10	adantl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐽 ) ) → 𝑖 ∈ ℕ0 )
12	1 2 7 8 9 11	knoppcnlem3	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐽 ) ) → ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ∈ ℝ )
13	6 12	fsumrecl	⊢ ( 𝜑 → Σ 𝑖 ∈ ( 0 ... 𝐽 ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ∈ ℝ )