Metamath Proof Explorer


Theorem knoppcnlem6

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

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

Proof

Step Hyp Ref Expression
1 knoppcnlem6.t 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
2 knoppcnlem6.f 𝐹 = ( 𝑦 ∈ ℝ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐶𝑛 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑛 ) · 𝑦 ) ) ) ) )
3 knoppcnlem6.n ( 𝜑𝑁 ∈ ℕ )
4 knoppcnlem6.1 ( 𝜑𝐶 ∈ ℝ )
5 knoppcnlem6.2 ( 𝜑 → ( abs ‘ 𝐶 ) < 1 )
6 nn0uz 0 = ( ℤ ‘ 0 )
7 0zd ( 𝜑 → 0 ∈ ℤ )
8 reex ℝ ∈ V
9 8 a1i ( 𝜑 → ℝ ∈ V )
10 1 2 3 4 knoppcnlem5 ( 𝜑 → ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹𝑧 ) ‘ 𝑚 ) ) ) : ℕ0 ⟶ ( ℂ ↑m ℝ ) )
11 nn0ex 0 ∈ V
12 11 mptex ( 𝑚 ∈ ℕ0 ↦ ( ( abs ‘ 𝐶 ) ↑ 𝑚 ) ) ∈ V
13 12 a1i ( 𝜑 → ( 𝑚 ∈ ℕ0 ↦ ( ( abs ‘ 𝐶 ) ↑ 𝑚 ) ) ∈ V )
14 eqid ( 𝑚 ∈ ℕ0 ↦ ( ( abs ‘ 𝐶 ) ↑ 𝑚 ) ) = ( 𝑚 ∈ ℕ0 ↦ ( ( abs ‘ 𝐶 ) ↑ 𝑚 ) )
15 14 a1i ( ( 𝜑𝑘 ∈ ℕ0 ) → ( 𝑚 ∈ ℕ0 ↦ ( ( abs ‘ 𝐶 ) ↑ 𝑚 ) ) = ( 𝑚 ∈ ℕ0 ↦ ( ( abs ‘ 𝐶 ) ↑ 𝑚 ) ) )
16 simpr ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ 𝑚 = 𝑘 ) → 𝑚 = 𝑘 )
17 16 oveq2d ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ 𝑚 = 𝑘 ) → ( ( abs ‘ 𝐶 ) ↑ 𝑚 ) = ( ( abs ‘ 𝐶 ) ↑ 𝑘 ) )
18 simpr ( ( 𝜑𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
19 ovexd ( ( 𝜑𝑘 ∈ ℕ0 ) → ( ( abs ‘ 𝐶 ) ↑ 𝑘 ) ∈ V )
20 15 17 18 19 fvmptd ( ( 𝜑𝑘 ∈ ℕ0 ) → ( ( 𝑚 ∈ ℕ0 ↦ ( ( abs ‘ 𝐶 ) ↑ 𝑚 ) ) ‘ 𝑘 ) = ( ( abs ‘ 𝐶 ) ↑ 𝑘 ) )
21 4 recnd ( 𝜑𝐶 ∈ ℂ )
22 21 abscld ( 𝜑 → ( abs ‘ 𝐶 ) ∈ ℝ )
23 22 adantr ( ( 𝜑𝑘 ∈ ℕ0 ) → ( abs ‘ 𝐶 ) ∈ ℝ )
24 23 18 reexpcld ( ( 𝜑𝑘 ∈ ℕ0 ) → ( ( abs ‘ 𝐶 ) ↑ 𝑘 ) ∈ ℝ )
25 20 24 eqeltrd ( ( 𝜑𝑘 ∈ ℕ0 ) → ( ( 𝑚 ∈ ℕ0 ↦ ( ( abs ‘ 𝐶 ) ↑ 𝑚 ) ) ‘ 𝑘 ) ∈ ℝ )
26 eqid ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹𝑧 ) ‘ 𝑚 ) ) ) = ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹𝑧 ) ‘ 𝑚 ) ) )
27 26 a1i ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ0𝑤 ∈ ℝ ) ) → ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹𝑧 ) ‘ 𝑚 ) ) ) = ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹𝑧 ) ‘ 𝑚 ) ) ) )
28 simpr ( ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ0𝑤 ∈ ℝ ) ) ∧ 𝑚 = 𝑘 ) → 𝑚 = 𝑘 )
29 28 fveq2d ( ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ0𝑤 ∈ ℝ ) ) ∧ 𝑚 = 𝑘 ) → ( ( 𝐹𝑧 ) ‘ 𝑚 ) = ( ( 𝐹𝑧 ) ‘ 𝑘 ) )
30 29 mpteq2dv ( ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ0𝑤 ∈ ℝ ) ) ∧ 𝑚 = 𝑘 ) → ( 𝑧 ∈ ℝ ↦ ( ( 𝐹𝑧 ) ‘ 𝑚 ) ) = ( 𝑧 ∈ ℝ ↦ ( ( 𝐹𝑧 ) ‘ 𝑘 ) ) )
31 18 adantrr ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ0𝑤 ∈ ℝ ) ) → 𝑘 ∈ ℕ0 )
32 8 mptex ( 𝑧 ∈ ℝ ↦ ( ( 𝐹𝑧 ) ‘ 𝑘 ) ) ∈ V
33 32 a1i ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ0𝑤 ∈ ℝ ) ) → ( 𝑧 ∈ ℝ ↦ ( ( 𝐹𝑧 ) ‘ 𝑘 ) ) ∈ V )
34 27 30 31 33 fvmptd ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ0𝑤 ∈ ℝ ) ) → ( ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹𝑧 ) ‘ 𝑚 ) ) ) ‘ 𝑘 ) = ( 𝑧 ∈ ℝ ↦ ( ( 𝐹𝑧 ) ‘ 𝑘 ) ) )
35 simpr ( ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ0𝑤 ∈ ℝ ) ) ∧ 𝑧 = 𝑤 ) → 𝑧 = 𝑤 )
36 35 fveq2d ( ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ0𝑤 ∈ ℝ ) ) ∧ 𝑧 = 𝑤 ) → ( 𝐹𝑧 ) = ( 𝐹𝑤 ) )
37 36 fveq1d ( ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ0𝑤 ∈ ℝ ) ) ∧ 𝑧 = 𝑤 ) → ( ( 𝐹𝑧 ) ‘ 𝑘 ) = ( ( 𝐹𝑤 ) ‘ 𝑘 ) )
38 simprr ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ0𝑤 ∈ ℝ ) ) → 𝑤 ∈ ℝ )
39 fvexd ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ0𝑤 ∈ ℝ ) ) → ( ( 𝐹𝑤 ) ‘ 𝑘 ) ∈ V )
40 34 37 38 39 fvmptd ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ0𝑤 ∈ ℝ ) ) → ( ( ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹𝑧 ) ‘ 𝑚 ) ) ) ‘ 𝑘 ) ‘ 𝑤 ) = ( ( 𝐹𝑤 ) ‘ 𝑘 ) )
41 40 fveq2d ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ0𝑤 ∈ ℝ ) ) → ( abs ‘ ( ( ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹𝑧 ) ‘ 𝑚 ) ) ) ‘ 𝑘 ) ‘ 𝑤 ) ) = ( abs ‘ ( ( 𝐹𝑤 ) ‘ 𝑘 ) ) )
42 3 adantr ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ0𝑤 ∈ ℝ ) ) → 𝑁 ∈ ℕ )
43 4 adantr ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ0𝑤 ∈ ℝ ) ) → 𝐶 ∈ ℝ )
44 1 2 42 43 38 31 knoppcnlem4 ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ0𝑤 ∈ ℝ ) ) → ( abs ‘ ( ( 𝐹𝑤 ) ‘ 𝑘 ) ) ≤ ( ( 𝑚 ∈ ℕ0 ↦ ( ( abs ‘ 𝐶 ) ↑ 𝑚 ) ) ‘ 𝑘 ) )
45 41 44 eqbrtrd ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ0𝑤 ∈ ℝ ) ) → ( abs ‘ ( ( ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹𝑧 ) ‘ 𝑚 ) ) ) ‘ 𝑘 ) ‘ 𝑤 ) ) ≤ ( ( 𝑚 ∈ ℕ0 ↦ ( ( abs ‘ 𝐶 ) ↑ 𝑚 ) ) ‘ 𝑘 ) )
46 22 recnd ( 𝜑 → ( abs ‘ 𝐶 ) ∈ ℂ )
47 absidm ( 𝐶 ∈ ℂ → ( abs ‘ ( abs ‘ 𝐶 ) ) = ( abs ‘ 𝐶 ) )
48 21 47 syl ( 𝜑 → ( abs ‘ ( abs ‘ 𝐶 ) ) = ( abs ‘ 𝐶 ) )
49 48 5 eqbrtrd ( 𝜑 → ( abs ‘ ( abs ‘ 𝐶 ) ) < 1 )
50 46 49 20 geolim ( 𝜑 → seq 0 ( + , ( 𝑚 ∈ ℕ0 ↦ ( ( abs ‘ 𝐶 ) ↑ 𝑚 ) ) ) ⇝ ( 1 / ( 1 − ( abs ‘ 𝐶 ) ) ) )
51 seqex seq 0 ( + , ( 𝑚 ∈ ℕ0 ↦ ( ( abs ‘ 𝐶 ) ↑ 𝑚 ) ) ) ∈ V
52 ovex ( 1 / ( 1 − ( abs ‘ 𝐶 ) ) ) ∈ V
53 51 52 breldm ( seq 0 ( + , ( 𝑚 ∈ ℕ0 ↦ ( ( abs ‘ 𝐶 ) ↑ 𝑚 ) ) ) ⇝ ( 1 / ( 1 − ( abs ‘ 𝐶 ) ) ) → seq 0 ( + , ( 𝑚 ∈ ℕ0 ↦ ( ( abs ‘ 𝐶 ) ↑ 𝑚 ) ) ) ∈ dom ⇝ )
54 50 53 syl ( 𝜑 → seq 0 ( + , ( 𝑚 ∈ ℕ0 ↦ ( ( abs ‘ 𝐶 ) ↑ 𝑚 ) ) ) ∈ dom ⇝ )
55 6 7 9 10 13 25 45 54 mtest ( 𝜑 → seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹𝑧 ) ‘ 𝑚 ) ) ) ) ∈ dom ( ⇝𝑢 ‘ ℝ ) )