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 26342

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

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 ∈ wcel 2109 ≠ wne 2925 ∀wral 3044 Vcvv 3444 ⊆ wss 3911 {csn 4585 {cpr 4587 class class class wbr 5102 ↦ cmpt 5183 × cxp 5629 dom cdm 5631 ↾ cres 5633 ∘ ccom 5635 Fn wfn 6494 ⟶wf 6495 ‘cfv 6499 (class class class)co 7369 ∘_f cof 7631 ↑_m cmap 8776 ℂcc 11042 ℝcr 11043 + caddc 11047 · cmul 11049 ℝ^*cxr 11183 < clt 11184 ≤ cle 11185 − cmin 11381 / cdiv 11811 2c2 12217 ℤcz 12505 ℤ_≥cuz 12769 ℝ⁺crp 12927 abscabs 15176 ⇝ cli 15426 ∞Metcxmet 21281 ballcbl 21283 D cdv 25797 ⇝_𝑢culm 26318

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5229 ax-sep 5246 ax-nul 5256 ax-pow 5315 ax-pr 5382 ax-un 7691 ax-cnex 11100 ax-resscn 11101 ax-1cn 11102 ax-icn 11103 ax-addcl 11104 ax-addrcl 11105 ax-mulcl 11106 ax-mulrcl 11107 ax-mulcom 11108 ax-addass 11109 ax-mulass 11110 ax-distr 11111 ax-i2m1 11112 ax-1ne0 11113 ax-1rid 11114 ax-rnegex 11115 ax-rrecex 11116 ax-cnre 11117 ax-pre-lttri 11118 ax-pre-lttrn 11119 ax-pre-ltadd 11120 ax-pre-mulgt0 11121 ax-pre-sup 11122 ax-addf 11123

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3351 df-reu 3352 df-rab 3403 df-v 3446 df-sbc 3751 df-csb 3860 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-pss 3931 df-nul 4293 df-if 4485 df-pw 4561 df-sn 4586 df-pr 4588 df-tp 4590 df-op 4592 df-uni 4868 df-int 4907 df-iun 4953 df-iin 4954 df-br 5103 df-opab 5165 df-mpt 5184 df-tr 5210 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-se 5585 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6262 df-ord 6323 df-on 6324 df-lim 6325 df-suc 6326 df-iota 6452 df-fun 6501 df-fn 6502 df-f 6503 df-f1 6504 df-fo 6505 df-f1o 6506 df-fv 6507 df-isom 6508 df-riota 7326 df-ov 7372 df-oprab 7373 df-mpo 7374 df-of 7633 df-om 7823 df-1st 7947 df-2nd 7948 df-supp 8117 df-frecs 8237 df-wrecs 8268 df-recs 8317 df-rdg 8355 df-1o 8411 df-2o 8412 df-er 8648 df-map 8778 df-pm 8779 df-ixp 8848 df-en 8896 df-dom 8897 df-sdom 8898 df-fin 8899 df-fsupp 9289 df-fi 9338 df-sup 9369 df-inf 9370 df-oi 9439 df-card 9868 df-pnf 11186 df-mnf 11187 df-xr 11188 df-ltxr 11189 df-le 11190 df-sub 11383 df-neg 11384 df-div 11812 df-nn 12163 df-2 12225 df-3 12226 df-4 12227 df-5 12228 df-6 12229 df-7 12230 df-8 12231 df-9 12232 df-n0 12419 df-z 12506 df-dec 12626 df-uz 12770 df-q 12884 df-rp 12928 df-xneg 13048 df-xadd 13049 df-xmul 13050 df-ioo 13286 df-ico 13288 df-icc 13289 df-fz 13445 df-fzo 13592 df-fl 13730 df-seq 13943 df-exp 14003 df-hash 14272 df-cj 15041 df-re 15042 df-im 15043 df-sqrt 15177 df-abs 15178 df-clim 15430 df-rlim 15431 df-struct 17093 df-sets 17110 df-slot 17128 df-ndx 17140 df-base 17156 df-ress 17177 df-plusg 17209 df-mulr 17210 df-starv 17211 df-sca 17212 df-vsca 17213 df-ip 17214 df-tset 17215 df-ple 17216 df-ds 17218 df-unif 17219 df-hom 17220 df-cco 17221 df-rest 17361 df-topn 17362 df-0g 17380 df-gsum 17381 df-topgen 17382 df-pt 17383 df-prds 17386 df-xrs 17441 df-qtop 17446 df-imas 17447 df-xps 17449 df-mre 17523 df-mrc 17524 df-acs 17526 df-mgm 18549 df-sgrp 18628 df-mnd 18644 df-submnd 18693 df-mulg 18982 df-cntz 19231 df-cmn 19696 df-psmet 21288 df-xmet 21289 df-met 21290 df-bl 21291 df-mopn 21292 df-fbas 21293 df-fg 21294 df-cnfld 21297 df-top 22814 df-topon 22831 df-topsp 22853 df-bases 22866 df-cld 22939 df-ntr 22940 df-cls 22941 df-nei 23018 df-lp 23056 df-perf 23057 df-cn 23147 df-cnp 23148 df-haus 23235 df-cmp 23307 df-tx 23482 df-hmeo 23675 df-fil 23766 df-fm 23858 df-flim 23859 df-flf 23860 df-xms 24241 df-ms 24242 df-tms 24243 df-cncf 24804 df-limc 25800 df-dv 25801 df-ulm 26319

This theorem is referenced by: ulmdvlem3 26344

W3C validator