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	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝐺 ‘ 𝑌 ) ∈ ℂ )
23	21 8	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝐺 ‘ 𝐶 ) ∈ ℂ )
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	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 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	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝐻 ‘ 𝐶 ) ∈ ℂ )
58	41 8	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝐶 ) ∈ ℂ )
59	9	rpred	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑅 ∈ ℝ )
60	53 58	subcld	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑌 − 𝐶 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝐶 ) ) ∈ ℂ )
61	60	abscld	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( abs ‘ ( ( ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑌 − 𝐶 ) ) − ( ( 𝑆 D ( 𝐹 ‘ 𝑁 ) ) ‘ 𝐶 ) ) ) ∈ ℝ )
62	4	adantr	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑋 ) )
63	62 15	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝐹 ‘ 𝑁 ) ∈ ( ℂ ↑m 𝑋 ) )
64		elmapi	⊢ ( ( 𝐹 ‘ 𝑁 ) ∈ ( ℂ ↑m 𝑋 ) → ( 𝐹 ‘ 𝑁 ) : 𝑋 ⟶ ℂ )
65	63 64	syl	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝐹 ‘ 𝑁 ) : 𝑋 ⟶ ℂ )
66	65 18	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑌 ) ∈ ℂ )
67	65 8	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝐹 ‘ 𝑁 ) ‘ 𝐶 ) ∈ ℂ )
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	ffvelrnda	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) ∈ ( ℂ ↑m 𝑋 ) )
110		elmapi	⊢ ( ( 𝐹 ‘ 𝑛 ) ∈ ( ℂ ↑m 𝑋 ) → ( 𝐹 ‘ 𝑛 ) : 𝑋 ⟶ ℂ )
111	109 110	syl	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) : 𝑋 ⟶ ℂ )
112	18	adantr	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ 𝑍 ) → 𝑌 ∈ 𝑋 )
113	111 112	ffvelrnd	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑌 ) ∈ ℂ )
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	ffvelrnd	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝐶 ) ∈ ℂ )
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	ffvelrnda	⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ∈ ℂ )
235	193	ffvelrnda	⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑁 ) ‘ 𝑦 ) ∈ ℂ )
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	ffvelrnd	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 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	ffvelrnda	⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑆 D ( 𝐹 ‘ 𝑛 ) ) ‘ 𝑦 ) ∈ ℂ )
281	258	ffvelrnda	⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑆 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 ‘ ( ( ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑌 − 𝐶 ) ) − ( 𝐻 ‘ 𝐶 ) ) ) < 𝑅 )