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 26291

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

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

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 = wceq 1533 ∈ wcel 2098 ≠ wne 2934 ∀wral 3055 Vcvv 3468 ⊆ wss 3943 {csn 4623 {cpr 4625 class class class wbr 5141 ↦ cmpt 5224 × cxp 5667 dom cdm 5669 ↾ cres 5671 ∘ ccom 5673 Fn wfn 6532 ⟶wf 6533 ‘cfv 6537 (class class class)co 7405 ∘_f cof 7665 ↑_m cmap 8822 ℂcc 11110 ℝcr 11111 + caddc 11115 · cmul 11117 ℝ^*cxr 11251 < clt 11252 ≤ cle 11253 − cmin 11448 / cdiv 11875 2c2 12271 ℤcz 12562 ℤ_≥cuz 12826 ℝ⁺crp 12980 abscabs 15187 ⇝ cli 15434 ∞Metcxmet 21225 ballcbl 21227 D cdv 25747 ⇝_𝑢culm 26267

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2163 ax-ext 2697 ax-rep 5278 ax-sep 5292 ax-nul 5299 ax-pow 5356 ax-pr 5420 ax-un 7722 ax-cnex 11168 ax-resscn 11169 ax-1cn 11170 ax-icn 11171 ax-addcl 11172 ax-addrcl 11173 ax-mulcl 11174 ax-mulrcl 11175 ax-mulcom 11176 ax-addass 11177 ax-mulass 11178 ax-distr 11179 ax-i2m1 11180 ax-1ne0 11181 ax-1rid 11182 ax-rnegex 11183 ax-rrecex 11184 ax-cnre 11185 ax-pre-lttri 11186 ax-pre-lttrn 11187 ax-pre-ltadd 11188 ax-pre-mulgt0 11189 ax-pre-sup 11190 ax-addf 11191

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2704 df-cleq 2718 df-clel 2804 df-nfc 2879 df-ne 2935 df-nel 3041 df-ral 3056 df-rex 3065 df-rmo 3370 df-reu 3371 df-rab 3427 df-v 3470 df-sbc 3773 df-csb 3889 df-dif 3946 df-un 3948 df-in 3950 df-ss 3960 df-pss 3962 df-nul 4318 df-if 4524 df-pw 4599 df-sn 4624 df-pr 4626 df-tp 4628 df-op 4630 df-uni 4903 df-int 4944 df-iun 4992 df-iin 4993 df-br 5142 df-opab 5204 df-mpt 5225 df-tr 5259 df-id 5567 df-eprel 5573 df-po 5581 df-so 5582 df-fr 5624 df-se 5625 df-we 5626 df-xp 5675 df-rel 5676 df-cnv 5677 df-co 5678 df-dm 5679 df-rn 5680 df-res 5681 df-ima 5682 df-pred 6294 df-ord 6361 df-on 6362 df-lim 6363 df-suc 6364 df-iota 6489 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-isom 6546 df-riota 7361 df-ov 7408 df-oprab 7409 df-mpo 7410 df-of 7667 df-om 7853 df-1st 7974 df-2nd 7975 df-supp 8147 df-frecs 8267 df-wrecs 8298 df-recs 8372 df-rdg 8411 df-1o 8467 df-2o 8468 df-er 8705 df-map 8824 df-pm 8825 df-ixp 8894 df-en 8942 df-dom 8943 df-sdom 8944 df-fin 8945 df-fsupp 9364 df-fi 9408 df-sup 9439 df-inf 9440 df-oi 9507 df-card 9936 df-pnf 11254 df-mnf 11255 df-xr 11256 df-ltxr 11257 df-le 11258 df-sub 11450 df-neg 11451 df-div 11876 df-nn 12217 df-2 12279 df-3 12280 df-4 12281 df-5 12282 df-6 12283 df-7 12284 df-8 12285 df-9 12286 df-n0 12477 df-z 12563 df-dec 12682 df-uz 12827 df-q 12937 df-rp 12981 df-xneg 13098 df-xadd 13099 df-xmul 13100 df-ioo 13334 df-ico 13336 df-icc 13337 df-fz 13491 df-fzo 13634 df-fl 13763 df-seq 13973 df-exp 14033 df-hash 14296 df-cj 15052 df-re 15053 df-im 15054 df-sqrt 15188 df-abs 15189 df-clim 15438 df-rlim 15439 df-struct 17089 df-sets 17106 df-slot 17124 df-ndx 17136 df-base 17154 df-ress 17183 df-plusg 17219 df-mulr 17220 df-starv 17221 df-sca 17222 df-vsca 17223 df-ip 17224 df-tset 17225 df-ple 17226 df-ds 17228 df-unif 17229 df-hom 17230 df-cco 17231 df-rest 17377 df-topn 17378 df-0g 17396 df-gsum 17397 df-topgen 17398 df-pt 17399 df-prds 17402 df-xrs 17457 df-qtop 17462 df-imas 17463 df-xps 17465 df-mre 17539 df-mrc 17540 df-acs 17542 df-mgm 18573 df-sgrp 18652 df-mnd 18668 df-submnd 18714 df-mulg 18996 df-cntz 19233 df-cmn 19702 df-psmet 21232 df-xmet 21233 df-met 21234 df-bl 21235 df-mopn 21236 df-fbas 21237 df-fg 21238 df-cnfld 21241 df-top 22751 df-topon 22768 df-topsp 22790 df-bases 22804 df-cld 22878 df-ntr 22879 df-cls 22880 df-nei 22957 df-lp 22995 df-perf 22996 df-cn 23086 df-cnp 23087 df-haus 23174 df-cmp 23246 df-tx 23421 df-hmeo 23614 df-fil 23705 df-fm 23797 df-flim 23798 df-flf 23799 df-xms 24181 df-ms 24182 df-tms 24183 df-cncf 24753 df-limc 25750 df-dv 25751 df-ulm 26268

This theorem is referenced by: ulmdvlem3 26293

W3C validator