Metamath Proof Explorer


Theorem knoppcnlem8

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

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

Proof

Step Hyp Ref Expression
1 knoppcnlem8.t 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
2 knoppcnlem8.f 𝐹 = ( 𝑦 ∈ ℝ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐶𝑛 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑛 ) · 𝑦 ) ) ) ) )
3 knoppcnlem8.n ( 𝜑𝑁 ∈ ℕ )
4 knoppcnlem8.1 ( 𝜑𝐶 ∈ ℝ )
5 3 adantr ( ( 𝜑𝑘 ∈ ℕ0 ) → 𝑁 ∈ ℕ )
6 4 adantr ( ( 𝜑𝑘 ∈ ℕ0 ) → 𝐶 ∈ ℝ )
7 simpr ( ( 𝜑𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
8 1 2 5 6 7 knoppcnlem7 ( ( 𝜑𝑘 ∈ ℕ0 ) → ( seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹𝑧 ) ‘ 𝑚 ) ) ) ) ‘ 𝑘 ) = ( 𝑤 ∈ ℝ ↦ ( seq 0 ( + , ( 𝐹𝑤 ) ) ‘ 𝑘 ) ) )
9 simplr ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ 𝑤 ∈ ℝ ) → 𝑘 ∈ ℕ0 )
10 nn0uz 0 = ( ℤ ‘ 0 )
11 9 10 eleqtrdi ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ 𝑤 ∈ ℝ ) → 𝑘 ∈ ( ℤ ‘ 0 ) )
12 5 ad2antrr ( ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ 𝑤 ∈ ℝ ) ∧ 𝑎 ∈ ( 0 ... 𝑘 ) ) → 𝑁 ∈ ℕ )
13 6 ad2antrr ( ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ 𝑤 ∈ ℝ ) ∧ 𝑎 ∈ ( 0 ... 𝑘 ) ) → 𝐶 ∈ ℝ )
14 simplr ( ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ 𝑤 ∈ ℝ ) ∧ 𝑎 ∈ ( 0 ... 𝑘 ) ) → 𝑤 ∈ ℝ )
15 elfznn0 ( 𝑎 ∈ ( 0 ... 𝑘 ) → 𝑎 ∈ ℕ0 )
16 15 adantl ( ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ 𝑤 ∈ ℝ ) ∧ 𝑎 ∈ ( 0 ... 𝑘 ) ) → 𝑎 ∈ ℕ0 )
17 1 2 12 13 14 16 knoppcnlem3 ( ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ 𝑤 ∈ ℝ ) ∧ 𝑎 ∈ ( 0 ... 𝑘 ) ) → ( ( 𝐹𝑤 ) ‘ 𝑎 ) ∈ ℝ )
18 17 recnd ( ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ 𝑤 ∈ ℝ ) ∧ 𝑎 ∈ ( 0 ... 𝑘 ) ) → ( ( 𝐹𝑤 ) ‘ 𝑎 ) ∈ ℂ )
19 addcl ( ( 𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ ) → ( 𝑎 + 𝑏 ) ∈ ℂ )
20 19 adantl ( ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ 𝑤 ∈ ℝ ) ∧ ( 𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ ) ) → ( 𝑎 + 𝑏 ) ∈ ℂ )
21 11 18 20 seqcl ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ 𝑤 ∈ ℝ ) → ( seq 0 ( + , ( 𝐹𝑤 ) ) ‘ 𝑘 ) ∈ ℂ )
22 21 fmpttd ( ( 𝜑𝑘 ∈ ℕ0 ) → ( 𝑤 ∈ ℝ ↦ ( seq 0 ( + , ( 𝐹𝑤 ) ) ‘ 𝑘 ) ) : ℝ ⟶ ℂ )
23 cnex ℂ ∈ V
24 reex ℝ ∈ V
25 23 24 pm3.2i ( ℂ ∈ V ∧ ℝ ∈ V )
26 elmapg ( ( ℂ ∈ V ∧ ℝ ∈ V ) → ( ( 𝑤 ∈ ℝ ↦ ( seq 0 ( + , ( 𝐹𝑤 ) ) ‘ 𝑘 ) ) ∈ ( ℂ ↑m ℝ ) ↔ ( 𝑤 ∈ ℝ ↦ ( seq 0 ( + , ( 𝐹𝑤 ) ) ‘ 𝑘 ) ) : ℝ ⟶ ℂ ) )
27 25 26 ax-mp ( ( 𝑤 ∈ ℝ ↦ ( seq 0 ( + , ( 𝐹𝑤 ) ) ‘ 𝑘 ) ) ∈ ( ℂ ↑m ℝ ) ↔ ( 𝑤 ∈ ℝ ↦ ( seq 0 ( + , ( 𝐹𝑤 ) ) ‘ 𝑘 ) ) : ℝ ⟶ ℂ )
28 22 27 sylibr ( ( 𝜑𝑘 ∈ ℕ0 ) → ( 𝑤 ∈ ℝ ↦ ( seq 0 ( + , ( 𝐹𝑤 ) ) ‘ 𝑘 ) ) ∈ ( ℂ ↑m ℝ ) )
29 8 28 eqeltrd ( ( 𝜑𝑘 ∈ ℕ0 ) → ( seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹𝑧 ) ‘ 𝑚 ) ) ) ) ‘ 𝑘 ) ∈ ( ℂ ↑m ℝ ) )
30 29 fmpttd ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ ( seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹𝑧 ) ‘ 𝑚 ) ) ) ) ‘ 𝑘 ) ) : ℕ0 ⟶ ( ℂ ↑m ℝ ) )
31 0z 0 ∈ ℤ
32 seqfn ( 0 ∈ ℤ → seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹𝑧 ) ‘ 𝑚 ) ) ) ) Fn ( ℤ ‘ 0 ) )
33 31 32 ax-mp seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹𝑧 ) ‘ 𝑚 ) ) ) ) Fn ( ℤ ‘ 0 )
34 10 fneq2i ( seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹𝑧 ) ‘ 𝑚 ) ) ) ) Fn ℕ0 ↔ seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹𝑧 ) ‘ 𝑚 ) ) ) ) Fn ( ℤ ‘ 0 ) )
35 33 34 mpbir seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹𝑧 ) ‘ 𝑚 ) ) ) ) Fn ℕ0
36 dffn5 ( seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹𝑧 ) ‘ 𝑚 ) ) ) ) Fn ℕ0 ↔ seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹𝑧 ) ‘ 𝑚 ) ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹𝑧 ) ‘ 𝑚 ) ) ) ) ‘ 𝑘 ) ) )
37 35 36 mpbi seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹𝑧 ) ‘ 𝑚 ) ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹𝑧 ) ‘ 𝑚 ) ) ) ) ‘ 𝑘 ) )
38 37 feq1i ( seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹𝑧 ) ‘ 𝑚 ) ) ) ) : ℕ0 ⟶ ( ℂ ↑m ℝ ) ↔ ( 𝑘 ∈ ℕ0 ↦ ( seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹𝑧 ) ‘ 𝑚 ) ) ) ) ‘ 𝑘 ) ) : ℕ0 ⟶ ( ℂ ↑m ℝ ) )
39 30 38 sylibr ( 𝜑 → seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹𝑧 ) ‘ 𝑚 ) ) ) ) : ℕ0 ⟶ ( ℂ ↑m ℝ ) )