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 25568

Description: Lemma for ulmdv 25571. (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 481	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → 𝐺:𝑋⟶ℂ)
3		ulmdvlem1.y	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → 𝑌 ∈ 𝑋)
4	2, 3	ffvelrnd 6971	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → (𝐺‘𝑌) ∈ ℂ)
5		ulmdvlem1.c	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → 𝐶 ∈ 𝑋)
6	2, 5	ffvelrnd 6971	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → (𝐺‘𝐶) ∈ ℂ)
7	4, 6	subcld 11341	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ((𝐺‘𝑌) − (𝐺‘𝐶)) ∈ ℂ)
8		ulmdvlem1.n	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → 𝑁 ∈ 𝑍)
9		fveq2 6783	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑁 → (𝐹‘𝑘) = (𝐹‘𝑁))
10	9	oveq2d 7300	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑁 → (𝑆 D (𝐹‘𝑘)) = (𝑆 D (𝐹‘𝑁)))
11		eqid 2739	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘))) = (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))
12		ovex 7317	. . . . . . . . . . . 12 ⊢ (𝑆 D (𝐹‘𝑁)) ∈ V
13	10, 11, 12	fvmpt 6884	. . . . . . . . . . 11 ⊢ (𝑁 ∈ 𝑍 → ((𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))‘𝑁) = (𝑆 D (𝐹‘𝑁)))
14	8, 13	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → ((𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))‘𝑁) = (𝑆 D (𝐹‘𝑁)))
15		ovex 7317	. . . . . . . . . . . . . . 15 ⊢ (𝑆 D (𝐹‘𝑘)) ∈ V
16	15	rgenw 3077	. . . . . . . . . . . . . 14 ⊢ ∀𝑘 ∈ 𝑍 (𝑆 D (𝐹‘𝑘)) ∈ V
17	11	fnmpt 6582	. . . . . . . . . . . . . 14 ⊢ (∀𝑘 ∈ 𝑍 (𝑆 D (𝐹‘𝑘)) ∈ V → (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘))) Fn 𝑍)
18	16, 17	mp1i 13	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘))) Fn 𝑍)
19		ulmdv.u	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))(⇝_𝑢‘𝑋)𝐻)
20		ulmf2 25552	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘))) Fn 𝑍 ∧ (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))(⇝_𝑢‘𝑋)𝐻) → (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘))):𝑍⟶(ℂ ↑_m 𝑋))
21	18, 19, 20	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘))):𝑍⟶(ℂ ↑_m 𝑋))
22	21	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘))):𝑍⟶(ℂ ↑_m 𝑋))
23	22, 8	ffvelrnd 6971	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → ((𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))‘𝑁) ∈ (ℂ ↑_m 𝑋))
24	14, 23	eqeltrrd 2841	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → (𝑆 D (𝐹‘𝑁)) ∈ (ℂ ↑_m 𝑋))
25		elmapi 8646	. . . . . . . . 9 ⊢ ((𝑆 D (𝐹‘𝑁)) ∈ (ℂ ↑_m 𝑋) → (𝑆 D (𝐹‘𝑁)):𝑋⟶ℂ)
26	24, 25	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → (𝑆 D (𝐹‘𝑁)):𝑋⟶ℂ)
27	26	fdmd 6620	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → dom (𝑆 D (𝐹‘𝑁)) = 𝑋)
28		dvbsss 25075	. . . . . . 7 ⊢ dom (𝑆 D (𝐹‘𝑁)) ⊆ 𝑆
29	27, 28	eqsstrrdi 3977	. . . . . 6 ⊢ ((𝜑 ∧ 𝜓) → 𝑋 ⊆ 𝑆)
30		ulmdv.s	. . . . . . . 8 ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})
31		recnprss 25077	. . . . . . . 8 ⊢ (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)
32	30, 31	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑆 ⊆ ℂ)
33	32	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝜓) → 𝑆 ⊆ ℂ)
34	29, 33	sstrd 3932	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → 𝑋 ⊆ ℂ)
35	34, 3	sseldd 3923	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝑌 ∈ ℂ)
36	34, 5	sseldd 3923	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝐶 ∈ ℂ)
37	35, 36	subcld 11341	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝑌 − 𝐶) ∈ ℂ)
38		ulmdvlem1.3	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝑌 ≠ 𝐶)
39	35, 36, 38	subne0d 11350	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝑌 − 𝐶) ≠ 0)
40	7, 37, 39	divcld 11760	. 2 ⊢ ((𝜑 ∧ 𝜓) → (((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) ∈ ℂ)
41		ulmcl 25549	. . . . 5 ⊢ ((𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))(⇝_𝑢‘𝑋)𝐻 → 𝐻:𝑋⟶ℂ)
42	19, 41	syl 17	. . . 4 ⊢ (𝜑 → 𝐻:𝑋⟶ℂ)
43	42	adantr 481	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝐻:𝑋⟶ℂ)
44	43, 5	ffvelrnd 6971	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝐻‘𝐶) ∈ ℂ)
45	26, 5	ffvelrnd 6971	. 2 ⊢ ((𝜑 ∧ 𝜓) → ((𝑆 D (𝐹‘𝑁))‘𝐶) ∈ ℂ)
46		ulmdvlem1.r	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝑅 ∈ ℝ⁺)
47	46	rpred 12781	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝑅 ∈ ℝ)
48	40, 45	subcld 11341	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → ((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((𝑆 D (𝐹‘𝑁))‘𝐶)) ∈ ℂ)
49	48	abscld 15157	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((𝑆 D (𝐹‘𝑁))‘𝐶))) ∈ ℝ)
50		ulmdv.f	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑_m 𝑋))
51	50	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → 𝐹:𝑍⟶(ℂ ↑_m 𝑋))
52	51, 8	ffvelrnd 6971	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → (𝐹‘𝑁) ∈ (ℂ ↑_m 𝑋))
53		elmapi 8646	. . . . . . . . . 10 ⊢ ((𝐹‘𝑁) ∈ (ℂ ↑_m 𝑋) → (𝐹‘𝑁):𝑋⟶ℂ)
54	52, 53	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → (𝐹‘𝑁):𝑋⟶ℂ)
55	54, 3	ffvelrnd 6971	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → ((𝐹‘𝑁)‘𝑌) ∈ ℂ)
56	54, 5	ffvelrnd 6971	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → ((𝐹‘𝑁)‘𝐶) ∈ ℂ)
57	55, 56	subcld 11341	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → (((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) ∈ ℂ)
58	57, 37, 39	divcld 11760	. . . . . 6 ⊢ ((𝜑 ∧ 𝜓) → ((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)) ∈ ℂ)
59	40, 58	subcld 11341	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → ((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶))) ∈ ℂ)
60	59	abscld 15157	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → (abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)))) ∈ ℝ)
61	58, 45	subcld 11341	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → (((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)) − ((𝑆 D (𝐹‘𝑁))‘𝐶)) ∈ ℂ)
62	61	abscld 15157	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → (abs‘(((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)) − ((𝑆 D (𝐹‘𝑁))‘𝐶))) ∈ ℝ)
63	60, 62	readdcld 11013	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ((abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)))) + (abs‘(((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)) − ((𝑆 D (𝐹‘𝑁))‘𝐶)))) ∈ ℝ)
64	47	rehalfcld 12229	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝑅 / 2) ∈ ℝ)
65	40, 45, 58	abs3difd 15181	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((𝑆 D (𝐹‘𝑁))‘𝐶))) ≤ ((abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)))) + (abs‘(((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)) − ((𝑆 D (𝐹‘𝑁))‘𝐶)))))
66	64	rehalfcld 12229	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → ((𝑅 / 2) / 2) ∈ ℝ)
67	4, 55, 6, 56	sub4d 11390	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → (((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶))) = (((𝐺‘𝑌) − (𝐺‘𝐶)) − (((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶))))
68	67	oveq1d 7299	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → ((((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶))) / (𝑌 − 𝐶)) = ((((𝐺‘𝑌) − (𝐺‘𝐶)) − (((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶))) / (𝑌 − 𝐶)))
69	7, 57, 37, 39	divsubdird 11799	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → ((((𝐺‘𝑌) − (𝐺‘𝐶)) − (((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶))) / (𝑌 − 𝐶)) = ((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶))))
70	68, 69	eqtrd 2779	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → ((((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶))) / (𝑌 − 𝐶)) = ((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶))))
71	70	fveq2d 6787	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → (abs‘((((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶))) / (𝑌 − 𝐶))) = (abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)))))
72	4, 55	subcld 11341	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → ((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) ∈ ℂ)
73	6, 56	subcld 11341	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶)) ∈ ℂ)
74	72, 73	subcld 11341	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → (((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶))) ∈ ℂ)
75	74, 37, 39	absdivd 15176	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → (abs‘((((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶))) / (𝑌 − 𝐶))) = ((abs‘(((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) / (abs‘(𝑌 − 𝐶))))
76	71, 75	eqtr3d 2781	. . . . . 6 ⊢ ((𝜑 ∧ 𝜓) → (abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)))) = ((abs‘(((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) / (abs‘(𝑌 − 𝐶))))
77		eqid 2739	. . . . . . . 8 ⊢ (ℤ_≥‘𝑁) = (ℤ_≥‘𝑁)
78		ulmdv.z	. . . . . . . . . 10 ⊢ 𝑍 = (ℤ_≥‘𝑀)
79	8, 78	eleqtrdi 2850	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → 𝑁 ∈ (ℤ_≥‘𝑀))
80		eluzelz 12601	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → 𝑁 ∈ ℤ)
81	79, 80	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → 𝑁 ∈ ℤ)
82		ulmdv.m	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℤ)
83	82	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → 𝑀 ∈ ℤ)
84		fveq2 6783	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑌 → ((𝐹‘𝑘)‘𝑧) = ((𝐹‘𝑘)‘𝑌))
85	84	mpteq2dv 5177	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑌 → (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑧)) = (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑌)))
86		fveq2 6783	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑌 → (𝐺‘𝑧) = (𝐺‘𝑌))
87	85, 86	breq12d 5088	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑌 → ((𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑧)) ⇝ (𝐺‘𝑧) ↔ (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑌)) ⇝ (𝐺‘𝑌)))
88		ulmdv.l	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑧)) ⇝ (𝐺‘𝑧))
89	88	ralrimiva 3104	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑧 ∈ 𝑋 (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑧)) ⇝ (𝐺‘𝑧))
90	89	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → ∀𝑧 ∈ 𝑋 (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑧)) ⇝ (𝐺‘𝑧))
91	87, 90, 3	rspcdva 3563	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑌)) ⇝ (𝐺‘𝑌))
92	78	fvexi 6797	. . . . . . . . . . . . 13 ⊢ 𝑍 ∈ V
93	92	mptex 7108	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌))) ∈ V
94	93	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌))) ∈ V)
95		fveq2 6783	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑛 → (𝐹‘𝑘) = (𝐹‘𝑛))
96	95	fveq1d 6785	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑛 → ((𝐹‘𝑘)‘𝑌) = ((𝐹‘𝑛)‘𝑌))
97		eqid 2739	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑌)) = (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑌))
98		fvex 6796	. . . . . . . . . . . . . 14 ⊢ ((𝐹‘𝑛)‘𝑌) ∈ V
99	96, 97, 98	fvmpt 6884	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ 𝑍 → ((𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑌))‘𝑛) = ((𝐹‘𝑛)‘𝑌))
100	99	adantl 482	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑌))‘𝑛) = ((𝐹‘𝑛)‘𝑌))
101	51	ffvelrnda 6970	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ∈ (ℂ ↑_m 𝑋))
102		elmapi 8646	. . . . . . . . . . . . . 14 ⊢ ((𝐹‘𝑛) ∈ (ℂ ↑_m 𝑋) → (𝐹‘𝑛):𝑋⟶ℂ)
103	101, 102	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛):𝑋⟶ℂ)
104	3	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → 𝑌 ∈ 𝑋)
105	103, 104	ffvelrnd 6971	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝐹‘𝑛)‘𝑌) ∈ ℂ)
106	100, 105	eqeltrd 2840	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑌))‘𝑛) ∈ ℂ)
107	96	oveq1d 7299	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑛 → (((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) = (((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)))
108		eqid 2739	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌))) = (𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)))
109		ovex 7317	. . . . . . . . . . . . . 14 ⊢ (((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) ∈ V
110	107, 108, 109	fvmpt 6884	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ 𝑍 → ((𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)))‘𝑛) = (((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)))
111	110	adantl 482	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)))‘𝑛) = (((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)))
112	100	oveq1d 7299	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → (((𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑌))‘𝑛) − ((𝐹‘𝑁)‘𝑌)) = (((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)))
113	111, 112	eqtr4d 2782	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)))‘𝑛) = (((𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑌))‘𝑛) − ((𝐹‘𝑁)‘𝑌)))
114	78, 83, 91, 55, 94, 106, 113	climsubc1 15356	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌))) ⇝ ((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)))
115	92	mptex 7108	. . . . . . . . . . 11 ⊢ (𝑘 ∈ 𝑍 ↦ ((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) ∈ V
116	115	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝑍 ↦ ((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) ∈ V)
117		fveq2 6783	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝐶 → ((𝐹‘𝑘)‘𝑧) = ((𝐹‘𝑘)‘𝐶))
118	117	mpteq2dv 5177	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝐶 → (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑧)) = (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝐶)))
119		fveq2 6783	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝐶 → (𝐺‘𝑧) = (𝐺‘𝐶))
120	118, 119	breq12d 5088	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝐶 → ((𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑧)) ⇝ (𝐺‘𝑧) ↔ (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝐶)) ⇝ (𝐺‘𝐶)))
121	120, 90, 5	rspcdva 3563	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝐶)) ⇝ (𝐺‘𝐶))
122	92	mptex 7108	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))) ∈ V
123	122	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))) ∈ V)
124	95	fveq1d 6785	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑛 → ((𝐹‘𝑘)‘𝐶) = ((𝐹‘𝑛)‘𝐶))
125		eqid 2739	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝐶)) = (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝐶))
126		fvex 6796	. . . . . . . . . . . . . 14 ⊢ ((𝐹‘𝑛)‘𝐶) ∈ V
127	124, 125, 126	fvmpt 6884	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ 𝑍 → ((𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝐶))‘𝑛) = ((𝐹‘𝑛)‘𝐶))
128	127	adantl 482	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝐶))‘𝑛) = ((𝐹‘𝑛)‘𝐶))
129	5	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → 𝐶 ∈ 𝑋)
130	103, 129	ffvelrnd 6971	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝐹‘𝑛)‘𝐶) ∈ ℂ)
131	128, 130	eqeltrd 2840	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝐶))‘𝑛) ∈ ℂ)
132	124	oveq1d 7299	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑛 → (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)) = (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))
133		eqid 2739	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))) = (𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))
134		ovex 7317	. . . . . . . . . . . . . 14 ⊢ (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)) ∈ V
135	132, 133, 134	fvmpt 6884	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ 𝑍 → ((𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))‘𝑛) = (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))
136	135	adantl 482	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))‘𝑛) = (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))
137	128	oveq1d 7299	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → (((𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝐶))‘𝑛) − ((𝐹‘𝑁)‘𝐶)) = (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))
138	136, 137	eqtr4d 2782	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))‘𝑛) = (((𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝐶))‘𝑛) − ((𝐹‘𝑁)‘𝐶)))
139	78, 83, 121, 56, 123, 131, 138	climsubc1 15356	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))) ⇝ ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶)))
140	55	adantr 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝐹‘𝑁)‘𝑌) ∈ ℂ)
141	105, 140	subcld 11341	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → (((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) ∈ ℂ)
142	111, 141	eqeltrd 2840	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)))‘𝑛) ∈ ℂ)
143	56	adantr 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝐹‘𝑁)‘𝐶) ∈ ℂ)
144	130, 143	subcld 11341	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)) ∈ ℂ)
145	136, 144	eqeltrd 2840	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))‘𝑛) ∈ ℂ)
146	107, 132	oveq12d 7302	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑛 → ((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))) = ((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))
147		eqid 2739	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ 𝑍 ↦ ((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) = (𝑘 ∈ 𝑍 ↦ ((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))
148		ovex 7317	. . . . . . . . . . . . 13 ⊢ ((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶))) ∈ V
149	146, 147, 148	fvmpt 6884	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ 𝑍 → ((𝑘 ∈ 𝑍 ↦ ((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))‘𝑛) = ((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))
150	149	adantl 482	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ ((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))‘𝑛) = ((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))
151	111, 136	oveq12d 7302	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → (((𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)))‘𝑛) − ((𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))‘𝑛)) = ((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))
152	150, 151	eqtr4d 2782	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ ((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))‘𝑛) = (((𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)))‘𝑛) − ((𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))‘𝑛)))
153	78, 83, 114, 116, 139, 142, 145, 152	climsub 15352	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝑍 ↦ ((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) ⇝ (((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶))))
154	92	mptex 7108	. . . . . . . . . 10 ⊢ (𝑘 ∈ 𝑍 ↦ (abs‘((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))) ∈ V
155	154	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝑍 ↦ (abs‘((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))) ∈ V)
156	141, 144	subcld 11341	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶))) ∈ ℂ)
157	150, 156	eqeltrd 2840	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ ((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))‘𝑛) ∈ ℂ)
158	146	fveq2d 6787	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑛 → (abs‘((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) = (abs‘((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))))
159		eqid 2739	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ 𝑍 ↦ (abs‘((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))) = (𝑘 ∈ 𝑍 ↦ (abs‘((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))))
160		fvex 6796	. . . . . . . . . . . 12 ⊢ (abs‘((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) ∈ V
161	158, 159, 160	fvmpt 6884	. . . . . . . . . . 11 ⊢ (𝑛 ∈ 𝑍 → ((𝑘 ∈ 𝑍 ↦ (abs‘((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))))‘𝑛) = (abs‘((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))))
162	161	adantl 482	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ (abs‘((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))))‘𝑛) = (abs‘((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))))
163	150	fveq2d 6787	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → (abs‘((𝑘 ∈ 𝑍 ↦ ((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))‘𝑛)) = (abs‘((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))))
164	162, 163	eqtr4d 2782	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ (abs‘((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))))‘𝑛) = (abs‘((𝑘 ∈ 𝑍 ↦ ((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))‘𝑛)))
165	78, 153, 155, 83, 157, 164	climabs 15322	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝑍 ↦ (abs‘((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))) ⇝ (abs‘(((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶)))))
166	37	abscld 15157	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → (abs‘(𝑌 − 𝐶)) ∈ ℝ)
167	66, 166	remulcld 11014	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → (((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶))) ∈ ℝ)
168	167	recnd 11012	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → (((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶))) ∈ ℂ)
169	78	eqimss2i 3981	. . . . . . . . . 10 ⊢ (ℤ_≥‘𝑀) ⊆ 𝑍
170	169, 92	climconst2 15266	. . . . . . . . 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 12610	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → 𝑛 ∈ 𝑍)
173	8, 172	sylan 580	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → 𝑛 ∈ 𝑍)
174	173, 161	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → ((𝑘 ∈ 𝑍 ↦ (abs‘((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))))‘𝑛) = (abs‘((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))))
175	156	abscld 15157	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → (abs‘((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) ∈ ℝ)
176	173, 175	syldan 591	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (abs‘((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) ∈ ℝ)
177	174, 176	eqeltrd 2840	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → ((𝑘 ∈ 𝑍 ↦ (abs‘((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))))‘𝑛) ∈ ℝ)
178		ovex 7317	. . . . . . . . . . 11 ⊢ (((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶))) ∈ V
179	178	fvconst2 7088	. . . . . . . . . 10 ⊢ (𝑛 ∈ 𝑍 → ((𝑍 × {(((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶)))})‘𝑛) = (((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶))))
180	173, 179	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → ((𝑍 × {(((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶)))})‘𝑛) = (((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶))))
181	167	adantr 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶))) ∈ ℝ)
182	180, 181	eqeltrd 2840	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → ((𝑍 × {(((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶)))})‘𝑛) ∈ ℝ)
183	173, 103	syldan 591	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝐹‘𝑛):𝑋⟶ℂ)
184	183	ffnd 6610	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝐹‘𝑛) Fn 𝑋)
185	54	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝐹‘𝑁):𝑋⟶ℂ)
186	185	ffnd 6610	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝐹‘𝑁) Fn 𝑋)
187		ulmscl 25547	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))(⇝_𝑢‘𝑋)𝐻 → 𝑋 ∈ V)
188	19, 187	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑋 ∈ V)
189	188	ad2antrr 723	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → 𝑋 ∈ V)
190	3	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → 𝑌 ∈ 𝑋)
191		fnfvof 7559	. . . . . . . . . . . . 13 ⊢ ((((𝐹‘𝑛) Fn 𝑋 ∧ (𝐹‘𝑁) Fn 𝑋) ∧ (𝑋 ∈ V ∧ 𝑌 ∈ 𝑋)) → (((𝐹‘𝑛) ∘_f − (𝐹‘𝑁))‘𝑌) = (((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)))
192	184, 186, 189, 190, 191	syl22anc 836	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (((𝐹‘𝑛) ∘_f − (𝐹‘𝑁))‘𝑌) = (((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)))
193	5	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → 𝐶 ∈ 𝑋)
194		fnfvof 7559	. . . . . . . . . . . . 13 ⊢ ((((𝐹‘𝑛) Fn 𝑋 ∧ (𝐹‘𝑁) Fn 𝑋) ∧ (𝑋 ∈ V ∧ 𝐶 ∈ 𝑋)) → (((𝐹‘𝑛) ∘_f − (𝐹‘𝑁))‘𝐶) = (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))
195	184, 186, 189, 193, 194	syl22anc 836	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (((𝐹‘𝑛) ∘_f − (𝐹‘𝑁))‘𝐶) = (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))
196	192, 195	oveq12d 7302	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → ((((𝐹‘𝑛) ∘_f − (𝐹‘𝑁))‘𝑌) − (((𝐹‘𝑛) ∘_f − (𝐹‘𝑁))‘𝐶)) = ((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))
197	196	fveq2d 6787	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (abs‘((((𝐹‘𝑛) ∘_f − (𝐹‘𝑁))‘𝑌) − (((𝐹‘𝑛) ∘_f − (𝐹‘𝑁))‘𝐶))) = (abs‘((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))))
198	29, 3	sseldd 3923	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝜓) → 𝑌 ∈ 𝑆)
199	29, 5	sseldd 3923	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝜓) → 𝐶 ∈ 𝑆)
200	198, 199	ovresd 7448	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝜓) → (𝑌((abs ∘ − ) ↾ (𝑆 × 𝑆))𝐶) = (𝑌(abs ∘ − )𝐶))
201		eqid 2739	. . . . . . . . . . . . . . . . . 18 ⊢ (abs ∘ − ) = (abs ∘ − )
202	201	cnmetdval 23943	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑌 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝑌(abs ∘ − )𝐶) = (abs‘(𝑌 − 𝐶)))
203	35, 36, 202	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝜓) → (𝑌(abs ∘ − )𝐶) = (abs‘(𝑌 − 𝐶)))
204	200, 203	eqtrd 2779	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → (𝑌((abs ∘ − ) ↾ (𝑆 × 𝑆))𝐶) = (abs‘(𝑌 − 𝐶)))
205		ulmdvlem1.a	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → (abs‘(𝑌 − 𝐶)) < 𝑈)
206	204, 205	eqbrtrd 5097	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → (𝑌((abs ∘ − ) ↾ (𝑆 × 𝑆))𝐶) < 𝑈)
207		cnxmet 23945	. . . . . . . . . . . . . . . 16 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
208		xmetres2 23523	. . . . . . . . . . . . . . . 16 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑆 ⊆ ℂ) → ((abs ∘ − ) ↾ (𝑆 × 𝑆)) ∈ (∞Met‘𝑆))
209	207, 33, 208	sylancr 587	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → ((abs ∘ − ) ↾ (𝑆 × 𝑆)) ∈ (∞Met‘𝑆))
210		ulmdvlem1.u	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝜓) → 𝑈 ∈ ℝ⁺)
211	210	rpxrd 12782	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → 𝑈 ∈ ℝ^*)
212		elbl3 23554	. . . . . . . . . . . . . . 15 ⊢ (((((abs ∘ − ) ↾ (𝑆 × 𝑆)) ∈ (∞Met‘𝑆) ∧ 𝑈 ∈ ℝ^*) ∧ (𝐶 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆)) → (𝑌 ∈ (𝐶(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑈) ↔ (𝑌((abs ∘ − ) ↾ (𝑆 × 𝑆))𝐶) < 𝑈))
213	209, 211, 199, 198, 212	syl22anc 836	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → (𝑌 ∈ (𝐶(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑈) ↔ (𝑌((abs ∘ − ) ↾ (𝑆 × 𝑆))𝐶) < 𝑈))
214	206, 213	mpbird 256	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → 𝑌 ∈ (𝐶(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑈))
215	214	adantr 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → 𝑌 ∈ (𝐶(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑈))
216		blcntr 23575	. . . . . . . . . . . . . 14 ⊢ ((((abs ∘ − ) ↾ (𝑆 × 𝑆)) ∈ (∞Met‘𝑆) ∧ 𝐶 ∈ 𝑆 ∧ 𝑈 ∈ ℝ⁺) → 𝐶 ∈ (𝐶(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑈))
217	209, 199, 210, 216	syl3anc 1370	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → 𝐶 ∈ (𝐶(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑈))
218	217	adantr 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → 𝐶 ∈ (𝐶(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑈))
219	215, 218	jca 512	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝑌 ∈ (𝐶(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑈) ∧ 𝐶 ∈ (𝐶(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑈)))
220	30	ad2antrr 723	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → 𝑆 ∈ {ℝ, ℂ})
221		eqid 2739	. . . . . . . . . . . 12 ⊢ ((abs ∘ − ) ↾ (𝑆 × 𝑆)) = ((abs ∘ − ) ↾ (𝑆 × 𝑆))
222	29	adantr 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → 𝑋 ⊆ 𝑆)
223		fvexd 6798	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → ((𝐹‘𝑛)‘𝑦) ∈ V)
224		fvexd 6798	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → ((𝐹‘𝑁)‘𝑦) ∈ V)
225	183	feqmptd 6846	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝐹‘𝑛) = (𝑦 ∈ 𝑋 ↦ ((𝐹‘𝑛)‘𝑦)))
226	185	feqmptd 6846	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝐹‘𝑁) = (𝑦 ∈ 𝑋 ↦ ((𝐹‘𝑁)‘𝑦)))
227	189, 223, 224, 225, 226	offval2 7562	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → ((𝐹‘𝑛) ∘_f − (𝐹‘𝑁)) = (𝑦 ∈ 𝑋 ↦ (((𝐹‘𝑛)‘𝑦) − ((𝐹‘𝑁)‘𝑦))))
228	183	ffvelrnda 6970	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → ((𝐹‘𝑛)‘𝑦) ∈ ℂ)
229	185	ffvelrnda 6970	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → ((𝐹‘𝑁)‘𝑦) ∈ ℂ)
230	228, 229	subcld 11341	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → (((𝐹‘𝑛)‘𝑦) − ((𝐹‘𝑁)‘𝑦)) ∈ ℂ)
231	227, 230	fmpt3d 6999	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → ((𝐹‘𝑛) ∘_f − (𝐹‘𝑁)):𝑋⟶ℂ)
232	199	adantr 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → 𝐶 ∈ 𝑆)
233	211	adantr 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → 𝑈 ∈ ℝ^*)
234		eqid 2739	. . . . . . . . . . . 12 ⊢ (𝐶(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑈) = (𝐶(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑈)
235		ulmdvlem1.b	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → (𝐶(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑈) ⊆ 𝑋)
236	235	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝐶(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑈) ⊆ 𝑋)
237	227	oveq2d 7300	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝑆 D ((𝐹‘𝑛) ∘_f − (𝐹‘𝑁))) = (𝑆 D (𝑦 ∈ 𝑋 ↦ (((𝐹‘𝑛)‘𝑦) − ((𝐹‘𝑁)‘𝑦)))))
238		fvexd 6798	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → ((𝑆 D (𝐹‘𝑛))‘𝑦) ∈ V)
239	225	oveq2d 7300	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝑆 D (𝐹‘𝑛)) = (𝑆 D (𝑦 ∈ 𝑋 ↦ ((𝐹‘𝑛)‘𝑦))))
240	95	oveq2d 7300	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = 𝑛 → (𝑆 D (𝐹‘𝑘)) = (𝑆 D (𝐹‘𝑛)))
241		ovex 7317	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑆 D (𝐹‘𝑛)) ∈ V
242	240, 11, 241	fvmpt 6884	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ 𝑍 → ((𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))‘𝑛) = (𝑆 D (𝐹‘𝑛)))
243	173, 242	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → ((𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))‘𝑛) = (𝑆 D (𝐹‘𝑛)))
244	21	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘))):𝑍⟶(ℂ ↑_m 𝑋))
245	244, 173	ffvelrnd 6971	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → ((𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))‘𝑛) ∈ (ℂ ↑_m 𝑋))
246	243, 245	eqeltrrd 2841	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝑆 D (𝐹‘𝑛)) ∈ (ℂ ↑_m 𝑋))
247		elmapi 8646	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑆 D (𝐹‘𝑛)) ∈ (ℂ ↑_m 𝑋) → (𝑆 D (𝐹‘𝑛)):𝑋⟶ℂ)
248	246, 247	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝑆 D (𝐹‘𝑛)):𝑋⟶ℂ)
249	248	feqmptd 6846	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝑆 D (𝐹‘𝑛)) = (𝑦 ∈ 𝑋 ↦ ((𝑆 D (𝐹‘𝑛))‘𝑦)))
250	239, 249	eqtr3d 2781	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝑆 D (𝑦 ∈ 𝑋 ↦ ((𝐹‘𝑛)‘𝑦))) = (𝑦 ∈ 𝑋 ↦ ((𝑆 D (𝐹‘𝑛))‘𝑦)))
251		fvexd 6798	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → ((𝑆 D (𝐹‘𝑁))‘𝑦) ∈ V)
252	226	oveq2d 7300	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝑆 D (𝐹‘𝑁)) = (𝑆 D (𝑦 ∈ 𝑋 ↦ ((𝐹‘𝑁)‘𝑦))))
253	26	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝑆 D (𝐹‘𝑁)):𝑋⟶ℂ)
254	253	feqmptd 6846	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝑆 D (𝐹‘𝑁)) = (𝑦 ∈ 𝑋 ↦ ((𝑆 D (𝐹‘𝑁))‘𝑦)))
255	252, 254	eqtr3d 2781	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝑆 D (𝑦 ∈ 𝑋 ↦ ((𝐹‘𝑁)‘𝑦))) = (𝑦 ∈ 𝑋 ↦ ((𝑆 D (𝐹‘𝑁))‘𝑦)))
256	220, 228, 238, 250, 229, 251, 255	dvmptsub 25140	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝑆 D (𝑦 ∈ 𝑋 ↦ (((𝐹‘𝑛)‘𝑦) − ((𝐹‘𝑁)‘𝑦)))) = (𝑦 ∈ 𝑋 ↦ (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦))))
257	237, 256	eqtrd 2779	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝑆 D ((𝐹‘𝑛) ∘_f − (𝐹‘𝑁))) = (𝑦 ∈ 𝑋 ↦ (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦))))
258	257	dmeqd 5817	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → dom (𝑆 D ((𝐹‘𝑛) ∘_f − (𝐹‘𝑁))) = dom (𝑦 ∈ 𝑋 ↦ (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦))))
259		ovex 7317	. . . . . . . . . . . . . . 15 ⊢ (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦)) ∈ V
260		eqid 2739	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ 𝑋 ↦ (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦))) = (𝑦 ∈ 𝑋 ↦ (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦)))
261	259, 260	dmmpti 6586	. . . . . . . . . . . . . 14 ⊢ dom (𝑦 ∈ 𝑋 ↦ (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦))) = 𝑋
262	258, 261	eqtrdi 2795	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → dom (𝑆 D ((𝐹‘𝑛) ∘_f − (𝐹‘𝑁))) = 𝑋)
263	236, 262	sseqtrrd 3963	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝐶(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑈) ⊆ dom (𝑆 D ((𝐹‘𝑛) ∘_f − (𝐹‘𝑁))))
264	66	adantr 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → ((𝑅 / 2) / 2) ∈ ℝ)
265	236	sselda 3922	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ (𝐶(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑈)) → 𝑦 ∈ 𝑋)
266	257	fveq1d 6785	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → ((𝑆 D ((𝐹‘𝑛) ∘_f − (𝐹‘𝑁)))‘𝑦) = ((𝑦 ∈ 𝑋 ↦ (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦)))‘𝑦))
267	260	fvmpt2 6895	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ 𝑋 ∧ (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦)) ∈ V) → ((𝑦 ∈ 𝑋 ↦ (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦)))‘𝑦) = (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦)))
268	259, 267	mpan2 688	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ 𝑋 → ((𝑦 ∈ 𝑋 ↦ (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦)))‘𝑦) = (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦)))
269	266, 268	sylan9eq 2799	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → ((𝑆 D ((𝐹‘𝑛) ∘_f − (𝐹‘𝑁)))‘𝑦) = (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦)))
270	269	fveq2d 6787	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → (abs‘((𝑆 D ((𝐹‘𝑛) ∘_f − (𝐹‘𝑁)))‘𝑦)) = (abs‘(((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦))))
271	259	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦)) ∈ V)
272	220, 230, 271, 256	dvmptcl 25132	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦)) ∈ ℂ)
273	272	abscld 15157	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → (abs‘(((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦))) ∈ ℝ)
274	66	ad2antrr 723	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → ((𝑅 / 2) / 2) ∈ ℝ)
275	248	ffvelrnda 6970	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → ((𝑆 D (𝐹‘𝑛))‘𝑦) ∈ ℂ)
276	253	ffvelrnda 6970	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → ((𝑆 D (𝐹‘𝑁))‘𝑦) ∈ ℂ)
277	275, 276	abssubd 15174	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → (abs‘(((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦))) = (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑦) − ((𝑆 D (𝐹‘𝑛))‘𝑦))))
278		ulmdvlem1.1	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝜓) → ∀𝑚 ∈ (ℤ_≥‘𝑁)∀𝑥 ∈ 𝑋 (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑚))‘𝑥))) < ((𝑅 / 2) / 2))
279		fveq2 6783	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑚 = 𝑛 → (𝐹‘𝑚) = (𝐹‘𝑛))
280	279	oveq2d 7300	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑚 = 𝑛 → (𝑆 D (𝐹‘𝑚)) = (𝑆 D (𝐹‘𝑛)))
281	280	fveq1d 6785	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑚 = 𝑛 → ((𝑆 D (𝐹‘𝑚))‘𝑥) = ((𝑆 D (𝐹‘𝑛))‘𝑥))
282	281	oveq2d 7300	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 = 𝑛 → (((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑚))‘𝑥)) = (((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑛))‘𝑥)))
283	282	fveq2d 6787	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = 𝑛 → (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑚))‘𝑥))) = (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑛))‘𝑥))))
284	283	breq1d 5085	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = 𝑛 → ((abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑚))‘𝑥))) < ((𝑅 / 2) / 2) ↔ (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑛))‘𝑥))) < ((𝑅 / 2) / 2)))
285	284	ralbidv 3113	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 𝑛 → (∀𝑥 ∈ 𝑋 (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑚))‘𝑥))) < ((𝑅 / 2) / 2) ↔ ∀𝑥 ∈ 𝑋 (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑛))‘𝑥))) < ((𝑅 / 2) / 2)))
286	285	rspccva 3561	. . . . . . . . . . . . . . . . . 18 ⊢ ((∀𝑚 ∈ (ℤ_≥‘𝑁)∀𝑥 ∈ 𝑋 (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑚))‘𝑥))) < ((𝑅 / 2) / 2) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → ∀𝑥 ∈ 𝑋 (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑛))‘𝑥))) < ((𝑅 / 2) / 2))
287	278, 286	sylan 580	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → ∀𝑥 ∈ 𝑋 (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑛))‘𝑥))) < ((𝑅 / 2) / 2))
288		fveq2 6783	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑦 → ((𝑆 D (𝐹‘𝑁))‘𝑥) = ((𝑆 D (𝐹‘𝑁))‘𝑦))
289		fveq2 6783	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑦 → ((𝑆 D (𝐹‘𝑛))‘𝑥) = ((𝑆 D (𝐹‘𝑛))‘𝑦))
290	288, 289	oveq12d 7302	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑦 → (((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑛))‘𝑥)) = (((𝑆 D (𝐹‘𝑁))‘𝑦) − ((𝑆 D (𝐹‘𝑛))‘𝑦)))
291	290	fveq2d 6787	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑦 → (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑛))‘𝑥))) = (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑦) − ((𝑆 D (𝐹‘𝑛))‘𝑦))))
292	291	breq1d 5085	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑦 → ((abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑛))‘𝑥))) < ((𝑅 / 2) / 2) ↔ (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑦) − ((𝑆 D (𝐹‘𝑛))‘𝑦))) < ((𝑅 / 2) / 2)))
293	292	rspccva 3561	. . . . . . . . . . . . . . . . 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 5097	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → (abs‘(((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦))) < ((𝑅 / 2) / 2))
296	273, 274, 295	ltled 11132	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → (abs‘(((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦))) ≤ ((𝑅 / 2) / 2))
297	270, 296	eqbrtrd 5097	. . . . . . . . . . . . 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 25168	. . . . . . . . . . 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 5099	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (abs‘((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) ≤ (((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶))))
302	301, 174, 180	3brtr4d 5107	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → ((𝑘 ∈ 𝑍 ↦ (abs‘((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))))‘𝑛) ≤ ((𝑍 × {(((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶)))})‘𝑛))
303	77, 81, 165, 171, 177, 182, 302	climle 15358	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → (abs‘(((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) ≤ (((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶))))
304	74	abscld 15157	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → (abs‘(((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) ∈ ℝ)
305	37, 39	absrpcld 15169	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → (abs‘(𝑌 − 𝐶)) ∈ ℝ⁺)
306	304, 66, 305	ledivmul2d 12835	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → (((abs‘(((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) / (abs‘(𝑌 − 𝐶))) ≤ ((𝑅 / 2) / 2) ↔ (abs‘(((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) ≤ (((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶)))))
307	303, 306	mpbird 256	. . . . . 6 ⊢ ((𝜑 ∧ 𝜓) → ((abs‘(((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) / (abs‘(𝑌 − 𝐶))) ≤ ((𝑅 / 2) / 2))
308	76, 307	eqbrtrd 5097	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → (abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)))) ≤ ((𝑅 / 2) / 2))
309	210	rpred 12781	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → 𝑈 ∈ ℝ)
310		ulmdvlem1.v	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → 𝑊 ∈ ℝ⁺)
311	310	rpred 12781	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → 𝑊 ∈ ℝ)
312		ulmdvlem1.l	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → 𝑈 < 𝑊)
313	166, 309, 311, 205, 312	lttrd 11145	. . . . . 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 11606	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → ((abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)))) + (abs‘(((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)) − ((𝑆 D (𝐹‘𝑁))‘𝐶)))) < (((𝑅 / 2) / 2) + ((𝑅 / 2) / 2)))
317	64	recnd 11012	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → (𝑅 / 2) ∈ ℂ)
318	317	2halvesd 12228	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → (((𝑅 / 2) / 2) + ((𝑅 / 2) / 2)) = (𝑅 / 2))
319	316, 318	breqtrd 5101	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ((abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)))) + (abs‘(((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)) − ((𝑆 D (𝐹‘𝑁))‘𝐶)))) < (𝑅 / 2))
320	49, 63, 64, 65, 319	lelttrd 11142	. 2 ⊢ ((𝜑 ∧ 𝜓) → (abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((𝑆 D (𝐹‘𝑁))‘𝐶))) < (𝑅 / 2))
321		ulmdvlem1.2	. 2 ⊢ ((𝜑 ∧ 𝜓) → (abs‘(((𝑆 D (𝐹‘𝑁))‘𝐶) − (𝐻‘𝐶))) < (𝑅 / 2))
322	40, 44, 45, 47, 320, 321	abs3lemd 15182	1 ⊢ ((𝜑 ∧ 𝜓) → (abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − (𝐻‘𝐶))) < 𝑅)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1539 ∈ wcel 2107 ≠ wne 2944 ∀wral 3065 Vcvv 3433 ⊆ wss 3888 {csn 4562 {cpr 4564 class class class wbr 5075 ↦ cmpt 5158 × cxp 5588 dom cdm 5590 ↾ cres 5592 ∘ ccom 5594 Fn wfn 6432 ⟶wf 6433 ‘cfv 6437 (class class class)co 7284 ∘_f cof 7540 ↑_m cmap 8624 ℂcc 10878 ℝcr 10879 + caddc 10883 · cmul 10885 ℝ^*cxr 11017 < clt 11018 ≤ cle 11019 − cmin 11214 / cdiv 11641 2c2 12037 ℤcz 12328 ℤ_≥cuz 12591 ℝ⁺crp 12739 abscabs 14954 ⇝ cli 15202 ∞Metcxmet 20591 ballcbl 20593 D cdv 25036 ⇝_𝑢culm 25544

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2710 ax-rep 5210 ax-sep 5224 ax-nul 5231 ax-pow 5289 ax-pr 5353 ax-un 7597 ax-cnex 10936 ax-resscn 10937 ax-1cn 10938 ax-icn 10939 ax-addcl 10940 ax-addrcl 10941 ax-mulcl 10942 ax-mulrcl 10943 ax-mulcom 10944 ax-addass 10945 ax-mulass 10946 ax-distr 10947 ax-i2m1 10948 ax-1ne0 10949 ax-1rid 10950 ax-rnegex 10951 ax-rrecex 10952 ax-cnre 10953 ax-pre-lttri 10954 ax-pre-lttrn 10955 ax-pre-ltadd 10956 ax-pre-mulgt0 10957 ax-pre-sup 10958 ax-addf 10959 ax-mulf 10960

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2541 df-eu 2570 df-clab 2717 df-cleq 2731 df-clel 2817 df-nfc 2890 df-ne 2945 df-nel 3051 df-ral 3070 df-rex 3071 df-rmo 3072 df-reu 3073 df-rab 3074 df-v 3435 df-sbc 3718 df-csb 3834 df-dif 3891 df-un 3893 df-in 3895 df-ss 3905 df-pss 3907 df-nul 4258 df-if 4461 df-pw 4536 df-sn 4563 df-pr 4565 df-tp 4567 df-op 4569 df-uni 4841 df-int 4881 df-iun 4927 df-iin 4928 df-br 5076 df-opab 5138 df-mpt 5159 df-tr 5193 df-id 5490 df-eprel 5496 df-po 5504 df-so 5505 df-fr 5545 df-se 5546 df-we 5547 df-xp 5596 df-rel 5597 df-cnv 5598 df-co 5599 df-dm 5600 df-rn 5601 df-res 5602 df-ima 5603 df-pred 6206 df-ord 6273 df-on 6274 df-lim 6275 df-suc 6276 df-iota 6395 df-fun 6439 df-fn 6440 df-f 6441 df-f1 6442 df-fo 6443 df-f1o 6444 df-fv 6445 df-isom 6446 df-riota 7241 df-ov 7287 df-oprab 7288 df-mpo 7289 df-of 7542 df-om 7722 df-1st 7840 df-2nd 7841 df-supp 7987 df-frecs 8106 df-wrecs 8137 df-recs 8211 df-rdg 8250 df-1o 8306 df-2o 8307 df-er 8507 df-map 8626 df-pm 8627 df-ixp 8695 df-en 8743 df-dom 8744 df-sdom 8745 df-fin 8746 df-fsupp 9138 df-fi 9179 df-sup 9210 df-inf 9211 df-oi 9278 df-card 9706 df-pnf 11020 df-mnf 11021 df-xr 11022 df-ltxr 11023 df-le 11024 df-sub 11216 df-neg 11217 df-div 11642 df-nn 11983 df-2 12045 df-3 12046 df-4 12047 df-5 12048 df-6 12049 df-7 12050 df-8 12051 df-9 12052 df-n0 12243 df-z 12329 df-dec 12447 df-uz 12592 df-q 12698 df-rp 12740 df-xneg 12857 df-xadd 12858 df-xmul 12859 df-ioo 13092 df-ico 13094 df-icc 13095 df-fz 13249 df-fzo 13392 df-fl 13521 df-seq 13731 df-exp 13792 df-hash 14054 df-cj 14819 df-re 14820 df-im 14821 df-sqrt 14955 df-abs 14956 df-clim 15206 df-rlim 15207 df-struct 16857 df-sets 16874 df-slot 16892 df-ndx 16904 df-base 16922 df-ress 16951 df-plusg 16984 df-mulr 16985 df-starv 16986 df-sca 16987 df-vsca 16988 df-ip 16989 df-tset 16990 df-ple 16991 df-ds 16993 df-unif 16994 df-hom 16995 df-cco 16996 df-rest 17142 df-topn 17143 df-0g 17161 df-gsum 17162 df-topgen 17163 df-pt 17164 df-prds 17167 df-xrs 17222 df-qtop 17227 df-imas 17228 df-xps 17230 df-mre 17304 df-mrc 17305 df-acs 17307 df-mgm 18335 df-sgrp 18384 df-mnd 18395 df-submnd 18440 df-mulg 18710 df-cntz 18932 df-cmn 19397 df-psmet 20598 df-xmet 20599 df-met 20600 df-bl 20601 df-mopn 20602 df-fbas 20603 df-fg 20604 df-cnfld 20607 df-top 22052 df-topon 22069 df-topsp 22091 df-bases 22105 df-cld 22179 df-ntr 22180 df-cls 22181 df-nei 22258 df-lp 22296 df-perf 22297 df-cn 22387 df-cnp 22388 df-haus 22475 df-cmp 22547 df-tx 22722 df-hmeo 22915 df-fil 23006 df-fm 23098 df-flim 23099 df-flf 23100 df-xms 23482 df-ms 23483 df-tms 23484 df-cncf 24050 df-limc 25039 df-dv 25040 df-ulm 25545

This theorem is referenced by: ulmdvlem3 25570

W3C validator