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 24988

Description: Lemma for ulmdv 24991. (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 483	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → 𝐺:𝑋⟶ℂ)
3		ulmdvlem1.y	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → 𝑌 ∈ 𝑋)
4	2, 3	ffvelrnd 6852	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → (𝐺‘𝑌) ∈ ℂ)
5		ulmdvlem1.c	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → 𝐶 ∈ 𝑋)
6	2, 5	ffvelrnd 6852	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → (𝐺‘𝐶) ∈ ℂ)
7	4, 6	subcld 10997	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ((𝐺‘𝑌) − (𝐺‘𝐶)) ∈ ℂ)
8		ulmdvlem1.n	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → 𝑁 ∈ 𝑍)
9		fveq2 6670	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑁 → (𝐹‘𝑘) = (𝐹‘𝑁))
10	9	oveq2d 7172	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑁 → (𝑆 D (𝐹‘𝑘)) = (𝑆 D (𝐹‘𝑁)))
11		eqid 2821	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘))) = (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))
12		ovex 7189	. . . . . . . . . . . 12 ⊢ (𝑆 D (𝐹‘𝑁)) ∈ V
13	10, 11, 12	fvmpt 6768	. . . . . . . . . . 11 ⊢ (𝑁 ∈ 𝑍 → ((𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))‘𝑁) = (𝑆 D (𝐹‘𝑁)))
14	8, 13	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → ((𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))‘𝑁) = (𝑆 D (𝐹‘𝑁)))
15		ovex 7189	. . . . . . . . . . . . . . 15 ⊢ (𝑆 D (𝐹‘𝑘)) ∈ V
16	15	rgenw 3150	. . . . . . . . . . . . . 14 ⊢ ∀𝑘 ∈ 𝑍 (𝑆 D (𝐹‘𝑘)) ∈ V
17	11	fnmpt 6488	. . . . . . . . . . . . . 14 ⊢ (∀𝑘 ∈ 𝑍 (𝑆 D (𝐹‘𝑘)) ∈ V → (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘))) Fn 𝑍)
18	16, 17	mp1i 13	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘))) Fn 𝑍)
19		ulmdv.u	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))(⇝_𝑢‘𝑋)𝐻)
20		ulmf2 24972	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘))) Fn 𝑍 ∧ (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))(⇝_𝑢‘𝑋)𝐻) → (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘))):𝑍⟶(ℂ ↑_m 𝑋))
21	18, 19, 20	syl2anc 586	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘))):𝑍⟶(ℂ ↑_m 𝑋))
22	21	adantr 483	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘))):𝑍⟶(ℂ ↑_m 𝑋))
23	22, 8	ffvelrnd 6852	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → ((𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))‘𝑁) ∈ (ℂ ↑_m 𝑋))
24	14, 23	eqeltrrd 2914	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → (𝑆 D (𝐹‘𝑁)) ∈ (ℂ ↑_m 𝑋))
25		elmapi 8428	. . . . . . . . 9 ⊢ ((𝑆 D (𝐹‘𝑁)) ∈ (ℂ ↑_m 𝑋) → (𝑆 D (𝐹‘𝑁)):𝑋⟶ℂ)
26	24, 25	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → (𝑆 D (𝐹‘𝑁)):𝑋⟶ℂ)
27	26	fdmd 6523	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → dom (𝑆 D (𝐹‘𝑁)) = 𝑋)
28		dvbsss 24500	. . . . . . 7 ⊢ dom (𝑆 D (𝐹‘𝑁)) ⊆ 𝑆
29	27, 28	eqsstrrdi 4022	. . . . . 6 ⊢ ((𝜑 ∧ 𝜓) → 𝑋 ⊆ 𝑆)
30		ulmdv.s	. . . . . . . 8 ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})
31		recnprss 24502	. . . . . . . 8 ⊢ (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)
32	30, 31	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑆 ⊆ ℂ)
33	32	adantr 483	. . . . . 6 ⊢ ((𝜑 ∧ 𝜓) → 𝑆 ⊆ ℂ)
34	29, 33	sstrd 3977	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → 𝑋 ⊆ ℂ)
35	34, 3	sseldd 3968	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝑌 ∈ ℂ)
36	34, 5	sseldd 3968	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝐶 ∈ ℂ)
37	35, 36	subcld 10997	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝑌 − 𝐶) ∈ ℂ)
38		ulmdvlem1.3	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝑌 ≠ 𝐶)
39	35, 36, 38	subne0d 11006	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝑌 − 𝐶) ≠ 0)
40	7, 37, 39	divcld 11416	. 2 ⊢ ((𝜑 ∧ 𝜓) → (((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) ∈ ℂ)
41		ulmcl 24969	. . . . 5 ⊢ ((𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))(⇝_𝑢‘𝑋)𝐻 → 𝐻:𝑋⟶ℂ)
42	19, 41	syl 17	. . . 4 ⊢ (𝜑 → 𝐻:𝑋⟶ℂ)
43	42	adantr 483	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝐻:𝑋⟶ℂ)
44	43, 5	ffvelrnd 6852	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝐻‘𝐶) ∈ ℂ)
45	26, 5	ffvelrnd 6852	. 2 ⊢ ((𝜑 ∧ 𝜓) → ((𝑆 D (𝐹‘𝑁))‘𝐶) ∈ ℂ)
46		ulmdvlem1.r	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝑅 ∈ ℝ⁺)
47	46	rpred 12432	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝑅 ∈ ℝ)
48	40, 45	subcld 10997	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → ((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((𝑆 D (𝐹‘𝑁))‘𝐶)) ∈ ℂ)
49	48	abscld 14796	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((𝑆 D (𝐹‘𝑁))‘𝐶))) ∈ ℝ)
50		ulmdv.f	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑_m 𝑋))
51	50	adantr 483	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → 𝐹:𝑍⟶(ℂ ↑_m 𝑋))
52	51, 8	ffvelrnd 6852	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → (𝐹‘𝑁) ∈ (ℂ ↑_m 𝑋))
53		elmapi 8428	. . . . . . . . . 10 ⊢ ((𝐹‘𝑁) ∈ (ℂ ↑_m 𝑋) → (𝐹‘𝑁):𝑋⟶ℂ)
54	52, 53	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → (𝐹‘𝑁):𝑋⟶ℂ)
55	54, 3	ffvelrnd 6852	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → ((𝐹‘𝑁)‘𝑌) ∈ ℂ)
56	54, 5	ffvelrnd 6852	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → ((𝐹‘𝑁)‘𝐶) ∈ ℂ)
57	55, 56	subcld 10997	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → (((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) ∈ ℂ)
58	57, 37, 39	divcld 11416	. . . . . 6 ⊢ ((𝜑 ∧ 𝜓) → ((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)) ∈ ℂ)
59	40, 58	subcld 10997	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → ((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶))) ∈ ℂ)
60	59	abscld 14796	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → (abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)))) ∈ ℝ)
61	58, 45	subcld 10997	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → (((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)) − ((𝑆 D (𝐹‘𝑁))‘𝐶)) ∈ ℂ)
62	61	abscld 14796	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → (abs‘(((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)) − ((𝑆 D (𝐹‘𝑁))‘𝐶))) ∈ ℝ)
63	60, 62	readdcld 10670	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ((abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)))) + (abs‘(((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)) − ((𝑆 D (𝐹‘𝑁))‘𝐶)))) ∈ ℝ)
64	47	rehalfcld 11885	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝑅 / 2) ∈ ℝ)
65	40, 45, 58	abs3difd 14820	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((𝑆 D (𝐹‘𝑁))‘𝐶))) ≤ ((abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)))) + (abs‘(((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)) − ((𝑆 D (𝐹‘𝑁))‘𝐶)))))
66	64	rehalfcld 11885	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → ((𝑅 / 2) / 2) ∈ ℝ)
67	4, 55, 6, 56	sub4d 11046	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → (((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶))) = (((𝐺‘𝑌) − (𝐺‘𝐶)) − (((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶))))
68	67	oveq1d 7171	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → ((((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶))) / (𝑌 − 𝐶)) = ((((𝐺‘𝑌) − (𝐺‘𝐶)) − (((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶))) / (𝑌 − 𝐶)))
69	7, 57, 37, 39	divsubdird 11455	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → ((((𝐺‘𝑌) − (𝐺‘𝐶)) − (((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶))) / (𝑌 − 𝐶)) = ((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶))))
70	68, 69	eqtrd 2856	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → ((((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶))) / (𝑌 − 𝐶)) = ((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶))))
71	70	fveq2d 6674	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → (abs‘((((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶))) / (𝑌 − 𝐶))) = (abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)))))
72	4, 55	subcld 10997	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → ((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) ∈ ℂ)
73	6, 56	subcld 10997	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶)) ∈ ℂ)
74	72, 73	subcld 10997	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → (((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶))) ∈ ℂ)
75	74, 37, 39	absdivd 14815	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → (abs‘((((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶))) / (𝑌 − 𝐶))) = ((abs‘(((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) / (abs‘(𝑌 − 𝐶))))
76	71, 75	eqtr3d 2858	. . . . . 6 ⊢ ((𝜑 ∧ 𝜓) → (abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)))) = ((abs‘(((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) / (abs‘(𝑌 − 𝐶))))
77		eqid 2821	. . . . . . . 8 ⊢ (ℤ_≥‘𝑁) = (ℤ_≥‘𝑁)
78		ulmdv.z	. . . . . . . . . 10 ⊢ 𝑍 = (ℤ_≥‘𝑀)
79	8, 78	eleqtrdi 2923	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → 𝑁 ∈ (ℤ_≥‘𝑀))
80		eluzelz 12254	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → 𝑁 ∈ ℤ)
81	79, 80	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → 𝑁 ∈ ℤ)
82		ulmdv.m	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℤ)
83	82	adantr 483	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → 𝑀 ∈ ℤ)
84		fveq2 6670	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑌 → ((𝐹‘𝑘)‘𝑧) = ((𝐹‘𝑘)‘𝑌))
85	84	mpteq2dv 5162	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑌 → (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑧)) = (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑌)))
86		fveq2 6670	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑌 → (𝐺‘𝑧) = (𝐺‘𝑌))
87	85, 86	breq12d 5079	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑌 → ((𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑧)) ⇝ (𝐺‘𝑧) ↔ (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑌)) ⇝ (𝐺‘𝑌)))
88		ulmdv.l	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑧)) ⇝ (𝐺‘𝑧))
89	88	ralrimiva 3182	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑧 ∈ 𝑋 (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑧)) ⇝ (𝐺‘𝑧))
90	89	adantr 483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → ∀𝑧 ∈ 𝑋 (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑧)) ⇝ (𝐺‘𝑧))
91	87, 90, 3	rspcdva 3625	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑌)) ⇝ (𝐺‘𝑌))
92	78	fvexi 6684	. . . . . . . . . . . . 13 ⊢ 𝑍 ∈ V
93	92	mptex 6986	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌))) ∈ V
94	93	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌))) ∈ V)
95		fveq2 6670	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑛 → (𝐹‘𝑘) = (𝐹‘𝑛))
96	95	fveq1d 6672	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑛 → ((𝐹‘𝑘)‘𝑌) = ((𝐹‘𝑛)‘𝑌))
97		eqid 2821	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑌)) = (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑌))
98		fvex 6683	. . . . . . . . . . . . . 14 ⊢ ((𝐹‘𝑛)‘𝑌) ∈ V
99	96, 97, 98	fvmpt 6768	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ 𝑍 → ((𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑌))‘𝑛) = ((𝐹‘𝑛)‘𝑌))
100	99	adantl 484	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑌))‘𝑛) = ((𝐹‘𝑛)‘𝑌))
101	51	ffvelrnda 6851	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ∈ (ℂ ↑_m 𝑋))
102		elmapi 8428	. . . . . . . . . . . . . 14 ⊢ ((𝐹‘𝑛) ∈ (ℂ ↑_m 𝑋) → (𝐹‘𝑛):𝑋⟶ℂ)
103	101, 102	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛):𝑋⟶ℂ)
104	3	adantr 483	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → 𝑌 ∈ 𝑋)
105	103, 104	ffvelrnd 6852	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝐹‘𝑛)‘𝑌) ∈ ℂ)
106	100, 105	eqeltrd 2913	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑌))‘𝑛) ∈ ℂ)
107	96	oveq1d 7171	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑛 → (((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) = (((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)))
108		eqid 2821	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌))) = (𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)))
109		ovex 7189	. . . . . . . . . . . . . 14 ⊢ (((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) ∈ V
110	107, 108, 109	fvmpt 6768	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ 𝑍 → ((𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)))‘𝑛) = (((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)))
111	110	adantl 484	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)))‘𝑛) = (((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)))
112	100	oveq1d 7171	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → (((𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑌))‘𝑛) − ((𝐹‘𝑁)‘𝑌)) = (((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)))
113	111, 112	eqtr4d 2859	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)))‘𝑛) = (((𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑌))‘𝑛) − ((𝐹‘𝑁)‘𝑌)))
114	78, 83, 91, 55, 94, 106, 113	climsubc1 14994	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌))) ⇝ ((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)))
115	92	mptex 6986	. . . . . . . . . . 11 ⊢ (𝑘 ∈ 𝑍 ↦ ((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) ∈ V
116	115	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝑍 ↦ ((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) ∈ V)
117		fveq2 6670	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝐶 → ((𝐹‘𝑘)‘𝑧) = ((𝐹‘𝑘)‘𝐶))
118	117	mpteq2dv 5162	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝐶 → (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑧)) = (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝐶)))
119		fveq2 6670	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝐶 → (𝐺‘𝑧) = (𝐺‘𝐶))
120	118, 119	breq12d 5079	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝐶 → ((𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑧)) ⇝ (𝐺‘𝑧) ↔ (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝐶)) ⇝ (𝐺‘𝐶)))
121	120, 90, 5	rspcdva 3625	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝐶)) ⇝ (𝐺‘𝐶))
122	92	mptex 6986	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))) ∈ V
123	122	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))) ∈ V)
124	95	fveq1d 6672	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑛 → ((𝐹‘𝑘)‘𝐶) = ((𝐹‘𝑛)‘𝐶))
125		eqid 2821	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝐶)) = (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝐶))
126		fvex 6683	. . . . . . . . . . . . . 14 ⊢ ((𝐹‘𝑛)‘𝐶) ∈ V
127	124, 125, 126	fvmpt 6768	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ 𝑍 → ((𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝐶))‘𝑛) = ((𝐹‘𝑛)‘𝐶))
128	127	adantl 484	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝐶))‘𝑛) = ((𝐹‘𝑛)‘𝐶))
129	5	adantr 483	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → 𝐶 ∈ 𝑋)
130	103, 129	ffvelrnd 6852	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝐹‘𝑛)‘𝐶) ∈ ℂ)
131	128, 130	eqeltrd 2913	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝐶))‘𝑛) ∈ ℂ)
132	124	oveq1d 7171	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑛 → (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)) = (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))
133		eqid 2821	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))) = (𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))
134		ovex 7189	. . . . . . . . . . . . . 14 ⊢ (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)) ∈ V
135	132, 133, 134	fvmpt 6768	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ 𝑍 → ((𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))‘𝑛) = (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))
136	135	adantl 484	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))‘𝑛) = (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))
137	128	oveq1d 7171	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → (((𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝐶))‘𝑛) − ((𝐹‘𝑁)‘𝐶)) = (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))
138	136, 137	eqtr4d 2859	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))‘𝑛) = (((𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝐶))‘𝑛) − ((𝐹‘𝑁)‘𝐶)))
139	78, 83, 121, 56, 123, 131, 138	climsubc1 14994	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))) ⇝ ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶)))
140	55	adantr 483	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝐹‘𝑁)‘𝑌) ∈ ℂ)
141	105, 140	subcld 10997	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → (((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) ∈ ℂ)
142	111, 141	eqeltrd 2913	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)))‘𝑛) ∈ ℂ)
143	56	adantr 483	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝐹‘𝑁)‘𝐶) ∈ ℂ)
144	130, 143	subcld 10997	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)) ∈ ℂ)
145	136, 144	eqeltrd 2913	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))‘𝑛) ∈ ℂ)
146	107, 132	oveq12d 7174	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑛 → ((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))) = ((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))
147		eqid 2821	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ 𝑍 ↦ ((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) = (𝑘 ∈ 𝑍 ↦ ((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))
148		ovex 7189	. . . . . . . . . . . . 13 ⊢ ((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶))) ∈ V
149	146, 147, 148	fvmpt 6768	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ 𝑍 → ((𝑘 ∈ 𝑍 ↦ ((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))‘𝑛) = ((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))
150	149	adantl 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ ((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))‘𝑛) = ((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))
151	111, 136	oveq12d 7174	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → (((𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)))‘𝑛) − ((𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))‘𝑛)) = ((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))
152	150, 151	eqtr4d 2859	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ ((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))‘𝑛) = (((𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)))‘𝑛) − ((𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))‘𝑛)))
153	78, 83, 114, 116, 139, 142, 145, 152	climsub 14990	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝑍 ↦ ((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) ⇝ (((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶))))
154	92	mptex 6986	. . . . . . . . . 10 ⊢ (𝑘 ∈ 𝑍 ↦ (abs‘((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))) ∈ V
155	154	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝑍 ↦ (abs‘((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))) ∈ V)
156	141, 144	subcld 10997	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶))) ∈ ℂ)
157	150, 156	eqeltrd 2913	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ ((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))‘𝑛) ∈ ℂ)
158	146	fveq2d 6674	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑛 → (abs‘((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) = (abs‘((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))))
159		eqid 2821	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ 𝑍 ↦ (abs‘((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))) = (𝑘 ∈ 𝑍 ↦ (abs‘((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))))
160		fvex 6683	. . . . . . . . . . . 12 ⊢ (abs‘((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) ∈ V
161	158, 159, 160	fvmpt 6768	. . . . . . . . . . 11 ⊢ (𝑛 ∈ 𝑍 → ((𝑘 ∈ 𝑍 ↦ (abs‘((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))))‘𝑛) = (abs‘((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))))
162	161	adantl 484	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ (abs‘((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))))‘𝑛) = (abs‘((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))))
163	150	fveq2d 6674	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → (abs‘((𝑘 ∈ 𝑍 ↦ ((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))‘𝑛)) = (abs‘((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))))
164	162, 163	eqtr4d 2859	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ (abs‘((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))))‘𝑛) = (abs‘((𝑘 ∈ 𝑍 ↦ ((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))‘𝑛)))
165	78, 153, 155, 83, 157, 164	climabs 14960	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝑍 ↦ (abs‘((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))) ⇝ (abs‘(((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶)))))
166	37	abscld 14796	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → (abs‘(𝑌 − 𝐶)) ∈ ℝ)
167	66, 166	remulcld 10671	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → (((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶))) ∈ ℝ)
168	167	recnd 10669	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → (((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶))) ∈ ℂ)
169	78	eqimss2i 4026	. . . . . . . . . 10 ⊢ (ℤ_≥‘𝑀) ⊆ 𝑍
170	169, 92	climconst2 14905	. . . . . . . . 9 ⊢ (((((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶))) ∈ ℂ ∧ 𝑀 ∈ ℤ) → (𝑍 × {(((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶)))}) ⇝ (((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶))))
171	168, 83, 170	syl2anc 586	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → (𝑍 × {(((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶)))}) ⇝ (((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶))))
172	78	uztrn2 12263	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → 𝑛 ∈ 𝑍)
173	8, 172	sylan 582	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → 𝑛 ∈ 𝑍)
174	173, 161	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → ((𝑘 ∈ 𝑍 ↦ (abs‘((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))))‘𝑛) = (abs‘((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))))
175	156	abscld 14796	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → (abs‘((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) ∈ ℝ)
176	173, 175	syldan 593	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (abs‘((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) ∈ ℝ)
177	174, 176	eqeltrd 2913	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → ((𝑘 ∈ 𝑍 ↦ (abs‘((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))))‘𝑛) ∈ ℝ)
178		ovex 7189	. . . . . . . . . . 11 ⊢ (((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶))) ∈ V
179	178	fvconst2 6966	. . . . . . . . . 10 ⊢ (𝑛 ∈ 𝑍 → ((𝑍 × {(((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶)))})‘𝑛) = (((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶))))
180	173, 179	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → ((𝑍 × {(((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶)))})‘𝑛) = (((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶))))
181	167	adantr 483	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶))) ∈ ℝ)
182	180, 181	eqeltrd 2913	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → ((𝑍 × {(((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶)))})‘𝑛) ∈ ℝ)
183	173, 103	syldan 593	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝐹‘𝑛):𝑋⟶ℂ)
184	183	ffnd 6515	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝐹‘𝑛) Fn 𝑋)
185	54	adantr 483	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝐹‘𝑁):𝑋⟶ℂ)
186	185	ffnd 6515	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝐹‘𝑁) Fn 𝑋)
187		ulmscl 24967	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))(⇝_𝑢‘𝑋)𝐻 → 𝑋 ∈ V)
188	19, 187	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑋 ∈ V)
189	188	ad2antrr 724	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → 𝑋 ∈ V)
190	3	adantr 483	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → 𝑌 ∈ 𝑋)
191		fnfvof 7423	. . . . . . . . . . . . 13 ⊢ ((((𝐹‘𝑛) Fn 𝑋 ∧ (𝐹‘𝑁) Fn 𝑋) ∧ (𝑋 ∈ V ∧ 𝑌 ∈ 𝑋)) → (((𝐹‘𝑛) ∘_f − (𝐹‘𝑁))‘𝑌) = (((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)))
192	184, 186, 189, 190, 191	syl22anc 836	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (((𝐹‘𝑛) ∘_f − (𝐹‘𝑁))‘𝑌) = (((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)))
193	5	adantr 483	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → 𝐶 ∈ 𝑋)
194		fnfvof 7423	. . . . . . . . . . . . 13 ⊢ ((((𝐹‘𝑛) Fn 𝑋 ∧ (𝐹‘𝑁) Fn 𝑋) ∧ (𝑋 ∈ V ∧ 𝐶 ∈ 𝑋)) → (((𝐹‘𝑛) ∘_f − (𝐹‘𝑁))‘𝐶) = (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))
195	184, 186, 189, 193, 194	syl22anc 836	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (((𝐹‘𝑛) ∘_f − (𝐹‘𝑁))‘𝐶) = (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))
196	192, 195	oveq12d 7174	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → ((((𝐹‘𝑛) ∘_f − (𝐹‘𝑁))‘𝑌) − (((𝐹‘𝑛) ∘_f − (𝐹‘𝑁))‘𝐶)) = ((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))
197	196	fveq2d 6674	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (abs‘((((𝐹‘𝑛) ∘_f − (𝐹‘𝑁))‘𝑌) − (((𝐹‘𝑛) ∘_f − (𝐹‘𝑁))‘𝐶))) = (abs‘((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))))
198	29, 3	sseldd 3968	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝜓) → 𝑌 ∈ 𝑆)
199	29, 5	sseldd 3968	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝜓) → 𝐶 ∈ 𝑆)
200	198, 199	ovresd 7315	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝜓) → (𝑌((abs ∘ − ) ↾ (𝑆 × 𝑆))𝐶) = (𝑌(abs ∘ − )𝐶))
201		eqid 2821	. . . . . . . . . . . . . . . . . 18 ⊢ (abs ∘ − ) = (abs ∘ − )
202	201	cnmetdval 23379	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑌 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝑌(abs ∘ − )𝐶) = (abs‘(𝑌 − 𝐶)))
203	35, 36, 202	syl2anc 586	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝜓) → (𝑌(abs ∘ − )𝐶) = (abs‘(𝑌 − 𝐶)))
204	200, 203	eqtrd 2856	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → (𝑌((abs ∘ − ) ↾ (𝑆 × 𝑆))𝐶) = (abs‘(𝑌 − 𝐶)))
205		ulmdvlem1.a	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → (abs‘(𝑌 − 𝐶)) < 𝑈)
206	204, 205	eqbrtrd 5088	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → (𝑌((abs ∘ − ) ↾ (𝑆 × 𝑆))𝐶) < 𝑈)
207		cnxmet 23381	. . . . . . . . . . . . . . . 16 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
208		xmetres2 22971	. . . . . . . . . . . . . . . 16 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑆 ⊆ ℂ) → ((abs ∘ − ) ↾ (𝑆 × 𝑆)) ∈ (∞Met‘𝑆))
209	207, 33, 208	sylancr 589	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → ((abs ∘ − ) ↾ (𝑆 × 𝑆)) ∈ (∞Met‘𝑆))
210		ulmdvlem1.u	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝜓) → 𝑈 ∈ ℝ⁺)
211	210	rpxrd 12433	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → 𝑈 ∈ ℝ^*)
212		elbl3 23002	. . . . . . . . . . . . . . 15 ⊢ (((((abs ∘ − ) ↾ (𝑆 × 𝑆)) ∈ (∞Met‘𝑆) ∧ 𝑈 ∈ ℝ^*) ∧ (𝐶 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆)) → (𝑌 ∈ (𝐶(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑈) ↔ (𝑌((abs ∘ − ) ↾ (𝑆 × 𝑆))𝐶) < 𝑈))
213	209, 211, 199, 198, 212	syl22anc 836	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → (𝑌 ∈ (𝐶(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑈) ↔ (𝑌((abs ∘ − ) ↾ (𝑆 × 𝑆))𝐶) < 𝑈))
214	206, 213	mpbird 259	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → 𝑌 ∈ (𝐶(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑈))
215	214	adantr 483	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → 𝑌 ∈ (𝐶(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑈))
216		blcntr 23023	. . . . . . . . . . . . . 14 ⊢ ((((abs ∘ − ) ↾ (𝑆 × 𝑆)) ∈ (∞Met‘𝑆) ∧ 𝐶 ∈ 𝑆 ∧ 𝑈 ∈ ℝ⁺) → 𝐶 ∈ (𝐶(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑈))
217	209, 199, 210, 216	syl3anc 1367	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → 𝐶 ∈ (𝐶(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑈))
218	217	adantr 483	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → 𝐶 ∈ (𝐶(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑈))
219	215, 218	jca 514	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝑌 ∈ (𝐶(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑈) ∧ 𝐶 ∈ (𝐶(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑈)))
220	30	ad2antrr 724	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → 𝑆 ∈ {ℝ, ℂ})
221		eqid 2821	. . . . . . . . . . . 12 ⊢ ((abs ∘ − ) ↾ (𝑆 × 𝑆)) = ((abs ∘ − ) ↾ (𝑆 × 𝑆))
222	29	adantr 483	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → 𝑋 ⊆ 𝑆)
223		fvexd 6685	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → ((𝐹‘𝑛)‘𝑦) ∈ V)
224		fvexd 6685	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → ((𝐹‘𝑁)‘𝑦) ∈ V)
225	183	feqmptd 6733	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝐹‘𝑛) = (𝑦 ∈ 𝑋 ↦ ((𝐹‘𝑛)‘𝑦)))
226	185	feqmptd 6733	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝐹‘𝑁) = (𝑦 ∈ 𝑋 ↦ ((𝐹‘𝑁)‘𝑦)))
227	189, 223, 224, 225, 226	offval2 7426	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → ((𝐹‘𝑛) ∘_f − (𝐹‘𝑁)) = (𝑦 ∈ 𝑋 ↦ (((𝐹‘𝑛)‘𝑦) − ((𝐹‘𝑁)‘𝑦))))
228	183	ffvelrnda 6851	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → ((𝐹‘𝑛)‘𝑦) ∈ ℂ)
229	185	ffvelrnda 6851	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → ((𝐹‘𝑁)‘𝑦) ∈ ℂ)
230	228, 229	subcld 10997	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → (((𝐹‘𝑛)‘𝑦) − ((𝐹‘𝑁)‘𝑦)) ∈ ℂ)
231	227, 230	fmpt3d 6880	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → ((𝐹‘𝑛) ∘_f − (𝐹‘𝑁)):𝑋⟶ℂ)
232	199	adantr 483	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → 𝐶 ∈ 𝑆)
233	211	adantr 483	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → 𝑈 ∈ ℝ^*)
234		eqid 2821	. . . . . . . . . . . 12 ⊢ (𝐶(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑈) = (𝐶(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑈)
235		ulmdvlem1.b	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → (𝐶(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑈) ⊆ 𝑋)
236	235	adantr 483	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝐶(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑈) ⊆ 𝑋)
237	227	oveq2d 7172	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝑆 D ((𝐹‘𝑛) ∘_f − (𝐹‘𝑁))) = (𝑆 D (𝑦 ∈ 𝑋 ↦ (((𝐹‘𝑛)‘𝑦) − ((𝐹‘𝑁)‘𝑦)))))
238		fvexd 6685	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → ((𝑆 D (𝐹‘𝑛))‘𝑦) ∈ V)
239	225	oveq2d 7172	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝑆 D (𝐹‘𝑛)) = (𝑆 D (𝑦 ∈ 𝑋 ↦ ((𝐹‘𝑛)‘𝑦))))
240	95	oveq2d 7172	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = 𝑛 → (𝑆 D (𝐹‘𝑘)) = (𝑆 D (𝐹‘𝑛)))
241		ovex 7189	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑆 D (𝐹‘𝑛)) ∈ V
242	240, 11, 241	fvmpt 6768	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ 𝑍 → ((𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))‘𝑛) = (𝑆 D (𝐹‘𝑛)))
243	173, 242	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → ((𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))‘𝑛) = (𝑆 D (𝐹‘𝑛)))
244	21	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘))):𝑍⟶(ℂ ↑_m 𝑋))
245	244, 173	ffvelrnd 6852	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → ((𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))‘𝑛) ∈ (ℂ ↑_m 𝑋))
246	243, 245	eqeltrrd 2914	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝑆 D (𝐹‘𝑛)) ∈ (ℂ ↑_m 𝑋))
247		elmapi 8428	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑆 D (𝐹‘𝑛)) ∈ (ℂ ↑_m 𝑋) → (𝑆 D (𝐹‘𝑛)):𝑋⟶ℂ)
248	246, 247	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝑆 D (𝐹‘𝑛)):𝑋⟶ℂ)
249	248	feqmptd 6733	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝑆 D (𝐹‘𝑛)) = (𝑦 ∈ 𝑋 ↦ ((𝑆 D (𝐹‘𝑛))‘𝑦)))
250	239, 249	eqtr3d 2858	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝑆 D (𝑦 ∈ 𝑋 ↦ ((𝐹‘𝑛)‘𝑦))) = (𝑦 ∈ 𝑋 ↦ ((𝑆 D (𝐹‘𝑛))‘𝑦)))
251		fvexd 6685	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → ((𝑆 D (𝐹‘𝑁))‘𝑦) ∈ V)
252	226	oveq2d 7172	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝑆 D (𝐹‘𝑁)) = (𝑆 D (𝑦 ∈ 𝑋 ↦ ((𝐹‘𝑁)‘𝑦))))
253	26	adantr 483	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝑆 D (𝐹‘𝑁)):𝑋⟶ℂ)
254	253	feqmptd 6733	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝑆 D (𝐹‘𝑁)) = (𝑦 ∈ 𝑋 ↦ ((𝑆 D (𝐹‘𝑁))‘𝑦)))
255	252, 254	eqtr3d 2858	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝑆 D (𝑦 ∈ 𝑋 ↦ ((𝐹‘𝑁)‘𝑦))) = (𝑦 ∈ 𝑋 ↦ ((𝑆 D (𝐹‘𝑁))‘𝑦)))
256	220, 228, 238, 250, 229, 251, 255	dvmptsub 24564	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝑆 D (𝑦 ∈ 𝑋 ↦ (((𝐹‘𝑛)‘𝑦) − ((𝐹‘𝑁)‘𝑦)))) = (𝑦 ∈ 𝑋 ↦ (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦))))
257	237, 256	eqtrd 2856	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝑆 D ((𝐹‘𝑛) ∘_f − (𝐹‘𝑁))) = (𝑦 ∈ 𝑋 ↦ (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦))))
258	257	dmeqd 5774	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → dom (𝑆 D ((𝐹‘𝑛) ∘_f − (𝐹‘𝑁))) = dom (𝑦 ∈ 𝑋 ↦ (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦))))
259		ovex 7189	. . . . . . . . . . . . . . 15 ⊢ (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦)) ∈ V
260		eqid 2821	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ 𝑋 ↦ (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦))) = (𝑦 ∈ 𝑋 ↦ (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦)))
261	259, 260	dmmpti 6492	. . . . . . . . . . . . . 14 ⊢ dom (𝑦 ∈ 𝑋 ↦ (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦))) = 𝑋
262	258, 261	syl6eq 2872	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → dom (𝑆 D ((𝐹‘𝑛) ∘_f − (𝐹‘𝑁))) = 𝑋)
263	236, 262	sseqtrrd 4008	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (𝐶(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑈) ⊆ dom (𝑆 D ((𝐹‘𝑛) ∘_f − (𝐹‘𝑁))))
264	66	adantr 483	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → ((𝑅 / 2) / 2) ∈ ℝ)
265	236	sselda 3967	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ (𝐶(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑈)) → 𝑦 ∈ 𝑋)
266	257	fveq1d 6672	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → ((𝑆 D ((𝐹‘𝑛) ∘_f − (𝐹‘𝑁)))‘𝑦) = ((𝑦 ∈ 𝑋 ↦ (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦)))‘𝑦))
267	260	fvmpt2 6779	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ 𝑋 ∧ (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦)) ∈ V) → ((𝑦 ∈ 𝑋 ↦ (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦)))‘𝑦) = (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦)))
268	259, 267	mpan2 689	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ 𝑋 → ((𝑦 ∈ 𝑋 ↦ (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦)))‘𝑦) = (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦)))
269	266, 268	sylan9eq 2876	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → ((𝑆 D ((𝐹‘𝑛) ∘_f − (𝐹‘𝑁)))‘𝑦) = (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦)))
270	269	fveq2d 6674	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → (abs‘((𝑆 D ((𝐹‘𝑛) ∘_f − (𝐹‘𝑁)))‘𝑦)) = (abs‘(((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦))))
271	259	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦)) ∈ V)
272	220, 230, 271, 256	dvmptcl 24556	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦)) ∈ ℂ)
273	272	abscld 14796	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → (abs‘(((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦))) ∈ ℝ)
274	66	ad2antrr 724	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → ((𝑅 / 2) / 2) ∈ ℝ)
275	248	ffvelrnda 6851	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → ((𝑆 D (𝐹‘𝑛))‘𝑦) ∈ ℂ)
276	253	ffvelrnda 6851	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → ((𝑆 D (𝐹‘𝑁))‘𝑦) ∈ ℂ)
277	275, 276	abssubd 14813	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → (abs‘(((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦))) = (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑦) − ((𝑆 D (𝐹‘𝑛))‘𝑦))))
278		ulmdvlem1.1	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝜓) → ∀𝑚 ∈ (ℤ_≥‘𝑁)∀𝑥 ∈ 𝑋 (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑚))‘𝑥))) < ((𝑅 / 2) / 2))
279		fveq2 6670	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑚 = 𝑛 → (𝐹‘𝑚) = (𝐹‘𝑛))
280	279	oveq2d 7172	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑚 = 𝑛 → (𝑆 D (𝐹‘𝑚)) = (𝑆 D (𝐹‘𝑛)))
281	280	fveq1d 6672	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑚 = 𝑛 → ((𝑆 D (𝐹‘𝑚))‘𝑥) = ((𝑆 D (𝐹‘𝑛))‘𝑥))
282	281	oveq2d 7172	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 = 𝑛 → (((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑚))‘𝑥)) = (((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑛))‘𝑥)))
283	282	fveq2d 6674	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = 𝑛 → (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑚))‘𝑥))) = (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑛))‘𝑥))))
284	283	breq1d 5076	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = 𝑛 → ((abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑚))‘𝑥))) < ((𝑅 / 2) / 2) ↔ (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑛))‘𝑥))) < ((𝑅 / 2) / 2)))
285	284	ralbidv 3197	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 𝑛 → (∀𝑥 ∈ 𝑋 (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑚))‘𝑥))) < ((𝑅 / 2) / 2) ↔ ∀𝑥 ∈ 𝑋 (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑛))‘𝑥))) < ((𝑅 / 2) / 2)))
286	285	rspccva 3622	. . . . . . . . . . . . . . . . . 18 ⊢ ((∀𝑚 ∈ (ℤ_≥‘𝑁)∀𝑥 ∈ 𝑋 (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑚))‘𝑥))) < ((𝑅 / 2) / 2) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → ∀𝑥 ∈ 𝑋 (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑛))‘𝑥))) < ((𝑅 / 2) / 2))
287	278, 286	sylan 582	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → ∀𝑥 ∈ 𝑋 (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑛))‘𝑥))) < ((𝑅 / 2) / 2))
288		fveq2 6670	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑦 → ((𝑆 D (𝐹‘𝑁))‘𝑥) = ((𝑆 D (𝐹‘𝑁))‘𝑦))
289		fveq2 6670	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑦 → ((𝑆 D (𝐹‘𝑛))‘𝑥) = ((𝑆 D (𝐹‘𝑛))‘𝑦))
290	288, 289	oveq12d 7174	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑦 → (((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑛))‘𝑥)) = (((𝑆 D (𝐹‘𝑁))‘𝑦) − ((𝑆 D (𝐹‘𝑛))‘𝑦)))
291	290	fveq2d 6674	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑦 → (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑛))‘𝑥))) = (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑦) − ((𝑆 D (𝐹‘𝑛))‘𝑦))))
292	291	breq1d 5076	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑦 → ((abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑛))‘𝑥))) < ((𝑅 / 2) / 2) ↔ (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑦) − ((𝑆 D (𝐹‘𝑛))‘𝑦))) < ((𝑅 / 2) / 2)))
293	292	rspccva 3622	. . . . . . . . . . . . . . . . 17 ⊢ ((∀𝑥 ∈ 𝑋 (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑛))‘𝑥))) < ((𝑅 / 2) / 2) ∧ 𝑦 ∈ 𝑋) → (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑦) − ((𝑆 D (𝐹‘𝑛))‘𝑦))) < ((𝑅 / 2) / 2))
294	287, 293	sylan 582	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑦) − ((𝑆 D (𝐹‘𝑛))‘𝑦))) < ((𝑅 / 2) / 2))
295	277, 294	eqbrtrd 5088	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → (abs‘(((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦))) < ((𝑅 / 2) / 2))
296	273, 274, 295	ltled 10788	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → (abs‘(((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦))) ≤ ((𝑅 / 2) / 2))
297	270, 296	eqbrtrd 5088	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → (abs‘((𝑆 D ((𝐹‘𝑛) ∘_f − (𝐹‘𝑁)))‘𝑦)) ≤ ((𝑅 / 2) / 2))
298	265, 297	syldan 593	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ 𝑦 ∈ (𝐶(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑈)) → (abs‘((𝑆 D ((𝐹‘𝑛) ∘_f − (𝐹‘𝑁)))‘𝑦)) ≤ ((𝑅 / 2) / 2))
299	220, 221, 222, 231, 232, 233, 234, 263, 264, 298	dvlip2 24592	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) ∧ (𝑌 ∈ (𝐶(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑈) ∧ 𝐶 ∈ (𝐶(ball‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))𝑈))) → (abs‘((((𝐹‘𝑛) ∘_f − (𝐹‘𝑁))‘𝑌) − (((𝐹‘𝑛) ∘_f − (𝐹‘𝑁))‘𝐶))) ≤ (((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶))))
300	219, 299	mpdan 685	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (abs‘((((𝐹‘𝑛) ∘_f − (𝐹‘𝑁))‘𝑌) − (((𝐹‘𝑛) ∘_f − (𝐹‘𝑁))‘𝐶))) ≤ (((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶))))
301	197, 300	eqbrtrrd 5090	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → (abs‘((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) ≤ (((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶))))
302	301, 174, 180	3brtr4d 5098	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ_≥‘𝑁)) → ((𝑘 ∈ 𝑍 ↦ (abs‘((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))))‘𝑛) ≤ ((𝑍 × {(((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶)))})‘𝑛))
303	77, 81, 165, 171, 177, 182, 302	climle 14996	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → (abs‘(((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) ≤ (((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶))))
304	74	abscld 14796	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → (abs‘(((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) ∈ ℝ)
305	37, 39	absrpcld 14808	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → (abs‘(𝑌 − 𝐶)) ∈ ℝ⁺)
306	304, 66, 305	ledivmul2d 12486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → (((abs‘(((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) / (abs‘(𝑌 − 𝐶))) ≤ ((𝑅 / 2) / 2) ↔ (abs‘(((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) ≤ (((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶)))))
307	303, 306	mpbird 259	. . . . . 6 ⊢ ((𝜑 ∧ 𝜓) → ((abs‘(((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) / (abs‘(𝑌 − 𝐶))) ≤ ((𝑅 / 2) / 2))
308	76, 307	eqbrtrd 5088	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → (abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)))) ≤ ((𝑅 / 2) / 2))
309	210	rpred 12432	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → 𝑈 ∈ ℝ)
310		ulmdvlem1.v	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → 𝑊 ∈ ℝ⁺)
311	310	rpred 12432	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → 𝑊 ∈ ℝ)
312		ulmdvlem1.l	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → 𝑈 < 𝑊)
313	166, 309, 311, 205, 312	lttrd 10801	. . . . . 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 11262	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → ((abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)))) + (abs‘(((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)) − ((𝑆 D (𝐹‘𝑁))‘𝐶)))) < (((𝑅 / 2) / 2) + ((𝑅 / 2) / 2)))
317	64	recnd 10669	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → (𝑅 / 2) ∈ ℂ)
318	317	2halvesd 11884	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → (((𝑅 / 2) / 2) + ((𝑅 / 2) / 2)) = (𝑅 / 2))
319	316, 318	breqtrd 5092	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ((abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)))) + (abs‘(((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)) − ((𝑆 D (𝐹‘𝑁))‘𝐶)))) < (𝑅 / 2))
320	49, 63, 64, 65, 319	lelttrd 10798	. 2 ⊢ ((𝜑 ∧ 𝜓) → (abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((𝑆 D (𝐹‘𝑁))‘𝐶))) < (𝑅 / 2))
321		ulmdvlem1.2	. 2 ⊢ ((𝜑 ∧ 𝜓) → (abs‘(((𝑆 D (𝐹‘𝑁))‘𝐶) − (𝐻‘𝐶))) < (𝑅 / 2))
322	40, 44, 45, 47, 320, 321	abs3lemd 14821	1 ⊢ ((𝜑 ∧ 𝜓) → (abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − (𝐻‘𝐶))) < 𝑅)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 = wceq 1537 ∈ wcel 2114 ≠ wne 3016 ∀wral 3138 Vcvv 3494 ⊆ wss 3936 {csn 4567 {cpr 4569 class class class wbr 5066 ↦ cmpt 5146 × cxp 5553 dom cdm 5555 ↾ cres 5557 ∘ ccom 5559 Fn wfn 6350 ⟶wf 6351 ‘cfv 6355 (class class class)co 7156 ∘_f cof 7407 ↑_m cmap 8406 ℂcc 10535 ℝcr 10536 + caddc 10540 · cmul 10542 ℝ^*cxr 10674 < clt 10675 ≤ cle 10676 − cmin 10870 / cdiv 11297 2c2 11693 ℤcz 11982 ℤ_≥cuz 12244 ℝ⁺crp 12390 abscabs 14593 ⇝ cli 14841 ∞Metcxmet 20530 ballcbl 20532 D cdv 24461 ⇝_𝑢culm 24964

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-rep 5190 ax-sep 5203 ax-nul 5210 ax-pow 5266 ax-pr 5330 ax-un 7461 ax-cnex 10593 ax-resscn 10594 ax-1cn 10595 ax-icn 10596 ax-addcl 10597 ax-addrcl 10598 ax-mulcl 10599 ax-mulrcl 10600 ax-mulcom 10601 ax-addass 10602 ax-mulass 10603 ax-distr 10604 ax-i2m1 10605 ax-1ne0 10606 ax-1rid 10607 ax-rnegex 10608 ax-rrecex 10609 ax-cnre 10610 ax-pre-lttri 10611 ax-pre-lttrn 10612 ax-pre-ltadd 10613 ax-pre-mulgt0 10614 ax-pre-sup 10615 ax-addf 10616 ax-mulf 10617

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-nel 3124 df-ral 3143 df-rex 3144 df-reu 3145 df-rmo 3146 df-rab 3147 df-v 3496 df-sbc 3773 df-csb 3884 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-pss 3954 df-nul 4292 df-if 4468 df-pw 4541 df-sn 4568 df-pr 4570 df-tp 4572 df-op 4574 df-uni 4839 df-int 4877 df-iun 4921 df-iin 4922 df-br 5067 df-opab 5129 df-mpt 5147 df-tr 5173 df-id 5460 df-eprel 5465 df-po 5474 df-so 5475 df-fr 5514 df-se 5515 df-we 5516 df-xp 5561 df-rel 5562 df-cnv 5563 df-co 5564 df-dm 5565 df-rn 5566 df-res 5567 df-ima 5568 df-pred 6148 df-ord 6194 df-on 6195 df-lim 6196 df-suc 6197 df-iota 6314 df-fun 6357 df-fn 6358 df-f 6359 df-f1 6360 df-fo 6361 df-f1o 6362 df-fv 6363 df-isom 6364 df-riota 7114 df-ov 7159 df-oprab 7160 df-mpo 7161 df-of 7409 df-om 7581 df-1st 7689 df-2nd 7690 df-supp 7831 df-wrecs 7947 df-recs 8008 df-rdg 8046 df-1o 8102 df-2o 8103 df-oadd 8106 df-er 8289 df-map 8408 df-pm 8409 df-ixp 8462 df-en 8510 df-dom 8511 df-sdom 8512 df-fin 8513 df-fsupp 8834 df-fi 8875 df-sup 8906 df-inf 8907 df-oi 8974 df-card 9368 df-pnf 10677 df-mnf 10678 df-xr 10679 df-ltxr 10680 df-le 10681 df-sub 10872 df-neg 10873 df-div 11298 df-nn 11639 df-2 11701 df-3 11702 df-4 11703 df-5 11704 df-6 11705 df-7 11706 df-8 11707 df-9 11708 df-n0 11899 df-z 11983 df-dec 12100 df-uz 12245 df-q 12350 df-rp 12391 df-xneg 12508 df-xadd 12509 df-xmul 12510 df-ioo 12743 df-ico 12745 df-icc 12746 df-fz 12894 df-fzo 13035 df-fl 13163 df-seq 13371 df-exp 13431 df-hash 13692 df-cj 14458 df-re 14459 df-im 14460 df-sqrt 14594 df-abs 14595 df-clim 14845 df-rlim 14846 df-struct 16485 df-ndx 16486 df-slot 16487 df-base 16489 df-sets 16490 df-ress 16491 df-plusg 16578 df-mulr 16579 df-starv 16580 df-sca 16581 df-vsca 16582 df-ip 16583 df-tset 16584 df-ple 16585 df-ds 16587 df-unif 16588 df-hom 16589 df-cco 16590 df-rest 16696 df-topn 16697 df-0g 16715 df-gsum 16716 df-topgen 16717 df-pt 16718 df-prds 16721 df-xrs 16775 df-qtop 16780 df-imas 16781 df-xps 16783 df-mre 16857 df-mrc 16858 df-acs 16860 df-mgm 17852 df-sgrp 17901 df-mnd 17912 df-submnd 17957 df-mulg 18225 df-cntz 18447 df-cmn 18908 df-psmet 20537 df-xmet 20538 df-met 20539 df-bl 20540 df-mopn 20541 df-fbas 20542 df-fg 20543 df-cnfld 20546 df-top 21502 df-topon 21519 df-topsp 21541 df-bases 21554 df-cld 21627 df-ntr 21628 df-cls 21629 df-nei 21706 df-lp 21744 df-perf 21745 df-cn 21835 df-cnp 21836 df-haus 21923 df-cmp 21995 df-tx 22170 df-hmeo 22363 df-fil 22454 df-fm 22546 df-flim 22547 df-flf 22548 df-xms 22930 df-ms 22931 df-tms 22932 df-cncf 23486 df-limc 24464 df-dv 24465 df-ulm 24965

This theorem is referenced by: ulmdvlem3 24990

W3C validator