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 ( ⇝𝑢 ‘ ℝ ) )