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 ffvelrnda ( ( 𝜑𝑘𝑍 ) → ( 𝐹𝑘 ) ∈ ( ℂ ↑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 ffvelrnda ( ( 𝜑𝑧𝑋 ) → ( 𝐻𝑧 ) ∈ ℂ )
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 ffvelrnda ( ( ( ( 𝜑𝑧𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑛𝑍 ) → ( ( 𝑘𝑍 ↦ ( 𝑆 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 ffvelrnda ( ( ( ( 𝜑𝑧𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑛𝑍 ) → ( 𝐹𝑛 ) ∈ ( ℂ ↑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 𝐺 ) ( 𝐻𝑧 ) )