dvlip2 - Metamath Proof Explorer

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

Theorem dvlip2 23979

Description: Combine the results of dvlip 23977 and dvlipcn 23978 into one. (Contributed by Mario Carneiro, 18-Mar-2015.) (Revised by Mario Carneiro, 8-Sep-2015.)

**Hypotheses**
Ref	Expression
dvlip2.s	⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})
dvlip2.j	⊢ 𝐽 = ((abs ∘ − ) ↾ (𝑆 × 𝑆))
dvlip2.x	⊢ (𝜑 → 𝑋 ⊆ 𝑆)
dvlip2.f	⊢ (𝜑 → 𝐹:𝑋⟶ℂ)
dvlip2.a	⊢ (𝜑 → 𝐴 ∈ 𝑆)
dvlip2.r	⊢ (𝜑 → 𝑅 ∈ ℝ^*)
dvlip2.b	⊢ 𝐵 = (𝐴(ball‘𝐽)𝑅)
dvlip2.d	⊢ (𝜑 → 𝐵 ⊆ dom (𝑆 D 𝐹))
dvlip2.m	⊢ (𝜑 → 𝑀 ∈ ℝ)
dvlip2.l	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (abs‘((𝑆 D 𝐹)‘𝑥)) ≤ 𝑀)

**Assertion**
Ref	Expression
dvlip2	⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (abs‘((𝐹‘𝑌) − (𝐹‘𝑍))) ≤ (𝑀 · (abs‘(𝑌 − 𝑍))))

Distinct variable groups: 𝑥,𝐴 𝑥,𝐵 𝑥,𝐹 𝑥,𝐽 𝜑,𝑥 𝑥,𝑀 𝑥,𝑅 𝑥,𝑆 𝑥,𝑌 𝑥,𝑍 Allowed substitution hint: 𝑋(𝑥)

