ulmdvlem1 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ulmdvlem1		Structured version Visualization version GIF version

Theorem ulmdvlem1 24445

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

**Hypotheses**
Ref	Expression
ulmdv.z	⊢ 𝑍 = (ℤ_≥‘𝑀)
ulmdv.s	⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})
ulmdv.m	⊢ (𝜑 → 𝑀 ∈ ℤ)
ulmdv.f	⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑_𝑚 𝑋))
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**
Ref	Expression
ulmdvlem1	⊢ ((𝜑 ∧ 𝜓) → (abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − (𝐻‘𝐶))) < 𝑅)

Distinct variable groups: 𝑘,𝑚,𝑥,𝑧,𝐹 𝑧,𝐺 𝑘,𝑁,𝑚,𝑥 𝐶,𝑘,𝑧 𝑧,𝐻 𝑘,𝑀,𝑥 𝜑,𝑘,𝑚,𝑥,𝑧 𝑆,𝑘,𝑚,𝑥,𝑧 𝑅,𝑚,𝑥 𝑘,𝑋,𝑚,𝑥,𝑧 𝑘,𝑌,𝑧 𝑘,𝑍,𝑚,𝑥,𝑧 Allowed substitution hints: 𝜓(𝑥,𝑧,𝑘,𝑚) 𝐶(𝑥,𝑚) 𝑅(𝑧,𝑘) 𝑈(𝑥,𝑧,𝑘,𝑚) 𝐺(𝑥,𝑘,𝑚) 𝐻(𝑥,𝑘,𝑚) 𝑀(𝑧,𝑚) 𝑁(𝑧) 𝑊(𝑥,𝑧,𝑘,𝑚) 𝑌(𝑥,𝑚)

