minveclem4 - Metamath Proof Explorer

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

Theorem minveclem4 25753

Description: Lemma for minvec 25757. The convergent point of the Cauchy sequence 𝐹 attains the minimum distance, and so is closer to 𝐴 than any other point in 𝑌. (Contributed by Mario Carneiro, 7-May-2014.) (Revised by Mario Carneiro, 15-Oct-2015.) (Revised by AV, 3-Oct-2020.)

**Hypotheses**
Ref	Expression
minvec.x	⊢ 𝑋 = (Base‘𝑈)
minvec.m	⊢ − = (-_g‘𝑈)
minvec.n	⊢ 𝑁 = (norm‘𝑈)
minvec.u	⊢ (𝜑 → 𝑈 ∈ ℂPreHil)
minvec.y	⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈))
minvec.w	⊢ (𝜑 → (𝑈 ↾_s 𝑌) ∈ CMetSp)
minvec.a	⊢ (𝜑 → 𝐴 ∈ 𝑋)
minvec.j	⊢ 𝐽 = (TopOpen‘𝑈)
minvec.r	⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))
minvec.s	⊢ 𝑆 = inf(𝑅, ℝ, < )
minvec.d	⊢ 𝐷 = ((dist‘𝑈) ↾ (𝑋 × 𝑋))
minvec.f	⊢ 𝐹 = ran (𝑟 ∈ ℝ⁺ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)})
minvec.p	⊢ 𝑃 = ∪ (𝐽 fLim (𝑋filGen𝐹))
minvec.t	⊢ 𝑇 = (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2))

**Assertion**
Ref	Expression
minveclem4	⊢ (𝜑 → ∃𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))

Distinct variable groups: 𝑥,𝑦, − 𝑥,𝑟,𝑦,𝐴 𝐽,𝑟,𝑥,𝑦 𝑥,𝑃,𝑦 𝑥,𝐹,𝑦 𝑥,𝑁,𝑦 𝜑,𝑟,𝑥,𝑦 𝑥,𝑅,𝑦 𝑥,𝑈,𝑦 𝑋,𝑟,𝑥,𝑦 𝑌,𝑟,𝑥,𝑦 𝐷,𝑟,𝑥,𝑦 𝑆,𝑟,𝑥,𝑦 𝑇,𝑟,𝑦 Allowed substitution hints: 𝑃(𝑟) 𝑅(𝑟) 𝑇(𝑥) 𝑈(𝑟) 𝐹(𝑟) − (𝑟) 𝑁(𝑟)

