This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ulmdvlem3

Description: Lemma for ulmdv . (Contributed by Mario Carneiro, 8-May-2015) (Proof shortened by Mario Carneiro, 28-Dec-2016)

Ref Expression
Hypotheses ulmdv.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
ulmdv.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
ulmdv.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
ulmdv.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑋 ) )
ulmdv.g ⊢ ( 𝜑 → 𝐺 : 𝑋 ⟶ ℂ )
ulmdv.l ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ⇝ ( 𝐺 ‘ 𝑧 ) )
ulmdv.u ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) ( ⇝𝑢 ‘ 𝑋 ) 𝐻 )
Assertion ulmdvlem3 ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → 𝑧 ( 𝑆 D 𝐺 ) ( 𝐻 ‘ 𝑧 ) )

Proof

Step Hyp Ref Expression
1 ulmdv.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 ulmdv.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
3 ulmdv.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
4 ulmdv.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑋 ) )
5 ulmdv.g ⊢ ( 𝜑 → 𝐺 : 𝑋 ⟶ ℂ )
6 ulmdv.l ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ⇝ ( 𝐺 ‘ 𝑧 ) )
7 ulmdv.u ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) ( ⇝𝑢 ‘ 𝑋 ) 𝐻 )
8 biidd ⊢ ( 𝑘 = 𝑀 → ( 𝑋 ⊆ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) ‘ 𝑋 ) ↔ 𝑋 ⊆ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) ‘ 𝑋 ) ) )
9 1 2 3 4 5 6 7 ulmdvlem2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → dom ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) = 𝑋 )
10 recnprss ⊢ ( 𝑆 ∈ { ℝ , ℂ } → 𝑆 ⊆ ℂ )
11 2 10 syl ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
12 11 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝑆 ⊆ ℂ )
13 4 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ( ℂ ↑m 𝑋 ) )
14 elmapi ⊢ ( ( 𝐹 ‘ 𝑘 ) ∈ ( ℂ ↑m 𝑋 ) → ( 𝐹 ‘ 𝑘 ) : 𝑋 ⟶ ℂ )
15 13 14 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) : 𝑋 ⟶ ℂ )
16 dvbsss ⊢ dom ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ⊆ 𝑆
17 9 16 eqsstrrdi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝑋 ⊆ 𝑆 )
18 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) = ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 )
19 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
20 12 15 17 18 19 dvbssntr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → dom ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ⊆ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) ‘ 𝑋 ) )
21 9 20 eqsstrrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝑋 ⊆ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) ‘ 𝑋 ) )
22 21 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝑍 𝑋 ⊆ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) ‘ 𝑋 ) )
23 uzid ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
24 3 23 syl ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
25 24 1 eleqtrrdi ⊢ ( 𝜑 → 𝑀 ∈ 𝑍 )
26 8 22 25 rspcdva ⊢ ( 𝜑 → 𝑋 ⊆ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) ‘ 𝑋 ) )
27 26 sselda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → 𝑧 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) ‘ 𝑋 ) )
28 ulmcl ⊢ ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) ( ⇝𝑢 ‘ 𝑋 ) 𝐻 → 𝐻 : 𝑋 ⟶ ℂ )
29 7 28 syl ⊢ ( 𝜑 → 𝐻 : 𝑋 ⟶ ℂ )
30 29 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → ( 𝐻 ‘ 𝑧 ) ∈ ℂ )
31 breq2 ⊢ ( 𝑠 = ( ( 𝑟 / 2 ) / 2 ) → ( ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < 𝑠 ↔ ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ) )
32 31 2ralbidv ⊢ ( 𝑠 = ( ( 𝑟 / 2 ) / 2 ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < 𝑠 ↔ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ) )
33 32 rexralbidv ⊢ ( 𝑠 = ( ( 𝑟 / 2 ) / 2 ) → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < 𝑠 ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ) )
34 ulmrel ⊢ Rel ( ⇝𝑢 ‘ 𝑋 )
35 releldm ⊢ ( ( Rel ( ⇝𝑢 ‘ 𝑋 ) ∧ ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) ( ⇝𝑢 ‘ 𝑋 ) 𝐻 ) → ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) ∈ dom ( ⇝𝑢 ‘ 𝑋 ) )
36 34 7 35 sylancr ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) ∈ dom ( ⇝𝑢 ‘ 𝑋 ) )
37 ulmscl ⊢ ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) ( ⇝𝑢 ‘ 𝑋 ) 𝐻 → 𝑋 ∈ V )
38 7 37 syl ⊢ ( 𝜑 → 𝑋 ∈ V )
39 ovex ⊢ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ∈ V
40 39 rgenw ⊢ ∀ 𝑘 ∈ 𝑍 ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ∈ V
41 eqid ⊢ ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) )
42 41 fnmpt ⊢ ( ∀ 𝑘 ∈ 𝑍 ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ∈ V → ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) Fn 𝑍 )
43 40 42 mp1i ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) Fn 𝑍 )
44 ulmf2 ⊢ ( ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) Fn 𝑍 ∧ ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) ( ⇝𝑢 ‘ 𝑋 ) 𝐻 ) → ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) : 𝑍 ⟶ ( ℂ ↑m 𝑋 ) )
45 43 7 44 syl2anc ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) : 𝑍 ⟶ ( ℂ ↑m 𝑋 ) )
46 1 3 38 45 ulmcau2 ⊢ ( 𝜑 → ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) ∈ dom ( ⇝𝑢 ‘ 𝑋 ) ↔ ∀ 𝑠 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) ‘ 𝑛 ) ‘ 𝑥 ) − ( ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) < 𝑠 ) )
47 36 46 mpbid ⊢ ( 𝜑 → ∀ 𝑠 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) ‘ 𝑛 ) ‘ 𝑥 ) − ( ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) < 𝑠 )
48 1 uztrn2 ⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑛 ∈ 𝑍 )
49 48 ad2ant2lr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) ) → 𝑛 ∈ 𝑍 )
50 fveq2 ⊢ ( 𝑘 = 𝑛 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑛 ) )
51 50 oveq2d ⊢ ( 𝑘 = 𝑛 → ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) = ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) )
52 ovex ⊢ ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ∈ V
53 51 41 52 fvmpt ⊢ ( 𝑛 ∈ 𝑍 → ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) ‘ 𝑛 ) = ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) )
54 49 53 syl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) ) → ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) ‘ 𝑛 ) = ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) )
55 54 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) ) → ( ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) ‘ 𝑛 ) ‘ 𝑥 ) = ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) )
56 simprr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) ) → 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) )
57 1 uztrn2 ⊢ ( ( 𝑛 ∈ 𝑍 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑚 ∈ 𝑍 )
58 49 56 57 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) ) → 𝑚 ∈ 𝑍 )
59 fveq2 ⊢ ( 𝑘 = 𝑚 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑚 ) )
60 59 oveq2d ⊢ ( 𝑘 = 𝑚 → ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) = ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) )
61 ovex ⊢ ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ∈ V
62 60 41 61 fvmpt ⊢ ( 𝑚 ∈ 𝑍 → ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) ‘ 𝑚 ) = ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) )
63 58 62 syl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) ) → ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) ‘ 𝑚 ) = ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) )
64 63 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) ) → ( ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) ‘ 𝑚 ) ‘ 𝑥 ) = ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) )
65 55 64 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) ) → ( ( ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) ‘ 𝑛 ) ‘ 𝑥 ) − ( ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) = ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) )
66 65 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) ) → ( abs ‘ ( ( ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) ‘ 𝑛 ) ‘ 𝑥 ) − ( ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) = ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) )
67 66 breq1d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) ) → ( ( abs ‘ ( ( ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) ‘ 𝑛 ) ‘ 𝑥 ) − ( ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) < 𝑠 ↔ ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < 𝑠 ) )
68 67 ralbidv ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) ) → ( ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) ‘ 𝑛 ) ‘ 𝑥 ) − ( ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) < 𝑠 ↔ ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < 𝑠 ) )
69 68 2ralbidva ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) ‘ 𝑛 ) ‘ 𝑥 ) − ( ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) < 𝑠 ↔ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < 𝑠 ) )
70 69 rexbidva ⊢ ( 𝜑 → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) ‘ 𝑛 ) ‘ 𝑥 ) − ( ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) < 𝑠 ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < 𝑠 ) )
71 70 ralbidv ⊢ ( 𝜑 → ( ∀ 𝑠 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) ‘ 𝑛 ) ‘ 𝑥 ) − ( ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) ‘ 𝑚 ) ‘ 𝑥 ) ) ) < 𝑠 ↔ ∀ 𝑠 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < 𝑠 ) )
72 47 71 mpbid ⊢ ( 𝜑 → ∀ 𝑠 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < 𝑠 )
73 72 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) → ∀ 𝑠 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < 𝑠 )
74 rphalfcl ⊢ ( 𝑟 ∈ ℝ+ → ( 𝑟 / 2 ) ∈ ℝ+ )
75 74 adantl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) → ( 𝑟 / 2 ) ∈ ℝ+ )
76 rphalfcl ⊢ ( ( 𝑟 / 2 ) ∈ ℝ+ → ( ( 𝑟 / 2 ) / 2 ) ∈ ℝ+ )
77 75 76 syl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) → ( ( 𝑟 / 2 ) / 2 ) ∈ ℝ+ )
78 33 73 77 rspcdva ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) )
79 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) → 𝑀 ∈ ℤ )
80 51 fveq1d ⊢ ( 𝑘 = 𝑛 → ( ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ‘ 𝑧 ) = ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) )
81 eqid ⊢ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ‘ 𝑧 ) ) = ( 𝑘 ∈ 𝑍 ↦ ( ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ‘ 𝑧 ) )
82 fvex ⊢ ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ∈ V
83 80 81 82 fvmpt ⊢ ( 𝑛 ∈ 𝑍 → ( ( 𝑘 ∈ 𝑍 ↦ ( ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ‘ 𝑧 ) ) ‘ 𝑛 ) = ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) )
84 83 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ ( ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ‘ 𝑧 ) ) ‘ 𝑛 ) = ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) )
85 45 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) → ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) : 𝑍 ⟶ ( ℂ ↑m 𝑋 ) )
86 simplr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) → 𝑧 ∈ 𝑋 )
87 1 fvexi ⊢ 𝑍 ∈ V
88 87 mptex ⊢ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ‘ 𝑧 ) ) ∈ V
89 88 a1i ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) → ( 𝑘 ∈ 𝑍 ↦ ( ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ‘ 𝑧 ) ) ∈ V )
90 53 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) ‘ 𝑛 ) = ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) )
91 90 fveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑛 ∈ 𝑍 ) → ( ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) ‘ 𝑛 ) ‘ 𝑧 ) = ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) )
92 91 84 eqtr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑛 ∈ 𝑍 ) → ( ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) ‘ 𝑛 ) ‘ 𝑧 ) = ( ( 𝑘 ∈ 𝑍 ↦ ( ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ‘ 𝑧 ) ) ‘ 𝑛 ) )
93 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) → ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) ( ⇝𝑢 ‘ 𝑋 ) 𝐻 )
94 1 79 85 86 89 92 93 ulmclm ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) → ( 𝑘 ∈ 𝑍 ↦ ( ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ‘ 𝑧 ) ) ⇝ ( 𝐻 ‘ 𝑧 ) )
95 1 79 75 84 94 climi2 ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) − ( 𝐻 ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) )
96 1 rexanuz2 ⊢ ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ∧ ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) − ( 𝐻 ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) ↔ ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ∧ ∃ 𝑗 ∈ 𝑍 ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) − ( 𝐻 ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) )
97 1 r19.2uz ⊢ ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ∧ ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) − ( 𝐻 ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) → ∃ 𝑛 ∈ 𝑍 ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ∧ ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) − ( 𝐻 ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) )
98 96 97 sylbir ⊢ ( ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ∧ ∃ 𝑗 ∈ 𝑍 ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) − ( 𝐻 ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) → ∃ 𝑛 ∈ 𝑍 ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ∧ ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) − ( 𝐻 ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) )
99 fveq2 ⊢ ( 𝑦 = 𝑣 → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) = ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) )
100 99 oveq1d ⊢ ( 𝑦 = 𝑣 → ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) = ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) )
101 oveq1 ⊢ ( 𝑦 = 𝑣 → ( 𝑦 − 𝑧 ) = ( 𝑣 − 𝑧 ) )
102 100 101 oveq12d ⊢ ( 𝑦 = 𝑣 → ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑦 − 𝑧 ) ) = ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) )
103 eqid ⊢ ( 𝑦 ∈ ( 𝑋 ∖ { 𝑧 } ) ↦ ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑦 − 𝑧 ) ) ) = ( 𝑦 ∈ ( 𝑋 ∖ { 𝑧 } ) ↦ ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑦 − 𝑧 ) ) )
104 ovex ⊢ ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) ∈ V
105 102 103 104 fvmpt ⊢ ( 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) → ( ( 𝑦 ∈ ( 𝑋 ∖ { 𝑧 } ) ↦ ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑦 − 𝑧 ) ) ) ‘ 𝑣 ) = ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) )
106 105 fvoveq1d ⊢ ( 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) → ( abs ‘ ( ( ( 𝑦 ∈ ( 𝑋 ∖ { 𝑧 } ) ↦ ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑦 − 𝑧 ) ) ) ‘ 𝑣 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) = ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) )
107 id ⊢ ( 𝑠 = ( ( 𝑟 / 2 ) / 2 ) → 𝑠 = ( ( 𝑟 / 2 ) / 2 ) )
108 106 107 breqan12rd ⊢ ( ( 𝑠 = ( ( 𝑟 / 2 ) / 2 ) ∧ 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ) → ( ( abs ‘ ( ( ( 𝑦 ∈ ( 𝑋 ∖ { 𝑧 } ) ↦ ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑦 − 𝑧 ) ) ) ‘ 𝑣 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < 𝑠 ↔ ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ) )
109 108 imbi2d ⊢ ( ( 𝑠 = ( ( 𝑟 / 2 ) / 2 ) ∧ 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ) → ( ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑤 ) → ( abs ‘ ( ( ( 𝑦 ∈ ( 𝑋 ∖ { 𝑧 } ) ↦ ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑦 − 𝑧 ) ) ) ‘ 𝑣 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < 𝑠 ) ↔ ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑤 ) → ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ) ) )
110 109 ralbidva ⊢ ( 𝑠 = ( ( 𝑟 / 2 ) / 2 ) → ( ∀ 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑤 ) → ( abs ‘ ( ( ( 𝑦 ∈ ( 𝑋 ∖ { 𝑧 } ) ↦ ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑦 − 𝑧 ) ) ) ‘ 𝑣 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < 𝑠 ) ↔ ∀ 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑤 ) → ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ) ) )
111 110 rexbidv ⊢ ( 𝑠 = ( ( 𝑟 / 2 ) / 2 ) → ( ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑤 ) → ( abs ‘ ( ( ( 𝑦 ∈ ( 𝑋 ∖ { 𝑧 } ) ↦ ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑦 − 𝑧 ) ) ) ‘ 𝑣 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < 𝑠 ) ↔ ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑤 ) → ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ) ) )
112 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑛 ∈ 𝑍 ) → 𝑧 ∈ 𝑋 )
113 85 ffvelcdmda ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) ‘ 𝑛 ) ∈ ( ℂ ↑m 𝑋 ) )
114 90 113 eqeltrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑛 ∈ 𝑍 ) → ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ∈ ( ℂ ↑m 𝑋 ) )
115 elmapi ⊢ ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ∈ ( ℂ ↑m 𝑋 ) → ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) : 𝑋 ⟶ ℂ )
116 fdm ⊢ ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) : 𝑋 ⟶ ℂ → dom ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) = 𝑋 )
117 114 115 116 3syl ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑛 ∈ 𝑍 ) → dom ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) = 𝑋 )
118 112 117 eleqtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑛 ∈ 𝑍 ) → 𝑧 ∈ dom ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) )
119 2 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑛 ∈ 𝑍 ) → 𝑆 ∈ { ℝ , ℂ } )
120 dvfg ⊢ ( 𝑆 ∈ { ℝ , ℂ } → ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) : dom ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ⟶ ℂ )
121 ffun ⊢ ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) : dom ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ⟶ ℂ → Fun ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) )
122 funfvbrb ⊢ ( Fun ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) → ( 𝑧 ∈ dom ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ↔ 𝑧 ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) )
123 119 120 121 122 4syl ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑛 ∈ 𝑍 ) → ( 𝑧 ∈ dom ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ↔ 𝑧 ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) )
124 118 123 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑛 ∈ 𝑍 ) → 𝑧 ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) )
125 119 10 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑛 ∈ 𝑍 ) → 𝑆 ⊆ ℂ )
126 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) → 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑋 ) )
127 126 ffvelcdmda ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) ∈ ( ℂ ↑m 𝑋 ) )
128 elmapi ⊢ ( ( 𝐹 ‘ 𝑛 ) ∈ ( ℂ ↑m 𝑋 ) → ( 𝐹 ‘ 𝑛 ) : 𝑋 ⟶ ℂ )
129 127 128 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) : 𝑋 ⟶ ℂ )
130 biidd ⊢ ( 𝑘 = 𝑀 → ( 𝑋 ⊆ 𝑆 ↔ 𝑋 ⊆ 𝑆 ) )
131 17 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝑍 𝑋 ⊆ 𝑆 )
132 130 131 25 rspcdva ⊢ ( 𝜑 → 𝑋 ⊆ 𝑆 )
133 132 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑛 ∈ 𝑍 ) → 𝑋 ⊆ 𝑆 )
134 18 19 103 125 129 133 eldv ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑛 ∈ 𝑍 ) → ( 𝑧 ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ↔ ( 𝑧 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) ‘ 𝑋 ) ∧ ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ∈ ( ( 𝑦 ∈ ( 𝑋 ∖ { 𝑧 } ) ↦ ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑦 − 𝑧 ) ) ) limℂ 𝑧 ) ) ) )
135 124 134 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑛 ∈ 𝑍 ) → ( 𝑧 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) ‘ 𝑋 ) ∧ ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ∈ ( ( 𝑦 ∈ ( 𝑋 ∖ { 𝑧 } ) ↦ ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑦 − 𝑧 ) ) ) limℂ 𝑧 ) ) )
136 135 simprd ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ∈ ( ( 𝑦 ∈ ( 𝑋 ∖ { 𝑧 } ) ↦ ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑦 − 𝑧 ) ) ) limℂ 𝑧 ) )
137 132 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → 𝑋 ⊆ 𝑆 )
138 11 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → 𝑆 ⊆ ℂ )
139 137 138 sstrd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → 𝑋 ⊆ ℂ )
140 139 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑛 ∈ 𝑍 ) → 𝑋 ⊆ ℂ )
141 129 140 112 dvlem ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑦 ∈ ( 𝑋 ∖ { 𝑧 } ) ) → ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑦 − 𝑧 ) ) ∈ ℂ )
142 141 fmpttd ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑛 ∈ 𝑍 ) → ( 𝑦 ∈ ( 𝑋 ∖ { 𝑧 } ) ↦ ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑦 − 𝑧 ) ) ) : ( 𝑋 ∖ { 𝑧 } ) ⟶ ℂ )
143 140 ssdifssd ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑛 ∈ 𝑍 ) → ( 𝑋 ∖ { 𝑧 } ) ⊆ ℂ )
144 140 112 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑛 ∈ 𝑍 ) → 𝑧 ∈ ℂ )
145 142 143 144 ellimc3 ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑛 ∈ 𝑍 ) → ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ∈ ( ( 𝑦 ∈ ( 𝑋 ∖ { 𝑧 } ) ↦ ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑦 − 𝑧 ) ) ) limℂ 𝑧 ) ↔ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ∈ ℂ ∧ ∀ 𝑠 ∈ ℝ+ ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑤 ) → ( abs ‘ ( ( ( 𝑦 ∈ ( 𝑋 ∖ { 𝑧 } ) ↦ ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑦 − 𝑧 ) ) ) ‘ 𝑣 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < 𝑠 ) ) ) )
146 136 145 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑛 ∈ 𝑍 ) → ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ∈ ℂ ∧ ∀ 𝑠 ∈ ℝ+ ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑤 ) → ( abs ‘ ( ( ( 𝑦 ∈ ( 𝑋 ∖ { 𝑧 } ) ↦ ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑦 − 𝑧 ) ) ) ‘ 𝑣 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < 𝑠 ) ) )
147 146 simprd ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑛 ∈ 𝑍 ) → ∀ 𝑠 ∈ ℝ+ ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑤 ) → ( abs ‘ ( ( ( 𝑦 ∈ ( 𝑋 ∖ { 𝑧 } ) ↦ ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑦 − 𝑧 ) ) ) ‘ 𝑣 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < 𝑠 ) )
148 77 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝑟 / 2 ) / 2 ) ∈ ℝ+ )
149 111 147 148 rspcdva ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑛 ∈ 𝑍 ) → ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑤 ) → ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ) )
150 149 adantrr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ∧ ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) − ( 𝐻 ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) ) ) → ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑤 ) → ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ) )
151 anass ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ∧ ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) − ( 𝐻 ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) ) ) ∧ ( 𝑢 ∈ ℝ+ ∧ ( 𝑢 < 𝑤 ∧ ( 𝑧 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑢 ) ⊆ 𝑋 ) ) ) ∧ 𝑤 ∈ ℝ+ ) ↔ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ∧ ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) − ( 𝐻 ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) ) ) ∧ ( ( 𝑢 ∈ ℝ+ ∧ ( 𝑢 < 𝑤 ∧ ( 𝑧 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑢 ) ⊆ 𝑋 ) ) ∧ 𝑤 ∈ ℝ+ ) ) )
152 df-3an ⊢ ( ( 𝑛 ∈ 𝑍 ∧ ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ∧ ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) − ( 𝐻 ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) ∧ ( ( ( 𝑢 ∈ ℝ+ ∧ ( 𝑢 < 𝑤 ∧ ( 𝑧 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑢 ) ⊆ 𝑋 ) ) ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ∧ ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑤 ) → ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ) ∧ ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑢 ) ) ) ) ↔ ( ( 𝑛 ∈ 𝑍 ∧ ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ∧ ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) − ( 𝐻 ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) ) ∧ ( ( ( 𝑢 ∈ ℝ+ ∧ ( 𝑢 < 𝑤 ∧ ( 𝑧 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑢 ) ⊆ 𝑋 ) ) ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ∧ ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑤 ) → ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ) ∧ ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑢 ) ) ) ) )
153 anass ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ↔ ( 𝜑 ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ) )
154 6 ralrimiva ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝑋 ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ⇝ ( 𝐺 ‘ 𝑧 ) )
155 fveq2 ⊢ ( 𝑧 = 𝑠 → ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) = ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑠 ) )
156 155 mpteq2dv ⊢ ( 𝑧 = 𝑠 → ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) = ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑠 ) ) )
157 fveq2 ⊢ ( 𝑧 = 𝑠 → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑠 ) )
158 156 157 breq12d ⊢ ( 𝑧 = 𝑠 → ( ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ⇝ ( 𝐺 ‘ 𝑧 ) ↔ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑠 ) ) ⇝ ( 𝐺 ‘ 𝑠 ) ) )
159 158 rspccva ⊢ ( ( ∀ 𝑧 ∈ 𝑋 ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ⇝ ( 𝐺 ‘ 𝑧 ) ∧ 𝑠 ∈ 𝑋 ) → ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑠 ) ) ⇝ ( 𝐺 ‘ 𝑠 ) )
160 154 159 sylan ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) → ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑠 ) ) ⇝ ( 𝐺 ‘ 𝑠 ) )
161 simprll ⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ∧ ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) − ( 𝐻 ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) ∧ ( ( ( 𝑢 ∈ ℝ+ ∧ ( 𝑢 < 𝑤 ∧ ( 𝑧 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑢 ) ⊆ 𝑋 ) ) ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ∧ ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑤 ) → ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ) ∧ ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑢 ) ) ) ) ) ) → 𝑧 ∈ 𝑋 )
162 simprlr ⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ∧ ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) − ( 𝐻 ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) ∧ ( ( ( 𝑢 ∈ ℝ+ ∧ ( 𝑢 < 𝑤 ∧ ( 𝑧 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑢 ) ⊆ 𝑋 ) ) ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ∧ ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑤 ) → ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ) ∧ ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑢 ) ) ) ) ) ) → 𝑟 ∈ ℝ+ )
163 simprr3 ⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ∧ ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) − ( 𝐻 ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) ∧ ( ( ( 𝑢 ∈ ℝ+ ∧ ( 𝑢 < 𝑤 ∧ ( 𝑧 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑢 ) ⊆ 𝑋 ) ) ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ∧ ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑤 ) → ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ) ∧ ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑢 ) ) ) ) ) ) → ( ( ( 𝑢 ∈ ℝ+ ∧ ( 𝑢 < 𝑤 ∧ ( 𝑧 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑢 ) ⊆ 𝑋 ) ) ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ∧ ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑤 ) → ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ) ∧ ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑢 ) ) ) )
164 simplll ⊢ ( ( ( ( 𝑢 ∈ ℝ+ ∧ ( 𝑢 < 𝑤 ∧ ( 𝑧 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑢 ) ⊆ 𝑋 ) ) ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ∧ ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑤 ) → ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ) ∧ ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑢 ) ) ) → 𝑢 ∈ ℝ+ )
165 163 164 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ∧ ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) − ( 𝐻 ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) ∧ ( ( ( 𝑢 ∈ ℝ+ ∧ ( 𝑢 < 𝑤 ∧ ( 𝑧 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑢 ) ⊆ 𝑋 ) ) ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ∧ ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑤 ) → ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ) ∧ ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑢 ) ) ) ) ) ) → 𝑢 ∈ ℝ+ )
166 simplr ⊢ ( ( ( ( 𝑢 ∈ ℝ+ ∧ ( 𝑢 < 𝑤 ∧ ( 𝑧 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑢 ) ⊆ 𝑋 ) ) ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ∧ ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑤 ) → ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ) ∧ ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑢 ) ) ) → 𝑤 ∈ ℝ+ )
167 163 166 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ∧ ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) − ( 𝐻 ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) ∧ ( ( ( 𝑢 ∈ ℝ+ ∧ ( 𝑢 < 𝑤 ∧ ( 𝑧 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑢 ) ⊆ 𝑋 ) ) ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ∧ ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑤 ) → ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ) ∧ ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑢 ) ) ) ) ) ) → 𝑤 ∈ ℝ+ )
168 simpllr ⊢ ( ( ( ( 𝑢 ∈ ℝ+ ∧ ( 𝑢 < 𝑤 ∧ ( 𝑧 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑢 ) ⊆ 𝑋 ) ) ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ∧ ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑤 ) → ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ) ∧ ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑢 ) ) ) → ( 𝑢 < 𝑤 ∧ ( 𝑧 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑢 ) ⊆ 𝑋 ) )
169 163 168 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ∧ ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) − ( 𝐻 ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) ∧ ( ( ( 𝑢 ∈ ℝ+ ∧ ( 𝑢 < 𝑤 ∧ ( 𝑧 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑢 ) ⊆ 𝑋 ) ) ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ∧ ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑤 ) → ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ) ∧ ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑢 ) ) ) ) ) ) → ( 𝑢 < 𝑤 ∧ ( 𝑧 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑢 ) ⊆ 𝑋 ) )
170 169 simpld ⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ∧ ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) − ( 𝐻 ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) ∧ ( ( ( 𝑢 ∈ ℝ+ ∧ ( 𝑢 < 𝑤 ∧ ( 𝑧 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑢 ) ⊆ 𝑋 ) ) ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ∧ ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑤 ) → ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ) ∧ ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑢 ) ) ) ) ) ) → 𝑢 < 𝑤 )
171 169 simprd ⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ∧ ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) − ( 𝐻 ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) ∧ ( ( ( 𝑢 ∈ ℝ+ ∧ ( 𝑢 < 𝑤 ∧ ( 𝑧 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑢 ) ⊆ 𝑋 ) ) ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ∧ ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑤 ) → ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ) ∧ ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑢 ) ) ) ) ) ) → ( 𝑧 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑢 ) ⊆ 𝑋 )
172 simpr3 ⊢ ( ( ( ( 𝑢 ∈ ℝ+ ∧ ( 𝑢 < 𝑤 ∧ ( 𝑧 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑢 ) ⊆ 𝑋 ) ) ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ∧ ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑤 ) → ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ) ∧ ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑢 ) ) ) → ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑢 ) )
173 163 172 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ∧ ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) − ( 𝐻 ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) ∧ ( ( ( 𝑢 ∈ ℝ+ ∧ ( 𝑢 < 𝑤 ∧ ( 𝑧 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑢 ) ⊆ 𝑋 ) ) ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ∧ ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑤 ) → ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ) ∧ ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑢 ) ) ) ) ) ) → ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑢 ) )
174 173 simprd ⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ∧ ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) − ( 𝐻 ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) ∧ ( ( ( 𝑢 ∈ ℝ+ ∧ ( 𝑢 < 𝑤 ∧ ( 𝑧 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑢 ) ⊆ 𝑋 ) ) ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ∧ ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑤 ) → ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ) ∧ ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑢 ) ) ) ) ) ) → ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑢 )
175 simprr1 ⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ∧ ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) − ( 𝐻 ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) ∧ ( ( ( 𝑢 ∈ ℝ+ ∧ ( 𝑢 < 𝑤 ∧ ( 𝑧 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑢 ) ⊆ 𝑋 ) ) ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ∧ ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑤 ) → ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ) ∧ ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑢 ) ) ) ) ) ) → 𝑛 ∈ 𝑍 )
176 simprr2 ⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ∧ ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) − ( 𝐻 ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) ∧ ( ( ( 𝑢 ∈ ℝ+ ∧ ( 𝑢 < 𝑤 ∧ ( 𝑧 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑢 ) ⊆ 𝑋 ) ) ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ∧ ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑤 ) → ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ) ∧ ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑢 ) ) ) ) ) ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ∧ ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) − ( 𝐻 ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) )
177 176 simpld ⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ∧ ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) − ( 𝐻 ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) ∧ ( ( ( 𝑢 ∈ ℝ+ ∧ ( 𝑢 < 𝑤 ∧ ( 𝑧 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑢 ) ⊆ 𝑋 ) ) ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ∧ ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑤 ) → ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ) ∧ ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑢 ) ) ) ) ) ) → ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) )
178 176 simprd ⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ∧ ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) − ( 𝐻 ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) ∧ ( ( ( 𝑢 ∈ ℝ+ ∧ ( 𝑢 < 𝑤 ∧ ( 𝑧 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑢 ) ⊆ 𝑋 ) ) ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ∧ ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑤 ) → ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ) ∧ ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑢 ) ) ) ) ) ) → ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) − ( 𝐻 ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) )
179 simpr1 ⊢ ( ( ( ( 𝑢 ∈ ℝ+ ∧ ( 𝑢 < 𝑤 ∧ ( 𝑧 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑢 ) ⊆ 𝑋 ) ) ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ∧ ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑤 ) → ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ) ∧ ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑢 ) ) ) → 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) )
180 163 179 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ∧ ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) − ( 𝐻 ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) ∧ ( ( ( 𝑢 ∈ ℝ+ ∧ ( 𝑢 < 𝑤 ∧ ( 𝑧 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑢 ) ⊆ 𝑋 ) ) ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ∧ ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑤 ) → ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ) ∧ ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑢 ) ) ) ) ) ) → 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) )
181 180 eldifad ⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ∧ ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) − ( 𝐻 ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) ∧ ( ( ( 𝑢 ∈ ℝ+ ∧ ( 𝑢 < 𝑤 ∧ ( 𝑧 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑢 ) ⊆ 𝑋 ) ) ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ∧ ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑤 ) → ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ) ∧ ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑢 ) ) ) ) ) ) → 𝑣 ∈ 𝑋 )
182 173 simpld ⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ∧ ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) − ( 𝐻 ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) ∧ ( ( ( 𝑢 ∈ ℝ+ ∧ ( 𝑢 < 𝑤 ∧ ( 𝑧 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑢 ) ⊆ 𝑋 ) ) ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ∧ ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑤 ) → ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ) ∧ ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑢 ) ) ) ) ) ) → 𝑣 ≠ 𝑧 )
183 simpr2 ⊢ ( ( ( ( 𝑢 ∈ ℝ+ ∧ ( 𝑢 < 𝑤 ∧ ( 𝑧 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑢 ) ⊆ 𝑋 ) ) ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ∧ ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑤 ) → ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ) ∧ ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑢 ) ) ) → ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑤 ) → ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ) )
184 163 183 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ∧ ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) − ( 𝐻 ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) ∧ ( ( ( 𝑢 ∈ ℝ+ ∧ ( 𝑢 < 𝑤 ∧ ( 𝑧 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑢 ) ⊆ 𝑋 ) ) ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ∧ ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑤 ) → ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ) ∧ ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑢 ) ) ) ) ) ) → ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑤 ) → ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ) )
185 182 184 mpand ⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ∧ ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) − ( 𝐻 ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) ∧ ( ( ( 𝑢 ∈ ℝ+ ∧ ( 𝑢 < 𝑤 ∧ ( 𝑧 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑢 ) ⊆ 𝑋 ) ) ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ∧ ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑤 ) → ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ) ∧ ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑢 ) ) ) ) ) ) → ( ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑤 → ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ) )
186 1 2 3 4 5 160 7 161 162 165 167 170 171 174 175 177 178 181 182 185 ulmdvlem1 ⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ∧ ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) − ( 𝐻 ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) ∧ ( ( ( 𝑢 ∈ ℝ+ ∧ ( 𝑢 < 𝑤 ∧ ( 𝑧 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑢 ) ⊆ 𝑋 ) ) ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ∧ ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑤 ) → ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ) ∧ ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑢 ) ) ) ) ) ) → ( abs ‘ ( ( ( ( 𝐺 ‘ 𝑣 ) − ( 𝐺 ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( 𝐻 ‘ 𝑧 ) ) ) < 𝑟 )
187 186 anassrs ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ) ∧ ( 𝑛 ∈ 𝑍 ∧ ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ∧ ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) − ( 𝐻 ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) ∧ ( ( ( 𝑢 ∈ ℝ+ ∧ ( 𝑢 < 𝑤 ∧ ( 𝑧 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑢 ) ⊆ 𝑋 ) ) ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ∧ ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑤 ) → ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ) ∧ ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑢 ) ) ) ) ) → ( abs ‘ ( ( ( ( 𝐺 ‘ 𝑣 ) − ( 𝐺 ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( 𝐻 ‘ 𝑧 ) ) ) < 𝑟 )
188 153 187 sylanb ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ∧ ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) − ( 𝐻 ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) ∧ ( ( ( 𝑢 ∈ ℝ+ ∧ ( 𝑢 < 𝑤 ∧ ( 𝑧 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑢 ) ⊆ 𝑋 ) ) ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ∧ ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑤 ) → ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ) ∧ ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑢 ) ) ) ) ) → ( abs ‘ ( ( ( ( 𝐺 ‘ 𝑣 ) − ( 𝐺 ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( 𝐻 ‘ 𝑧 ) ) ) < 𝑟 )
189 152 188 sylan2br ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑛 ∈ 𝑍 ∧ ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ∧ ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) − ( 𝐻 ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) ) ∧ ( ( ( 𝑢 ∈ ℝ+ ∧ ( 𝑢 < 𝑤 ∧ ( 𝑧 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑢 ) ⊆ 𝑋 ) ) ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ∧ ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑤 ) → ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ) ∧ ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑢 ) ) ) ) ) → ( abs ‘ ( ( ( ( 𝐺 ‘ 𝑣 ) − ( 𝐺 ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( 𝐻 ‘ 𝑧 ) ) ) < 𝑟 )
190 189 anassrs ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ∧ ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) − ( 𝐻 ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) ) ) ∧ ( ( ( 𝑢 ∈ ℝ+ ∧ ( 𝑢 < 𝑤 ∧ ( 𝑧 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑢 ) ⊆ 𝑋 ) ) ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ∧ ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑤 ) → ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ) ∧ ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑢 ) ) ) ) → ( abs ‘ ( ( ( ( 𝐺 ‘ 𝑣 ) − ( 𝐺 ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( 𝐻 ‘ 𝑧 ) ) ) < 𝑟 )
191 190 anassrs ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ∧ ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) − ( 𝐻 ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) ) ) ∧ ( ( 𝑢 ∈ ℝ+ ∧ ( 𝑢 < 𝑤 ∧ ( 𝑧 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑢 ) ⊆ 𝑋 ) ) ∧ 𝑤 ∈ ℝ+ ) ) ∧ ( 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ∧ ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑤 ) → ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ) ∧ ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑢 ) ) ) → ( abs ‘ ( ( ( ( 𝐺 ‘ 𝑣 ) − ( 𝐺 ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( 𝐻 ‘ 𝑧 ) ) ) < 𝑟 )
192 151 191 sylanb ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ∧ ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) − ( 𝐻 ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) ) ) ∧ ( 𝑢 ∈ ℝ+ ∧ ( 𝑢 < 𝑤 ∧ ( 𝑧 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑢 ) ⊆ 𝑋 ) ) ) ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ∧ ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑤 ) → ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ) ∧ ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑢 ) ) ) → ( abs ‘ ( ( ( ( 𝐺 ‘ 𝑣 ) − ( 𝐺 ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( 𝐻 ‘ 𝑧 ) ) ) < 𝑟 )
193 192 3exp2 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ∧ ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) − ( 𝐻 ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) ) ) ∧ ( 𝑢 ∈ ℝ+ ∧ ( 𝑢 < 𝑤 ∧ ( 𝑧 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑢 ) ⊆ 𝑋 ) ) ) ∧ 𝑤 ∈ ℝ+ ) → ( 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) → ( ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑤 ) → ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ) → ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑢 ) → ( abs ‘ ( ( ( ( 𝐺 ‘ 𝑣 ) − ( 𝐺 ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( 𝐻 ‘ 𝑧 ) ) ) < 𝑟 ) ) ) )
194 193 imp ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ∧ ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) − ( 𝐻 ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) ) ) ∧ ( 𝑢 ∈ ℝ+ ∧ ( 𝑢 < 𝑤 ∧ ( 𝑧 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑢 ) ⊆ 𝑋 ) ) ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ) → ( ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑤 ) → ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ) → ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑢 ) → ( abs ‘ ( ( ( ( 𝐺 ‘ 𝑣 ) − ( 𝐺 ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( 𝐻 ‘ 𝑧 ) ) ) < 𝑟 ) ) )
195 fveq2 ⊢ ( 𝑦 = 𝑣 → ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑣 ) )
196 195 oveq1d ⊢ ( 𝑦 = 𝑣 → ( ( 𝐺 ‘ 𝑦 ) − ( 𝐺 ‘ 𝑧 ) ) = ( ( 𝐺 ‘ 𝑣 ) − ( 𝐺 ‘ 𝑧 ) ) )
197 196 101 oveq12d ⊢ ( 𝑦 = 𝑣 → ( ( ( 𝐺 ‘ 𝑦 ) − ( 𝐺 ‘ 𝑧 ) ) / ( 𝑦 − 𝑧 ) ) = ( ( ( 𝐺 ‘ 𝑣 ) − ( 𝐺 ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) )
198 eqid ⊢ ( 𝑦 ∈ ( 𝑋 ∖ { 𝑧 } ) ↦ ( ( ( 𝐺 ‘ 𝑦 ) − ( 𝐺 ‘ 𝑧 ) ) / ( 𝑦 − 𝑧 ) ) ) = ( 𝑦 ∈ ( 𝑋 ∖ { 𝑧 } ) ↦ ( ( ( 𝐺 ‘ 𝑦 ) − ( 𝐺 ‘ 𝑧 ) ) / ( 𝑦 − 𝑧 ) ) )
199 ovex ⊢ ( ( ( 𝐺 ‘ 𝑣 ) − ( 𝐺 ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) ∈ V
200 197 198 199 fvmpt ⊢ ( 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) → ( ( 𝑦 ∈ ( 𝑋 ∖ { 𝑧 } ) ↦ ( ( ( 𝐺 ‘ 𝑦 ) − ( 𝐺 ‘ 𝑧 ) ) / ( 𝑦 − 𝑧 ) ) ) ‘ 𝑣 ) = ( ( ( 𝐺 ‘ 𝑣 ) − ( 𝐺 ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) )
201 200 fvoveq1d ⊢ ( 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) → ( abs ‘ ( ( ( 𝑦 ∈ ( 𝑋 ∖ { 𝑧 } ) ↦ ( ( ( 𝐺 ‘ 𝑦 ) − ( 𝐺 ‘ 𝑧 ) ) / ( 𝑦 − 𝑧 ) ) ) ‘ 𝑣 ) − ( 𝐻 ‘ 𝑧 ) ) ) = ( abs ‘ ( ( ( ( 𝐺 ‘ 𝑣 ) − ( 𝐺 ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( 𝐻 ‘ 𝑧 ) ) ) )
202 201 breq1d ⊢ ( 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) → ( ( abs ‘ ( ( ( 𝑦 ∈ ( 𝑋 ∖ { 𝑧 } ) ↦ ( ( ( 𝐺 ‘ 𝑦 ) − ( 𝐺 ‘ 𝑧 ) ) / ( 𝑦 − 𝑧 ) ) ) ‘ 𝑣 ) − ( 𝐻 ‘ 𝑧 ) ) ) < 𝑟 ↔ ( abs ‘ ( ( ( ( 𝐺 ‘ 𝑣 ) − ( 𝐺 ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( 𝐻 ‘ 𝑧 ) ) ) < 𝑟 ) )
203 202 imbi2d ⊢ ( 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) → ( ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑢 ) → ( abs ‘ ( ( ( 𝑦 ∈ ( 𝑋 ∖ { 𝑧 } ) ↦ ( ( ( 𝐺 ‘ 𝑦 ) − ( 𝐺 ‘ 𝑧 ) ) / ( 𝑦 − 𝑧 ) ) ) ‘ 𝑣 ) − ( 𝐻 ‘ 𝑧 ) ) ) < 𝑟 ) ↔ ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑢 ) → ( abs ‘ ( ( ( ( 𝐺 ‘ 𝑣 ) − ( 𝐺 ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( 𝐻 ‘ 𝑧 ) ) ) < 𝑟 ) ) )
204 203 adantl ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ∧ ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) − ( 𝐻 ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) ) ) ∧ ( 𝑢 ∈ ℝ+ ∧ ( 𝑢 < 𝑤 ∧ ( 𝑧 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑢 ) ⊆ 𝑋 ) ) ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ) → ( ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑢 ) → ( abs ‘ ( ( ( 𝑦 ∈ ( 𝑋 ∖ { 𝑧 } ) ↦ ( ( ( 𝐺 ‘ 𝑦 ) − ( 𝐺 ‘ 𝑧 ) ) / ( 𝑦 − 𝑧 ) ) ) ‘ 𝑣 ) − ( 𝐻 ‘ 𝑧 ) ) ) < 𝑟 ) ↔ ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑢 ) → ( abs ‘ ( ( ( ( 𝐺 ‘ 𝑣 ) − ( 𝐺 ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( 𝐻 ‘ 𝑧 ) ) ) < 𝑟 ) ) )
205 194 204 sylibrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ∧ ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) − ( 𝐻 ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) ) ) ∧ ( 𝑢 ∈ ℝ+ ∧ ( 𝑢 < 𝑤 ∧ ( 𝑧 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑢 ) ⊆ 𝑋 ) ) ) ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ) → ( ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑤 ) → ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ) → ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑢 ) → ( abs ‘ ( ( ( 𝑦 ∈ ( 𝑋 ∖ { 𝑧 } ) ↦ ( ( ( 𝐺 ‘ 𝑦 ) − ( 𝐺 ‘ 𝑧 ) ) / ( 𝑦 − 𝑧 ) ) ) ‘ 𝑣 ) − ( 𝐻 ‘ 𝑧 ) ) ) < 𝑟 ) ) )
206 205 ralimdva ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ∧ ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) − ( 𝐻 ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) ) ) ∧ ( 𝑢 ∈ ℝ+ ∧ ( 𝑢 < 𝑤 ∧ ( 𝑧 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑢 ) ⊆ 𝑋 ) ) ) ∧ 𝑤 ∈ ℝ+ ) → ( ∀ 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑤 ) → ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ) → ∀ 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑢 ) → ( abs ‘ ( ( ( 𝑦 ∈ ( 𝑋 ∖ { 𝑧 } ) ↦ ( ( ( 𝐺 ‘ 𝑦 ) − ( 𝐺 ‘ 𝑧 ) ) / ( 𝑦 − 𝑧 ) ) ) ‘ 𝑣 ) − ( 𝐻 ‘ 𝑧 ) ) ) < 𝑟 ) ) )
207 206 impr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ∧ ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) − ( 𝐻 ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) ) ) ∧ ( 𝑢 ∈ ℝ+ ∧ ( 𝑢 < 𝑤 ∧ ( 𝑧 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑢 ) ⊆ 𝑋 ) ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ ∀ 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑤 ) → ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ) ) ) → ∀ 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑢 ) → ( abs ‘ ( ( ( 𝑦 ∈ ( 𝑋 ∖ { 𝑧 } ) ↦ ( ( ( 𝐺 ‘ 𝑦 ) − ( 𝐺 ‘ 𝑧 ) ) / ( 𝑦 − 𝑧 ) ) ) ‘ 𝑣 ) − ( 𝐻 ‘ 𝑧 ) ) ) < 𝑟 ) )
208 207 an32s ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ∧ ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) − ( 𝐻 ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ ∀ 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑤 ) → ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ) ) ) ∧ ( 𝑢 ∈ ℝ+ ∧ ( 𝑢 < 𝑤 ∧ ( 𝑧 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑢 ) ⊆ 𝑋 ) ) ) → ∀ 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑢 ) → ( abs ‘ ( ( ( 𝑦 ∈ ( 𝑋 ∖ { 𝑧 } ) ↦ ( ( ( 𝐺 ‘ 𝑦 ) − ( 𝐺 ‘ 𝑧 ) ) / ( 𝑦 − 𝑧 ) ) ) ‘ 𝑣 ) − ( 𝐻 ‘ 𝑧 ) ) ) < 𝑟 ) )
209 cnxmet ⊢ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ )
210 xmetres2 ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝑆 ⊆ ℂ ) → ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ∈ ( ∞Met ‘ 𝑆 ) )
211 209 138 210 sylancr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ∈ ( ∞Met ‘ 𝑆 ) )
212 211 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ∧ ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) − ( 𝐻 ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ ∀ 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑤 ) → ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ) ) ) → ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ∈ ( ∞Met ‘ 𝑆 ) )
213 19 cnfldtop ⊢ ( TopOpen ‘ ℂfld ) ∈ Top
214 resttop ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ Top ∧ 𝑆 ∈ { ℝ , ℂ } ) → ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ∈ Top )
215 213 2 214 sylancr ⊢ ( 𝜑 → ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ∈ Top )
216 19 cnfldtopon ⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
217 resttopon ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ 𝑆 ⊆ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) )
218 216 11 217 sylancr ⊢ ( 𝜑 → ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) )
219 toponuni ⊢ ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) → 𝑆 = ∪ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
220 218 219 syl ⊢ ( 𝜑 → 𝑆 = ∪ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
221 132 220 sseqtrd ⊢ ( 𝜑 → 𝑋 ⊆ ∪ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
222 eqid ⊢ ∪ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) = ∪ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 )
223 222 ntrss2 ⊢ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ∈ Top ∧ 𝑋 ⊆ ∪ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) → ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) ‘ 𝑋 ) ⊆ 𝑋 )
224 215 221 223 syl2anc ⊢ ( 𝜑 → ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) ‘ 𝑋 ) ⊆ 𝑋 )
225 224 26 eqssd ⊢ ( 𝜑 → ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) ‘ 𝑋 ) = 𝑋 )
226 222 isopn3 ⊢ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ∈ Top ∧ 𝑋 ⊆ ∪ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) → ( 𝑋 ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ↔ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) ‘ 𝑋 ) = 𝑋 ) )
227 215 221 226 syl2anc ⊢ ( 𝜑 → ( 𝑋 ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ↔ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) ‘ 𝑋 ) = 𝑋 ) )
228 225 227 mpbird ⊢ ( 𝜑 → 𝑋 ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
229 eqid ⊢ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) = ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) )
230 19 cnfldtopn ⊢ ( TopOpen ‘ ℂfld ) = ( MetOpen ‘ ( abs ∘ − ) )
231 eqid ⊢ ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) )
232 229 230 231 metrest ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝑆 ⊆ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) )
233 209 11 232 sylancr ⊢ ( 𝜑 → ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) )
234 228 233 eleqtrd ⊢ ( 𝜑 → 𝑋 ∈ ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) )
235 234 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → 𝑋 ∈ ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) )
236 235 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ∧ ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) − ( 𝐻 ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ ∀ 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑤 ) → ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ) ) ) → 𝑋 ∈ ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) )
237 86 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ∧ ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) − ( 𝐻 ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ ∀ 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑤 ) → ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ) ) ) → 𝑧 ∈ 𝑋 )
238 simprl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ∧ ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) − ( 𝐻 ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ ∀ 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑤 ) → ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ) ) ) → 𝑤 ∈ ℝ+ )
239 231 mopni3 ⊢ ( ( ( ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ∈ ( ∞Met ‘ 𝑆 ) ∧ 𝑋 ∈ ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑤 ∈ ℝ+ ) → ∃ 𝑢 ∈ ℝ+ ( 𝑢 < 𝑤 ∧ ( 𝑧 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑢 ) ⊆ 𝑋 ) )
240 212 236 237 238 239 syl31anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ∧ ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) − ( 𝐻 ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ ∀ 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑤 ) → ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ) ) ) → ∃ 𝑢 ∈ ℝ+ ( 𝑢 < 𝑤 ∧ ( 𝑧 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑢 ) ⊆ 𝑋 ) )
241 208 240 reximddv ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ∧ ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) − ( 𝐻 ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) ) ) ∧ ( 𝑤 ∈ ℝ+ ∧ ∀ 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑤 ) → ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑣 ) − ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) / ( 𝑣 − 𝑧 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ) ) ) → ∃ 𝑢 ∈ ℝ+ ∀ 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑢 ) → ( abs ‘ ( ( ( 𝑦 ∈ ( 𝑋 ∖ { 𝑧 } ) ↦ ( ( ( 𝐺 ‘ 𝑦 ) − ( 𝐺 ‘ 𝑧 ) ) / ( 𝑦 − 𝑧 ) ) ) ‘ 𝑣 ) − ( 𝐻 ‘ 𝑧 ) ) ) < 𝑟 ) )
242 150 241 rexlimddv ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ∧ ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) − ( 𝐻 ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) ) ) → ∃ 𝑢 ∈ ℝ+ ∀ 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑢 ) → ( abs ‘ ( ( ( 𝑦 ∈ ( 𝑋 ∖ { 𝑧 } ) ↦ ( ( ( 𝐺 ‘ 𝑦 ) − ( 𝐺 ‘ 𝑧 ) ) / ( 𝑦 − 𝑧 ) ) ) ‘ 𝑣 ) − ( 𝐻 ‘ 𝑧 ) ) ) < 𝑟 ) )
243 242 rexlimdvaa ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) → ( ∃ 𝑛 ∈ 𝑍 ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ∧ ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) − ( 𝐻 ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) → ∃ 𝑢 ∈ ℝ+ ∀ 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑢 ) → ( abs ‘ ( ( ( 𝑦 ∈ ( 𝑋 ∖ { 𝑧 } ) ↦ ( ( ( 𝐺 ‘ 𝑦 ) − ( 𝐺 ‘ 𝑧 ) ) / ( 𝑦 − 𝑧 ) ) ) ‘ 𝑣 ) − ( 𝐻 ‘ 𝑧 ) ) ) < 𝑟 ) ) )
244 98 243 syl5 ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) → ( ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑟 / 2 ) / 2 ) ∧ ∃ 𝑗 ∈ 𝑍 ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑧 ) − ( 𝐻 ‘ 𝑧 ) ) ) < ( 𝑟 / 2 ) ) → ∃ 𝑢 ∈ ℝ+ ∀ 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑢 ) → ( abs ‘ ( ( ( 𝑦 ∈ ( 𝑋 ∖ { 𝑧 } ) ↦ ( ( ( 𝐺 ‘ 𝑦 ) − ( 𝐺 ‘ 𝑧 ) ) / ( 𝑦 − 𝑧 ) ) ) ‘ 𝑣 ) − ( 𝐻 ‘ 𝑧 ) ) ) < 𝑟 ) ) )
245 78 95 244 mp2and ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) → ∃ 𝑢 ∈ ℝ+ ∀ 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑢 ) → ( abs ‘ ( ( ( 𝑦 ∈ ( 𝑋 ∖ { 𝑧 } ) ↦ ( ( ( 𝐺 ‘ 𝑦 ) − ( 𝐺 ‘ 𝑧 ) ) / ( 𝑦 − 𝑧 ) ) ) ‘ 𝑣 ) − ( 𝐻 ‘ 𝑧 ) ) ) < 𝑟 ) )
246 245 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → ∀ 𝑟 ∈ ℝ+ ∃ 𝑢 ∈ ℝ+ ∀ 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑢 ) → ( abs ‘ ( ( ( 𝑦 ∈ ( 𝑋 ∖ { 𝑧 } ) ↦ ( ( ( 𝐺 ‘ 𝑦 ) − ( 𝐺 ‘ 𝑧 ) ) / ( 𝑦 − 𝑧 ) ) ) ‘ 𝑣 ) − ( 𝐻 ‘ 𝑧 ) ) ) < 𝑟 ) )
247 5 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → 𝐺 : 𝑋 ⟶ ℂ )
248 simpr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → 𝑧 ∈ 𝑋 )
249 247 139 248 dvlem ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑦 ∈ ( 𝑋 ∖ { 𝑧 } ) ) → ( ( ( 𝐺 ‘ 𝑦 ) − ( 𝐺 ‘ 𝑧 ) ) / ( 𝑦 − 𝑧 ) ) ∈ ℂ )
250 249 fmpttd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → ( 𝑦 ∈ ( 𝑋 ∖ { 𝑧 } ) ↦ ( ( ( 𝐺 ‘ 𝑦 ) − ( 𝐺 ‘ 𝑧 ) ) / ( 𝑦 − 𝑧 ) ) ) : ( 𝑋 ∖ { 𝑧 } ) ⟶ ℂ )
251 139 ssdifssd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → ( 𝑋 ∖ { 𝑧 } ) ⊆ ℂ )
252 139 248 sseldd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → 𝑧 ∈ ℂ )
253 250 251 252 ellimc3 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → ( ( 𝐻 ‘ 𝑧 ) ∈ ( ( 𝑦 ∈ ( 𝑋 ∖ { 𝑧 } ) ↦ ( ( ( 𝐺 ‘ 𝑦 ) − ( 𝐺 ‘ 𝑧 ) ) / ( 𝑦 − 𝑧 ) ) ) limℂ 𝑧 ) ↔ ( ( 𝐻 ‘ 𝑧 ) ∈ ℂ ∧ ∀ 𝑟 ∈ ℝ+ ∃ 𝑢 ∈ ℝ+ ∀ 𝑣 ∈ ( 𝑋 ∖ { 𝑧 } ) ( ( 𝑣 ≠ 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑧 ) ) < 𝑢 ) → ( abs ‘ ( ( ( 𝑦 ∈ ( 𝑋 ∖ { 𝑧 } ) ↦ ( ( ( 𝐺 ‘ 𝑦 ) − ( 𝐺 ‘ 𝑧 ) ) / ( 𝑦 − 𝑧 ) ) ) ‘ 𝑣 ) − ( 𝐻 ‘ 𝑧 ) ) ) < 𝑟 ) ) ) )
254 30 246 253 mpbir2and ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → ( 𝐻 ‘ 𝑧 ) ∈ ( ( 𝑦 ∈ ( 𝑋 ∖ { 𝑧 } ) ↦ ( ( ( 𝐺 ‘ 𝑦 ) − ( 𝐺 ‘ 𝑧 ) ) / ( 𝑦 − 𝑧 ) ) ) limℂ 𝑧 ) )
255 18 19 198 138 247 137 eldv ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → ( 𝑧 ( 𝑆 D 𝐺 ) ( 𝐻 ‘ 𝑧 ) ↔ ( 𝑧 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) ‘ 𝑋 ) ∧ ( 𝐻 ‘ 𝑧 ) ∈ ( ( 𝑦 ∈ ( 𝑋 ∖ { 𝑧 } ) ↦ ( ( ( 𝐺 ‘ 𝑦 ) − ( 𝐺 ‘ 𝑧 ) ) / ( 𝑦 − 𝑧 ) ) ) limℂ 𝑧 ) ) ) )
256 27 254 255 mpbir2and ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → 𝑧 ( 𝑆 D 𝐺 ) ( 𝐻 ‘ 𝑧 ) )