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

Metamath Proof Explorer

Theorem ulmdvlem1

Description: Lemma for ulmdv . (Contributed by Mario Carneiro, 3-Mar-2015)

Ref Expression
Hypotheses ulmdv.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
ulmdv.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
ulmdv.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
ulmdv.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑋 ) )
ulmdv.g ⊢ ( 𝜑 → 𝐺 : 𝑋 ⟶ ℂ )
ulmdv.l ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ⇝ ( 𝐺 ‘ 𝑧 ) )
ulmdv.u ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) ( ⇝𝑢 ‘ 𝑋 ) 𝐻 )
ulmdvlem1.c ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐶 ∈ 𝑋 )
ulmdvlem1.r ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑅 ∈ ℝ+ )
ulmdvlem1.u ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑈 ∈ ℝ+ )
ulmdvlem1.v ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑊 ∈ ℝ+ )
ulmdvlem1.l ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑈 < 𝑊 )
ulmdvlem1.b ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝐶 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑈 ) ⊆ 𝑋 )
ulmdvlem1.a ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( abs ‘ ( 𝑌 − 𝐶 ) ) < 𝑈 )
ulmdvlem1.n ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑁 ∈ 𝑍 )
ulmdvlem1.1 ⊢ ( ( 𝜑 ∧ 𝜓 ) → ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑅 / 2 ) / 2 ) )
ulmdvlem1.2 ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝐶 ) − ( 𝐻 ‘ 𝐶 ) ) ) < ( 𝑅 / 2 ) )
ulmdvlem1.y ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑌 ∈ 𝑋 )
ulmdvlem1.3 ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑌 ≠ 𝐶 )
ulmdvlem1.4 ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( abs ‘ ( 𝑌 − 𝐶 ) ) < 𝑊 → ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) / ( 𝑌 − 𝐶 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝐶 ) ) ) < ( ( 𝑅 / 2 ) / 2 ) ) )
Assertion ulmdvlem1 ( ( 𝜑 ∧ 𝜓 ) → ( abs ‘ ( ( ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑌 − 𝐶 ) ) − ( 𝐻 ‘ 𝐶 ) ) ) < 𝑅 )

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 ulmdvlem1.c ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐶 ∈ 𝑋 )
9 ulmdvlem1.r ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑅 ∈ ℝ+ )
10 ulmdvlem1.u ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑈 ∈ ℝ+ )
11 ulmdvlem1.v ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑊 ∈ ℝ+ )
12 ulmdvlem1.l ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑈 < 𝑊 )
13 ulmdvlem1.b ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝐶 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑈 ) ⊆ 𝑋 )
14 ulmdvlem1.a ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( abs ‘ ( 𝑌 − 𝐶 ) ) < 𝑈 )
15 ulmdvlem1.n ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑁 ∈ 𝑍 )
16 ulmdvlem1.1 ⊢ ( ( 𝜑 ∧ 𝜓 ) → ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑅 / 2 ) / 2 ) )
17 ulmdvlem1.2 ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝐶 ) − ( 𝐻 ‘ 𝐶 ) ) ) < ( 𝑅 / 2 ) )
18 ulmdvlem1.y ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑌 ∈ 𝑋 )
19 ulmdvlem1.3 ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑌 ≠ 𝐶 )
20 ulmdvlem1.4 ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( abs ‘ ( 𝑌 − 𝐶 ) ) < 𝑊 → ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) / ( 𝑌 − 𝐶 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝐶 ) ) ) < ( ( 𝑅 / 2 ) / 2 ) ) )
21 5 adantr ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐺 : 𝑋 ⟶ ℂ )
22 21 18 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝐺 ‘ 𝑌 ) ∈ ℂ )
23 21 8 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝐺 ‘ 𝐶 ) ∈ ℂ )
24 22 23 subcld ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝐶 ) ) ∈ ℂ )
25 fveq2 ⊢ ( 𝑘 = 𝑁 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑁 ) )
26 25 oveq2d ⊢ ( 𝑘 = 𝑁 → ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) = ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) )
27 eqid ⊢ ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) )
28 ovex ⊢ ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ∈ V
29 26 27 28 fvmpt ⊢ ( 𝑁 ∈ 𝑍 → ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) ‘ 𝑁 ) = ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) )
30 15 29 syl ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) ‘ 𝑁 ) = ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) )
31 ovex ⊢ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ∈ V
32 31 rgenw ⊢ ∀ 𝑘 ∈ 𝑍 ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ∈ V
33 27 fnmpt ⊢ ( ∀ 𝑘 ∈ 𝑍 ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ∈ V → ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) Fn 𝑍 )
34 32 33 mp1i ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) Fn 𝑍 )
35 ulmf2 ⊢ ( ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) Fn 𝑍 ∧ ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) ( ⇝𝑢 ‘ 𝑋 ) 𝐻 ) → ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) : 𝑍 ⟶ ( ℂ ↑m 𝑋 ) )
36 34 7 35 syl2anc ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) : 𝑍 ⟶ ( ℂ ↑m 𝑋 ) )
37 36 adantr ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) : 𝑍 ⟶ ( ℂ ↑m 𝑋 ) )
38 37 15 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) ‘ 𝑁 ) ∈ ( ℂ ↑m 𝑋 ) )
39 30 38 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ∈ ( ℂ ↑m 𝑋 ) )
40 elmapi ⊢ ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ∈ ( ℂ ↑m 𝑋 ) → ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) : 𝑋 ⟶ ℂ )
41 39 40 syl ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) : 𝑋 ⟶ ℂ )
42 41 fdmd ⊢ ( ( 𝜑 ∧ 𝜓 ) → dom ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) = 𝑋 )
43 dvbsss ⊢ dom ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ⊆ 𝑆
44 42 43 eqsstrrdi ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑋 ⊆ 𝑆 )
45 recnprss ⊢ ( 𝑆 ∈ { ℝ , ℂ } → 𝑆 ⊆ ℂ )
46 2 45 syl ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
47 46 adantr ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑆 ⊆ ℂ )
48 44 47 sstrd ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑋 ⊆ ℂ )
49 48 18 sseldd ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑌 ∈ ℂ )
50 48 8 sseldd ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐶 ∈ ℂ )
51 49 50 subcld ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑌 − 𝐶 ) ∈ ℂ )
52 49 50 19 subne0d ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑌 − 𝐶 ) ≠ 0 )
53 24 51 52 divcld ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑌 − 𝐶 ) ) ∈ ℂ )
54 ulmcl ⊢ ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) ( ⇝𝑢 ‘ 𝑋 ) 𝐻 → 𝐻 : 𝑋 ⟶ ℂ )
55 7 54 syl ⊢ ( 𝜑 → 𝐻 : 𝑋 ⟶ ℂ )
56 55 adantr ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐻 : 𝑋 ⟶ ℂ )
57 56 8 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝐻 ‘ 𝐶 ) ∈ ℂ )
58 41 8 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝐶 ) ∈ ℂ )
59 9 rpred ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑅 ∈ ℝ )
60 53 58 subcld ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑌 − 𝐶 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝐶 ) ) ∈ ℂ )
61 60 abscld ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( abs ‘ ( ( ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑌 − 𝐶 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝐶 ) ) ) ∈ ℝ )
62 4 adantr ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑋 ) )
63 62 15 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝐹 ‘ 𝑁 ) ∈ ( ℂ ↑m 𝑋 ) )
64 elmapi ⊢ ( ( 𝐹 ‘ 𝑁 ) ∈ ( ℂ ↑m 𝑋 ) → ( 𝐹 ‘ 𝑁 ) : 𝑋 ⟶ ℂ )
65 63 64 syl ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝐹 ‘ 𝑁 ) : 𝑋 ⟶ ℂ )
66 65 18 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ∈ ℂ )
67 65 8 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ∈ ℂ )
68 66 67 subcld ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ∈ ℂ )
69 68 51 52 divcld ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) / ( 𝑌 − 𝐶 ) ) ∈ ℂ )
70 53 69 subcld ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑌 − 𝐶 ) ) − ( ( ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) / ( 𝑌 − 𝐶 ) ) ) ∈ ℂ )
71 70 abscld ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( abs ‘ ( ( ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑌 − 𝐶 ) ) − ( ( ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) / ( 𝑌 − 𝐶 ) ) ) ) ∈ ℝ )
72 69 58 subcld ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( ( ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) / ( 𝑌 − 𝐶 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝐶 ) ) ∈ ℂ )
73 72 abscld ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) / ( 𝑌 − 𝐶 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝐶 ) ) ) ∈ ℝ )
74 71 73 readdcld ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( abs ‘ ( ( ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑌 − 𝐶 ) ) − ( ( ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) / ( 𝑌 − 𝐶 ) ) ) ) + ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) / ( 𝑌 − 𝐶 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝐶 ) ) ) ) ∈ ℝ )
75 59 rehalfcld ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑅 / 2 ) ∈ ℝ )
76 53 58 69 abs3difd ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( abs ‘ ( ( ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑌 − 𝐶 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝐶 ) ) ) ≤ ( ( abs ‘ ( ( ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑌 − 𝐶 ) ) − ( ( ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) / ( 𝑌 − 𝐶 ) ) ) ) + ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) / ( 𝑌 − 𝐶 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝐶 ) ) ) ) )
77 75 rehalfcld ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑅 / 2 ) / 2 ) ∈ ℝ )
78 22 66 23 67 sub4d ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( ( 𝐺 ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) − ( ( 𝐺 ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) = ( ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝐶 ) ) − ( ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) )
79 78 oveq1d ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( ( ( 𝐺 ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) − ( ( 𝐺 ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) / ( 𝑌 − 𝐶 ) ) = ( ( ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝐶 ) ) − ( ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) / ( 𝑌 − 𝐶 ) ) )
80 24 68 51 52 divsubdird ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝐶 ) ) − ( ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) / ( 𝑌 − 𝐶 ) ) = ( ( ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑌 − 𝐶 ) ) − ( ( ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) / ( 𝑌 − 𝐶 ) ) ) )
81 79 80 eqtrd ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( ( ( 𝐺 ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) − ( ( 𝐺 ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) / ( 𝑌 − 𝐶 ) ) = ( ( ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑌 − 𝐶 ) ) − ( ( ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) / ( 𝑌 − 𝐶 ) ) ) )
82 81 fveq2d ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( abs ‘ ( ( ( ( 𝐺 ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) − ( ( 𝐺 ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) / ( 𝑌 − 𝐶 ) ) ) = ( abs ‘ ( ( ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑌 − 𝐶 ) ) − ( ( ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) / ( 𝑌 − 𝐶 ) ) ) ) )
83 22 66 subcld ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝐺 ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) ∈ ℂ )
84 23 67 subcld ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝐺 ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ∈ ℂ )
85 83 84 subcld ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( ( 𝐺 ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) − ( ( 𝐺 ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) ∈ ℂ )
86 85 51 52 absdivd ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( abs ‘ ( ( ( ( 𝐺 ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) − ( ( 𝐺 ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) / ( 𝑌 − 𝐶 ) ) ) = ( ( abs ‘ ( ( ( 𝐺 ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) − ( ( 𝐺 ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) ) / ( abs ‘ ( 𝑌 − 𝐶 ) ) ) )
87 82 86 eqtr3d ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( abs ‘ ( ( ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑌 − 𝐶 ) ) − ( ( ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) / ( 𝑌 − 𝐶 ) ) ) ) = ( ( abs ‘ ( ( ( 𝐺 ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) − ( ( 𝐺 ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) ) / ( abs ‘ ( 𝑌 − 𝐶 ) ) ) )
88 eqid ⊢ ( ℤ≥ ‘ 𝑁 ) = ( ℤ≥ ‘ 𝑁 )
89 15 1 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
90 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ℤ )
91 89 90 syl ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑁 ∈ ℤ )
92 3 adantr ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑀 ∈ ℤ )
93 fveq2 ⊢ ( 𝑧 = 𝑌 → ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) = ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑌 ) )
94 93 mpteq2dv ⊢ ( 𝑧 = 𝑌 → ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) = ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑌 ) ) )
95 fveq2 ⊢ ( 𝑧 = 𝑌 → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑌 ) )
96 94 95 breq12d ⊢ ( 𝑧 = 𝑌 → ( ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ⇝ ( 𝐺 ‘ 𝑧 ) ↔ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑌 ) ) ⇝ ( 𝐺 ‘ 𝑌 ) ) )
97 6 ralrimiva ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝑋 ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ⇝ ( 𝐺 ‘ 𝑧 ) )
98 97 adantr ⊢ ( ( 𝜑 ∧ 𝜓 ) → ∀ 𝑧 ∈ 𝑋 ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ⇝ ( 𝐺 ‘ 𝑧 ) )
99 96 98 18 rspcdva ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑌 ) ) ⇝ ( 𝐺 ‘ 𝑌 ) )
100 1 fvexi ⊢ 𝑍 ∈ V
101 100 mptex ⊢ ( 𝑘 ∈ 𝑍 ↦ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) ) ∈ V
102 101 a1i ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑘 ∈ 𝑍 ↦ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) ) ∈ V )
103 fveq2 ⊢ ( 𝑘 = 𝑛 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑛 ) )
104 103 fveq1d ⊢ ( 𝑘 = 𝑛 → ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑌 ) = ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑌 ) )
105 eqid ⊢ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑌 ) ) = ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑌 ) )
106 fvex ⊢ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑌 ) ∈ V
107 104 105 106 fvmpt ⊢ ( 𝑛 ∈ 𝑍 → ( ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑌 ) ) ‘ 𝑛 ) = ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑌 ) )
108 107 adantl ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑌 ) ) ‘ 𝑛 ) = ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑌 ) )
109 62 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) ∈ ( ℂ ↑m 𝑋 ) )
110 elmapi ⊢ ( ( 𝐹 ‘ 𝑛 ) ∈ ( ℂ ↑m 𝑋 ) → ( 𝐹 ‘ 𝑛 ) : 𝑋 ⟶ ℂ )
111 109 110 syl ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) : 𝑋 ⟶ ℂ )
112 18 adantr ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ 𝑍 ) → 𝑌 ∈ 𝑋 )
113 111 112 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑌 ) ∈ ℂ )
114 108 113 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑌 ) ) ‘ 𝑛 ) ∈ ℂ )
115 104 oveq1d ⊢ ( 𝑘 = 𝑛 → ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) = ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) )
116 eqid ⊢ ( 𝑘 ∈ 𝑍 ↦ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) ) = ( 𝑘 ∈ 𝑍 ↦ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) )
117 ovex ⊢ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) ∈ V
118 115 116 117 fvmpt ⊢ ( 𝑛 ∈ 𝑍 → ( ( 𝑘 ∈ 𝑍 ↦ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) ) ‘ 𝑛 ) = ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) )
119 118 adantl ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) ) ‘ 𝑛 ) = ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) )
120 108 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ 𝑍 ) → ( ( ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑌 ) ) ‘ 𝑛 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) = ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) )
121 119 120 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) ) ‘ 𝑛 ) = ( ( ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑌 ) ) ‘ 𝑛 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) )
122 1 92 99 66 102 114 121 climsubc1 ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑘 ∈ 𝑍 ↦ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) ) ⇝ ( ( 𝐺 ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) )
123 100 mptex ⊢ ( 𝑘 ∈ 𝑍 ↦ ( ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) − ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) ) ∈ V
124 123 a1i ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑘 ∈ 𝑍 ↦ ( ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) − ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) ) ∈ V )
125 fveq2 ⊢ ( 𝑧 = 𝐶 → ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) = ( ( 𝐹 ‘ 𝑘 ) ‘ 𝐶 ) )
126 125 mpteq2dv ⊢ ( 𝑧 = 𝐶 → ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) = ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝐶 ) ) )
127 fveq2 ⊢ ( 𝑧 = 𝐶 → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) )
128 126 127 breq12d ⊢ ( 𝑧 = 𝐶 → ( ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ⇝ ( 𝐺 ‘ 𝑧 ) ↔ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝐶 ) ) ⇝ ( 𝐺 ‘ 𝐶 ) ) )
129 128 98 8 rspcdva ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝐶 ) ) ⇝ ( 𝐺 ‘ 𝐶 ) )
130 100 mptex ⊢ ( 𝑘 ∈ 𝑍 ↦ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) ∈ V
131 130 a1i ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑘 ∈ 𝑍 ↦ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) ∈ V )
132 103 fveq1d ⊢ ( 𝑘 = 𝑛 → ( ( 𝐹 ‘ 𝑘 ) ‘ 𝐶 ) = ( ( 𝐹 ‘ 𝑛 ) ‘ 𝐶 ) )
133 eqid ⊢ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝐶 ) ) = ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝐶 ) )
134 fvex ⊢ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝐶 ) ∈ V
135 132 133 134 fvmpt ⊢ ( 𝑛 ∈ 𝑍 → ( ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝐶 ) ) ‘ 𝑛 ) = ( ( 𝐹 ‘ 𝑛 ) ‘ 𝐶 ) )
136 135 adantl ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝐶 ) ) ‘ 𝑛 ) = ( ( 𝐹 ‘ 𝑛 ) ‘ 𝐶 ) )
137 8 adantr ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ 𝑍 ) → 𝐶 ∈ 𝑋 )
138 111 137 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝐶 ) ∈ ℂ )
139 136 138 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝐶 ) ) ‘ 𝑛 ) ∈ ℂ )
140 132 oveq1d ⊢ ( 𝑘 = 𝑛 → ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) = ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) )
141 eqid ⊢ ( 𝑘 ∈ 𝑍 ↦ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) = ( 𝑘 ∈ 𝑍 ↦ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) )
142 ovex ⊢ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ∈ V
143 140 141 142 fvmpt ⊢ ( 𝑛 ∈ 𝑍 → ( ( 𝑘 ∈ 𝑍 ↦ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) ‘ 𝑛 ) = ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) )
144 143 adantl ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) ‘ 𝑛 ) = ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) )
145 136 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ 𝑍 ) → ( ( ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝐶 ) ) ‘ 𝑛 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) = ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) )
146 144 145 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) ‘ 𝑛 ) = ( ( ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝐶 ) ) ‘ 𝑛 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) )
147 1 92 129 67 131 139 146 climsubc1 ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑘 ∈ 𝑍 ↦ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) ⇝ ( ( 𝐺 ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) )
148 66 adantr ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ∈ ℂ )
149 113 148 subcld ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ 𝑍 ) → ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) ∈ ℂ )
150 119 149 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) ) ‘ 𝑛 ) ∈ ℂ )
151 67 adantr ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ∈ ℂ )
152 138 151 subcld ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ 𝑍 ) → ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ∈ ℂ )
153 144 152 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) ‘ 𝑛 ) ∈ ℂ )
154 115 140 oveq12d ⊢ ( 𝑘 = 𝑛 → ( ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) − ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) = ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) − ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) )
155 eqid ⊢ ( 𝑘 ∈ 𝑍 ↦ ( ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) − ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) ) = ( 𝑘 ∈ 𝑍 ↦ ( ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) − ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) )
156 ovex ⊢ ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) − ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) ∈ V
157 154 155 156 fvmpt ⊢ ( 𝑛 ∈ 𝑍 → ( ( 𝑘 ∈ 𝑍 ↦ ( ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) − ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) ) ‘ 𝑛 ) = ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) − ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) )
158 157 adantl ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ ( ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) − ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) ) ‘ 𝑛 ) = ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) − ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) )
159 119 144 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ 𝑍 ) → ( ( ( 𝑘 ∈ 𝑍 ↦ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) ) ‘ 𝑛 ) − ( ( 𝑘 ∈ 𝑍 ↦ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) ‘ 𝑛 ) ) = ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) − ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) )
160 158 159 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ ( ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) − ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) ) ‘ 𝑛 ) = ( ( ( 𝑘 ∈ 𝑍 ↦ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) ) ‘ 𝑛 ) − ( ( 𝑘 ∈ 𝑍 ↦ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) ‘ 𝑛 ) ) )
161 1 92 122 124 147 150 153 160 climsub ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑘 ∈ 𝑍 ↦ ( ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) − ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) ) ⇝ ( ( ( 𝐺 ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) − ( ( 𝐺 ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) )
162 100 mptex ⊢ ( 𝑘 ∈ 𝑍 ↦ ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) − ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) ) ) ∈ V
163 162 a1i ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑘 ∈ 𝑍 ↦ ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) − ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) ) ) ∈ V )
164 149 152 subcld ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ 𝑍 ) → ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) − ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) ∈ ℂ )
165 158 164 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ ( ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) − ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) ) ‘ 𝑛 ) ∈ ℂ )
166 154 fveq2d ⊢ ( 𝑘 = 𝑛 → ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) − ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) ) = ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) − ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) ) )
167 eqid ⊢ ( 𝑘 ∈ 𝑍 ↦ ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) − ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) ) ) = ( 𝑘 ∈ 𝑍 ↦ ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) − ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) ) )
168 fvex ⊢ ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) − ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) ) ∈ V
169 166 167 168 fvmpt ⊢ ( 𝑛 ∈ 𝑍 → ( ( 𝑘 ∈ 𝑍 ↦ ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) − ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) ) ) ‘ 𝑛 ) = ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) − ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) ) )
170 169 adantl ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) − ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) ) ) ‘ 𝑛 ) = ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) − ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) ) )
171 158 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ 𝑍 ) → ( abs ‘ ( ( 𝑘 ∈ 𝑍 ↦ ( ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) − ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) ) ‘ 𝑛 ) ) = ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) − ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) ) )
172 170 171 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) − ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) ) ) ‘ 𝑛 ) = ( abs ‘ ( ( 𝑘 ∈ 𝑍 ↦ ( ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) − ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) ) ‘ 𝑛 ) ) )
173 1 161 163 92 165 172 climabs ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑘 ∈ 𝑍 ↦ ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) − ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) ) ) ⇝ ( abs ‘ ( ( ( 𝐺 ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) − ( ( 𝐺 ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) ) )
174 51 abscld ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( abs ‘ ( 𝑌 − 𝐶 ) ) ∈ ℝ )
175 77 174 remulcld ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( ( 𝑅 / 2 ) / 2 ) · ( abs ‘ ( 𝑌 − 𝐶 ) ) ) ∈ ℝ )
176 175 recnd ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( ( 𝑅 / 2 ) / 2 ) · ( abs ‘ ( 𝑌 − 𝐶 ) ) ) ∈ ℂ )
177 1 eqimss2i ⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ 𝑍
178 177 100 climconst2 ⊢ ( ( ( ( ( 𝑅 / 2 ) / 2 ) · ( abs ‘ ( 𝑌 − 𝐶 ) ) ) ∈ ℂ ∧ 𝑀 ∈ ℤ ) → ( 𝑍 × { ( ( ( 𝑅 / 2 ) / 2 ) · ( abs ‘ ( 𝑌 − 𝐶 ) ) ) } ) ⇝ ( ( ( 𝑅 / 2 ) / 2 ) · ( abs ‘ ( 𝑌 − 𝐶 ) ) ) )
179 176 92 178 syl2anc ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑍 × { ( ( ( 𝑅 / 2 ) / 2 ) · ( abs ‘ ( 𝑌 − 𝐶 ) ) ) } ) ⇝ ( ( ( 𝑅 / 2 ) / 2 ) · ( abs ‘ ( 𝑌 − 𝐶 ) ) ) )
180 1 uztrn2 ⊢ ( ( 𝑁 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑛 ∈ 𝑍 )
181 15 180 sylan ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑛 ∈ 𝑍 )
182 181 169 syl ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝑘 ∈ 𝑍 ↦ ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) − ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) ) ) ‘ 𝑛 ) = ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) − ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) ) )
183 164 abscld ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ 𝑍 ) → ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) − ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) ) ∈ ℝ )
184 181 183 syldan ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) − ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) ) ∈ ℝ )
185 182 184 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝑘 ∈ 𝑍 ↦ ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) − ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) ) ) ‘ 𝑛 ) ∈ ℝ )
186 ovex ⊢ ( ( ( 𝑅 / 2 ) / 2 ) · ( abs ‘ ( 𝑌 − 𝐶 ) ) ) ∈ V
187 186 fvconst2 ⊢ ( 𝑛 ∈ 𝑍 → ( ( 𝑍 × { ( ( ( 𝑅 / 2 ) / 2 ) · ( abs ‘ ( 𝑌 − 𝐶 ) ) ) } ) ‘ 𝑛 ) = ( ( ( 𝑅 / 2 ) / 2 ) · ( abs ‘ ( 𝑌 − 𝐶 ) ) ) )
188 181 187 syl ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝑍 × { ( ( ( 𝑅 / 2 ) / 2 ) · ( abs ‘ ( 𝑌 − 𝐶 ) ) ) } ) ‘ 𝑛 ) = ( ( ( 𝑅 / 2 ) / 2 ) · ( abs ‘ ( 𝑌 − 𝐶 ) ) ) )
189 175 adantr ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( ( 𝑅 / 2 ) / 2 ) · ( abs ‘ ( 𝑌 − 𝐶 ) ) ) ∈ ℝ )
190 188 189 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝑍 × { ( ( ( 𝑅 / 2 ) / 2 ) · ( abs ‘ ( 𝑌 − 𝐶 ) ) ) } ) ‘ 𝑛 ) ∈ ℝ )
191 181 111 syldan ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝐹 ‘ 𝑛 ) : 𝑋 ⟶ ℂ )
192 191 ffnd ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝐹 ‘ 𝑛 ) Fn 𝑋 )
193 65 adantr ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝐹 ‘ 𝑁 ) : 𝑋 ⟶ ℂ )
194 193 ffnd ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝐹 ‘ 𝑁 ) Fn 𝑋 )
195 ulmscl ⊢ ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) ( ⇝𝑢 ‘ 𝑋 ) 𝐻 → 𝑋 ∈ V )
196 7 195 syl ⊢ ( 𝜑 → 𝑋 ∈ V )
197 196 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑋 ∈ V )
198 18 adantr ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑌 ∈ 𝑋 )
199 fnfvof ⊢ ( ( ( ( 𝐹 ‘ 𝑛 ) Fn 𝑋 ∧ ( 𝐹 ‘ 𝑁 ) Fn 𝑋 ) ∧ ( 𝑋 ∈ V ∧ 𝑌 ∈ 𝑋 ) ) → ( ( ( 𝐹 ‘ 𝑛 ) ∘f − ( 𝐹 ‘ 𝑁 ) ) ‘ 𝑌 ) = ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) )
200 192 194 197 198 199 syl22anc ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( ( 𝐹 ‘ 𝑛 ) ∘f − ( 𝐹 ‘ 𝑁 ) ) ‘ 𝑌 ) = ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) )
201 8 adantr ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝐶 ∈ 𝑋 )
202 fnfvof ⊢ ( ( ( ( 𝐹 ‘ 𝑛 ) Fn 𝑋 ∧ ( 𝐹 ‘ 𝑁 ) Fn 𝑋 ) ∧ ( 𝑋 ∈ V ∧ 𝐶 ∈ 𝑋 ) ) → ( ( ( 𝐹 ‘ 𝑛 ) ∘f − ( 𝐹 ‘ 𝑁 ) ) ‘ 𝐶 ) = ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) )
203 192 194 197 201 202 syl22anc ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( ( 𝐹 ‘ 𝑛 ) ∘f − ( 𝐹 ‘ 𝑁 ) ) ‘ 𝐶 ) = ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) )
204 200 203 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( ( ( 𝐹 ‘ 𝑛 ) ∘f − ( 𝐹 ‘ 𝑁 ) ) ‘ 𝑌 ) − ( ( ( 𝐹 ‘ 𝑛 ) ∘f − ( 𝐹 ‘ 𝑁 ) ) ‘ 𝐶 ) ) = ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) − ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) )
205 204 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑛 ) ∘f − ( 𝐹 ‘ 𝑁 ) ) ‘ 𝑌 ) − ( ( ( 𝐹 ‘ 𝑛 ) ∘f − ( 𝐹 ‘ 𝑁 ) ) ‘ 𝐶 ) ) ) = ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) − ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) ) )
206 44 18 sseldd ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑌 ∈ 𝑆 )
207 44 8 sseldd ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐶 ∈ 𝑆 )
208 206 207 ovresd ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑌 ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) 𝐶 ) = ( 𝑌 ( abs ∘ − ) 𝐶 ) )
209 eqid ⊢ ( abs ∘ − ) = ( abs ∘ − )
210 209 cnmetdval ⊢ ( ( 𝑌 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝑌 ( abs ∘ − ) 𝐶 ) = ( abs ‘ ( 𝑌 − 𝐶 ) ) )
211 49 50 210 syl2anc ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑌 ( abs ∘ − ) 𝐶 ) = ( abs ‘ ( 𝑌 − 𝐶 ) ) )
212 208 211 eqtrd ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑌 ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) 𝐶 ) = ( abs ‘ ( 𝑌 − 𝐶 ) ) )
213 212 14 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑌 ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) 𝐶 ) < 𝑈 )
214 cnxmet ⊢ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ )
215 xmetres2 ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝑆 ⊆ ℂ ) → ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ∈ ( ∞Met ‘ 𝑆 ) )
216 214 47 215 sylancr ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ∈ ( ∞Met ‘ 𝑆 ) )
217 10 rpxrd ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑈 ∈ ℝ* )
218 elbl3 ⊢ ( ( ( ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ∈ ( ∞Met ‘ 𝑆 ) ∧ 𝑈 ∈ ℝ* ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ) → ( 𝑌 ∈ ( 𝐶 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑈 ) ↔ ( 𝑌 ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) 𝐶 ) < 𝑈 ) )
219 216 217 207 206 218 syl22anc ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑌 ∈ ( 𝐶 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑈 ) ↔ ( 𝑌 ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) 𝐶 ) < 𝑈 ) )
220 213 219 mpbird ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑌 ∈ ( 𝐶 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑈 ) )
221 220 adantr ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑌 ∈ ( 𝐶 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑈 ) )
222 blcntr ⊢ ( ( ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ∈ ( ∞Met ‘ 𝑆 ) ∧ 𝐶 ∈ 𝑆 ∧ 𝑈 ∈ ℝ+ ) → 𝐶 ∈ ( 𝐶 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑈 ) )
223 216 207 10 222 syl3anc ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐶 ∈ ( 𝐶 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑈 ) )
224 223 adantr ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝐶 ∈ ( 𝐶 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑈 ) )
225 221 224 jca ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑌 ∈ ( 𝐶 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑈 ) ∧ 𝐶 ∈ ( 𝐶 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑈 ) ) )
226 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑆 ∈ { ℝ , ℂ } )
227 eqid ⊢ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) = ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) )
228 44 adantr ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑋 ⊆ 𝑆 )
229 fvexd ⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ∈ V )
230 fvexd ⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑦 ) ∈ V )
231 191 feqmptd ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝐹 ‘ 𝑛 ) = ( 𝑦 ∈ 𝑋 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) )
232 193 feqmptd ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝐹 ‘ 𝑁 ) = ( 𝑦 ∈ 𝑋 ↦ ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑦 ) ) )
233 197 229 230 231 232 offval2 ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝐹 ‘ 𝑛 ) ∘f − ( 𝐹 ‘ 𝑁 ) ) = ( 𝑦 ∈ 𝑋 ↦ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑦 ) ) ) )
234 191 ffvelcdmda ⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ∈ ℂ )
235 193 ffvelcdmda ⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑦 ) ∈ ℂ )
236 234 235 subcld ⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑦 ∈ 𝑋 ) → ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑦 ) ) ∈ ℂ )
237 233 236 fmpt3d ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝐹 ‘ 𝑛 ) ∘f − ( 𝐹 ‘ 𝑁 ) ) : 𝑋 ⟶ ℂ )
238 207 adantr ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝐶 ∈ 𝑆 )
239 217 adantr ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑈 ∈ ℝ* )
240 eqid ⊢ ( 𝐶 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑈 ) = ( 𝐶 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑈 )
241 13 adantr ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝐶 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑈 ) ⊆ 𝑋 )
242 233 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑆 D ( ( 𝐹 ‘ 𝑛 ) ∘f − ( 𝐹 ‘ 𝑁 ) ) ) = ( 𝑆 D ( 𝑦 ∈ 𝑋 ↦ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑦 ) ) ) ) )
243 fvexd ⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑦 ) ∈ V )
244 231 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) = ( 𝑆 D ( 𝑦 ∈ 𝑋 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ) )
245 103 oveq2d ⊢ ( 𝑘 = 𝑛 → ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) = ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) )
246 ovex ⊢ ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ∈ V
247 245 27 246 fvmpt ⊢ ( 𝑛 ∈ 𝑍 → ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) ‘ 𝑛 ) = ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) )
248 181 247 syl ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) ‘ 𝑛 ) = ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) )
249 36 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) : 𝑍 ⟶ ( ℂ ↑m 𝑋 ) )
250 249 181 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) ‘ 𝑛 ) ∈ ( ℂ ↑m 𝑋 ) )
251 248 250 eqeltrrd ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ∈ ( ℂ ↑m 𝑋 ) )
252 elmapi ⊢ ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ∈ ( ℂ ↑m 𝑋 ) → ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) : 𝑋 ⟶ ℂ )
253 251 252 syl ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) : 𝑋 ⟶ ℂ )
254 253 feqmptd ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) = ( 𝑦 ∈ 𝑋 ↦ ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑦 ) ) )
255 244 254 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑆 D ( 𝑦 ∈ 𝑋 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) ) = ( 𝑦 ∈ 𝑋 ↦ ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑦 ) ) )
256 fvexd ⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝑦 ) ∈ V )
257 232 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) = ( 𝑆 D ( 𝑦 ∈ 𝑋 ↦ ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑦 ) ) ) )
258 41 adantr ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) : 𝑋 ⟶ ℂ )
259 258 feqmptd ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) = ( 𝑦 ∈ 𝑋 ↦ ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝑦 ) ) )
260 257 259 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑆 D ( 𝑦 ∈ 𝑋 ↦ ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑦 ) ) ) = ( 𝑦 ∈ 𝑋 ↦ ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝑦 ) ) )
261 226 234 243 255 235 256 260 dvmptsub ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑆 D ( 𝑦 ∈ 𝑋 ↦ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑦 ) ) ) ) = ( 𝑦 ∈ 𝑋 ↦ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑦 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝑦 ) ) ) )
262 242 261 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑆 D ( ( 𝐹 ‘ 𝑛 ) ∘f − ( 𝐹 ‘ 𝑁 ) ) ) = ( 𝑦 ∈ 𝑋 ↦ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑦 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝑦 ) ) ) )
263 262 dmeqd ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → dom ( 𝑆 D ( ( 𝐹 ‘ 𝑛 ) ∘f − ( 𝐹 ‘ 𝑁 ) ) ) = dom ( 𝑦 ∈ 𝑋 ↦ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑦 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝑦 ) ) ) )
264 ovex ⊢ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑦 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝑦 ) ) ∈ V
265 eqid ⊢ ( 𝑦 ∈ 𝑋 ↦ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑦 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝑦 ) ) ) = ( 𝑦 ∈ 𝑋 ↦ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑦 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝑦 ) ) )
266 264 265 dmmpti ⊢ dom ( 𝑦 ∈ 𝑋 ↦ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑦 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝑦 ) ) ) = 𝑋
267 263 266 eqtrdi ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → dom ( 𝑆 D ( ( 𝐹 ‘ 𝑛 ) ∘f − ( 𝐹 ‘ 𝑁 ) ) ) = 𝑋 )
268 241 267 sseqtrrd ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝐶 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑈 ) ⊆ dom ( 𝑆 D ( ( 𝐹 ‘ 𝑛 ) ∘f − ( 𝐹 ‘ 𝑁 ) ) ) )
269 77 adantr ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝑅 / 2 ) / 2 ) ∈ ℝ )
270 241 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝐶 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑈 ) ) → 𝑦 ∈ 𝑋 )
271 262 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝑆 D ( ( 𝐹 ‘ 𝑛 ) ∘f − ( 𝐹 ‘ 𝑁 ) ) ) ‘ 𝑦 ) = ( ( 𝑦 ∈ 𝑋 ↦ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑦 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝑦 ) ) ) ‘ 𝑦 ) )
272 265 fvmpt2 ⊢ ( ( 𝑦 ∈ 𝑋 ∧ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑦 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝑦 ) ) ∈ V ) → ( ( 𝑦 ∈ 𝑋 ↦ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑦 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝑦 ) ) ) ‘ 𝑦 ) = ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑦 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝑦 ) ) )
273 264 272 mpan2 ⊢ ( 𝑦 ∈ 𝑋 → ( ( 𝑦 ∈ 𝑋 ↦ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑦 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝑦 ) ) ) ‘ 𝑦 ) = ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑦 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝑦 ) ) )
274 271 273 sylan9eq ⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑆 D ( ( 𝐹 ‘ 𝑛 ) ∘f − ( 𝐹 ‘ 𝑁 ) ) ) ‘ 𝑦 ) = ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑦 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝑦 ) ) )
275 274 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑦 ∈ 𝑋 ) → ( abs ‘ ( ( 𝑆 D ( ( 𝐹 ‘ 𝑛 ) ∘f − ( 𝐹 ‘ 𝑁 ) ) ) ‘ 𝑦 ) ) = ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑦 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝑦 ) ) ) )
276 264 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑦 ∈ 𝑋 ) → ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑦 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝑦 ) ) ∈ V )
277 226 236 276 261 dvmptcl ⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑦 ∈ 𝑋 ) → ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑦 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝑦 ) ) ∈ ℂ )
278 277 abscld ⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑦 ∈ 𝑋 ) → ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑦 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝑦 ) ) ) ∈ ℝ )
279 77 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑅 / 2 ) / 2 ) ∈ ℝ )
280 253 ffvelcdmda ⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑦 ) ∈ ℂ )
281 258 ffvelcdmda ⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝑦 ) ∈ ℂ )
282 280 281 abssubd ⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑦 ∈ 𝑋 ) → ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑦 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝑦 ) ) ) = ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝑦 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑦 ) ) ) )
283 fveq2 ⊢ ( 𝑚 = 𝑛 → ( 𝐹 ‘ 𝑚 ) = ( 𝐹 ‘ 𝑛 ) )
284 283 oveq2d ⊢ ( 𝑚 = 𝑛 → ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) = ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) )
285 284 fveq1d ⊢ ( 𝑚 = 𝑛 → ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) = ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) )
286 285 oveq2d ⊢ ( 𝑚 = 𝑛 → ( ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) = ( ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) ) )
287 286 fveq2d ⊢ ( 𝑚 = 𝑛 → ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) = ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) ) ) )
288 287 breq1d ⊢ ( 𝑚 = 𝑛 → ( ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑅 / 2 ) / 2 ) ↔ ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑅 / 2 ) / 2 ) ) )
289 288 ralbidv ⊢ ( 𝑚 = 𝑛 → ( ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑅 / 2 ) / 2 ) ↔ ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑅 / 2 ) / 2 ) ) )
290 289 rspccva ⊢ ( ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑚 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑅 / 2 ) / 2 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑅 / 2 ) / 2 ) )
291 16 290 sylan ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑅 / 2 ) / 2 ) )
292 fveq2 ⊢ ( 𝑥 = 𝑦 → ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝑥 ) = ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝑦 ) )
293 fveq2 ⊢ ( 𝑥 = 𝑦 → ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) = ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑦 ) )
294 292 293 oveq12d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) ) = ( ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝑦 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑦 ) ) )
295 294 fveq2d ⊢ ( 𝑥 = 𝑦 → ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) ) ) = ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝑦 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑦 ) ) ) )
296 295 breq1d ⊢ ( 𝑥 = 𝑦 → ( ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑅 / 2 ) / 2 ) ↔ ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝑦 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑦 ) ) ) < ( ( 𝑅 / 2 ) / 2 ) ) )
297 296 rspccva ⊢ ( ( ∀ 𝑥 ∈ 𝑋 ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝑥 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑥 ) ) ) < ( ( 𝑅 / 2 ) / 2 ) ∧ 𝑦 ∈ 𝑋 ) → ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝑦 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑦 ) ) ) < ( ( 𝑅 / 2 ) / 2 ) )
298 291 297 sylan ⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑦 ∈ 𝑋 ) → ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝑦 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑦 ) ) ) < ( ( 𝑅 / 2 ) / 2 ) )
299 282 298 eqbrtrd ⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑦 ∈ 𝑋 ) → ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑦 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝑦 ) ) ) < ( ( 𝑅 / 2 ) / 2 ) )
300 278 279 299 ltled ⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑦 ∈ 𝑋 ) → ( abs ‘ ( ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑦 ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝑦 ) ) ) ≤ ( ( 𝑅 / 2 ) / 2 ) )
301 275 300 eqbrtrd ⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑦 ∈ 𝑋 ) → ( abs ‘ ( ( 𝑆 D ( ( 𝐹 ‘ 𝑛 ) ∘f − ( 𝐹 ‘ 𝑁 ) ) ) ‘ 𝑦 ) ) ≤ ( ( 𝑅 / 2 ) / 2 ) )
302 270 301 syldan ⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝐶 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑈 ) ) → ( abs ‘ ( ( 𝑆 D ( ( 𝐹 ‘ 𝑛 ) ∘f − ( 𝐹 ‘ 𝑁 ) ) ) ‘ 𝑦 ) ) ≤ ( ( 𝑅 / 2 ) / 2 ) )
303 226 227 228 237 238 239 240 268 269 302 dvlip2 ⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ ( 𝑌 ∈ ( 𝐶 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑈 ) ∧ 𝐶 ∈ ( 𝐶 ( ball ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) 𝑈 ) ) ) → ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑛 ) ∘f − ( 𝐹 ‘ 𝑁 ) ) ‘ 𝑌 ) − ( ( ( 𝐹 ‘ 𝑛 ) ∘f − ( 𝐹 ‘ 𝑁 ) ) ‘ 𝐶 ) ) ) ≤ ( ( ( 𝑅 / 2 ) / 2 ) · ( abs ‘ ( 𝑌 − 𝐶 ) ) ) )
304 225 303 mpdan ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑛 ) ∘f − ( 𝐹 ‘ 𝑁 ) ) ‘ 𝑌 ) − ( ( ( 𝐹 ‘ 𝑛 ) ∘f − ( 𝐹 ‘ 𝑁 ) ) ‘ 𝐶 ) ) ) ≤ ( ( ( 𝑅 / 2 ) / 2 ) · ( abs ‘ ( 𝑌 − 𝐶 ) ) ) )
305 205 304 eqbrtrrd ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) − ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) ) ≤ ( ( ( 𝑅 / 2 ) / 2 ) · ( abs ‘ ( 𝑌 − 𝐶 ) ) ) )
306 305 182 188 3brtr4d ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝑘 ∈ 𝑍 ↦ ( abs ‘ ( ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) − ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) ) ) ‘ 𝑛 ) ≤ ( ( 𝑍 × { ( ( ( 𝑅 / 2 ) / 2 ) · ( abs ‘ ( 𝑌 − 𝐶 ) ) ) } ) ‘ 𝑛 ) )
307 88 91 173 179 185 190 306 climle ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( abs ‘ ( ( ( 𝐺 ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) − ( ( 𝐺 ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) ) ≤ ( ( ( 𝑅 / 2 ) / 2 ) · ( abs ‘ ( 𝑌 − 𝐶 ) ) ) )
308 85 abscld ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( abs ‘ ( ( ( 𝐺 ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) − ( ( 𝐺 ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) ) ∈ ℝ )
309 51 52 absrpcld ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( abs ‘ ( 𝑌 − 𝐶 ) ) ∈ ℝ+ )
310 308 77 309 ledivmul2d ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( ( abs ‘ ( ( ( 𝐺 ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) − ( ( 𝐺 ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) ) / ( abs ‘ ( 𝑌 − 𝐶 ) ) ) ≤ ( ( 𝑅 / 2 ) / 2 ) ↔ ( abs ‘ ( ( ( 𝐺 ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) − ( ( 𝐺 ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) ) ≤ ( ( ( 𝑅 / 2 ) / 2 ) · ( abs ‘ ( 𝑌 − 𝐶 ) ) ) ) )
311 307 310 mpbird ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( abs ‘ ( ( ( 𝐺 ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ) − ( ( 𝐺 ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) ) ) / ( abs ‘ ( 𝑌 − 𝐶 ) ) ) ≤ ( ( 𝑅 / 2 ) / 2 ) )
312 87 311 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( abs ‘ ( ( ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑌 − 𝐶 ) ) − ( ( ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) / ( 𝑌 − 𝐶 ) ) ) ) ≤ ( ( 𝑅 / 2 ) / 2 ) )
313 10 rpred ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑈 ∈ ℝ )
314 11 rpred ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑊 ∈ ℝ )
315 174 313 314 14 12 lttrd ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( abs ‘ ( 𝑌 − 𝐶 ) ) < 𝑊 )
316 315 20 mpd ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) / ( 𝑌 − 𝐶 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝐶 ) ) ) < ( ( 𝑅 / 2 ) / 2 ) )
317 71 73 77 77 312 316 leltaddd ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( abs ‘ ( ( ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑌 − 𝐶 ) ) − ( ( ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) / ( 𝑌 − 𝐶 ) ) ) ) + ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) / ( 𝑌 − 𝐶 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝐶 ) ) ) ) < ( ( ( 𝑅 / 2 ) / 2 ) + ( ( 𝑅 / 2 ) / 2 ) ) )
318 75 recnd ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑅 / 2 ) ∈ ℂ )
319 318 2halvesd ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( ( 𝑅 / 2 ) / 2 ) + ( ( 𝑅 / 2 ) / 2 ) ) = ( 𝑅 / 2 ) )
320 317 319 breqtrd ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( abs ‘ ( ( ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑌 − 𝐶 ) ) − ( ( ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) / ( 𝑌 − 𝐶 ) ) ) ) + ( abs ‘ ( ( ( ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) − ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ) / ( 𝑌 − 𝐶 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝐶 ) ) ) ) < ( 𝑅 / 2 ) )
321 61 74 75 76 320 lelttrd ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( abs ‘ ( ( ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑌 − 𝐶 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝐶 ) ) ) < ( 𝑅 / 2 ) )
322 53 57 58 59 321 17 abs3lemd ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( abs ‘ ( ( ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑌 − 𝐶 ) ) − ( 𝐻 ‘ 𝐶 ) ) ) < 𝑅 )