Proof of Theorem dvlip2 Dummy variable 𝑟 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dvlip2.j	. . . . . . . 8 ⊢ 𝐽 = ((abs ∘ − ) ↾ (𝑆 × 𝑆))
2		cnxmet 22797	. . . . . . . . 9 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
3		dvlip2.s	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})
4		recnprss 23889	. . . . . . . . . 10 ⊢ (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)
5	3, 4	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ⊆ ℂ)
6		xmetres2 22387	. . . . . . . . 9 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑆 ⊆ ℂ) → ((abs ∘ − ) ↾ (𝑆 × 𝑆)) ∈ (∞Met‘𝑆))
7	2, 5, 6	sylancr 569	. . . . . . . 8 ⊢ (𝜑 → ((abs ∘ − ) ↾ (𝑆 × 𝑆)) ∈ (∞Met‘𝑆))
8	1, 7	syl5eqel 2854	. . . . . . 7 ⊢ (𝜑 → 𝐽 ∈ (∞Met‘𝑆))
9	8	ad2antrr 699	. . . . . 6 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → 𝐽 ∈ (∞Met‘𝑆))
10		dvlip2.a	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ 𝑆)
11	10	ad2antrr 699	. . . . . 6 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → 𝐴 ∈ 𝑆)
12		simplrr 757	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → 𝑍 ∈ 𝐵)
13		dvlip2.b	. . . . . . . . 9 ⊢ 𝐵 = (𝐴(ball‘𝐽)𝑅)
14	12, 13	syl6eleq 2860	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → 𝑍 ∈ (𝐴(ball‘𝐽)𝑅))
15		dvlip2.r	. . . . . . . . . 10 ⊢ (𝜑 → 𝑅 ∈ ℝ^*)
16	15	ad2antrr 699	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → 𝑅 ∈ ℝ^*)
17		elbl 22414	. . . . . . . . 9 ⊢ ((𝐽 ∈ (∞Met‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ 𝑅 ∈ ℝ^*) → (𝑍 ∈ (𝐴(ball‘𝐽)𝑅) ↔ (𝑍 ∈ 𝑆 ∧ (𝐴𝐽𝑍) < 𝑅)))
18	9, 11, 16, 17	syl3anc 1476	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → (𝑍 ∈ (𝐴(ball‘𝐽)𝑅) ↔ (𝑍 ∈ 𝑆 ∧ (𝐴𝐽𝑍) < 𝑅)))
19	14, 18	mpbid 222	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → (𝑍 ∈ 𝑆 ∧ (𝐴𝐽𝑍) < 𝑅))
20	19	simpld 478	. . . . . 6 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → 𝑍 ∈ 𝑆)
21		xmetcl 22357	. . . . . 6 ⊢ ((𝐽 ∈ (∞Met‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ 𝑍 ∈ 𝑆) → (𝐴𝐽𝑍) ∈ ℝ^*)
22	9, 11, 20, 21	syl3anc 1476	. . . . 5 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → (𝐴𝐽𝑍) ∈ ℝ^*)
23		simplrl 756	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → 𝑌 ∈ 𝐵)
24	23, 13	syl6eleq 2860	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → 𝑌 ∈ (𝐴(ball‘𝐽)𝑅))
25		elbl 22414	. . . . . . . . 9 ⊢ ((𝐽 ∈ (∞Met‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ 𝑅 ∈ ℝ^*) → (𝑌 ∈ (𝐴(ball‘𝐽)𝑅) ↔ (𝑌 ∈ 𝑆 ∧ (𝐴𝐽𝑌) < 𝑅)))
26	9, 11, 16, 25	syl3anc 1476	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → (𝑌 ∈ (𝐴(ball‘𝐽)𝑅) ↔ (𝑌 ∈ 𝑆 ∧ (𝐴𝐽𝑌) < 𝑅)))
27	24, 26	mpbid 222	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → (𝑌 ∈ 𝑆 ∧ (𝐴𝐽𝑌) < 𝑅))
28	27	simpld 478	. . . . . 6 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → 𝑌 ∈ 𝑆)
29		xmetcl 22357	. . . . . 6 ⊢ ((𝐽 ∈ (∞Met‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) → (𝐴𝐽𝑌) ∈ ℝ^*)
30	9, 11, 28, 29	syl3anc 1476	. . . . 5 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → (𝐴𝐽𝑌) ∈ ℝ^*)
31	22, 30	ifcld 4271	. . . 4 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → if((𝐴𝐽𝑌) ≤ (𝐴𝐽𝑍), (𝐴𝐽𝑍), (𝐴𝐽𝑌)) ∈ ℝ^*)
32	19	simprd 479	. . . . 5 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → (𝐴𝐽𝑍) < 𝑅)
33	27	simprd 479	. . . . 5 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → (𝐴𝐽𝑌) < 𝑅)
34		breq1 4790	. . . . . 6 ⊢ ((𝐴𝐽𝑍) = if((𝐴𝐽𝑌) ≤ (𝐴𝐽𝑍), (𝐴𝐽𝑍), (𝐴𝐽𝑌)) → ((𝐴𝐽𝑍) < 𝑅 ↔ if((𝐴𝐽𝑌) ≤ (𝐴𝐽𝑍), (𝐴𝐽𝑍), (𝐴𝐽𝑌)) < 𝑅))
35		breq1 4790	. . . . . 6 ⊢ ((𝐴𝐽𝑌) = if((𝐴𝐽𝑌) ≤ (𝐴𝐽𝑍), (𝐴𝐽𝑍), (𝐴𝐽𝑌)) → ((𝐴𝐽𝑌) < 𝑅 ↔ if((𝐴𝐽𝑌) ≤ (𝐴𝐽𝑍), (𝐴𝐽𝑍), (𝐴𝐽𝑌)) < 𝑅))
36	34, 35	ifboth 4264	. . . . 5 ⊢ (((𝐴𝐽𝑍) < 𝑅 ∧ (𝐴𝐽𝑌) < 𝑅) → if((𝐴𝐽𝑌) ≤ (𝐴𝐽𝑍), (𝐴𝐽𝑍), (𝐴𝐽𝑌)) < 𝑅)
37	32, 33, 36	syl2anc 567	. . . 4 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → if((𝐴𝐽𝑌) ≤ (𝐴𝐽𝑍), (𝐴𝐽𝑍), (𝐴𝐽𝑌)) < 𝑅)
38		qbtwnxr 12237	. . . 4 ⊢ ((if((𝐴𝐽𝑌) ≤ (𝐴𝐽𝑍), (𝐴𝐽𝑍), (𝐴𝐽𝑌)) ∈ ℝ^* ∧ 𝑅 ∈ ℝ^* ∧ if((𝐴𝐽𝑌) ≤ (𝐴𝐽𝑍), (𝐴𝐽𝑍), (𝐴𝐽𝑌)) < 𝑅) → ∃𝑟 ∈ ℚ (if((𝐴𝐽𝑌) ≤ (𝐴𝐽𝑍), (𝐴𝐽𝑍), (𝐴𝐽𝑌)) < 𝑟 ∧ 𝑟 < 𝑅))
39	31, 16, 37, 38	syl3anc 1476	. . 3 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → ∃𝑟 ∈ ℚ (if((𝐴𝐽𝑌) ≤ (𝐴𝐽𝑍), (𝐴𝐽𝑍), (𝐴𝐽𝑌)) < 𝑟 ∧ 𝑟 < 𝑅))
40		qre 11997	. . . . 5 ⊢ (𝑟 ∈ ℚ → 𝑟 ∈ ℝ)
41	30	adantr 466	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) → (𝐴𝐽𝑌) ∈ ℝ^*)
42	22	adantr 466	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) → (𝐴𝐽𝑍) ∈ ℝ^*)
43		rexr 10288	. . . . . . . . 9 ⊢ (𝑟 ∈ ℝ → 𝑟 ∈ ℝ^*)
44	43	adantl 467	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) → 𝑟 ∈ ℝ^*)
45		xrmaxlt 12218	. . . . . . . 8 ⊢ (((𝐴𝐽𝑌) ∈ ℝ^* ∧ (𝐴𝐽𝑍) ∈ ℝ^* ∧ 𝑟 ∈ ℝ^*) → (if((𝐴𝐽𝑌) ≤ (𝐴𝐽𝑍), (𝐴𝐽𝑍), (𝐴𝐽𝑌)) < 𝑟 ↔ ((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟)))
46	41, 42, 44, 45	syl3anc 1476	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) → (if((𝐴𝐽𝑌) ≤ (𝐴𝐽𝑍), (𝐴𝐽𝑍), (𝐴𝐽𝑌)) < 𝑟 ↔ ((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟)))
47		ioossicc 12465	. . . . . . . . . . . . 13 ⊢ ((𝐴 − 𝑟)(,)(𝐴 + 𝑟)) ⊆ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))
48		simpr 471	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → 𝑆 = ℝ)
49	28, 48	eleqtrd 2852	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → 𝑌 ∈ ℝ)
50	49	ad2antrr 699	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → 𝑌 ∈ ℝ)
51		xmetsym 22373	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐽 ∈ (∞Met‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) → (𝐴𝐽𝑌) = (𝑌𝐽𝐴))
52	9, 11, 28, 51	syl3anc 1476	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → (𝐴𝐽𝑌) = (𝑌𝐽𝐴))
53	48	sqxpeqd 5282	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → (𝑆 × 𝑆) = (ℝ × ℝ))
54	53	reseq2d 5535	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → ((abs ∘ − ) ↾ (𝑆 × 𝑆)) = ((abs ∘ − ) ↾ (ℝ × ℝ)))
55	1, 54	syl5eq 2817	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → 𝐽 = ((abs ∘ − ) ↾ (ℝ × ℝ)))
56	55	oveqd 6811	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → (𝑌𝐽𝐴) = (𝑌((abs ∘ − ) ↾ (ℝ × ℝ))𝐴))
57	11, 48	eleqtrd 2852	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → 𝐴 ∈ ℝ)
58		eqid 2771	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((abs ∘ − ) ↾ (ℝ × ℝ)) = ((abs ∘ − ) ↾ (ℝ × ℝ))
59	58	remetdval 22813	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑌 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝑌((abs ∘ − ) ↾ (ℝ × ℝ))𝐴) = (abs‘(𝑌 − 𝐴)))
60	49, 57, 59	syl2anc 567	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → (𝑌((abs ∘ − ) ↾ (ℝ × ℝ))𝐴) = (abs‘(𝑌 − 𝐴)))
61	52, 56, 60	3eqtrd 2809	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → (𝐴𝐽𝑌) = (abs‘(𝑌 − 𝐴)))
62	61	ad2antrr 699	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → (𝐴𝐽𝑌) = (abs‘(𝑌 − 𝐴)))
63		simprll 758	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → (𝐴𝐽𝑌) < 𝑟)
64	62, 63	eqbrtrrd 4811	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → (abs‘(𝑌 − 𝐴)) < 𝑟)
65	57	ad2antrr 699	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → 𝐴 ∈ ℝ)
66		simplr 746	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → 𝑟 ∈ ℝ)
67	50, 65, 66	absdifltd 14381	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → ((abs‘(𝑌 − 𝐴)) < 𝑟 ↔ ((𝐴 − 𝑟) < 𝑌 ∧ 𝑌 < (𝐴 + 𝑟))))
68	64, 67	mpbid 222	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → ((𝐴 − 𝑟) < 𝑌 ∧ 𝑌 < (𝐴 + 𝑟)))
69	68	simpld 478	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → (𝐴 − 𝑟) < 𝑌)
70	68	simprd 479	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → 𝑌 < (𝐴 + 𝑟))
71	65, 66	resubcld 10661	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → (𝐴 − 𝑟) ∈ ℝ)
72	71	rexrd 10292	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → (𝐴 − 𝑟) ∈ ℝ^*)
73	65, 66	readdcld 10272	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → (𝐴 + 𝑟) ∈ ℝ)
74	73	rexrd 10292	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → (𝐴 + 𝑟) ∈ ℝ^*)
75		elioo2 12422	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 − 𝑟) ∈ ℝ^* ∧ (𝐴 + 𝑟) ∈ ℝ^*) → (𝑌 ∈ ((𝐴 − 𝑟)(,)(𝐴 + 𝑟)) ↔ (𝑌 ∈ ℝ ∧ (𝐴 − 𝑟) < 𝑌 ∧ 𝑌 < (𝐴 + 𝑟))))
76	72, 74, 75	syl2anc 567	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → (𝑌 ∈ ((𝐴 − 𝑟)(,)(𝐴 + 𝑟)) ↔ (𝑌 ∈ ℝ ∧ (𝐴 − 𝑟) < 𝑌 ∧ 𝑌 < (𝐴 + 𝑟))))
77	50, 69, 70, 76	mpbir3and 1427	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → 𝑌 ∈ ((𝐴 − 𝑟)(,)(𝐴 + 𝑟)))
78	47, 77	sseldi 3751	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → 𝑌 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟)))
79		fvres 6349	. . . . . . . . . . . 12 ⊢ (𝑌 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟)) → ((𝐹 ↾ ((𝐴 − 𝑟)[,](𝐴 + 𝑟)))‘𝑌) = (𝐹‘𝑌))
80	78, 79	syl 17	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → ((𝐹 ↾ ((𝐴 − 𝑟)[,](𝐴 + 𝑟)))‘𝑌) = (𝐹‘𝑌))
81	20, 48	eleqtrd 2852	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → 𝑍 ∈ ℝ)
82	81	ad2antrr 699	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → 𝑍 ∈ ℝ)
83		xmetsym 22373	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐽 ∈ (∞Met‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ 𝑍 ∈ 𝑆) → (𝐴𝐽𝑍) = (𝑍𝐽𝐴))
84	9, 11, 20, 83	syl3anc 1476	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → (𝐴𝐽𝑍) = (𝑍𝐽𝐴))
85	55	oveqd 6811	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → (𝑍𝐽𝐴) = (𝑍((abs ∘ − ) ↾ (ℝ × ℝ))𝐴))
86	58	remetdval 22813	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑍 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝑍((abs ∘ − ) ↾ (ℝ × ℝ))𝐴) = (abs‘(𝑍 − 𝐴)))
87	81, 57, 86	syl2anc 567	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → (𝑍((abs ∘ − ) ↾ (ℝ × ℝ))𝐴) = (abs‘(𝑍 − 𝐴)))
88	84, 85, 87	3eqtrd 2809	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → (𝐴𝐽𝑍) = (abs‘(𝑍 − 𝐴)))
89	88	ad2antrr 699	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → (𝐴𝐽𝑍) = (abs‘(𝑍 − 𝐴)))
90		simprlr 759	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → (𝐴𝐽𝑍) < 𝑟)
91	89, 90	eqbrtrrd 4811	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → (abs‘(𝑍 − 𝐴)) < 𝑟)
92	82, 65, 66	absdifltd 14381	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → ((abs‘(𝑍 − 𝐴)) < 𝑟 ↔ ((𝐴 − 𝑟) < 𝑍 ∧ 𝑍 < (𝐴 + 𝑟))))
93	91, 92	mpbid 222	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → ((𝐴 − 𝑟) < 𝑍 ∧ 𝑍 < (𝐴 + 𝑟)))
94	93	simpld 478	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → (𝐴 − 𝑟) < 𝑍)
95	93	simprd 479	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → 𝑍 < (𝐴 + 𝑟))
96		elioo2 12422	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 − 𝑟) ∈ ℝ^* ∧ (𝐴 + 𝑟) ∈ ℝ^*) → (𝑍 ∈ ((𝐴 − 𝑟)(,)(𝐴 + 𝑟)) ↔ (𝑍 ∈ ℝ ∧ (𝐴 − 𝑟) < 𝑍 ∧ 𝑍 < (𝐴 + 𝑟))))
97	72, 74, 96	syl2anc 567	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → (𝑍 ∈ ((𝐴 − 𝑟)(,)(𝐴 + 𝑟)) ↔ (𝑍 ∈ ℝ ∧ (𝐴 − 𝑟) < 𝑍 ∧ 𝑍 < (𝐴 + 𝑟))))
98	82, 94, 95, 97	mpbir3and 1427	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → 𝑍 ∈ ((𝐴 − 𝑟)(,)(𝐴 + 𝑟)))
99	47, 98	sseldi 3751	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → 𝑍 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟)))
100		fvres 6349	. . . . . . . . . . . 12 ⊢ (𝑍 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟)) → ((𝐹 ↾ ((𝐴 − 𝑟)[,](𝐴 + 𝑟)))‘𝑍) = (𝐹‘𝑍))
101	99, 100	syl 17	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → ((𝐹 ↾ ((𝐴 − 𝑟)[,](𝐴 + 𝑟)))‘𝑍) = (𝐹‘𝑍))
102	80, 101	oveq12d 6812	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → (((𝐹 ↾ ((𝐴 − 𝑟)[,](𝐴 + 𝑟)))‘𝑌) − ((𝐹 ↾ ((𝐴 − 𝑟)[,](𝐴 + 𝑟)))‘𝑍)) = ((𝐹‘𝑌) − (𝐹‘𝑍)))
103	102	fveq2d 6337	. . . . . . . . 9 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → (abs‘(((𝐹 ↾ ((𝐴 − 𝑟)[,](𝐴 + 𝑟)))‘𝑌) − ((𝐹 ↾ ((𝐴 − 𝑟)[,](𝐴 + 𝑟)))‘𝑍))) = (abs‘((𝐹‘𝑌) − (𝐹‘𝑍))))
104	9	ad3antrrr 703	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))) → 𝐽 ∈ (∞Met‘𝑆))
105		elicc2 12444	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐴 − 𝑟) ∈ ℝ ∧ (𝐴 + 𝑟) ∈ ℝ) → (𝑥 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟)) ↔ (𝑥 ∈ ℝ ∧ (𝐴 − 𝑟) ≤ 𝑥 ∧ 𝑥 ≤ (𝐴 + 𝑟))))
106	71, 73, 105	syl2anc 567	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → (𝑥 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟)) ↔ (𝑥 ∈ ℝ ∧ (𝐴 − 𝑟) ≤ 𝑥 ∧ 𝑥 ≤ (𝐴 + 𝑟))))
107	106	biimpa 462	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))) → (𝑥 ∈ ℝ ∧ (𝐴 − 𝑟) ≤ 𝑥 ∧ 𝑥 ≤ (𝐴 + 𝑟)))
108	107	simp1d 1136	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))) → 𝑥 ∈ ℝ)
109	48	ad3antrrr 703	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))) → 𝑆 = ℝ)
110	108, 109	eleqtrrd 2853	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))) → 𝑥 ∈ 𝑆)
111	11	ad3antrrr 703	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))) → 𝐴 ∈ 𝑆)
112		xmetcl 22357	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐽 ∈ (∞Met‘𝑆) ∧ 𝑥 ∈ 𝑆 ∧ 𝐴 ∈ 𝑆) → (𝑥𝐽𝐴) ∈ ℝ^*)
113	104, 110, 111, 112	syl3anc 1476	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))) → (𝑥𝐽𝐴) ∈ ℝ^*)
114	66	adantr 466	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))) → 𝑟 ∈ ℝ)
115	114	rexrd 10292	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))) → 𝑟 ∈ ℝ^*)
116	16	ad3antrrr 703	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))) → 𝑅 ∈ ℝ^*)
117	55	ad3antrrr 703	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))) → 𝐽 = ((abs ∘ − ) ↾ (ℝ × ℝ)))
118	117	oveqd 6811	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))) → (𝑥𝐽𝐴) = (𝑥((abs ∘ − ) ↾ (ℝ × ℝ))𝐴))
119	65	adantr 466	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))) → 𝐴 ∈ ℝ)
120	58	remetdval 22813	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝑥((abs ∘ − ) ↾ (ℝ × ℝ))𝐴) = (abs‘(𝑥 − 𝐴)))
121	108, 119, 120	syl2anc 567	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))) → (𝑥((abs ∘ − ) ↾ (ℝ × ℝ))𝐴) = (abs‘(𝑥 − 𝐴)))
122	118, 121	eqtrd 2805	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))) → (𝑥𝐽𝐴) = (abs‘(𝑥 − 𝐴)))
123	107	simp2d 1137	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))) → (𝐴 − 𝑟) ≤ 𝑥)
124	107	simp3d 1138	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))) → 𝑥 ≤ (𝐴 + 𝑟))
125	108, 119, 114	absdifled 14382	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))) → ((abs‘(𝑥 − 𝐴)) ≤ 𝑟 ↔ ((𝐴 − 𝑟) ≤ 𝑥 ∧ 𝑥 ≤ (𝐴 + 𝑟))))
126	123, 124, 125	mpbir2and 686	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))) → (abs‘(𝑥 − 𝐴)) ≤ 𝑟)
127	122, 126	eqbrtrd 4809	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))) → (𝑥𝐽𝐴) ≤ 𝑟)
128		simplrr 757	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))) → 𝑟 < 𝑅)
129	113, 115, 116, 127, 128	xrlelttrd 12197	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))) → (𝑥𝐽𝐴) < 𝑅)
130		elbl3 22418	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐽 ∈ (∞Met‘𝑆) ∧ 𝑅 ∈ ℝ^*) ∧ (𝐴 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆)) → (𝑥 ∈ (𝐴(ball‘𝐽)𝑅) ↔ (𝑥𝐽𝐴) < 𝑅))
131	104, 116, 111, 110, 130	syl22anc 1477	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))) → (𝑥 ∈ (𝐴(ball‘𝐽)𝑅) ↔ (𝑥𝐽𝐴) < 𝑅))
132	129, 131	mpbird 247	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))) → 𝑥 ∈ (𝐴(ball‘𝐽)𝑅))
133	132	ex 397	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → (𝑥 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟)) → 𝑥 ∈ (𝐴(ball‘𝐽)𝑅)))
134	133	ssrdv 3759	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → ((𝐴 − 𝑟)[,](𝐴 + 𝑟)) ⊆ (𝐴(ball‘𝐽)𝑅))
135	134, 13	syl6sseqr 3802	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → ((𝐴 − 𝑟)[,](𝐴 + 𝑟)) ⊆ 𝐵)
136	135	resabs1d 5570	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → ((𝐹 ↾ 𝐵) ↾ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))) = (𝐹 ↾ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))))
137		ax-resscn 10196	. . . . . . . . . . . . . . . 16 ⊢ ℝ ⊆ ℂ
138	137	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → ℝ ⊆ ℂ)
139		dvlip2.f	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐹:𝑋⟶ℂ)
140	139	ad4antr 706	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → 𝐹:𝑋⟶ℂ)
141		dvlip2.d	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 ⊆ dom (𝑆 D 𝐹))
142		dvlip2.x	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑋 ⊆ 𝑆)
143	5, 139, 142	dvbss 23886	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → dom (𝑆 D 𝐹) ⊆ 𝑋)
144	141, 143	sstrd 3763	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐵 ⊆ 𝑋)
145	144	ad4antr 706	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → 𝐵 ⊆ 𝑋)
146	140, 145	fssresd 6212	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → (𝐹 ↾ 𝐵):𝐵⟶ℂ)
147		blssm 22444	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐽 ∈ (∞Met‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ 𝑅 ∈ ℝ^*) → (𝐴(ball‘𝐽)𝑅) ⊆ 𝑆)
148	9, 11, 16, 147	syl3anc 1476	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → (𝐴(ball‘𝐽)𝑅) ⊆ 𝑆)
149	13, 148	syl5eqss 3799	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → 𝐵 ⊆ 𝑆)
150	149, 48	sseqtrd 3791	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → 𝐵 ⊆ ℝ)
151	150	ad2antrr 699	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → 𝐵 ⊆ ℝ)
152	137	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → ℝ ⊆ ℂ)
153	139	ad2antrr 699	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → 𝐹:𝑋⟶ℂ)
154	142	ad2antrr 699	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → 𝑋 ⊆ 𝑆)
155	154, 48	sseqtrd 3791	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → 𝑋 ⊆ ℝ)
156		eqid 2771	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
157	156	tgioo2 22827	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
158	156, 157	dvres 23896	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℝ ⊆ ℂ ∧ 𝐹:𝑋⟶ℂ) ∧ (𝑋 ⊆ ℝ ∧ 𝐵 ⊆ ℝ)) → (ℝ D (𝐹 ↾ 𝐵)) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘𝐵)))
159	152, 153, 155, 150, 158	syl22anc 1477	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → (ℝ D (𝐹 ↾ 𝐵)) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘𝐵)))
160		retop 22786	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (topGen‘ran (,)) ∈ Top
161	55	fveq2d 6337	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → (ball‘𝐽) = (ball‘((abs ∘ − ) ↾ (ℝ × ℝ))))
162	161	oveqd 6811	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → (𝐴(ball‘𝐽)𝑅) = (𝐴(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑅))
163	13, 162	syl5eq 2817	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → 𝐵 = (𝐴(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑅))
164	55, 9	eqeltrrd 2851	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → ((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘𝑆))
165		eqid 2771	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ))) = (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ)))
166	58, 165	tgioo 22820	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (topGen‘ran (,)) = (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ)))
167	166	blopn 22526	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ 𝑅 ∈ ℝ^*) → (𝐴(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑅) ∈ (topGen‘ran (,)))
168	164, 11, 16, 167	syl3anc 1476	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → (𝐴(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑅) ∈ (topGen‘ran (,)))
169	163, 168	eqeltrd 2850	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → 𝐵 ∈ (topGen‘ran (,)))
170		isopn3i 21108	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((topGen‘ran (,)) ∈ Top ∧ 𝐵 ∈ (topGen‘ran (,))) → ((int‘(topGen‘ran (,)))‘𝐵) = 𝐵)
171	160, 169, 170	sylancr 569	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → ((int‘(topGen‘ran (,)))‘𝐵) = 𝐵)
172	171	reseq2d 5535	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘𝐵)) = ((ℝ D 𝐹) ↾ 𝐵))
173	159, 172	eqtrd 2805	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → (ℝ D (𝐹 ↾ 𝐵)) = ((ℝ D 𝐹) ↾ 𝐵))
174	173	dmeqd 5465	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → dom (ℝ D (𝐹 ↾ 𝐵)) = dom ((ℝ D 𝐹) ↾ 𝐵))
175		dmres 5561	. . . . . . . . . . . . . . . . . 18 ⊢ dom ((ℝ D 𝐹) ↾ 𝐵) = (𝐵 ∩ dom (ℝ D 𝐹))
176	141	ad2antrr 699	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → 𝐵 ⊆ dom (𝑆 D 𝐹))
177	48	oveq1d 6809	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → (𝑆 D 𝐹) = (ℝ D 𝐹))
178	177	dmeqd 5465	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → dom (𝑆 D 𝐹) = dom (ℝ D 𝐹))
179	176, 178	sseqtrd 3791	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → 𝐵 ⊆ dom (ℝ D 𝐹))
180		df-ss 3738	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ⊆ dom (ℝ D 𝐹) ↔ (𝐵 ∩ dom (ℝ D 𝐹)) = 𝐵)
181	179, 180	sylib 208	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → (𝐵 ∩ dom (ℝ D 𝐹)) = 𝐵)
182	175, 181	syl5eq 2817	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → dom ((ℝ D 𝐹) ↾ 𝐵) = 𝐵)
183	174, 182	eqtrd 2805	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → dom (ℝ D (𝐹 ↾ 𝐵)) = 𝐵)
184	183	ad2antrr 699	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → dom (ℝ D (𝐹 ↾ 𝐵)) = 𝐵)
185		dvcn 23905	. . . . . . . . . . . . . . 15 ⊢ (((ℝ ⊆ ℂ ∧ (𝐹 ↾ 𝐵):𝐵⟶ℂ ∧ 𝐵 ⊆ ℝ) ∧ dom (ℝ D (𝐹 ↾ 𝐵)) = 𝐵) → (𝐹 ↾ 𝐵) ∈ (𝐵–cn→ℂ))
186	138, 146, 151, 184, 185	syl31anc 1479	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → (𝐹 ↾ 𝐵) ∈ (𝐵–cn→ℂ))
187		rescncf 22921	. . . . . . . . . . . . . 14 ⊢ (((𝐴 − 𝑟)[,](𝐴 + 𝑟)) ⊆ 𝐵 → ((𝐹 ↾ 𝐵) ∈ (𝐵–cn→ℂ) → ((𝐹 ↾ 𝐵) ↾ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))) ∈ (((𝐴 − 𝑟)[,](𝐴 + 𝑟))–cn→ℂ)))
188	135, 186, 187	sylc 65	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → ((𝐹 ↾ 𝐵) ↾ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))) ∈ (((𝐴 − 𝑟)[,](𝐴 + 𝑟))–cn→ℂ))
189	136, 188	eqeltrrd 2851	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → (𝐹 ↾ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))) ∈ (((𝐴 − 𝑟)[,](𝐴 + 𝑟))–cn→ℂ))
190	135, 151	sstrd 3763	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → ((𝐴 − 𝑟)[,](𝐴 + 𝑟)) ⊆ ℝ)
191	156, 157	dvres 23896	. . . . . . . . . . . . . . . 16 ⊢ (((ℝ ⊆ ℂ ∧ (𝐹 ↾ 𝐵):𝐵⟶ℂ) ∧ (𝐵 ⊆ ℝ ∧ ((𝐴 − 𝑟)[,](𝐴 + 𝑟)) ⊆ ℝ)) → (ℝ D ((𝐹 ↾ 𝐵) ↾ ((𝐴 − 𝑟)[,](𝐴 + 𝑟)))) = ((ℝ D (𝐹 ↾ 𝐵)) ↾ ((int‘(topGen‘ran (,)))‘((𝐴 − 𝑟)[,](𝐴 + 𝑟)))))
192	138, 146, 151, 190, 191	syl22anc 1477	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → (ℝ D ((𝐹 ↾ 𝐵) ↾ ((𝐴 − 𝑟)[,](𝐴 + 𝑟)))) = ((ℝ D (𝐹 ↾ 𝐵)) ↾ ((int‘(topGen‘ran (,)))‘((𝐴 − 𝑟)[,](𝐴 + 𝑟)))))
193	136	oveq2d 6810	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → (ℝ D ((𝐹 ↾ 𝐵) ↾ ((𝐴 − 𝑟)[,](𝐴 + 𝑟)))) = (ℝ D (𝐹 ↾ ((𝐴 − 𝑟)[,](𝐴 + 𝑟)))))
194		iccntr 22845	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 − 𝑟) ∈ ℝ ∧ (𝐴 + 𝑟) ∈ ℝ) → ((int‘(topGen‘ran (,)))‘((𝐴 − 𝑟)[,](𝐴 + 𝑟))) = ((𝐴 − 𝑟)(,)(𝐴 + 𝑟)))
195	71, 73, 194	syl2anc 567	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → ((int‘(topGen‘ran (,)))‘((𝐴 − 𝑟)[,](𝐴 + 𝑟))) = ((𝐴 − 𝑟)(,)(𝐴 + 𝑟)))
196	195	reseq2d 5535	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → ((ℝ D (𝐹 ↾ 𝐵)) ↾ ((int‘(topGen‘ran (,)))‘((𝐴 − 𝑟)[,](𝐴 + 𝑟)))) = ((ℝ D (𝐹 ↾ 𝐵)) ↾ ((𝐴 − 𝑟)(,)(𝐴 + 𝑟))))
197	192, 193, 196	3eqtr3d 2813	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → (ℝ D (𝐹 ↾ ((𝐴 − 𝑟)[,](𝐴 + 𝑟)))) = ((ℝ D (𝐹 ↾ 𝐵)) ↾ ((𝐴 − 𝑟)(,)(𝐴 + 𝑟))))
198	197	dmeqd 5465	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → dom (ℝ D (𝐹 ↾ ((𝐴 − 𝑟)[,](𝐴 + 𝑟)))) = dom ((ℝ D (𝐹 ↾ 𝐵)) ↾ ((𝐴 − 𝑟)(,)(𝐴 + 𝑟))))
199		dmres 5561	. . . . . . . . . . . . . 14 ⊢ dom ((ℝ D (𝐹 ↾ 𝐵)) ↾ ((𝐴 − 𝑟)(,)(𝐴 + 𝑟))) = (((𝐴 − 𝑟)(,)(𝐴 + 𝑟)) ∩ dom (ℝ D (𝐹 ↾ 𝐵)))
200	47, 135	syl5ss 3764	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → ((𝐴 − 𝑟)(,)(𝐴 + 𝑟)) ⊆ 𝐵)
201	200, 184	sseqtr4d 3792	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → ((𝐴 − 𝑟)(,)(𝐴 + 𝑟)) ⊆ dom (ℝ D (𝐹 ↾ 𝐵)))
202		df-ss 3738	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 − 𝑟)(,)(𝐴 + 𝑟)) ⊆ dom (ℝ D (𝐹 ↾ 𝐵)) ↔ (((𝐴 − 𝑟)(,)(𝐴 + 𝑟)) ∩ dom (ℝ D (𝐹 ↾ 𝐵))) = ((𝐴 − 𝑟)(,)(𝐴 + 𝑟)))
203	201, 202	sylib 208	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → (((𝐴 − 𝑟)(,)(𝐴 + 𝑟)) ∩ dom (ℝ D (𝐹 ↾ 𝐵))) = ((𝐴 − 𝑟)(,)(𝐴 + 𝑟)))
204	199, 203	syl5eq 2817	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → dom ((ℝ D (𝐹 ↾ 𝐵)) ↾ ((𝐴 − 𝑟)(,)(𝐴 + 𝑟))) = ((𝐴 − 𝑟)(,)(𝐴 + 𝑟)))
205	198, 204	eqtrd 2805	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → dom (ℝ D (𝐹 ↾ ((𝐴 − 𝑟)[,](𝐴 + 𝑟)))) = ((𝐴 − 𝑟)(,)(𝐴 + 𝑟)))
206		dvlip2.m	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ ℝ)
207	206	ad4antr 706	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → 𝑀 ∈ ℝ)
208	197	fveq1d 6335	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → ((ℝ D (𝐹 ↾ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))))‘𝑥) = (((ℝ D (𝐹 ↾ 𝐵)) ↾ ((𝐴 − 𝑟)(,)(𝐴 + 𝑟)))‘𝑥))
209		fvres 6349	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ((𝐴 − 𝑟)(,)(𝐴 + 𝑟)) → (((ℝ D (𝐹 ↾ 𝐵)) ↾ ((𝐴 − 𝑟)(,)(𝐴 + 𝑟)))‘𝑥) = ((ℝ D (𝐹 ↾ 𝐵))‘𝑥))
210	208, 209	sylan9eq 2825	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)(,)(𝐴 + 𝑟))) → ((ℝ D (𝐹 ↾ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))))‘𝑥) = ((ℝ D (𝐹 ↾ 𝐵))‘𝑥))
211	177	reseq1d 5534	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → ((𝑆 D 𝐹) ↾ 𝐵) = ((ℝ D 𝐹) ↾ 𝐵))
212	173, 211	eqtr4d 2808	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → (ℝ D (𝐹 ↾ 𝐵)) = ((𝑆 D 𝐹) ↾ 𝐵))
213	212	fveq1d 6335	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → ((ℝ D (𝐹 ↾ 𝐵))‘𝑥) = (((𝑆 D 𝐹) ↾ 𝐵)‘𝑥))
214	213	ad3antrrr 703	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)(,)(𝐴 + 𝑟))) → ((ℝ D (𝐹 ↾ 𝐵))‘𝑥) = (((𝑆 D 𝐹) ↾ 𝐵)‘𝑥))
215	200	sselda 3753	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)(,)(𝐴 + 𝑟))) → 𝑥 ∈ 𝐵)
216		fvres 6349	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ 𝐵 → (((𝑆 D 𝐹) ↾ 𝐵)‘𝑥) = ((𝑆 D 𝐹)‘𝑥))
217	215, 216	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)(,)(𝐴 + 𝑟))) → (((𝑆 D 𝐹) ↾ 𝐵)‘𝑥) = ((𝑆 D 𝐹)‘𝑥))
218	210, 214, 217	3eqtrd 2809	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)(,)(𝐴 + 𝑟))) → ((ℝ D (𝐹 ↾ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))))‘𝑥) = ((𝑆 D 𝐹)‘𝑥))
219	218	fveq2d 6337	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)(,)(𝐴 + 𝑟))) → (abs‘((ℝ D (𝐹 ↾ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))))‘𝑥)) = (abs‘((𝑆 D 𝐹)‘𝑥)))
220		simp-4l 762	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → 𝜑)
221		dvlip2.l	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (abs‘((𝑆 D 𝐹)‘𝑥)) ≤ 𝑀)
222	220, 221	sylan 563	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ 𝐵) → (abs‘((𝑆 D 𝐹)‘𝑥)) ≤ 𝑀)
223	215, 222	syldan 573	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)(,)(𝐴 + 𝑟))) → (abs‘((𝑆 D 𝐹)‘𝑥)) ≤ 𝑀)
224	219, 223	eqbrtrd 4809	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)(,)(𝐴 + 𝑟))) → (abs‘((ℝ D (𝐹 ↾ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))))‘𝑥)) ≤ 𝑀)
225	71, 73, 189, 205, 207, 224	dvlip 23977	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ (𝑌 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟)) ∧ 𝑍 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟)))) → (abs‘(((𝐹 ↾ ((𝐴 − 𝑟)[,](𝐴 + 𝑟)))‘𝑌) − ((𝐹 ↾ ((𝐴 − 𝑟)[,](𝐴 + 𝑟)))‘𝑍))) ≤ (𝑀 · (abs‘(𝑌 − 𝑍))))
226	225	ex 397	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → ((𝑌 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟)) ∧ 𝑍 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))) → (abs‘(((𝐹 ↾ ((𝐴 − 𝑟)[,](𝐴 + 𝑟)))‘𝑌) − ((𝐹 ↾ ((𝐴 − 𝑟)[,](𝐴 + 𝑟)))‘𝑍))) ≤ (𝑀 · (abs‘(𝑌 − 𝑍)))))
227	78, 99, 226	mp2and 673	. . . . . . . . 9 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → (abs‘(((𝐹 ↾ ((𝐴 − 𝑟)[,](𝐴 + 𝑟)))‘𝑌) − ((𝐹 ↾ ((𝐴 − 𝑟)[,](𝐴 + 𝑟)))‘𝑍))) ≤ (𝑀 · (abs‘(𝑌 − 𝑍))))
228	103, 227	eqbrtrrd 4811	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → (abs‘((𝐹‘𝑌) − (𝐹‘𝑍))) ≤ (𝑀 · (abs‘(𝑌 − 𝑍))))
229	228	exp32 407	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) → (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) → (𝑟 < 𝑅 → (abs‘((𝐹‘𝑌) − (𝐹‘𝑍))) ≤ (𝑀 · (abs‘(𝑌 − 𝑍))))))
230	46, 229	sylbid 230	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) → (if((𝐴𝐽𝑌) ≤ (𝐴𝐽𝑍), (𝐴𝐽𝑍), (𝐴𝐽𝑌)) < 𝑟 → (𝑟 < 𝑅 → (abs‘((𝐹‘𝑌) − (𝐹‘𝑍))) ≤ (𝑀 · (abs‘(𝑌 − 𝑍))))))
231	230	impd 396	. . . . 5 ⊢ ((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) → ((if((𝐴𝐽𝑌) ≤ (𝐴𝐽𝑍), (𝐴𝐽𝑍), (𝐴𝐽𝑌)) < 𝑟 ∧ 𝑟 < 𝑅) → (abs‘((𝐹‘𝑌) − (𝐹‘𝑍))) ≤ (𝑀 · (abs‘(𝑌 − 𝑍)))))
232	40, 231	sylan2 574	. . . 4 ⊢ ((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℚ) → ((if((𝐴𝐽𝑌) ≤ (𝐴𝐽𝑍), (𝐴𝐽𝑍), (𝐴𝐽𝑌)) < 𝑟 ∧ 𝑟 < 𝑅) → (abs‘((𝐹‘𝑌) − (𝐹‘𝑍))) ≤ (𝑀 · (abs‘(𝑌 − 𝑍)))))
233	232	rexlimdva 3179	. . 3 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → (∃𝑟 ∈ ℚ (if((𝐴𝐽𝑌) ≤ (𝐴𝐽𝑍), (𝐴𝐽𝑍), (𝐴𝐽𝑌)) < 𝑟 ∧ 𝑟 < 𝑅) → (abs‘((𝐹‘𝑌) − (𝐹‘𝑍))) ≤ (𝑀 · (abs‘(𝑌 − 𝑍)))))
234	39, 233	mpd 15	. 2 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → (abs‘((𝐹‘𝑌) − (𝐹‘𝑍))) ≤ (𝑀 · (abs‘(𝑌 − 𝑍))))
235		simpr 471	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑆 = ℂ) → 𝑆 = ℂ)
236	235	sqxpeqd 5282	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑆 = ℂ) → (𝑆 × 𝑆) = (ℂ × ℂ))
237	236	reseq2d 5535	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑆 = ℂ) → ((abs ∘ − ) ↾ (𝑆 × 𝑆)) = ((abs ∘ − ) ↾ (ℂ × ℂ)))
238		absf 14286	. . . . . . . . . . . . . 14 ⊢ abs:ℂ⟶ℝ
239		subf 10486	. . . . . . . . . . . . . 14 ⊢ − :(ℂ × ℂ)⟶ℂ
240		fco 6199	. . . . . . . . . . . . . 14 ⊢ ((abs:ℂ⟶ℝ ∧ − :(ℂ × ℂ)⟶ℂ) → (abs ∘ − ):(ℂ × ℂ)⟶ℝ)
241	238, 239, 240	mp2an 666	. . . . . . . . . . . . 13 ⊢ (abs ∘ − ):(ℂ × ℂ)⟶ℝ
242		ffn 6186	. . . . . . . . . . . . 13 ⊢ ((abs ∘ − ):(ℂ × ℂ)⟶ℝ → (abs ∘ − ) Fn (ℂ × ℂ))
243		fnresdm 6141	. . . . . . . . . . . . 13 ⊢ ((abs ∘ − ) Fn (ℂ × ℂ) → ((abs ∘ − ) ↾ (ℂ × ℂ)) = (abs ∘ − ))
244	241, 242, 243	mp2b 10	. . . . . . . . . . . 12 ⊢ ((abs ∘ − ) ↾ (ℂ × ℂ)) = (abs ∘ − )
245	237, 244	syl6eq 2821	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑆 = ℂ) → ((abs ∘ − ) ↾ (𝑆 × 𝑆)) = (abs ∘ − ))
246	1, 245	syl5eq 2817	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑆 = ℂ) → 𝐽 = (abs ∘ − ))
247	246	fveq2d 6337	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑆 = ℂ) → (ball‘𝐽) = (ball‘(abs ∘ − )))
248	247	oveqd 6811	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑆 = ℂ) → (𝐴(ball‘𝐽)𝑅) = (𝐴(ball‘(abs ∘ − ))𝑅))
249	13, 248	syl5eq 2817	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑆 = ℂ) → 𝐵 = (𝐴(ball‘(abs ∘ − ))𝑅))
250	249	eleq2d 2836	. . . . . 6 ⊢ ((𝜑 ∧ 𝑆 = ℂ) → (𝑌 ∈ 𝐵 ↔ 𝑌 ∈ (𝐴(ball‘(abs ∘ − ))𝑅)))
251	249	eleq2d 2836	. . . . . 6 ⊢ ((𝜑 ∧ 𝑆 = ℂ) → (𝑍 ∈ 𝐵 ↔ 𝑍 ∈ (𝐴(ball‘(abs ∘ − ))𝑅)))
252	250, 251	anbi12d 610	. . . . 5 ⊢ ((𝜑 ∧ 𝑆 = ℂ) → ((𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ↔ (𝑌 ∈ (𝐴(ball‘(abs ∘ − ))𝑅) ∧ 𝑍 ∈ (𝐴(ball‘(abs ∘ − ))𝑅))))
253	252	biimpa 462	. . . 4 ⊢ (((𝜑 ∧ 𝑆 = ℂ) ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑌 ∈ (𝐴(ball‘(abs ∘ − ))𝑅) ∧ 𝑍 ∈ (𝐴(ball‘(abs ∘ − ))𝑅)))
254	142	adantr 466	. . . . . 6 ⊢ ((𝜑 ∧ 𝑆 = ℂ) → 𝑋 ⊆ 𝑆)
255	254, 235	sseqtrd 3791	. . . . 5 ⊢ ((𝜑 ∧ 𝑆 = ℂ) → 𝑋 ⊆ ℂ)
256	139	adantr 466	. . . . 5 ⊢ ((𝜑 ∧ 𝑆 = ℂ) → 𝐹:𝑋⟶ℂ)
257	10	adantr 466	. . . . . 6 ⊢ ((𝜑 ∧ 𝑆 = ℂ) → 𝐴 ∈ 𝑆)
258	257, 235	eleqtrd 2852	. . . . 5 ⊢ ((𝜑 ∧ 𝑆 = ℂ) → 𝐴 ∈ ℂ)
259	15	adantr 466	. . . . 5 ⊢ ((𝜑 ∧ 𝑆 = ℂ) → 𝑅 ∈ ℝ^*)
260		eqid 2771	. . . . 5 ⊢ (𝐴(ball‘(abs ∘ − ))𝑅) = (𝐴(ball‘(abs ∘ − ))𝑅)
261	141	adantr 466	. . . . . 6 ⊢ ((𝜑 ∧ 𝑆 = ℂ) → 𝐵 ⊆ dom (𝑆 D 𝐹))
262	235	oveq1d 6809	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑆 = ℂ) → (𝑆 D 𝐹) = (ℂ D 𝐹))
263	262	dmeqd 5465	. . . . . 6 ⊢ ((𝜑 ∧ 𝑆 = ℂ) → dom (𝑆 D 𝐹) = dom (ℂ D 𝐹))
264	261, 249, 263	3sstr3d 3797	. . . . 5 ⊢ ((𝜑 ∧ 𝑆 = ℂ) → (𝐴(ball‘(abs ∘ − ))𝑅) ⊆ dom (ℂ D 𝐹))
265	206	adantr 466	. . . . 5 ⊢ ((𝜑 ∧ 𝑆 = ℂ) → 𝑀 ∈ ℝ)
266	221	ex 397	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐵 → (abs‘((𝑆 D 𝐹)‘𝑥)) ≤ 𝑀))
267	266	adantr 466	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑆 = ℂ) → (𝑥 ∈ 𝐵 → (abs‘((𝑆 D 𝐹)‘𝑥)) ≤ 𝑀))
268	249	eleq2d 2836	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑆 = ℂ) → (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ (𝐴(ball‘(abs ∘ − ))𝑅)))
269	262	fveq1d 6335	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑆 = ℂ) → ((𝑆 D 𝐹)‘𝑥) = ((ℂ D 𝐹)‘𝑥))
270	269	fveq2d 6337	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑆 = ℂ) → (abs‘((𝑆 D 𝐹)‘𝑥)) = (abs‘((ℂ D 𝐹)‘𝑥)))
271	270	breq1d 4797	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑆 = ℂ) → ((abs‘((𝑆 D 𝐹)‘𝑥)) ≤ 𝑀 ↔ (abs‘((ℂ D 𝐹)‘𝑥)) ≤ 𝑀))
272	267, 268, 271	3imtr3d 282	. . . . . 6 ⊢ ((𝜑 ∧ 𝑆 = ℂ) → (𝑥 ∈ (𝐴(ball‘(abs ∘ − ))𝑅) → (abs‘((ℂ D 𝐹)‘𝑥)) ≤ 𝑀))
273	272	imp 393	. . . . 5 ⊢ (((𝜑 ∧ 𝑆 = ℂ) ∧ 𝑥 ∈ (𝐴(ball‘(abs ∘ − ))𝑅)) → (abs‘((ℂ D 𝐹)‘𝑥)) ≤ 𝑀)
274	255, 256, 258, 259, 260, 264, 265, 273	dvlipcn 23978	. . . 4 ⊢ (((𝜑 ∧ 𝑆 = ℂ) ∧ (𝑌 ∈ (𝐴(ball‘(abs ∘ − ))𝑅) ∧ 𝑍 ∈ (𝐴(ball‘(abs ∘ − ))𝑅))) → (abs‘((𝐹‘𝑌) − (𝐹‘𝑍))) ≤ (𝑀 · (abs‘(𝑌 − 𝑍))))
275	253, 274	syldan 573	. . 3 ⊢ (((𝜑 ∧ 𝑆 = ℂ) ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (abs‘((𝐹‘𝑌) − (𝐹‘𝑍))) ≤ (𝑀 · (abs‘(𝑌 − 𝑍))))
276	275	an32s 625	. 2 ⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℂ) → (abs‘((𝐹‘𝑌) − (𝐹‘𝑍))) ≤ (𝑀 · (abs‘(𝑌 − 𝑍))))
277		elpri 4338	. . . 4 ⊢ (𝑆 ∈ {ℝ, ℂ} → (𝑆 = ℝ ∨ 𝑆 = ℂ))
278	3, 277	syl 17	. . 3 ⊢ (𝜑 → (𝑆 = ℝ ∨ 𝑆 = ℂ))
279	278	adantr 466	. 2 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑆 = ℝ ∨ 𝑆 = ℂ))
280	234, 276, 279	mpjaodan 933	1 ⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (abs‘((𝐹‘𝑌) − (𝐹‘𝑍))) ≤ (𝑀 · (abs‘(𝑌 − 𝑍))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 196 ∧ wa 382 ∨ wo 828 ∧ w3a 1071 = wceq 1631 ∈ wcel 2145 ∃wrex 3062 ∩ cin 3723 ⊆ wss 3724 ifcif 4226 {cpr 4319 class class class wbr 4787 × cxp 5248 dom cdm 5250 ran crn 5251 ↾ cres 5252 ∘ ccom 5254 Fn wfn 6027 ⟶wf 6028 ‘cfv 6032 (class class class)co 6794 ℂcc 10137 ℝcr 10138 + caddc 10142 · cmul 10144 ℝ^*cxr 10276 < clt 10277 ≤ cle 10278 − cmin 10469 ℚcq 11992 (,)cioo 12381 [,]cicc 12384 abscabs 14183 TopOpenctopn 16291 topGenctg 16307 ∞Metcxmt 19947 ballcbl 19949 MetOpencmopn 19952 ℂ_fldccnfld 19962 Topctop 20919 intcnt 21043 –cn→ccncf 22900 D cdv 23848

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-8 2147 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 ax-rep 4905 ax-sep 4916 ax-nul 4924 ax-pow 4975 ax-pr 5035 ax-un 7097 ax-inf2 8703 ax-cnex 10195 ax-resscn 10196 ax-1cn 10197 ax-icn 10198 ax-addcl 10199 ax-addrcl 10200 ax-mulcl 10201 ax-mulrcl 10202 ax-mulcom 10203 ax-addass 10204 ax-mulass 10205 ax-distr 10206 ax-i2m1 10207 ax-1ne0 10208 ax-1rid 10209 ax-rnegex 10210 ax-rrecex 10211 ax-cnre 10212 ax-pre-lttri 10213 ax-pre-lttrn 10214 ax-pre-ltadd 10215 ax-pre-mulgt0 10216 ax-pre-sup 10217 ax-addf 10218 ax-mulf 10219

This theorem depends on definitions: df-bi 197 df-an 383 df-or 829 df-3or 1072 df-3an 1073 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-eu 2622 df-mo 2623 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-ne 2944 df-nel 3047 df-ral 3066 df-rex 3067 df-reu 3068 df-rmo 3069 df-rab 3070 df-v 3353 df-sbc 3589 df-csb 3684 df-dif 3727 df-un 3729 df-in 3731 df-ss 3738 df-pss 3740 df-nul 4065 df-if 4227 df-pw 4300 df-sn 4318 df-pr 4320 df-tp 4322 df-op 4324 df-uni 4576 df-int 4613 df-iun 4657 df-iin 4658 df-br 4788 df-opab 4848 df-mpt 4865 df-tr 4888 df-id 5158 df-eprel 5163 df-po 5171 df-so 5172 df-fr 5209 df-se 5210 df-we 5211 df-xp 5256 df-rel 5257 df-cnv 5258 df-co 5259 df-dm 5260 df-rn 5261 df-res 5262 df-ima 5263 df-pred 5824 df-ord 5870 df-on 5871 df-lim 5872 df-suc 5873 df-iota 5995 df-fun 6034 df-fn 6035 df-f 6036 df-f1 6037 df-fo 6038 df-f1o 6039 df-fv 6040 df-isom 6041 df-riota 6755 df-ov 6797 df-oprab 6798 df-mpt2 6799 df-of 7045 df-om 7214 df-1st 7316 df-2nd 7317 df-supp 7448 df-wrecs 7560 df-recs 7622 df-rdg 7660 df-1o 7714 df-2o 7715 df-oadd 7718 df-er 7897 df-map 8012 df-pm 8013 df-ixp 8064 df-en 8111 df-dom 8112 df-sdom 8113 df-fin 8114 df-fsupp 8433 df-fi 8474 df-sup 8505 df-inf 8506 df-oi 8572 df-card 8966 df-cda 9193 df-pnf 10279 df-mnf 10280 df-xr 10281 df-ltxr 10282 df-le 10283 df-sub 10471 df-neg 10472 df-div 10888 df-nn 11224 df-2 11282 df-3 11283 df-4 11284 df-5 11285 df-6 11286 df-7 11287 df-8 11288 df-9 11289 df-n0 11496 df-z 11581 df-dec 11697 df-uz 11890 df-q 11993 df-rp 12037 df-xneg 12152 df-xadd 12153 df-xmul 12154 df-ioo 12385 df-ico 12387 df-icc 12388 df-fz 12535 df-fzo 12675 df-seq 13010 df-exp 13069 df-hash 13323 df-cj 14048 df-re 14049 df-im 14050 df-sqrt 14184 df-abs 14185 df-struct 16067 df-ndx 16068 df-slot 16069 df-base 16071 df-sets 16072 df-ress 16073 df-plusg 16163 df-mulr 16164 df-starv 16165 df-sca 16166 df-vsca 16167 df-ip 16168 df-tset 16169 df-ple 16170 df-ds 16173 df-unif 16174 df-hom 16175 df-cco 16176 df-rest 16292 df-topn 16293 df-0g 16311 df-gsum 16312 df-topgen 16313 df-pt 16314 df-prds 16317 df-xrs 16371 df-qtop 16376 df-imas 16377 df-xps 16379 df-mre 16455 df-mrc 16456 df-acs 16458 df-mgm 17451 df-sgrp 17493 df-mnd 17504 df-submnd 17545 df-mulg 17750 df-cntz 17958 df-cmn 18403 df-psmet 19954 df-xmet 19955 df-met 19956 df-bl 19957 df-mopn 19958 df-fbas 19959 df-fg 19960 df-cnfld 19963 df-top 20920 df-topon 20937 df-topsp 20959 df-bases 20972 df-cld 21045 df-ntr 21046 df-cls 21047 df-nei 21124 df-lp 21162 df-perf 21163 df-cn 21253 df-cnp 21254 df-haus 21341 df-cmp 21412 df-tx 21587 df-hmeo 21780 df-fil 21871 df-fm 21963 df-flim 21964 df-flf 21965 df-xms 22346 df-ms 22347 df-tms 22348 df-cncf 22902 df-limc 23851 df-dv 23852

This theorem is referenced by: ulmdvlem1 24375 dvconstbi 39060

W3C validator