Metamath Proof Explorer

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 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ( ⇝𝑢 ‘ ℝ ) 𝑊 )