Theorem knoppcnlem5

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

	Ref	Expression
Hypotheses	knoppcnlem5.t	⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
	knoppcnlem5.f	⊢ 𝐹 = ( 𝑦 ∈ ℝ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐶 ↑ 𝑛 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑛 ) · 𝑦 ) ) ) ) )
	knoppcnlem5.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	knoppcnlem5.1	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
Assertion	knoppcnlem5	⊢ ( 𝜑 → ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) : ℕ0 ⟶ ( ℂ ↑m ℝ ) )

Proof

Step	Hyp	Ref	Expression
1		knoppcnlem5.t	⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
2		knoppcnlem5.f	⊢ 𝐹 = ( 𝑦 ∈ ℝ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐶 ↑ 𝑛 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑛 ) · 𝑦 ) ) ) ) )
3		knoppcnlem5.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4		knoppcnlem5.1	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
5	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑧 ∈ ℝ ) → 𝑁 ∈ ℕ )
6	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑧 ∈ ℝ ) → 𝐶 ∈ ℝ )
7		simpr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑧 ∈ ℝ ) → 𝑧 ∈ ℝ )
8		simplr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑧 ∈ ℝ ) → 𝑚 ∈ ℕ0 )
9	1 2 5 6 7 8	knoppcnlem3	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑧 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ∈ ℝ )
10	9	recnd	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑧 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ∈ ℂ )
11	10	fmpttd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) : ℝ ⟶ ℂ )
12		cnex	⊢ ℂ ∈ V
13		reex	⊢ ℝ ∈ V
14	12 13	pm3.2i	⊢ ( ℂ ∈ V ∧ ℝ ∈ V )
15		elmapg	⊢ ( ( ℂ ∈ V ∧ ℝ ∈ V ) → ( ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ∈ ( ℂ ↑m ℝ ) ↔ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) : ℝ ⟶ ℂ ) )
16	14 15	ax-mp	⊢ ( ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ∈ ( ℂ ↑m ℝ ) ↔ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) : ℝ ⟶ ℂ )
17	11 16	sylibr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ∈ ( ℂ ↑m ℝ ) )
18	17	fmpttd	⊢ ( 𝜑 → ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) : ℕ0 ⟶ ( ℂ ↑m ℝ ) )