Proof of Theorem minveclem4 Dummy variable 𝑤 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		minvec.x	. . . 4 ⊢ 𝑋 = (Base‘𝑈)
2		minvec.m	. . . 4 ⊢ − = (-_g‘𝑈)
3		minvec.n	. . . 4 ⊢ 𝑁 = (norm‘𝑈)
4		minvec.u	. . . 4 ⊢ (𝜑 → 𝑈 ∈ ℂPreHil)
5		minvec.y	. . . 4 ⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈))
6		minvec.w	. . . 4 ⊢ (𝜑 → (𝑈 ↾_s 𝑌) ∈ CMetSp)
7		minvec.a	. . . 4 ⊢ (𝜑 → 𝐴 ∈ 𝑋)
8		minvec.j	. . . 4 ⊢ 𝐽 = (TopOpen‘𝑈)
9		minvec.r	. . . 4 ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))
10		minvec.s	. . . 4 ⊢ 𝑆 = inf(𝑅, ℝ, < )
11		minvec.d	. . . 4 ⊢ 𝐷 = ((dist‘𝑈) ↾ (𝑋 × 𝑋))
12		minvec.f	. . . 4 ⊢ 𝐹 = ran (𝑟 ∈ ℝ⁺ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)})
13		minvec.p	. . . 4 ⊢ 𝑃 = ∪ (𝐽 fLim (𝑋filGen𝐹))
14	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13	minveclem4a 25751	. . 3 ⊢ (𝜑 → 𝑃 ∈ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌))
15	14	elin2d 4102	. 2 ⊢ (𝜑 → 𝑃 ∈ 𝑌)
16	11	oveqi 7433	. . . . . . 7 ⊢ (𝐴𝐷𝑃) = (𝐴((dist‘𝑈) ↾ (𝑋 × 𝑋))𝑃)
17	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13	minveclem4b 25752	. . . . . . . 8 ⊢ (𝜑 → 𝑃 ∈ 𝑋)
18	7, 17	ovresd 7587	. . . . . . 7 ⊢ (𝜑 → (𝐴((dist‘𝑈) ↾ (𝑋 × 𝑋))𝑃) = (𝐴(dist‘𝑈)𝑃))
19	16, 18	eqtrid 2807	. . . . . 6 ⊢ (𝜑 → (𝐴𝐷𝑃) = (𝐴(dist‘𝑈)𝑃))
20		cphngp 25494	. . . . . . . 8 ⊢ (𝑈 ∈ ℂPreHil → 𝑈 ∈ NrmGrp)
21	4, 20	syl 18	. . . . . . 7 ⊢ (𝜑 → 𝑈 ∈ NrmGrp)
22		eqid 2760	. . . . . . . 8 ⊢ (dist‘𝑈) = (dist‘𝑈)
23	3, 1, 2, 22	ngpds 24923	. . . . . . 7 ⊢ ((𝑈 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝐴(dist‘𝑈)𝑃) = (𝑁‘(𝐴 − 𝑃)))
24	21, 7, 17, 23	syl3anc 1398	. . . . . 6 ⊢ (𝜑 → (𝐴(dist‘𝑈)𝑃) = (𝑁‘(𝐴 − 𝑃)))
25	19, 24	eqtrd 2795	. . . . 5 ⊢ (𝜑 → (𝐴𝐷𝑃) = (𝑁‘(𝐴 − 𝑃)))
26	25	adantr 486	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝐴𝐷𝑃) = (𝑁‘(𝐴 − 𝑃)))
27		ngpms 24919	. . . . . . . 8 ⊢ (𝑈 ∈ NrmGrp → 𝑈 ∈ MetSp)
28	1, 11	msmet 24776	. . . . . . . 8 ⊢ (𝑈 ∈ MetSp → 𝐷 ∈ (Met‘𝑋))
29	21, 27, 28	3syl 19	. . . . . . 7 ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋))
30		metcl 24651	. . . . . . 7 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝐴𝐷𝑃) ∈ ℝ)
31	29, 7, 17, 30	syl3anc 1398	. . . . . 6 ⊢ (𝜑 → (𝐴𝐷𝑃) ∈ ℝ)
32	31	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝐴𝐷𝑃) ∈ ℝ)
33	1, 2, 3, 4, 5, 6, 7, 8, 9, 10	minveclem4c 25746	. . . . . 6 ⊢ (𝜑 → 𝑆 ∈ ℝ)
34	33	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑆 ∈ ℝ)
35	21	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑈 ∈ NrmGrp)
36		cphlmod 25495	. . . . . . . . 9 ⊢ (𝑈 ∈ ℂPreHil → 𝑈 ∈ LMod)
37	4, 36	syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝑈 ∈ LMod)
38	37	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑈 ∈ LMod)
39	7	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝐴 ∈ 𝑋)
40		eqid 2760	. . . . . . . . . 10 ⊢ (LSubSp‘𝑈) = (LSubSp‘𝑈)
41	1, 40	lssss 21211	. . . . . . . . 9 ⊢ (𝑌 ∈ (LSubSp‘𝑈) → 𝑌 ⊆ 𝑋)
42	5, 41	syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ⊆ 𝑋)
43	42	sselda 3908	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝑋)
44	1, 2	lmodvsubcl 21182	. . . . . . 7 ⊢ ((𝑈 ∈ LMod ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐴 − 𝑦) ∈ 𝑋)
45	38, 39, 43, 44	syl3anc 1398	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝐴 − 𝑦) ∈ 𝑋)
46	1, 3	nmcl 24935	. . . . . 6 ⊢ ((𝑈 ∈ NrmGrp ∧ (𝐴 − 𝑦) ∈ 𝑋) → (𝑁‘(𝐴 − 𝑦)) ∈ ℝ)
47	35, 45, 46	syl2anc 596	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝑁‘(𝐴 − 𝑦)) ∈ ℝ)
48	33, 31	ltnled 11457	. . . . . . . 8 ⊢ (𝜑 → (𝑆 < (𝐴𝐷𝑃) ↔ ¬ (𝐴𝐷𝑃) ≤ 𝑆))
49	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12	minveclem3b 25749	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐹 ∈ (fBas‘𝑌))
50		fbsspw 24151	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐹 ∈ (fBas‘𝑌) → 𝐹 ⊆ 𝒫 𝑌)
51	49, 50	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐹 ⊆ 𝒫 𝑌)
52	42	sspwd 4569	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝒫 𝑌 ⊆ 𝒫 𝑋)
53	51, 52	sstrd 3918	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐹 ⊆ 𝒫 𝑋)
54	1	fvexi 6899	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑋 ∈ V
55	54	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑋 ∈ V)
56		fbasweak 24184	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹 ∈ (fBas‘𝑌) ∧ 𝐹 ⊆ 𝒫 𝑋 ∧ 𝑋 ∈ V) → 𝐹 ∈ (fBas‘𝑋))
57	49, 53, 55, 56	syl3anc 1398	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐹 ∈ (fBas‘𝑋))
58	57	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝐹 ∈ (fBas‘𝑋))
59		fgcl 24197	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ (fBas‘𝑋) → (𝑋filGen𝐹) ∈ (Fil‘𝑋))
60	58, 59	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (𝑋filGen𝐹) ∈ (Fil‘𝑋))
61		ssfg 24191	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 ∈ (fBas‘𝑋) → 𝐹 ⊆ (𝑋filGen𝐹))
62	58, 61	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝐹 ⊆ (𝑋filGen𝐹))
63		minvec.t	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑇 = (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2))
64	31, 33	readdcld 11338	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((𝐴𝐷𝑃) + 𝑆) ∈ ℝ)
65	64	rehalfcld 12593	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (((𝐴𝐷𝑃) + 𝑆) / 2) ∈ ℝ)
66	65	resqcld 14268	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) ∈ ℝ)
67	33	resqcld 14268	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑆↑2) ∈ ℝ)
68	66, 67	resubcld 11744	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈ ℝ)
69	68	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈ ℝ)
70	33, 31, 33	ltadd1d 11909	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑆 < (𝐴𝐷𝑃) ↔ (𝑆 + 𝑆) < ((𝐴𝐷𝑃) + 𝑆)))
71	33	recnd 11337	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝑆 ∈ ℂ)
72	71	2timesd 12589	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (2 · 𝑆) = (𝑆 + 𝑆))
73	72	breq1d 5112	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((2 · 𝑆) < ((𝐴𝐷𝑃) + 𝑆) ↔ (𝑆 + 𝑆) < ((𝐴𝐷𝑃) + 𝑆)))
74		2re 12417	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 2 ∈ ℝ
75		2pos 12447	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 0 < 2
76	74, 75	pm3.2i 476	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (2 ∈ ℝ ∧ 0 < 2)
77	76	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (2 ∈ ℝ ∧ 0 < 2))
78		ltmuldiv2 12191	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑆 ∈ ℝ ∧ ((𝐴𝐷𝑃) + 𝑆) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · 𝑆) < ((𝐴𝐷𝑃) + 𝑆) ↔ 𝑆 < (((𝐴𝐷𝑃) + 𝑆) / 2)))
79	33, 64, 77, 78	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((2 · 𝑆) < ((𝐴𝐷𝑃) + 𝑆) ↔ 𝑆 < (((𝐴𝐷𝑃) + 𝑆) / 2)))
80	70, 73, 79	3bitr2d 310	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑆 < (𝐴𝐷𝑃) ↔ 𝑆 < (((𝐴𝐷𝑃) + 𝑆) / 2)))
81	1, 2, 3, 4, 5, 6, 7, 8, 9	minveclem1 25745	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤))
82	81	simp3d 1162	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ∀𝑤 ∈ 𝑅 0 ≤ 𝑤)
83	81	simp1d 1160	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝑅 ⊆ ℝ)
84	81	simp2d 1161	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝑅 ≠ ∅)
85		0re 11310	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 0 ∈ ℝ
86		breq1 5105	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 = 0 → (𝑥 ≤ 𝑤 ↔ 0 ≤ 𝑤))
87	86	ralbidv 3185	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 = 0 → (∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ↔ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤))
88	87	rspcev 3576	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((0 ∈ ℝ ∧ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤) → ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤)
89	85, 82, 88	sylancr 599	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤)
90	85	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 0 ∈ ℝ)
91		infregelb 12301	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤) ∧ 0 ∈ ℝ) → (0 ≤ inf(𝑅, ℝ, < ) ↔ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤))
92	83, 84, 89, 90, 91	syl31anc 1400	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (0 ≤ inf(𝑅, ℝ, < ) ↔ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤))
93	82, 92	mpbird 260	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 0 ≤ inf(𝑅, ℝ, < ))
94	93, 10	breqtrrdi 5146	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 0 ≤ 𝑆)
95		metge0 24664	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → 0 ≤ (𝐴𝐷𝑃))
96	29, 7, 17, 95	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 0 ≤ (𝐴𝐷𝑃))
97	31, 33, 96, 94	addge0d 11892	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 0 ≤ ((𝐴𝐷𝑃) + 𝑆))
98		divge0 12186	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐴𝐷𝑃) + 𝑆) ∈ ℝ ∧ 0 ≤ ((𝐴𝐷𝑃) + 𝑆)) ∧ (2 ∈ ℝ ∧ 0 < 2)) → 0 ≤ (((𝐴𝐷𝑃) + 𝑆) / 2))
99	64, 97, 77, 98	syl21anc 851	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 0 ≤ (((𝐴𝐷𝑃) + 𝑆) / 2))
100	33, 65, 94, 99	lt2sqd 14400	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑆 < (((𝐴𝐷𝑃) + 𝑆) / 2) ↔ (𝑆↑2) < ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2)))
101	67, 66	posdifd 11903	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((𝑆↑2) < ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) ↔ 0 < (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2))))
102	80, 100, 101	3bitrd 308	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑆 < (𝐴𝐷𝑃) ↔ 0 < (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2))))
103	102	biimpa 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 0 < (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2)))
104	69, 103	elrpd 13161	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈ ℝ⁺)
105	63, 104	eqeltrid 2864	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝑇 ∈ ℝ⁺)
106	5	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝑌 ∈ (LSubSp‘𝑈))
107		rabexg 5298	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑌 ∈ (LSubSp‘𝑈) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ∈ V)
108	106, 107	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ∈ V)
109		eqid 2760	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑟 ∈ ℝ⁺ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}) = (𝑟 ∈ ℝ⁺ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)})
110		oveq2 7428	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑟 = 𝑇 → ((𝑆↑2) + 𝑟) = ((𝑆↑2) + 𝑇))
111	110	breq2d 5114	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑟 = 𝑇 → (((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟) ↔ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)))
112	111	rabbidv 3419	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑟 = 𝑇 → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)} = {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)})
113	109, 112	elrnmpt1s 5940	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑇 ∈ ℝ⁺ ∧ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ∈ V) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ∈ ran (𝑟 ∈ ℝ⁺ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}))
114	105, 108, 113	syl2anc 596	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ∈ ran (𝑟 ∈ ℝ⁺ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}))
115	114, 12	eleqtrrdi 2871	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ∈ 𝐹)
116	62, 115	sseldd 3909	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ∈ (𝑋filGen𝐹))
117		ssrab2 4005	. . . . . . . . . . . . . . . 16 ⊢ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ⊆ 𝑋
118	117	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ⊆ 𝑋)
119	63	oveq2i 7431	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑆↑2) + 𝑇) = ((𝑆↑2) + (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2)))
120	67	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → (𝑆↑2) ∈ ℝ)
121	120	recnd 11337	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → (𝑆↑2) ∈ ℂ)
122	65	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → (((𝐴𝐷𝑃) + 𝑆) / 2) ∈ ℝ)
123	122	resqcld 14268	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) ∈ ℝ)
124	123	recnd 11337	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) ∈ ℂ)
125	121, 124	pncan3d 11672	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → ((𝑆↑2) + (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2))) = ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2))
126	119, 125	eqtrid 2807	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → ((𝑆↑2) + 𝑇) = ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2))
127	126	breq2d 5114	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → (((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇) ↔ ((𝐴𝐷𝑦)↑2) ≤ ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2)))
128	29	ad2antrr 739	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → 𝐷 ∈ (Met‘𝑋))
129	7	ad2antrr 739	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → 𝐴 ∈ 𝑋)
130	43	adantlr 728	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝑋)
131		metcl 24651	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐴𝐷𝑦) ∈ ℝ)
132	128, 129, 130, 131	syl3anc 1398	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → (𝐴𝐷𝑦) ∈ ℝ)
133		metge0 24664	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → 0 ≤ (𝐴𝐷𝑦))
134	128, 129, 130, 133	syl3anc 1398	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → 0 ≤ (𝐴𝐷𝑦))
135	99	ad2antrr 739	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → 0 ≤ (((𝐴𝐷𝑃) + 𝑆) / 2))
136	132, 122, 134, 135	le2sqd 14401	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → ((𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2) ↔ ((𝐴𝐷𝑦)↑2) ≤ ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2)))
137	127, 136	bitr4d 285	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → (((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇) ↔ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)))
138	137	rabbidva 3418	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} = {𝑦 ∈ 𝑌 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)})
139	42	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝑌 ⊆ 𝑋)
140		rabss2 4002	. . . . . . . . . . . . . . . . 17 ⊢ (𝑌 ⊆ 𝑋 → {𝑦 ∈ 𝑌 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ⊆ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)})
141	139, 140	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑌 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ⊆ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)})
142	138, 141	eqsstrd 3942	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ⊆ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)})
143		filss 24172	. . . . . . . . . . . . . . 15 ⊢ (((𝑋filGen𝐹) ∈ (Fil‘𝑋) ∧ ({𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ∈ (𝑋filGen𝐹) ∧ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ⊆ 𝑋 ∧ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ⊆ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)})) → {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ∈ (𝑋filGen𝐹))
144	60, 116, 118, 142, 143	syl13anc 1399	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ∈ (𝑋filGen𝐹))
145		flimclsi 24297	. . . . . . . . . . . . . 14 ⊢ ({𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ∈ (𝑋filGen𝐹) → (𝐽 fLim (𝑋filGen𝐹)) ⊆ ((cls‘𝐽)‘{𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)}))
146	144, 145	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (𝐽 fLim (𝑋filGen𝐹)) ⊆ ((cls‘𝐽)‘{𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)}))
147	14	elin1d 4101	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑃 ∈ (𝐽 fLim (𝑋filGen𝐹)))
148	147	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝑃 ∈ (𝐽 fLim (𝑋filGen𝐹)))
149	146, 148	sseldd 3909	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝑃 ∈ ((cls‘𝐽)‘{𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)}))
150		ngpxms 24920	. . . . . . . . . . . . . . . . 17 ⊢ (𝑈 ∈ NrmGrp → 𝑈 ∈ ∞MetSp)
151	1, 11	xmsxmet 24775	. . . . . . . . . . . . . . . . 17 ⊢ (𝑈 ∈ ∞MetSp → 𝐷 ∈ (∞Met‘𝑋))
152	21, 150, 151	3syl 19	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))
153	152	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝐷 ∈ (∞Met‘𝑋))
154	7	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝐴 ∈ 𝑋)
155	65	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (((𝐴𝐷𝑃) + 𝑆) / 2) ∈ ℝ)
156	155	rexrd 11359	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (((𝐴𝐷𝑃) + 𝑆) / 2) ∈ ℝ^*)
157		eqid 2760	. . . . . . . . . . . . . . . 16 ⊢ (MetOpen‘𝐷) = (MetOpen‘𝐷)
158		eqid 2760	. . . . . . . . . . . . . . . 16 ⊢ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} = {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)}
159	157, 158	blcld 24824	. . . . . . . . . . . . . . 15 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ (((𝐴𝐷𝑃) + 𝑆) / 2) ∈ ℝ^*) → {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ∈ (Clsd‘(MetOpen‘𝐷)))
160	153, 154, 156, 159	syl3anc 1398	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ∈ (Clsd‘(MetOpen‘𝐷)))
161	8, 1, 11	xmstopn 24770	. . . . . . . . . . . . . . . . 17 ⊢ (𝑈 ∈ ∞MetSp → 𝐽 = (MetOpen‘𝐷))
162	21, 150, 161	3syl 19	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐽 = (MetOpen‘𝐷))
163	162	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝐽 = (MetOpen‘𝐷))
164	163	fveq2d 6889	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (Clsd‘𝐽) = (Clsd‘(MetOpen‘𝐷)))
165	160, 164	eleqtrrd 2863	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ∈ (Clsd‘𝐽))
166		cldcls 23360	. . . . . . . . . . . . 13 ⊢ ({𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ∈ (Clsd‘𝐽) → ((cls‘𝐽)‘{𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)}) = {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)})
167	165, 166	syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → ((cls‘𝐽)‘{𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)}) = {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)})
168	149, 167	eleqtrd 2862	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝑃 ∈ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)})
169		oveq2 7428	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑃 → (𝐴𝐷𝑦) = (𝐴𝐷𝑃))
170	169	breq1d 5112	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑃 → ((𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2) ↔ (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)))
171	170	elrab 3644	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ↔ (𝑃 ∈ 𝑋 ∧ (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)))
172	171	simprbi 503	. . . . . . . . . . 11 ⊢ (𝑃 ∈ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} → (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2))
173	168, 172	syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2))
174	31, 33, 31	leadd2d 11911	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴𝐷𝑃) ≤ 𝑆 ↔ ((𝐴𝐷𝑃) + (𝐴𝐷𝑃)) ≤ ((𝐴𝐷𝑃) + 𝑆)))
175	31	recnd 11337	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴𝐷𝑃) ∈ ℂ)
176	175	2timesd 12589	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 · (𝐴𝐷𝑃)) = ((𝐴𝐷𝑃) + (𝐴𝐷𝑃)))
177	176	breq1d 5112	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · (𝐴𝐷𝑃)) ≤ ((𝐴𝐷𝑃) + 𝑆) ↔ ((𝐴𝐷𝑃) + (𝐴𝐷𝑃)) ≤ ((𝐴𝐷𝑃) + 𝑆)))
178		lemuldiv2 12198	. . . . . . . . . . . . . 14 ⊢ (((𝐴𝐷𝑃) ∈ ℝ ∧ ((𝐴𝐷𝑃) + 𝑆) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · (𝐴𝐷𝑃)) ≤ ((𝐴𝐷𝑃) + 𝑆) ↔ (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)))
179	76, 178	mp3an3 1479	. . . . . . . . . . . . 13 ⊢ (((𝐴𝐷𝑃) ∈ ℝ ∧ ((𝐴𝐷𝑃) + 𝑆) ∈ ℝ) → ((2 · (𝐴𝐷𝑃)) ≤ ((𝐴𝐷𝑃) + 𝑆) ↔ (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)))
180	31, 64, 179	syl2anc 596	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · (𝐴𝐷𝑃)) ≤ ((𝐴𝐷𝑃) + 𝑆) ↔ (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)))
181	174, 177, 180	3bitr2d 310	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴𝐷𝑃) ≤ 𝑆 ↔ (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)))
182	181	biimpar 483	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)) → (𝐴𝐷𝑃) ≤ 𝑆)
183	173, 182	syldan 603	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (𝐴𝐷𝑃) ≤ 𝑆)
184	183	ex 418	. . . . . . . 8 ⊢ (𝜑 → (𝑆 < (𝐴𝐷𝑃) → (𝐴𝐷𝑃) ≤ 𝑆))
185	48, 184	sylbird 263	. . . . . . 7 ⊢ (𝜑 → (¬ (𝐴𝐷𝑃) ≤ 𝑆 → (𝐴𝐷𝑃) ≤ 𝑆))
186	185	pm2.18d 128	. . . . . 6 ⊢ (𝜑 → (𝐴𝐷𝑃) ≤ 𝑆)
187	186	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝐴𝐷𝑃) ≤ 𝑆)
188	83	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑅 ⊆ ℝ)
189	89	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤)
190		simpr 490	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝑌)
191		fvex 6898	. . . . . . . . 9 ⊢ (𝑁‘(𝐴 − 𝑦)) ∈ V
192		eqid 2760	. . . . . . . . . 10 ⊢ (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦))) = (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))
193	192	elrnmpt1 5941	. . . . . . . . 9 ⊢ ((𝑦 ∈ 𝑌 ∧ (𝑁‘(𝐴 − 𝑦)) ∈ V) → (𝑁‘(𝐴 − 𝑦)) ∈ ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦))))
194	190, 191, 193	sylancl 598	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝑁‘(𝐴 − 𝑦)) ∈ ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦))))
195	194, 9	eleqtrrdi 2871	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝑁‘(𝐴 − 𝑦)) ∈ 𝑅)
196		infrelb 12302	. . . . . . 7 ⊢ ((𝑅 ⊆ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ∧ (𝑁‘(𝐴 − 𝑦)) ∈ 𝑅) → inf(𝑅, ℝ, < ) ≤ (𝑁‘(𝐴 − 𝑦)))
197	188, 189, 195, 196	syl3anc 1398	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → inf(𝑅, ℝ, < ) ≤ (𝑁‘(𝐴 − 𝑦)))
198	10, 197	eqbrtrid 5139	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑆 ≤ (𝑁‘(𝐴 − 𝑦)))
199	32, 34, 47, 187, 198	letrd 11467	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝐴𝐷𝑃) ≤ (𝑁‘(𝐴 − 𝑦)))
200	26, 199	eqbrtrrd 5128	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝑁‘(𝐴 − 𝑃)) ≤ (𝑁‘(𝐴 − 𝑦)))
201	200	ralrimiva 3154	. 2 ⊢ (𝜑 → ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑃)) ≤ (𝑁‘(𝐴 − 𝑦)))
202		oveq2 7428	. . . . . 6 ⊢ (𝑥 = 𝑃 → (𝐴 − 𝑥) = (𝐴 − 𝑃))
203	202	fveq2d 6889	. . . . 5 ⊢ (𝑥 = 𝑃 → (𝑁‘(𝐴 − 𝑥)) = (𝑁‘(𝐴 − 𝑃)))
204	203	breq1d 5112	. . . 4 ⊢ (𝑥 = 𝑃 → ((𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)) ↔ (𝑁‘(𝐴 − 𝑃)) ≤ (𝑁‘(𝐴 − 𝑦))))
205	204	ralbidv 3185	. . 3 ⊢ (𝑥 = 𝑃 → (∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)) ↔ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑃)) ≤ (𝑁‘(𝐴 − 𝑦))))
206	205	rspcev 3576	. 2 ⊢ ((𝑃 ∈ 𝑌 ∧ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑃)) ≤ (𝑁‘(𝐴 − 𝑦))) → ∃𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))
207	15, 201, 206	syl2anc 596	1 ⊢ (𝜑 → ∃𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1569 ∈ wcel 2144 ≠ wne 2955 ∀wral 3076 ∃wrex 3086 {crab 3412 Vcvv 3450 ⊆ wss 3895 ∅c0 4278 𝒫 cpw 4556 ∪ cuni 4866 class class class wbr 5102 ↦ cmpt 5185 × cxp 5648 ran crn 5651 ↾ cres 5652 ‘cfv 6538 (class class class)co 7420 infcinf 9433 ℝcr 11199 0cc0 11200 + caddc 11203 · cmul 11205 ℝ^*cxr 11342 < clt 11343 ≤ cle 11344 − cmin 11541 / cdiv 11973 2c2 12397 ℝ⁺crp 13120 ↑cexp 14204 Basecbs 17387 ↾_s cress 17408 distcds 17437 TopOpenctopn 17592 -_gcsg 19146 LModclmod 21135 LSubSpclss 21206 ∞Metcxmet 21663 Metcmet 21664 fBascfbas 21666 filGencfg 21667 MetOpencmopn 21668 Clsdccld 23334 clsccl 23336 Filcfil 24164 fLim cflim 24253 ∞MetSpcxms 24636 MetSpcms 24637 normcnm 24895 NrmGrpcngp 24896 ℂPreHilccph 25487 CMetSpccms 25653

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7751 ax-cnex 11256 ax-resscn 11257 ax-1cn 11258 ax-icn 11259 ax-addcl 11260 ax-addrcl 11261 ax-mulcl 11262 ax-mulrcl 11263 ax-mulcom 11264 ax-addass 11265 ax-mulass 11266 ax-distr 11267 ax-i2m1 11268 ax-1ne0 11269 ax-1rid 11270 ax-rnegex 11271 ax-rrecex 11272 ax-cnre 11273 ax-pre-lttri 11274 ax-pre-lttrn 11275 ax-pre-ltadd 11276 ax-pre-mulgt0 11277 ax-pre-sup 11278 ax-addf 11279 ax-mulf 11280

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4584 df-pr 4586 df-tp 4588 df-op 4590 df-uni 4867 df-int 4907 df-iun 4952 df-iin 4953 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-om 7878 df-1st 8001 df-2nd 8002 df-tpos 8243 df-frecs 8299 df-wrecs 8330 df-recs 8379 df-rdg 8418 df-1o 8476 df-er 8717 df-map 8849 df-en 8974 df-dom 8975 df-sdom 8976 df-fin 8977 df-fi 9403 df-sup 9434 df-inf 9435 df-pnf 11345 df-mnf 11346 df-xr 11347 df-ltxr 11348 df-le 11349 df-sub 11543 df-neg 11544 df-div 11974 df-nn 12336 df-2 12405 df-3 12406 df-4 12407 df-5 12408 df-6 12409 df-7 12410 df-8 12411 df-9 12412 df-n0 12607 df-z 12694 df-dec 12815 df-uz 12966 df-q 13076 df-rp 13121 df-xneg 13241 df-xadd 13242 df-xmul 13243 df-ico 13482 df-icc 13483 df-fz 13640 df-seq 14145 df-exp 14205 df-cj 15266 df-re 15267 df-im 15268 df-sqrt 15402 df-abs 15403 df-struct 17325 df-sets 17342 df-slot 17360 df-ndx 17372 df-base 17388 df-ress 17409 df-plusg 17441 df-mulr 17442 df-starv 17443 df-sca 17444 df-vsca 17445 df-ip 17446 df-tset 17447 df-ple 17448 df-ds 17450 df-unif 17451 df-rest 17593 df-0g 17612 df-topgen 17614 df-mgm 18816 df-sgrp 18908 df-mnd 18924 df-mhm 18978 df-grp 19147 df-minusg 19148 df-sbg 19149 df-mulg 19278 df-subg 19333 df-ghm 19428 df-cmn 19996 df-abl 19997 df-mgp 20361 df-rng 20375 df-ur 20408 df-ring 20461 df-cring 20462 df-oppr 20567 df-dvdsr 20587 df-unit 20588 df-invr 20618 df-dvr 20631 df-rhm 20702 df-subrg 20822 df-drng 20982 df-staf 21096 df-srng 21097 df-lmod 21137 df-lss 21207 df-lmhm 21297 df-lvec 21378 df-sra 21448 df-rgmod 21449 df-psmet 21670 df-xmet 21671 df-met 21672 df-bl 21673 df-mopn 21674 df-fbas 21675 df-fg 21676 df-cnfld 21679 df-phl 21932 df-top 23212 df-topon 23229 df-topsp 23251 df-bases 23264 df-cld 23337 df-ntr 23338 df-cls 23339 df-nei 23416 df-haus 23633 df-fil 24165 df-flim 24258 df-xms 24639 df-ms 24640 df-nm 24901 df-ngp 24902 df-nlm 24905 df-clm 25384 df-cph 25489 df-cfil 25576 df-cmet 25578 df-cms 25656

This theorem is used by: minveclem5 25754

W3C validator