Theorem knoppcnlem9

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

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

Proof

Step	Hyp	Ref	Expression
1		knoppcnlem9.t	⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
2		knoppcnlem9.f	⊢ 𝐹 = ( 𝑦 ∈ ℝ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐶 ↑ 𝑛 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑛 ) · 𝑦 ) ) ) ) )
3		knoppcnlem9.w	⊢ 𝑊 = ( 𝑤 ∈ ℝ ↦ Σ 𝑖 ∈ ℕ0 ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑖 ) )
4		knoppcnlem9.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
5		knoppcnlem9.1	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
6		knoppcnlem9.2	⊢ ( 𝜑 → ( abs ‘ 𝐶 ) < 1 )
7	1 2 4 5 6	knoppcnlem6	⊢ ( 𝜑 → seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ∈ dom ( ⇝𝑢 ‘ ℝ ) )
8		seqex	⊢ seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ∈ V
9	8	eldm	⊢ ( seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ∈ dom ( ⇝𝑢 ‘ ℝ ) ↔ ∃ 𝑓 seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ( ⇝𝑢 ‘ ℝ ) 𝑓 )
10	7 9	sylib	⊢ ( 𝜑 → ∃ 𝑓 seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ( ⇝𝑢 ‘ ℝ ) 𝑓 )
11		simpr	⊢ ( ( 𝜑 ∧ seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ( ⇝𝑢 ‘ ℝ ) 𝑓 ) → seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ( ⇝𝑢 ‘ ℝ ) 𝑓 )
12		ulmcl	⊢ ( seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ( ⇝𝑢 ‘ ℝ ) 𝑓 → 𝑓 : ℝ ⟶ ℂ )
13	12	feqmptd	⊢ ( seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ( ⇝𝑢 ‘ ℝ ) 𝑓 → 𝑓 = ( 𝑤 ∈ ℝ ↦ ( 𝑓 ‘ 𝑤 ) ) )
14	13	adantl	⊢ ( ( 𝜑 ∧ seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ( ⇝𝑢 ‘ ℝ ) 𝑓 ) → 𝑓 = ( 𝑤 ∈ ℝ ↦ ( 𝑓 ‘ 𝑤 ) ) )
15		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
16		0zd	⊢ ( ( ( 𝜑 ∧ seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ( ⇝𝑢 ‘ ℝ ) 𝑓 ) ∧ 𝑤 ∈ ℝ ) → 0 ∈ ℤ )
17		eqidd	⊢ ( ( ( ( 𝜑 ∧ seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ( ⇝𝑢 ‘ ℝ ) 𝑓 ) ∧ 𝑤 ∈ ℝ ) ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑖 ) = ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑖 ) )
18	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑖 ∈ ℕ0 ) → 𝑁 ∈ ℕ )
19	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑖 ∈ ℕ0 ) → 𝐶 ∈ ℝ )
20		simplr	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑖 ∈ ℕ0 ) → 𝑤 ∈ ℝ )
21		simpr	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑖 ∈ ℕ0 ) → 𝑖 ∈ ℕ0 )
22	1 2 18 19 20 21	knoppcnlem3	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑖 ) ∈ ℝ )
23	22	adantllr	⊢ ( ( ( ( 𝜑 ∧ seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ( ⇝𝑢 ‘ ℝ ) 𝑓 ) ∧ 𝑤 ∈ ℝ ) ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑖 ) ∈ ℝ )
24	23	recnd	⊢ ( ( ( ( 𝜑 ∧ seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ( ⇝𝑢 ‘ ℝ ) 𝑓 ) ∧ 𝑤 ∈ ℝ ) ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑖 ) ∈ ℂ )
25	1 2 4 5	knoppcnlem8	⊢ ( 𝜑 → seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) : ℕ0 ⟶ ( ℂ ↑m ℝ ) )
26	25	ad2antrr	⊢ ( ( ( 𝜑 ∧ seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ( ⇝𝑢 ‘ ℝ ) 𝑓 ) ∧ 𝑤 ∈ ℝ ) → seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) : ℕ0 ⟶ ( ℂ ↑m ℝ ) )
27		simpr	⊢ ( ( ( 𝜑 ∧ seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ( ⇝𝑢 ‘ ℝ ) 𝑓 ) ∧ 𝑤 ∈ ℝ ) → 𝑤 ∈ ℝ )
28		seqex	⊢ seq 0 ( + , ( 𝐹 ‘ 𝑤 ) ) ∈ V
29	28	a1i	⊢ ( ( ( 𝜑 ∧ seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ( ⇝𝑢 ‘ ℝ ) 𝑓 ) ∧ 𝑤 ∈ ℝ ) → seq 0 ( + , ( 𝐹 ‘ 𝑤 ) ) ∈ V )
30	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑘 ∈ ℕ0 ) → 𝑁 ∈ ℕ )
31	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑘 ∈ ℕ0 ) → 𝐶 ∈ ℝ )
32		simpr	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
33	1 2 30 31 32	knoppcnlem7	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑘 ∈ ℕ0 ) → ( seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ‘ 𝑘 ) = ( 𝑣 ∈ ℝ ↦ ( seq 0 ( + , ( 𝐹 ‘ 𝑣 ) ) ‘ 𝑘 ) ) )
34	33	adantllr	⊢ ( ( ( ( 𝜑 ∧ seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ( ⇝𝑢 ‘ ℝ ) 𝑓 ) ∧ 𝑤 ∈ ℝ ) ∧ 𝑘 ∈ ℕ0 ) → ( seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ‘ 𝑘 ) = ( 𝑣 ∈ ℝ ↦ ( seq 0 ( + , ( 𝐹 ‘ 𝑣 ) ) ‘ 𝑘 ) ) )
35	34	fveq1d	⊢ ( ( ( ( 𝜑 ∧ seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ( ⇝𝑢 ‘ ℝ ) 𝑓 ) ∧ 𝑤 ∈ ℝ ) ∧ 𝑘 ∈ ℕ0 ) → ( ( seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ‘ 𝑘 ) ‘ 𝑤 ) = ( ( 𝑣 ∈ ℝ ↦ ( seq 0 ( + , ( 𝐹 ‘ 𝑣 ) ) ‘ 𝑘 ) ) ‘ 𝑤 ) )
36		eqid	⊢ ( 𝑣 ∈ ℝ ↦ ( seq 0 ( + , ( 𝐹 ‘ 𝑣 ) ) ‘ 𝑘 ) ) = ( 𝑣 ∈ ℝ ↦ ( seq 0 ( + , ( 𝐹 ‘ 𝑣 ) ) ‘ 𝑘 ) )
37		fveq2	⊢ ( 𝑣 = 𝑤 → ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝑤 ) )
38	37	seqeq3d	⊢ ( 𝑣 = 𝑤 → seq 0 ( + , ( 𝐹 ‘ 𝑣 ) ) = seq 0 ( + , ( 𝐹 ‘ 𝑤 ) ) )
39	38	fveq1d	⊢ ( 𝑣 = 𝑤 → ( seq 0 ( + , ( 𝐹 ‘ 𝑣 ) ) ‘ 𝑘 ) = ( seq 0 ( + , ( 𝐹 ‘ 𝑤 ) ) ‘ 𝑘 ) )
40	27	adantr	⊢ ( ( ( ( 𝜑 ∧ seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ( ⇝𝑢 ‘ ℝ ) 𝑓 ) ∧ 𝑤 ∈ ℝ ) ∧ 𝑘 ∈ ℕ0 ) → 𝑤 ∈ ℝ )
41		fvexd	⊢ ( ( ( ( 𝜑 ∧ seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ( ⇝𝑢 ‘ ℝ ) 𝑓 ) ∧ 𝑤 ∈ ℝ ) ∧ 𝑘 ∈ ℕ0 ) → ( seq 0 ( + , ( 𝐹 ‘ 𝑤 ) ) ‘ 𝑘 ) ∈ V )
42	36 39 40 41	fvmptd3	⊢ ( ( ( ( 𝜑 ∧ seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ( ⇝𝑢 ‘ ℝ ) 𝑓 ) ∧ 𝑤 ∈ ℝ ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑣 ∈ ℝ ↦ ( seq 0 ( + , ( 𝐹 ‘ 𝑣 ) ) ‘ 𝑘 ) ) ‘ 𝑤 ) = ( seq 0 ( + , ( 𝐹 ‘ 𝑤 ) ) ‘ 𝑘 ) )
43	35 42	eqtrd	⊢ ( ( ( ( 𝜑 ∧ seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ( ⇝𝑢 ‘ ℝ ) 𝑓 ) ∧ 𝑤 ∈ ℝ ) ∧ 𝑘 ∈ ℕ0 ) → ( ( seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ‘ 𝑘 ) ‘ 𝑤 ) = ( seq 0 ( + , ( 𝐹 ‘ 𝑤 ) ) ‘ 𝑘 ) )
44		simplr	⊢ ( ( ( 𝜑 ∧ seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ( ⇝𝑢 ‘ ℝ ) 𝑓 ) ∧ 𝑤 ∈ ℝ ) → seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ( ⇝𝑢 ‘ ℝ ) 𝑓 )
45	15 16 26 27 29 43 44	ulmclm	⊢ ( ( ( 𝜑 ∧ seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ( ⇝𝑢 ‘ ℝ ) 𝑓 ) ∧ 𝑤 ∈ ℝ ) → seq 0 ( + , ( 𝐹 ‘ 𝑤 ) ) ⇝ ( 𝑓 ‘ 𝑤 ) )
46	15 16 17 24 45	isumclim	⊢ ( ( ( 𝜑 ∧ seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ( ⇝𝑢 ‘ ℝ ) 𝑓 ) ∧ 𝑤 ∈ ℝ ) → Σ 𝑖 ∈ ℕ0 ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑖 ) = ( 𝑓 ‘ 𝑤 ) )
47	46	eqcomd	⊢ ( ( ( 𝜑 ∧ seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ( ⇝𝑢 ‘ ℝ ) 𝑓 ) ∧ 𝑤 ∈ ℝ ) → ( 𝑓 ‘ 𝑤 ) = Σ 𝑖 ∈ ℕ0 ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑖 ) )
48	47	mpteq2dva	⊢ ( ( 𝜑 ∧ seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ( ⇝𝑢 ‘ ℝ ) 𝑓 ) → ( 𝑤 ∈ ℝ ↦ ( 𝑓 ‘ 𝑤 ) ) = ( 𝑤 ∈ ℝ ↦ Σ 𝑖 ∈ ℕ0 ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑖 ) ) )
49	3	a1i	⊢ ( ( 𝜑 ∧ seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ( ⇝𝑢 ‘ ℝ ) 𝑓 ) → 𝑊 = ( 𝑤 ∈ ℝ ↦ Σ 𝑖 ∈ ℕ0 ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑖 ) ) )
50	49	eqcomd	⊢ ( ( 𝜑 ∧ seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ( ⇝𝑢 ‘ ℝ ) 𝑓 ) → ( 𝑤 ∈ ℝ ↦ Σ 𝑖 ∈ ℕ0 ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑖 ) ) = 𝑊 )
51	14 48 50	3eqtrd	⊢ ( ( 𝜑 ∧ seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ( ⇝𝑢 ‘ ℝ ) 𝑓 ) → 𝑓 = 𝑊 )
52	11 51	breqtrd	⊢ ( ( 𝜑 ∧ seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ( ⇝𝑢 ‘ ℝ ) 𝑓 ) → seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ( ⇝𝑢 ‘ ℝ ) 𝑊 )
53	52	ex	⊢ ( 𝜑 → ( seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ( ⇝𝑢 ‘ ℝ ) 𝑓 → seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ( ⇝𝑢 ‘ ℝ ) 𝑊 ) )
54	53	exlimdv	⊢ ( 𝜑 → ( ∃ 𝑓 seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ( ⇝𝑢 ‘ ℝ ) 𝑓 → seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ( ⇝𝑢 ‘ ℝ ) 𝑊 ) )
55	10 54	mpd	⊢ ( 𝜑 → seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ( ⇝𝑢 ‘ ℝ ) 𝑊 )