Proof of Theorem ulmdvlem1 Dummy variables 𝑛 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ulmdv.g	. . . . . 6 ⊢ (𝜑 → 𝐺:𝑋⟶ℂ)
2	1	adantr 472	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → 𝐺:𝑋⟶ℂ)
3		ulmdvlem1.y	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → 𝑌 ∈ 𝑋)
4	2, 3	ffvelrnd 6550	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → (𝐺‘𝑌) ∈ ℂ)
5		ulmdvlem1.c	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → 𝐶 ∈ 𝑋)
6	2, 5	ffvelrnd 6550	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → (𝐺‘𝐶) ∈ ℂ)
7	4, 6	subcld 10646	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ((𝐺‘𝑌) − (𝐺‘𝐶)) ∈ ℂ)
8		ulmdvlem1.n	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → 𝑁 ∈ 𝑍)
9		fveq2 6375	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑁 → (𝐹‘𝑘) = (𝐹‘𝑁))
10	9	oveq2d 6858	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑁 → (𝑆 D (𝐹‘𝑘)) = (𝑆 D (𝐹‘𝑁)))
11		eqid 2765	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘))) = (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))
12		ovex 6874	. . . . . . . . . . . 12 ⊢ (𝑆 D (𝐹‘𝑁)) ∈ V
13	10, 11, 12	fvmpt 6471	. . . . . . . . . . 11 ⊢ (𝑁 ∈ 𝑍 → ((𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))‘𝑁) = (𝑆 D (𝐹‘𝑁)))
14	8, 13	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → ((𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))‘𝑁) = (𝑆 D (𝐹‘𝑁)))
15		ovex 6874	. . . . . . . . . . . . . . 15 ⊢ (𝑆 D (𝐹‘𝑘)) ∈ V
16	15	rgenw 3071	. . . . . . . . . . . . . 14 ⊢ ∀𝑘 ∈ 𝑍 (𝑆 D (𝐹‘𝑘)) ∈ V
17	11	fnmpt 6198	. . . . . . . . . . . . . 14 ⊢ (∀𝑘 ∈ 𝑍 (𝑆 D (𝐹‘𝑘)) ∈ V → (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘))) Fn 𝑍)
18	16, 17	mp1i 13	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘))) Fn 𝑍)
19		ulmdv.u	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))(⇝_𝑢‘𝑋)𝐻)
20		ulmf2 24429	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘))) Fn 𝑍 ∧ (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))(⇝_𝑢‘𝑋)𝐻) → (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘))):𝑍⟶(ℂ ↑_𝑚 𝑋))
21	18, 19, 20	syl2anc 579	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘))):𝑍⟶(ℂ ↑_𝑚 𝑋))
22	21	adantr 472	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘))):𝑍⟶(ℂ ↑_𝑚 𝑋))
23	22, 8	ffvelrnd 6550	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → ((𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))‘𝑁) ∈ (ℂ ↑_𝑚 𝑋))
24	14, 23	eqeltrrd 2845	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → (𝑆 D (𝐹‘𝑁)) ∈ (ℂ ↑_𝑚 𝑋))
25		elmapi 8082	. . . . . . . . 9 ⊢ ((𝑆 D (𝐹‘𝑁)) ∈ (ℂ ↑_𝑚 𝑋) → (𝑆 D (𝐹‘𝑁)):𝑋⟶ℂ)
26	24, 25	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → (𝑆 D (𝐹‘𝑁)):𝑋⟶ℂ)
27	26	fdmd 6232	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → dom (𝑆 D (𝐹‘𝑁)) = 𝑋)
28		dvbsss 23957	. . . . . . 7 ⊢ dom (𝑆 D (𝐹‘𝑁)) ⊆ 𝑆
29	27, 28	syl6eqssr 3816	. . . . . 6 ⊢ ((𝜑 ∧ 𝜓) → 𝑋 ⊆ 𝑆)
30		ulmdv.s	. . . . . . . 8 ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})
31		recnprss 23959	. . . . . . . 8 ⊢ (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)
32	30, 31	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑆 ⊆ ℂ)
33	32	adantr 472	. . . . . 6 ⊢ ((𝜑 ∧ 𝜓) → 𝑆 ⊆ ℂ)
34	29, 33	sstrd 3771	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → 𝑋 ⊆ ℂ)
35	34, 3	sseldd 3762	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝑌 ∈ ℂ)
36	34, 5	sseldd 3762	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝐶 ∈ ℂ)
37	35, 36	subcld 10646	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝑌 − 𝐶) ∈ ℂ)
38		ulmdvlem1.3	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝑌 ≠ 𝐶)
39	35, 36, 38	subne0d 10655	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝑌 − 𝐶) ≠ 0)
40	7, 37, 39	divcld 11055	. 2 ⊢ ((𝜑 ∧ 𝜓) → (((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) ∈ ℂ)
41		ulmcl 24426	. . . . 5 ⊢ ((𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))(⇝_𝑢‘𝑋)𝐻 → 𝐻:𝑋⟶ℂ)
42	19, 41	syl 17	. . . 4 ⊢ (𝜑 → 𝐻:𝑋⟶ℂ)
43	42	adantr 472	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝐻:𝑋⟶ℂ)
44	43, 5	ffvelrnd 6550	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝐻‘𝐶) ∈ ℂ)
45	26, 5	ffvelrnd 6550	. 2 ⊢ ((𝜑 ∧ 𝜓) → ((𝑆 D (𝐹‘𝑁))‘𝐶) ∈ ℂ)
46		ulmdvlem1.r	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝑅 ∈ ℝ⁺)
47	46	rpred 12070	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝑅 ∈ ℝ)
48	40, 45	subcld 10646	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → ((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((𝑆 D (𝐹‘𝑁))‘𝐶)) ∈ ℂ)
49	48	abscld 14460	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((𝑆 D (𝐹‘𝑁))‘𝐶))) ∈ ℝ)
50		ulmdv.f	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑_𝑚 𝑋))
51	50	adantr 472	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → 𝐹:𝑍⟶(ℂ ↑_𝑚 𝑋))
52	51, 8	ffvelrnd 6550	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → (𝐹‘𝑁) ∈ (ℂ ↑_𝑚 𝑋))
53		elmapi 8082	. . . . . . . . . 10 ⊢ ((𝐹‘𝑁) ∈ (ℂ ↑_𝑚 𝑋) → (𝐹‘𝑁):𝑋⟶ℂ)
54	52, 53	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → (𝐹‘𝑁):𝑋⟶ℂ)
55	54, 3	ffvelrnd 6550	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → ((𝐹‘𝑁)‘𝑌) ∈ ℂ)
56	54, 5	ffvelrnd 6550	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → ((𝐹‘𝑁)‘𝐶) ∈ ℂ)
57	55, 56	subcld 10646	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → (((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) ∈ ℂ)
58	57, 37, 39	divcld 11055	. . . . . 6 ⊢ ((𝜑 ∧ 𝜓) → ((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)) ∈ ℂ)
59	40, 58	subcld 10646	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → ((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶))) ∈ ℂ)
60	59	abscld 14460	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → (abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)))) ∈ ℝ)
61	58, 45	subcld 10646	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → (((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)) − ((𝑆 D (𝐹‘𝑁))‘𝐶)) ∈ ℂ)
62	61	abscld 14460	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → (abs‘(((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)) − ((𝑆 D (𝐹‘𝑁))‘𝐶))) ∈ ℝ)
63	60, 62	readdcld 10323	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ((abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)))) + (abs‘(((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)) − ((𝑆 D (𝐹‘𝑁))‘𝐶)))) ∈ ℝ)
64	47	rehalfcld 11525	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝑅 / 2) ∈ ℝ)
65	40, 45, 58	abs3difd 14484	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((𝑆 D (𝐹‘𝑁))‘𝐶))) ≤ ((abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)))) + (abs‘(((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)) − ((𝑆 D (𝐹‘𝑁))‘𝐶)))))
66	64	rehalfcld 11525	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → ((𝑅 / 2) / 2) ∈ ℝ)
67	4, 55, 6, 56	sub4d 10695	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → (((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶))) = (((𝐺‘𝑌) − (𝐺‘𝐶)) − (((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶))))
68	67	oveq1d 6857	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → ((((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶))) / (𝑌 − 𝐶)) = ((((𝐺‘𝑌) − (𝐺‘𝐶)) − (((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶))) / (𝑌 − 𝐶)))
69	7, 57, 37, 39	divsubdird 11094	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → ((((𝐺‘𝑌) − (𝐺‘𝐶)) − (((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶))) / (𝑌 − 𝐶)) = ((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶))))
70	68, 69	eqtrd 2799	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → ((((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶))) / (𝑌 − 𝐶)) = ((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶))))
71	70	fveq2d 6379	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → (abs‘((((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶))) / (𝑌 − 𝐶))) = (abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)))))
72	4, 55	subcld 10646	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → ((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) ∈ ℂ)
73	6, 56	subcld 10646	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶)) ∈ ℂ)
74	72, 73	subcld 10646	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → (((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶))) ∈ ℂ)
75	74, 37, 39	absdivd 14479	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → (abs‘((((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶))) / (𝑌 − 𝐶))) = ((abs‘(((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) / (abs‘(𝑌 − 𝐶))))
76	71, 75	eqtr3d 2801	. . . . . 6 ⊢ ((𝜑 ∧ 𝜓) → (abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)))) = ((abs‘(((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) / (abs‘(𝑌 − 𝐶))))
77		eqid 2765	. . . . . . . 8 ⊢ (ℤ_≥‘𝑁) = (ℤ_≥‘𝑁)
78		ulmdv.z	. . . . . . . . . 10 ⊢ 𝑍 = (ℤ_≥‘𝑀)
79	8, 78	syl6eleq 2854	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → 𝑁 ∈ (ℤ_≥‘𝑀))
80		eluzelz 11896	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → 𝑁 ∈ ℤ)
81	79, 80	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → 𝑁 ∈ ℤ)
82		ulmdv.m	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℤ)
83	82	adantr 472	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → 𝑀 ∈ ℤ)
84		fveq2 6375	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑌 → ((𝐹‘𝑘)‘𝑧) = ((𝐹‘𝑘)‘𝑌))
85	84	mpteq2dv 4904	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑌 → (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑧)) = (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑌)))
86		fveq2 6375	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑌 → (𝐺‘𝑧) = (𝐺‘𝑌))
87	85, 86	breq12d 4822	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑌 → ((𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑧)) ⇝ (𝐺‘𝑧) ↔ (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑌)) ⇝ (𝐺‘𝑌)))
88		ulmdv.l	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑧)) ⇝ (𝐺‘𝑧))
89	88	ralrimiva 3113	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑧 ∈ 𝑋 (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑧)) ⇝ (𝐺‘𝑧))
90	89	adantr 472	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → ∀𝑧 ∈ 𝑋 (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑧)) ⇝ (𝐺‘𝑧))
91	87, 90, 3	rspcdva 3467	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑌)) ⇝ (𝐺‘𝑌))
92	78	fvexi 6389	. . . . . . . . . . . . 13 ⊢ 𝑍 ∈ V
93	92	mptex 6679	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌))) ∈ V
94	93	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌))) ∈ V)
95		fveq2 6375	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑛 → (𝐹‘𝑘) = (𝐹‘𝑛))
96	95	fveq1d 6377	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑛 → ((𝐹‘𝑘)‘𝑌) = ((𝐹‘𝑛)‘𝑌))
97		eqid 2765	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑌)) = (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑌))
98		fvex 6388	. . . . . . . . . . . . . 14 ⊢ ((𝐹‘𝑛)‘𝑌) ∈ V
99	96, 97, 98	fvmpt 6471	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ 𝑍 → ((𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑌))‘𝑛) = ((𝐹‘𝑛)‘𝑌))
100	99	adantl 473	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑌))‘𝑛) = ((𝐹‘𝑛)‘𝑌))
101	51	ffvelrnda 6549	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ∈ (ℂ ↑_𝑚 𝑋))
102		elmapi 8082	. . . . . . . . . . . . . 14 ⊢ ((𝐹‘𝑛) ∈ (ℂ ↑_𝑚 𝑋) → (𝐹‘𝑛):𝑋⟶ℂ)
103	101, 102	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛):𝑋⟶ℂ)
104	3	adantr 472	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → 𝑌 ∈ 𝑋)
105	103, 104	ffvelrnd 6550	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝐹‘𝑛)‘𝑌) ∈ ℂ)
106	100, 105	eqeltrd 2844	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑌))‘𝑛) ∈ ℂ)
107	96	oveq1d 6857	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑛 → (((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) = (((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)))
108		eqid 2765	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌))) = (𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)))
109		ovex 6874	. . . . . . . . . . . . . 14 ⊢ (((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) ∈ V
110	107, 108, 109	fvmpt 6471	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ 𝑍 → ((𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)))‘𝑛) = (((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)))
111	110	adantl 473	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)))‘𝑛) = (((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)))
112	100	oveq1d 6857	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → (((𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑌))‘𝑛) − ((𝐹‘𝑁)‘𝑌)) = (((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)))
113	111, 112	eqtr4d 2802	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)))‘𝑛) = (((𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑌))‘𝑛) − ((𝐹‘𝑁)‘𝑌)))
114	78, 83, 91, 55, 94, 106, 113	climsubc1 14653	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌))) ⇝ ((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)))
115	92	mptex 6679	. . . . . . . . . . 11 ⊢ (𝑘 ∈ 𝑍 ↦ ((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) ∈ V
116	115	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝑍 ↦ ((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) ∈ V)
117		fveq2 6375	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝐶 → ((𝐹‘𝑘)‘𝑧) = ((𝐹‘𝑘)‘𝐶))
118	117	mpteq2dv 4904	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝐶 → (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑧)) = (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝐶)))
119		fveq2 6375	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝐶 → (𝐺‘𝑧) = (𝐺‘𝐶))
120	118, 119	breq12d 4822	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝐶 → ((𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑧)) ⇝ (𝐺‘𝑧) ↔ (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝐶)) ⇝ (𝐺‘𝐶)))
121	120, 90, 5	rspcdva 3467	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝐶)) ⇝ (𝐺‘𝐶))
122	92	mptex 6679	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))) ∈ V
123	122	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))) ∈ V)
124	95	fveq1d 6377	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑛 → ((𝐹‘𝑘)‘𝐶) = ((𝐹‘𝑛)‘𝐶))
125		eqid 2765	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝐶)) = (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝐶))
126		fvex 6388	. . . . . . . . . . . . . 14 ⊢ ((𝐹‘𝑛)‘𝐶) ∈ V
127	124, 125, 126	fvmpt 6471	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ 𝑍 → ((𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝐶))‘𝑛) = ((𝐹‘𝑛)‘𝐶))
128	127	adantl 473	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝐶))‘𝑛) = ((𝐹‘𝑛)‘𝐶))
129	5	adantr 472	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → 𝐶 ∈ 𝑋)
130	103, 129	ffvelrnd 6550	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝐹‘𝑛)‘𝐶) ∈ ℂ)
131	128, 130	eqeltrd 2844	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝐶))‘𝑛) ∈ ℂ)
132	124	oveq1d 6857	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑛 → (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)) = (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))
133		eqid 2765	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))) = (𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))
134		ovex 6874	. . . . . . . . . . . . . 14 ⊢ (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)) ∈ V
135	132, 133, 134	fvmpt 6471	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ 𝑍 → ((𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))‘𝑛) = (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))
136	135	adantl 473	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))‘𝑛) = (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))
137	128	oveq1d 6857	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → (((𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝐶))‘𝑛) − ((𝐹‘𝑁)‘𝐶)) = (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))
138	136, 137	eqtr4d 2802	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))‘𝑛) = (((𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝐶))‘𝑛) − ((𝐹‘𝑁)‘𝐶)))
139	78, 83, 121, 56, 123, 131, 138	climsubc1 14653	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))) ⇝ ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶)))
140	55	adantr 472	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝐹‘𝑁)‘𝑌) ∈ ℂ)
141	105, 140	subcld 10646	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → (((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) ∈ ℂ)
142	111, 141	eqeltrd 2844	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)))‘𝑛) ∈ ℂ)
143	56	adantr 472	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝐹‘𝑁)‘𝐶) ∈ ℂ)
144	130, 143	subcld 10646	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)) ∈ ℂ)
145	136, 144	eqeltrd 2844	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))‘𝑛) ∈ ℂ)
146	107, 132	oveq12d 6860	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑛 → ((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))) = ((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))
147		eqid 2765	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ 𝑍 ↦ ((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) = (𝑘 ∈ 𝑍 ↦ ((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))
148		ovex 6874	. . . . . . . . . . . . 13 ⊢ ((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶))) ∈ V
149	146, 147, 148	fvmpt 6471	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ 𝑍 → ((𝑘 ∈ 𝑍 ↦ ((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))‘𝑛) = ((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))
150	149	adantl 473	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ ((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))‘𝑛) = ((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))
151	111, 136	oveq12d 6860	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → (((𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)))‘𝑛) − ((𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))‘𝑛)) = ((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))
152	150, 151	eqtr4d 2802	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ ((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))‘𝑛) = (((𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)))‘𝑛) − ((𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))‘𝑛)))
153	78, 83, 114, 116, 139, 142, 145, 152	climsub 14649	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝑍 ↦ ((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) ⇝ (((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶))))
154	92	mptex 6679	. . . . . . . . . 10 ⊢ (𝑘 ∈ 𝑍 ↦ (abs‘((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))) ∈ V
155	154	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝑍 ↦ (abs‘((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))) ∈ V)
156	141, 144	subcld 10646	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶))) ∈ ℂ)
157	150, 156	eqeltrd 2844	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ ((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))‘𝑛) ∈ ℂ)
158	146	fveq2d 6379	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑛 → (abs‘((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) = (abs‘((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))))
159		eqid 2765	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ 𝑍 ↦ (abs‘((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))) = (𝑘 ∈ 𝑍 ↦ (abs‘((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))))
160		fvex 6388	. . . . . . . . . . . 12 ⊢ (abs‘((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) ∈ V
161	158, 159, 160	fvmpt 6471	. . . . . . . . . . 11 ⊢ (𝑛 ∈ 𝑍 → ((𝑘 ∈ 𝑍 ↦ (abs‘((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))))‘𝑛) = (abs‘((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))))
162	161	adantl 473	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ (abs‘((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))))‘𝑛) = (abs‘((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))))
163	150	fveq2d 6379	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → (abs‘((𝑘 ∈ 𝑍 ↦ ((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))‘𝑛)) = (abs‘((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))))
164	162, 163	eqtr4d 2802	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ (abs‘((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))))‘𝑛) = (abs‘((𝑘 ∈ 𝑍 ↦ ((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))‘𝑛)))
165	78, 153, 155, 83, 157, 164	climabs 14619	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝑍 ↦ (abs‘((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))) ⇝ (abs‘(((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶)))))
166	37	abscld 14460	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → (abs‘(𝑌 − 𝐶)) ∈ ℝ)
167	66, 166	remulcld 10324	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → (((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶))) ∈ ℝ)
168	167	recnd 10322	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → (((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶))) ∈ ℂ)
169	78	eqimss2i 3820	. . . . . . . . . 10 ⊢ (ℤ_≥‘𝑀) ⊆ 𝑍
170	169, 92	climconst2 14564	. . . . . . . . 9 ⊢ (((((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶))) ∈ ℂ ∧ 𝑀 ∈ ℤ) → (𝑍 × {(((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶)))}) ⇝ (((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶))))
171	168, 83, 170	syl2anc 579	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → (𝑍 × {(((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶)))}) ⇝ (((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶))))
172	78	uztrn2 11904	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → 𝑛 ∈ 𝑍)
173	8, 172	sylan 575	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → 𝑛 ∈ 𝑍)
174	173, 161	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → ((𝑘 ∈ 𝑍 ↦ (abs‘((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))))‘𝑛) = (abs‘((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))))
175	156	abscld 14460	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → (abs‘((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) ∈ ℝ)
176	173, 175	syldan 585	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (abs‘((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) ∈ ℝ)
177	174, 176	eqeltrd 2844	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → ((𝑘 ∈ 𝑍 ↦ (abs‘((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))))‘𝑛) ∈ ℝ)
178		ovex 6874	. . . . . . . . . . 11 ⊢ (((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶))) ∈ V
179	178	fvconst2 6662	. . . . . . . . . 10 ⊢ (𝑛 ∈ 𝑍 → ((𝑍 × {(((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶)))})‘𝑛) = (((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶))))
180	173, 179	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → ((𝑍 × {(((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶)))})‘𝑛) = (((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶))))
181	167	adantr 472	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶))) ∈ ℝ)
182	180, 181	eqeltrd 2844	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → ((𝑍 × {(((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶)))})‘𝑛) ∈ ℝ)
183	173, 103	syldan 585	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝐹‘𝑛):𝑋⟶ℂ)
184	183	ffnd 6224	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝐹‘𝑛) Fn 𝑋)
185	54	adantr 472	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝐹‘𝑁):𝑋⟶ℂ)
186	185	ffnd 6224	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝐹‘𝑁) Fn 𝑋)
187		ulmscl 24424	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))(⇝_𝑢‘𝑋)𝐻 → 𝑋 ∈ V)
188	19, 187	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑋 ∈ V)
189	188	ad2antrr 717	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → 𝑋 ∈ V)
190	3	adantr 472	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → 𝑌 ∈ 𝑋)
191		fnfvof 7109	. . . . . . . . . . . . 13 ⊢ ((((𝐹‘𝑛) Fn 𝑋 ∧ (𝐹‘𝑁) Fn 𝑋) ∧ (𝑋 ∈ V ∧ 𝑌 ∈ 𝑋)) → (((𝐹‘𝑛) ∘_𝑓 − (𝐹‘𝑁))‘𝑌) = (((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)))
192	184, 186, 189, 190, 191	syl22anc 867	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (((𝐹‘𝑛) ∘_𝑓 − (𝐹‘𝑁))‘𝑌) = (((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)))
193	5	adantr 472	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → 𝐶 ∈ 𝑋)
194		fnfvof 7109	. . . . . . . . . . . . 13 ⊢ ((((𝐹‘𝑛) Fn 𝑋 ∧ (𝐹‘𝑁) Fn 𝑋) ∧ (𝑋 ∈ V ∧ 𝐶 ∈ 𝑋)) → (((𝐹‘𝑛) ∘_𝑓 − (𝐹‘𝑁))‘𝐶) = (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))
195	184, 186, 189, 193, 194	syl22anc 867	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (((𝐹‘𝑛) ∘_𝑓 − (𝐹‘𝑁))‘𝐶) = (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))
196	192, 195	oveq12d 6860	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → ((((𝐹‘𝑛) ∘_𝑓 − (𝐹‘𝑁))‘𝑌) − (((𝐹‘𝑛) ∘_𝑓 − (𝐹‘𝑁))‘𝐶)) = ((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))
197	196	fveq2d 6379	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (abs‘((((𝐹‘𝑛) ∘_𝑓 − (𝐹‘𝑁))‘𝑌) − (((𝐹‘𝑛) ∘_𝑓 − (𝐹‘𝑁))‘𝐶))) = (abs‘((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))))
198	29, 3	sseldd 3762	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝜓) → 𝑌 ∈ 𝑆)
199	29, 5	sseldd 3762	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝜓) → 𝐶 ∈ 𝑆)
200	198, 199	ovresd 6999	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝜓) → (𝑌((abs ∘ − ) ↾ (𝑆 × 𝑆))𝐶) = (𝑌(abs ∘ − )𝐶))
201		eqid 2765	. . . . . . . . . . . . . . . . . 18 ⊢ (abs ∘ − ) = (abs ∘ − )
202	201	cnmetdval 22853	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑌 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝑌(abs ∘ − )𝐶) = (abs‘(𝑌 − 𝐶)))
203	35, 36, 202	syl2anc 579	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝜓) → (𝑌(abs ∘ − )𝐶) = (abs‘(𝑌 − 𝐶)))
204	200, 203	eqtrd 2799	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → (𝑌((abs ∘ − ) ↾ (𝑆 × 𝑆))𝐶) = (abs‘(𝑌 − 𝐶)))
205		ulmdvlem1.a	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → (abs‘(𝑌 − 𝐶)) < 𝑈)
206	204, 205	eqbrtrd 4831	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → (𝑌((abs ∘ − ) ↾ (𝑆 × 𝑆))𝐶) < 𝑈)
207		cnxmet 22855	. . . . . . . . . . . . . . . 16 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
208		xmetres2 22445	. . . . . . . . . . . . . . . 16 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑆 ⊆ ℂ) → ((abs ∘ − ) ↾ (𝑆 × 𝑆)) ∈ (∞Met‘𝑆))
209	207, 33, 208	sylancr 581	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → ((abs ∘ − ) ↾ (𝑆 × 𝑆)) ∈ (∞Met‘𝑆))
210		ulmdvlem1.u	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝜓) → 𝑈 ∈ ℝ⁺)
211	210	rpxrd 12071	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → 𝑈 ∈ ℝ^*)
212		elbl3 22476	. . . . . . . . . . . . . . 15 ⊢ (((((abs ∘ − ) ↾ (𝑆 × 𝑆)) ∈ (∞Met‘𝑆) ∧ 𝑈 ∈ ℝ^*) ∧ (𝐶 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆)) → (𝑌 ∈ (𝐶(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑈) ↔ (𝑌((abs ∘ − ) ↾ (𝑆 × 𝑆))𝐶) < 𝑈))
213	209, 211, 199, 198, 212	syl22anc 867	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → (𝑌 ∈ (𝐶(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑈) ↔ (𝑌((abs ∘ − ) ↾ (𝑆 × 𝑆))𝐶) < 𝑈))
214	206, 213	mpbird 248	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → 𝑌 ∈ (𝐶(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑈))
215	214	adantr 472	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → 𝑌 ∈ (𝐶(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑈))
216		blcntr 22497	. . . . . . . . . . . . . 14 ⊢ ((((abs ∘ − ) ↾ (𝑆 × 𝑆)) ∈ (∞Met‘𝑆) ∧ 𝐶 ∈ 𝑆 ∧ 𝑈 ∈ ℝ⁺) → 𝐶 ∈ (𝐶(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑈))
217	209, 199, 210, 216	syl3anc 1490	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → 𝐶 ∈ (𝐶(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑈))
218	217	adantr 472	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → 𝐶 ∈ (𝐶(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑈))
219	215, 218	jca 507	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝑌 ∈ (𝐶(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑈) ∧ 𝐶 ∈ (𝐶(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑈)))
220	30	ad2antrr 717	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → 𝑆 ∈ {ℝ, ℂ})
221		eqid 2765	. . . . . . . . . . . 12 ⊢ ((abs ∘ − ) ↾ (𝑆 × 𝑆)) = ((abs ∘ − ) ↾ (𝑆 × 𝑆))
222	29	adantr 472	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → 𝑋 ⊆ 𝑆)
223	183	ffvelrnda 6549	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → ((𝐹‘𝑛)‘𝑦) ∈ ℂ)
224	185	ffvelrnda 6549	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → ((𝐹‘𝑁)‘𝑦) ∈ ℂ)
225	223, 224	subcld 10646	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → (((𝐹‘𝑛)‘𝑦) − ((𝐹‘𝑁)‘𝑦)) ∈ ℂ)
226	225	fmpttd 6575	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝑦 ∈ 𝑋 ↦ (((𝐹‘𝑛)‘𝑦) − ((𝐹‘𝑁)‘𝑦))):𝑋⟶ℂ)
227		fvexd 6390	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → ((𝐹‘𝑛)‘𝑦) ∈ V)
228		fvexd 6390	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → ((𝐹‘𝑁)‘𝑦) ∈ V)
229	183	feqmptd 6438	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝐹‘𝑛) = (𝑦 ∈ 𝑋 ↦ ((𝐹‘𝑛)‘𝑦)))
230	185	feqmptd 6438	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝐹‘𝑁) = (𝑦 ∈ 𝑋 ↦ ((𝐹‘𝑁)‘𝑦)))
231	189, 227, 228, 229, 230	offval2 7112	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → ((𝐹‘𝑛) ∘_𝑓 − (𝐹‘𝑁)) = (𝑦 ∈ 𝑋 ↦ (((𝐹‘𝑛)‘𝑦) − ((𝐹‘𝑁)‘𝑦))))
232	231	feq1d 6208	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (((𝐹‘𝑛) ∘_𝑓 − (𝐹‘𝑁)):𝑋⟶ℂ ↔ (𝑦 ∈ 𝑋 ↦ (((𝐹‘𝑛)‘𝑦) − ((𝐹‘𝑁)‘𝑦))):𝑋⟶ℂ))
233	226, 232	mpbird 248	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → ((𝐹‘𝑛) ∘_𝑓 − (𝐹‘𝑁)):𝑋⟶ℂ)
234	199	adantr 472	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → 𝐶 ∈ 𝑆)
235	211	adantr 472	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → 𝑈 ∈ ℝ^*)
236		eqid 2765	. . . . . . . . . . . 12 ⊢ (𝐶(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑈) = (𝐶(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑈)
237		ulmdvlem1.b	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → (𝐶(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑈) ⊆ 𝑋)
238	237	adantr 472	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝐶(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑈) ⊆ 𝑋)
239	231	oveq2d 6858	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝑆 D ((𝐹‘𝑛) ∘_𝑓 − (𝐹‘𝑁))) = (𝑆 D (𝑦 ∈ 𝑋 ↦ (((𝐹‘𝑛)‘𝑦) − ((𝐹‘𝑁)‘𝑦)))))
240		fvexd 6390	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → ((𝑆 D (𝐹‘𝑛))‘𝑦) ∈ V)
241	229	oveq2d 6858	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝑆 D (𝐹‘𝑛)) = (𝑆 D (𝑦 ∈ 𝑋 ↦ ((𝐹‘𝑛)‘𝑦))))
242	95	oveq2d 6858	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = 𝑛 → (𝑆 D (𝐹‘𝑘)) = (𝑆 D (𝐹‘𝑛)))
243		ovex 6874	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑆 D (𝐹‘𝑛)) ∈ V
244	242, 11, 243	fvmpt 6471	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ 𝑍 → ((𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))‘𝑛) = (𝑆 D (𝐹‘𝑛)))
245	173, 244	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → ((𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))‘𝑛) = (𝑆 D (𝐹‘𝑛)))
246	21	ad2antrr 717	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘))):𝑍⟶(ℂ ↑_𝑚 𝑋))
247	246, 173	ffvelrnd 6550	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → ((𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))‘𝑛) ∈ (ℂ ↑_𝑚 𝑋))
248	245, 247	eqeltrrd 2845	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝑆 D (𝐹‘𝑛)) ∈ (ℂ ↑_𝑚 𝑋))
249		elmapi 8082	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑆 D (𝐹‘𝑛)) ∈ (ℂ ↑_𝑚 𝑋) → (𝑆 D (𝐹‘𝑛)):𝑋⟶ℂ)
250	248, 249	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝑆 D (𝐹‘𝑛)):𝑋⟶ℂ)
251	250	feqmptd 6438	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝑆 D (𝐹‘𝑛)) = (𝑦 ∈ 𝑋 ↦ ((𝑆 D (𝐹‘𝑛))‘𝑦)))
252	241, 251	eqtr3d 2801	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝑆 D (𝑦 ∈ 𝑋 ↦ ((𝐹‘𝑛)‘𝑦))) = (𝑦 ∈ 𝑋 ↦ ((𝑆 D (𝐹‘𝑛))‘𝑦)))
253		fvexd 6390	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → ((𝑆 D (𝐹‘𝑁))‘𝑦) ∈ V)
254	230	oveq2d 6858	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝑆 D (𝐹‘𝑁)) = (𝑆 D (𝑦 ∈ 𝑋 ↦ ((𝐹‘𝑁)‘𝑦))))
255	26	adantr 472	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝑆 D (𝐹‘𝑁)):𝑋⟶ℂ)
256	255	feqmptd 6438	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝑆 D (𝐹‘𝑁)) = (𝑦 ∈ 𝑋 ↦ ((𝑆 D (𝐹‘𝑁))‘𝑦)))
257	254, 256	eqtr3d 2801	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝑆 D (𝑦 ∈ 𝑋 ↦ ((𝐹‘𝑁)‘𝑦))) = (𝑦 ∈ 𝑋 ↦ ((𝑆 D (𝐹‘𝑁))‘𝑦)))
258	220, 223, 240, 252, 224, 253, 257	dvmptsub 24021	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝑆 D (𝑦 ∈ 𝑋 ↦ (((𝐹‘𝑛)‘𝑦) − ((𝐹‘𝑁)‘𝑦)))) = (𝑦 ∈ 𝑋 ↦ (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦))))
259	239, 258	eqtrd 2799	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝑆 D ((𝐹‘𝑛) ∘_𝑓 − (𝐹‘𝑁))) = (𝑦 ∈ 𝑋 ↦ (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦))))
260	259	dmeqd 5494	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → dom (𝑆 D ((𝐹‘𝑛) ∘_𝑓 − (𝐹‘𝑁))) = dom (𝑦 ∈ 𝑋 ↦ (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦))))
261		ovex 6874	. . . . . . . . . . . . . . 15 ⊢ (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦)) ∈ V
262		eqid 2765	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ 𝑋 ↦ (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦))) = (𝑦 ∈ 𝑋 ↦ (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦)))
263	261, 262	dmmpti 6201	. . . . . . . . . . . . . 14 ⊢ dom (𝑦 ∈ 𝑋 ↦ (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦))) = 𝑋
264	260, 263	syl6eq 2815	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → dom (𝑆 D ((𝐹‘𝑛) ∘_𝑓 − (𝐹‘𝑁))) = 𝑋)
265	238, 264	sseqtr4d 3802	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝐶(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑈) ⊆ dom (𝑆 D ((𝐹‘𝑛) ∘_𝑓 − (𝐹‘𝑁))))
266	66	adantr 472	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → ((𝑅 / 2) / 2) ∈ ℝ)
267	238	sselda 3761	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ (𝐶(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑈)) → 𝑦 ∈ 𝑋)
268	259	fveq1d 6377	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → ((𝑆 D ((𝐹‘𝑛) ∘_𝑓 − (𝐹‘𝑁)))‘𝑦) = ((𝑦 ∈ 𝑋 ↦ (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦)))‘𝑦))
269	262	fvmpt2 6480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ 𝑋 ∧ (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦)) ∈ V) → ((𝑦 ∈ 𝑋 ↦ (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦)))‘𝑦) = (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦)))
270	261, 269	mpan2 682	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ 𝑋 → ((𝑦 ∈ 𝑋 ↦ (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦)))‘𝑦) = (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦)))
271	268, 270	sylan9eq 2819	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → ((𝑆 D ((𝐹‘𝑛) ∘_𝑓 − (𝐹‘𝑁)))‘𝑦) = (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦)))
272	271	fveq2d 6379	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → (abs‘((𝑆 D ((𝐹‘𝑛) ∘_𝑓 − (𝐹‘𝑁)))‘𝑦)) = (abs‘(((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦))))
273	261	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦)) ∈ V)
274	220, 225, 273, 258	dvmptcl 24013	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦)) ∈ ℂ)
275	274	abscld 14460	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → (abs‘(((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦))) ∈ ℝ)
276	66	ad2antrr 717	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → ((𝑅 / 2) / 2) ∈ ℝ)
277	250	ffvelrnda 6549	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → ((𝑆 D (𝐹‘𝑛))‘𝑦) ∈ ℂ)
278	255	ffvelrnda 6549	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → ((𝑆 D (𝐹‘𝑁))‘𝑦) ∈ ℂ)
279	277, 278	abssubd 14477	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → (abs‘(((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦))) = (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑦) − ((𝑆 D (𝐹‘𝑛))‘𝑦))))
280		ulmdvlem1.1	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝜓) → ∀𝑚 ∈ (ℤ_≥‘𝑁)∀𝑥 ∈ 𝑋 (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑚))‘𝑥))) < ((𝑅 / 2) / 2))
281		fveq2 6375	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑚 = 𝑛 → (𝐹‘𝑚) = (𝐹‘𝑛))
282	281	oveq2d 6858	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑚 = 𝑛 → (𝑆 D (𝐹‘𝑚)) = (𝑆 D (𝐹‘𝑛)))
283	282	fveq1d 6377	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑚 = 𝑛 → ((𝑆 D (𝐹‘𝑚))‘𝑥) = ((𝑆 D (𝐹‘𝑛))‘𝑥))
284	283	oveq2d 6858	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 = 𝑛 → (((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑚))‘𝑥)) = (((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑛))‘𝑥)))
285	284	fveq2d 6379	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = 𝑛 → (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑚))‘𝑥))) = (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑛))‘𝑥))))
286	285	breq1d 4819	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = 𝑛 → ((abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑚))‘𝑥))) < ((𝑅 / 2) / 2) ↔ (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑛))‘𝑥))) < ((𝑅 / 2) / 2)))
287	286	ralbidv 3133	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 𝑛 → (∀𝑥 ∈ 𝑋 (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑚))‘𝑥))) < ((𝑅 / 2) / 2) ↔ ∀𝑥 ∈ 𝑋 (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑛))‘𝑥))) < ((𝑅 / 2) / 2)))
288	287	rspccva 3460	. . . . . . . . . . . . . . . . . 18 ⊢ ((∀𝑚 ∈ (ℤ_≥‘𝑁)∀𝑥 ∈ 𝑋 (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑚))‘𝑥))) < ((𝑅 / 2) / 2) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → ∀𝑥 ∈ 𝑋 (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑛))‘𝑥))) < ((𝑅 / 2) / 2))
289	280, 288	sylan 575	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → ∀𝑥 ∈ 𝑋 (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑛))‘𝑥))) < ((𝑅 / 2) / 2))
290		fveq2 6375	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑦 → ((𝑆 D (𝐹‘𝑁))‘𝑥) = ((𝑆 D (𝐹‘𝑁))‘𝑦))
291		fveq2 6375	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑦 → ((𝑆 D (𝐹‘𝑛))‘𝑥) = ((𝑆 D (𝐹‘𝑛))‘𝑦))
292	290, 291	oveq12d 6860	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑦 → (((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑛))‘𝑥)) = (((𝑆 D (𝐹‘𝑁))‘𝑦) − ((𝑆 D (𝐹‘𝑛))‘𝑦)))
293	292	fveq2d 6379	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑦 → (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑛))‘𝑥))) = (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑦) − ((𝑆 D (𝐹‘𝑛))‘𝑦))))
294	293	breq1d 4819	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑦 → ((abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑛))‘𝑥))) < ((𝑅 / 2) / 2) ↔ (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑦) − ((𝑆 D (𝐹‘𝑛))‘𝑦))) < ((𝑅 / 2) / 2)))
295	294	rspccva 3460	. . . . . . . . . . . . . . . . 17 ⊢ ((∀𝑥 ∈ 𝑋 (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑛))‘𝑥))) < ((𝑅 / 2) / 2) ∧ 𝑦 ∈ 𝑋) → (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑦) − ((𝑆 D (𝐹‘𝑛))‘𝑦))) < ((𝑅 / 2) / 2))
296	289, 295	sylan 575	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑦) − ((𝑆 D (𝐹‘𝑛))‘𝑦))) < ((𝑅 / 2) / 2))
297	279, 296	eqbrtrd 4831	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → (abs‘(((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦))) < ((𝑅 / 2) / 2))
298	275, 276, 297	ltled 10439	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → (abs‘(((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦))) ≤ ((𝑅 / 2) / 2))
299	272, 298	eqbrtrd 4831	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → (abs‘((𝑆 D ((𝐹‘𝑛) ∘_𝑓 − (𝐹‘𝑁)))‘𝑦)) ≤ ((𝑅 / 2) / 2))
300	267, 299	syldan 585	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ (𝐶(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑈)) → (abs‘((𝑆 D ((𝐹‘𝑛) ∘_𝑓 − (𝐹‘𝑁)))‘𝑦)) ≤ ((𝑅 / 2) / 2))
301	220, 221, 222, 233, 234, 235, 236, 265, 266, 300	dvlip2 24049	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ (𝑌 ∈ (𝐶(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑈) ∧ 𝐶 ∈ (𝐶(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑈))) → (abs‘((((𝐹‘𝑛) ∘_𝑓 − (𝐹‘𝑁))‘𝑌) − (((𝐹‘𝑛) ∘_𝑓 − (𝐹‘𝑁))‘𝐶))) ≤ (((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶))))
302	219, 301	mpdan 678	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (abs‘((((𝐹‘𝑛) ∘_𝑓 − (𝐹‘𝑁))‘𝑌) − (((𝐹‘𝑛) ∘_𝑓 − (𝐹‘𝑁))‘𝐶))) ≤ (((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶))))
303	197, 302	eqbrtrrd 4833	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (abs‘((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) ≤ (((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶))))
304	303, 174, 180	3brtr4d 4841	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → ((𝑘 ∈ 𝑍 ↦ (abs‘((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))))‘𝑛) ≤ ((𝑍 × {(((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶)))})‘𝑛))
305	77, 81, 165, 171, 177, 182, 304	climle 14655	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → (abs‘(((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) ≤ (((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶))))
306	74	abscld 14460	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → (abs‘(((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) ∈ ℝ)
307	37, 39	absrpcld 14472	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → (abs‘(𝑌 − 𝐶)) ∈ ℝ⁺)
308	306, 66, 307	ledivmul2d 12124	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → (((abs‘(((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) / (abs‘(𝑌 − 𝐶))) ≤ ((𝑅 / 2) / 2) ↔ (abs‘(((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) ≤ (((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶)))))
309	305, 308	mpbird 248	. . . . . 6 ⊢ ((𝜑 ∧ 𝜓) → ((abs‘(((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) / (abs‘(𝑌 − 𝐶))) ≤ ((𝑅 / 2) / 2))
310	76, 309	eqbrtrd 4831	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → (abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)))) ≤ ((𝑅 / 2) / 2))
311	210	rpred 12070	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → 𝑈 ∈ ℝ)
312		ulmdvlem1.v	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → 𝑊 ∈ ℝ⁺)
313	312	rpred 12070	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → 𝑊 ∈ ℝ)
314		ulmdvlem1.l	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → 𝑈 < 𝑊)
315	166, 311, 313, 205, 314	lttrd 10452	. . . . . 6 ⊢ ((𝜑 ∧ 𝜓) → (abs‘(𝑌 − 𝐶)) < 𝑊)
316		ulmdvlem1.4	. . . . . 6 ⊢ ((𝜑 ∧ 𝜓) → ((abs‘(𝑌 − 𝐶)) < 𝑊 → (abs‘(((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)) − ((𝑆 D (𝐹‘𝑁))‘𝐶))) < ((𝑅 / 2) / 2)))
317	315, 316	mpd 15	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → (abs‘(((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)) − ((𝑆 D (𝐹‘𝑁))‘𝐶))) < ((𝑅 / 2) / 2))
318	60, 62, 66, 66, 310, 317	leltaddd 10903	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → ((abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)))) + (abs‘(((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)) − ((𝑆 D (𝐹‘𝑁))‘𝐶)))) < (((𝑅 / 2) / 2) + ((𝑅 / 2) / 2)))
319	64	recnd 10322	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → (𝑅 / 2) ∈ ℂ)
320	319	2halvesd 11524	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → (((𝑅 / 2) / 2) + ((𝑅 / 2) / 2)) = (𝑅 / 2))
321	318, 320	breqtrd 4835	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ((abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)))) + (abs‘(((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)) − ((𝑆 D (𝐹‘𝑁))‘𝐶)))) < (𝑅 / 2))
322	49, 63, 64, 65, 321	lelttrd 10449	. 2 ⊢ ((𝜑 ∧ 𝜓) → (abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((𝑆 D (𝐹‘𝑁))‘𝐶))) < (𝑅 / 2))
323		ulmdvlem1.2	. 2 ⊢ ((𝜑 ∧ 𝜓) → (abs‘(((𝑆 D (𝐹‘𝑁))‘𝐶) − (𝐻‘𝐶))) < (𝑅 / 2))
324	40, 44, 45, 47, 322, 323	abs3lemd 14485	1 ⊢ ((𝜑 ∧ 𝜓) → (abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − (𝐻‘𝐶))) < 𝑅)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 197 ∧ wa 384 = wceq 1652 ∈ wcel 2155 ≠ wne 2937 ∀wral 3055 Vcvv 3350 ⊆ wss 3732 {csn 4334 {cpr 4336 class class class wbr 4809 ↦ cmpt 4888 × cxp 5275 dom cdm 5277 ↾ cres 5279 ∘ ccom 5281 Fn wfn 6063 ⟶wf 6064 ‘cfv 6068 (class class class)co 6842 ∘_𝑓 cof 7093 ↑_𝑚 cmap 8060 ℂcc 10187 ℝcr 10188 + caddc 10192 · cmul 10194 ℝ^*cxr 10327 < clt 10328 ≤ cle 10329 − cmin 10520 / cdiv 10938 2c2 11327 ℤcz 11624 ℤ_≥cuz 11886 ℝ⁺crp 12028 abscabs 14259 ⇝ cli 14500 ∞Metcxmet 20004 ballcbl 20006 D cdv 23918 ⇝_𝑢culm 24421

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1890 ax-4 1904 ax-5 2005 ax-6 2070 ax-7 2105 ax-8 2157 ax-9 2164 ax-10 2183 ax-11 2198 ax-12 2211 ax-13 2352 ax-ext 2743 ax-rep 4930 ax-sep 4941 ax-nul 4949 ax-pow 5001 ax-pr 5062 ax-un 7147 ax-inf2 8753 ax-cnex 10245 ax-resscn 10246 ax-1cn 10247 ax-icn 10248 ax-addcl 10249 ax-addrcl 10250 ax-mulcl 10251 ax-mulrcl 10252 ax-mulcom 10253 ax-addass 10254 ax-mulass 10255 ax-distr 10256 ax-i2m1 10257 ax-1ne0 10258 ax-1rid 10259 ax-rnegex 10260 ax-rrecex 10261 ax-cnre 10262 ax-pre-lttri 10263 ax-pre-lttrn 10264 ax-pre-ltadd 10265 ax-pre-mulgt0 10266 ax-pre-sup 10267 ax-addf 10268 ax-mulf 10269

This theorem depends on definitions: df-bi 198 df-an 385 df-or 874 df-3or 1108 df-3an 1109 df-tru 1656 df-ex 1875 df-nf 1879 df-sb 2063 df-mo 2565 df-eu 2582 df-clab 2752 df-cleq 2758 df-clel 2761 df-nfc 2896 df-ne 2938 df-nel 3041 df-ral 3060 df-rex 3061 df-reu 3062 df-rmo 3063 df-rab 3064 df-v 3352 df-sbc 3597 df-csb 3692 df-dif 3735 df-un 3737 df-in 3739 df-ss 3746 df-pss 3748 df-nul 4080 df-if 4244 df-pw 4317 df-sn 4335 df-pr 4337 df-tp 4339 df-op 4341 df-uni 4595 df-int 4634 df-iun 4678 df-iin 4679 df-br 4810 df-opab 4872 df-mpt 4889 df-tr 4912 df-id 5185 df-eprel 5190 df-po 5198 df-so 5199 df-fr 5236 df-se 5237 df-we 5238 df-xp 5283 df-rel 5284 df-cnv 5285 df-co 5286 df-dm 5287 df-rn 5288 df-res 5289 df-ima 5290 df-pred 5865 df-ord 5911 df-on 5912 df-lim 5913 df-suc 5914 df-iota 6031 df-fun 6070 df-fn 6071 df-f 6072 df-f1 6073 df-fo 6074 df-f1o 6075 df-fv 6076 df-isom 6077 df-riota 6803 df-ov 6845 df-oprab 6846 df-mpt2 6847 df-of 7095 df-om 7264 df-1st 7366 df-2nd 7367 df-supp 7498 df-wrecs 7610 df-recs 7672 df-rdg 7710 df-1o 7764 df-2o 7765 df-oadd 7768 df-er 7947 df-map 8062 df-pm 8063 df-ixp 8114 df-en 8161 df-dom 8162 df-sdom 8163 df-fin 8164 df-fsupp 8483 df-fi 8524 df-sup 8555 df-inf 8556 df-oi 8622 df-card 9016 df-cda 9243 df-pnf 10330 df-mnf 10331 df-xr 10332 df-ltxr 10333 df-le 10334 df-sub 10522 df-neg 10523 df-div 10939 df-nn 11275 df-2 11335 df-3 11336 df-4 11337 df-5 11338 df-6 11339 df-7 11340 df-8 11341 df-9 11342 df-n0 11539 df-z 11625 df-dec 11741 df-uz 11887 df-q 11990 df-rp 12029 df-xneg 12146 df-xadd 12147 df-xmul 12148 df-ioo 12381 df-ico 12383 df-icc 12384 df-fz 12534 df-fzo 12674 df-fl 12801 df-seq 13009 df-exp 13068 df-hash 13322 df-cj 14124 df-re 14125 df-im 14126 df-sqrt 14260 df-abs 14261 df-clim 14504 df-rlim 14505 df-struct 16132 df-ndx 16133 df-slot 16134 df-base 16136 df-sets 16137 df-ress 16138 df-plusg 16227 df-mulr 16228 df-starv 16229 df-sca 16230 df-vsca 16231 df-ip 16232 df-tset 16233 df-ple 16234 df-ds 16236 df-unif 16237 df-hom 16238 df-cco 16239 df-rest 16349 df-topn 16350 df-0g 16368 df-gsum 16369 df-topgen 16370 df-pt 16371 df-prds 16374 df-xrs 16428 df-qtop 16433 df-imas 16434 df-xps 16436 df-mre 16512 df-mrc 16513 df-acs 16515 df-mgm 17508 df-sgrp 17550 df-mnd 17561 df-submnd 17602 df-mulg 17808 df-cntz 18013 df-cmn 18461 df-psmet 20011 df-xmet 20012 df-met 20013 df-bl 20014 df-mopn 20015 df-fbas 20016 df-fg 20017 df-cnfld 20020 df-top 20978 df-topon 20995 df-topsp 21017 df-bases 21030 df-cld 21103 df-ntr 21104 df-cls 21105 df-nei 21182 df-lp 21220 df-perf 21221 df-cn 21311 df-cnp 21312 df-haus 21399 df-cmp 21470 df-tx 21645 df-hmeo 21838 df-fil 21929 df-fm 22021 df-flim 22022 df-flf 22023 df-xms 22404 df-ms 22405 df-tms 22406 df-cncf 22960 df-limc 23921 df-dv 23922 df-ulm 24422

This theorem is referenced by: ulmdvlem3 24447

W3C validator