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 23203

Description: Lemma for minvec 23207. 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		inss2 3834	. . 3 ⊢ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) ⊆ 𝑌
2		minvec.x	. . . 4 ⊢ 𝑋 = (Base‘𝑈)
3		minvec.m	. . . 4 ⊢ − = (-_g‘𝑈)
4		minvec.n	. . . 4 ⊢ 𝑁 = (norm‘𝑈)
5		minvec.u	. . . 4 ⊢ (𝜑 → 𝑈 ∈ ℂPreHil)
6		minvec.y	. . . 4 ⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈))
7		minvec.w	. . . 4 ⊢ (𝜑 → (𝑈 ↾_s 𝑌) ∈ CMetSp)
8		minvec.a	. . . 4 ⊢ (𝜑 → 𝐴 ∈ 𝑋)
9		minvec.j	. . . 4 ⊢ 𝐽 = (TopOpen‘𝑈)
10		minvec.r	. . . 4 ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))
11		minvec.s	. . . 4 ⊢ 𝑆 = inf(𝑅, ℝ, < )
12		minvec.d	. . . 4 ⊢ 𝐷 = ((dist‘𝑈) ↾ (𝑋 × 𝑋))
13		minvec.f	. . . 4 ⊢ 𝐹 = ran (𝑟 ∈ ℝ⁺ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)})
14		minvec.p	. . . 4 ⊢ 𝑃 = ∪ (𝐽 fLim (𝑋filGen𝐹))
15	2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14	minveclem4a 23201	. . 3 ⊢ (𝜑 → 𝑃 ∈ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌))
16	1, 15	sseldi 3601	. 2 ⊢ (𝜑 → 𝑃 ∈ 𝑌)
17	12	oveqi 6663	. . . . . . 7 ⊢ (𝐴𝐷𝑃) = (𝐴((dist‘𝑈) ↾ (𝑋 × 𝑋))𝑃)
18	2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14	minveclem4b 23202	. . . . . . . 8 ⊢ (𝜑 → 𝑃 ∈ 𝑋)
19	8, 18	ovresd 6801	. . . . . . 7 ⊢ (𝜑 → (𝐴((dist‘𝑈) ↾ (𝑋 × 𝑋))𝑃) = (𝐴(dist‘𝑈)𝑃))
20	17, 19	syl5eq 2668	. . . . . 6 ⊢ (𝜑 → (𝐴𝐷𝑃) = (𝐴(dist‘𝑈)𝑃))
21		cphngp 22973	. . . . . . . 8 ⊢ (𝑈 ∈ ℂPreHil → 𝑈 ∈ NrmGrp)
22	5, 21	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑈 ∈ NrmGrp)
23		eqid 2622	. . . . . . . 8 ⊢ (dist‘𝑈) = (dist‘𝑈)
24	4, 2, 3, 23	ngpds 22408	. . . . . . 7 ⊢ ((𝑈 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝐴(dist‘𝑈)𝑃) = (𝑁‘(𝐴 − 𝑃)))
25	22, 8, 18, 24	syl3anc 1326	. . . . . 6 ⊢ (𝜑 → (𝐴(dist‘𝑈)𝑃) = (𝑁‘(𝐴 − 𝑃)))
26	20, 25	eqtrd 2656	. . . . 5 ⊢ (𝜑 → (𝐴𝐷𝑃) = (𝑁‘(𝐴 − 𝑃)))
27	26	adantr 481	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝐴𝐷𝑃) = (𝑁‘(𝐴 − 𝑃)))
28		ngpms 22404	. . . . . . . 8 ⊢ (𝑈 ∈ NrmGrp → 𝑈 ∈ MetSp)
29	2, 12	msmet 22262	. . . . . . . 8 ⊢ (𝑈 ∈ MetSp → 𝐷 ∈ (Met‘𝑋))
30	22, 28, 29	3syl 18	. . . . . . 7 ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋))
31		metcl 22137	. . . . . . 7 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝐴𝐷𝑃) ∈ ℝ)
32	30, 8, 18, 31	syl3anc 1326	. . . . . 6 ⊢ (𝜑 → (𝐴𝐷𝑃) ∈ ℝ)
33	32	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝐴𝐷𝑃) ∈ ℝ)
34	2, 3, 4, 5, 6, 7, 8, 9, 10, 11	minveclem4c 23196	. . . . . 6 ⊢ (𝜑 → 𝑆 ∈ ℝ)
35	34	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑆 ∈ ℝ)
36	22	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑈 ∈ NrmGrp)
37		cphlmod 22974	. . . . . . . . 9 ⊢ (𝑈 ∈ ℂPreHil → 𝑈 ∈ LMod)
38	5, 37	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑈 ∈ LMod)
39	38	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑈 ∈ LMod)
40	8	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝐴 ∈ 𝑋)
41		eqid 2622	. . . . . . . . . 10 ⊢ (LSubSp‘𝑈) = (LSubSp‘𝑈)
42	2, 41	lssss 18937	. . . . . . . . 9 ⊢ (𝑌 ∈ (LSubSp‘𝑈) → 𝑌 ⊆ 𝑋)
43	6, 42	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ⊆ 𝑋)
44	43	sselda 3603	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝑋)
45	2, 3	lmodvsubcl 18908	. . . . . . 7 ⊢ ((𝑈 ∈ LMod ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐴 − 𝑦) ∈ 𝑋)
46	39, 40, 44, 45	syl3anc 1326	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝐴 − 𝑦) ∈ 𝑋)
47	2, 4	nmcl 22420	. . . . . 6 ⊢ ((𝑈 ∈ NrmGrp ∧ (𝐴 − 𝑦) ∈ 𝑋) → (𝑁‘(𝐴 − 𝑦)) ∈ ℝ)
48	36, 46, 47	syl2anc 693	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝑁‘(𝐴 − 𝑦)) ∈ ℝ)
49	34, 32	ltnled 10184	. . . . . . . 8 ⊢ (𝜑 → (𝑆 < (𝐴𝐷𝑃) ↔ ¬ (𝐴𝐷𝑃) ≤ 𝑆))
50	2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13	minveclem3b 23199	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐹 ∈ (fBas‘𝑌))
51		fbsspw 21636	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐹 ∈ (fBas‘𝑌) → 𝐹 ⊆ 𝒫 𝑌)
52	50, 51	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐹 ⊆ 𝒫 𝑌)
53		sspwb 4917	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑌 ⊆ 𝑋 ↔ 𝒫 𝑌 ⊆ 𝒫 𝑋)
54	43, 53	sylib 208	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝒫 𝑌 ⊆ 𝒫 𝑋)
55	52, 54	sstrd 3613	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐹 ⊆ 𝒫 𝑋)
56		fvex 6201	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Base‘𝑈) ∈ V
57	2, 56	eqeltri 2697	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑋 ∈ V
58	57	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑋 ∈ V)
59		fbasweak 21669	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹 ∈ (fBas‘𝑌) ∧ 𝐹 ⊆ 𝒫 𝑋 ∧ 𝑋 ∈ V) → 𝐹 ∈ (fBas‘𝑋))
60	50, 55, 58, 59	syl3anc 1326	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐹 ∈ (fBas‘𝑋))
61	60	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝐹 ∈ (fBas‘𝑋))
62		fgcl 21682	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ (fBas‘𝑋) → (𝑋filGen𝐹) ∈ (Fil‘𝑋))
63	61, 62	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (𝑋filGen𝐹) ∈ (Fil‘𝑋))
64		ssfg 21676	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 ∈ (fBas‘𝑋) → 𝐹 ⊆ (𝑋filGen𝐹))
65	61, 64	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝐹 ⊆ (𝑋filGen𝐹))
66		minvec.t	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑇 = (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2))
67	32, 34	readdcld 10069	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((𝐴𝐷𝑃) + 𝑆) ∈ ℝ)
68	67	rehalfcld 11279	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (((𝐴𝐷𝑃) + 𝑆) / 2) ∈ ℝ)
69	68	resqcld 13035	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) ∈ ℝ)
70	34	resqcld 13035	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑆↑2) ∈ ℝ)
71	69, 70	resubcld 10458	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈ ℝ)
72	71	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈ ℝ)
73	34, 32, 34	ltadd1d 10620	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑆 < (𝐴𝐷𝑃) ↔ (𝑆 + 𝑆) < ((𝐴𝐷𝑃) + 𝑆)))
74	34	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝑆 ∈ ℂ)
75	74	2timesd 11275	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (2 · 𝑆) = (𝑆 + 𝑆))
76	75	breq1d 4663	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((2 · 𝑆) < ((𝐴𝐷𝑃) + 𝑆) ↔ (𝑆 + 𝑆) < ((𝐴𝐷𝑃) + 𝑆)))
77		2re 11090	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 2 ∈ ℝ
78		2pos 11112	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 0 < 2
79	77, 78	pm3.2i 471	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (2 ∈ ℝ ∧ 0 < 2)
80	79	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (2 ∈ ℝ ∧ 0 < 2))
81		ltmuldiv2 10897	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑆 ∈ ℝ ∧ ((𝐴𝐷𝑃) + 𝑆) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · 𝑆) < ((𝐴𝐷𝑃) + 𝑆) ↔ 𝑆 < (((𝐴𝐷𝑃) + 𝑆) / 2)))
82	34, 67, 80, 81	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((2 · 𝑆) < ((𝐴𝐷𝑃) + 𝑆) ↔ 𝑆 < (((𝐴𝐷𝑃) + 𝑆) / 2)))
83	73, 76, 82	3bitr2d 296	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑆 < (𝐴𝐷𝑃) ↔ 𝑆 < (((𝐴𝐷𝑃) + 𝑆) / 2)))
84	2, 3, 4, 5, 6, 7, 8, 9, 10	minveclem1 23195	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤))
85	84	simp3d 1075	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ∀𝑤 ∈ 𝑅 0 ≤ 𝑤)
86	84	simp1d 1073	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝑅 ⊆ ℝ)
87	84	simp2d 1074	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝑅 ≠ ∅)
88		0re 10040	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 0 ∈ ℝ
89		breq1 4656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 = 0 → (𝑥 ≤ 𝑤 ↔ 0 ≤ 𝑤))
90	89	ralbidv 2986	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 = 0 → (∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ↔ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤))
91	90	rspcev 3309	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((0 ∈ ℝ ∧ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤) → ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤)
92	88, 85, 91	sylancr 695	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤)
93	88	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 0 ∈ ℝ)
94		infregelb 11007	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤) ∧ 0 ∈ ℝ) → (0 ≤ inf(𝑅, ℝ, < ) ↔ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤))
95	86, 87, 92, 93, 94	syl31anc 1329	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (0 ≤ inf(𝑅, ℝ, < ) ↔ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤))
96	85, 95	mpbird 247	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 0 ≤ inf(𝑅, ℝ, < ))
97	96, 11	syl6breqr 4695	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 0 ≤ 𝑆)
98		metge0 22150	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → 0 ≤ (𝐴𝐷𝑃))
99	30, 8, 18, 98	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 0 ≤ (𝐴𝐷𝑃))
100	32, 34, 99, 97	addge0d 10603	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 0 ≤ ((𝐴𝐷𝑃) + 𝑆))
101		divge0 10892	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐴𝐷𝑃) + 𝑆) ∈ ℝ ∧ 0 ≤ ((𝐴𝐷𝑃) + 𝑆)) ∧ (2 ∈ ℝ ∧ 0 < 2)) → 0 ≤ (((𝐴𝐷𝑃) + 𝑆) / 2))
102	67, 100, 80, 101	syl21anc 1325	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 0 ≤ (((𝐴𝐷𝑃) + 𝑆) / 2))
103	34, 68, 97, 102	lt2sqd 13043	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑆 < (((𝐴𝐷𝑃) + 𝑆) / 2) ↔ (𝑆↑2) < ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2)))
104	70, 69	posdifd 10614	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((𝑆↑2) < ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) ↔ 0 < (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2))))
105	83, 103, 104	3bitrd 294	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑆 < (𝐴𝐷𝑃) ↔ 0 < (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2))))
106	105	biimpa 501	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 0 < (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2)))
107	72, 106	elrpd 11869	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈ ℝ⁺)
108	66, 107	syl5eqel 2705	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝑇 ∈ ℝ⁺)
109	6	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝑌 ∈ (LSubSp‘𝑈))
110		rabexg 4812	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑌 ∈ (LSubSp‘𝑈) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ∈ V)
111	109, 110	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ∈ V)
112		eqid 2622	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑟 ∈ ℝ⁺ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}) = (𝑟 ∈ ℝ⁺ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)})
113		oveq2 6658	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑟 = 𝑇 → ((𝑆↑2) + 𝑟) = ((𝑆↑2) + 𝑇))
114	113	breq2d 4665	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑟 = 𝑇 → (((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟) ↔ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)))
115	114	rabbidv 3189	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑟 = 𝑇 → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)} = {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)})
116	112, 115	elrnmpt1s 5373	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑇 ∈ ℝ⁺ ∧ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ∈ V) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ∈ ran (𝑟 ∈ ℝ⁺ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}))
117	108, 111, 116	syl2anc 693	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ∈ ran (𝑟 ∈ ℝ⁺ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}))
118	117, 13	syl6eleqr 2712	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ∈ 𝐹)
119	65, 118	sseldd 3604	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ∈ (𝑋filGen𝐹))
120		ssrab2 3687	. . . . . . . . . . . . . . . 16 ⊢ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ⊆ 𝑋
121	120	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ⊆ 𝑋)
122	66	oveq2i 6661	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑆↑2) + 𝑇) = ((𝑆↑2) + (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2)))
123	70	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → (𝑆↑2) ∈ ℝ)
124	123	recnd 10068	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → (𝑆↑2) ∈ ℂ)
125	68	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → (((𝐴𝐷𝑃) + 𝑆) / 2) ∈ ℝ)
126	125	resqcld 13035	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) ∈ ℝ)
127	126	recnd 10068	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) ∈ ℂ)
128	124, 127	pncan3d 10395	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → ((𝑆↑2) + (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2))) = ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2))
129	122, 128	syl5eq 2668	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → ((𝑆↑2) + 𝑇) = ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2))
130	129	breq2d 4665	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → (((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇) ↔ ((𝐴𝐷𝑦)↑2) ≤ ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2)))
131	30	ad2antrr 762	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → 𝐷 ∈ (Met‘𝑋))
132	8	ad2antrr 762	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → 𝐴 ∈ 𝑋)
133	44	adantlr 751	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝑋)
134		metcl 22137	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐴𝐷𝑦) ∈ ℝ)
135	131, 132, 133, 134	syl3anc 1326	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → (𝐴𝐷𝑦) ∈ ℝ)
136		metge0 22150	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → 0 ≤ (𝐴𝐷𝑦))
137	131, 132, 133, 136	syl3anc 1326	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → 0 ≤ (𝐴𝐷𝑦))
138	102	ad2antrr 762	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → 0 ≤ (((𝐴𝐷𝑃) + 𝑆) / 2))
139	135, 125, 137, 138	le2sqd 13044	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → ((𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2) ↔ ((𝐴𝐷𝑦)↑2) ≤ ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2)))
140	130, 139	bitr4d 271	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → (((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇) ↔ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)))
141	140	rabbidva 3188	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} = {𝑦 ∈ 𝑌 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)})
142	43	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝑌 ⊆ 𝑋)
143		rabss2 3685	. . . . . . . . . . . . . . . . 17 ⊢ (𝑌 ⊆ 𝑋 → {𝑦 ∈ 𝑌 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ⊆ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)})
144	142, 143	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑌 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ⊆ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)})
145	141, 144	eqsstrd 3639	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ⊆ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)})
146		filss 21657	. . . . . . . . . . . . . . 15 ⊢ (((𝑋filGen𝐹) ∈ (Fil‘𝑋) ∧ ({𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ∈ (𝑋filGen𝐹) ∧ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ⊆ 𝑋 ∧ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ⊆ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)})) → {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ∈ (𝑋filGen𝐹))
147	63, 119, 121, 145, 146	syl13anc 1328	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ∈ (𝑋filGen𝐹))
148		flimclsi 21782	. . . . . . . . . . . . . 14 ⊢ ({𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ∈ (𝑋filGen𝐹) → (𝐽 fLim (𝑋filGen𝐹)) ⊆ ((cls‘𝐽)‘{𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)}))
149	147, 148	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (𝐽 fLim (𝑋filGen𝐹)) ⊆ ((cls‘𝐽)‘{𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)}))
150		inss1 3833	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) ⊆ (𝐽 fLim (𝑋filGen𝐹))
151	150, 15	sseldi 3601	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑃 ∈ (𝐽 fLim (𝑋filGen𝐹)))
152	151	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝑃 ∈ (𝐽 fLim (𝑋filGen𝐹)))
153	149, 152	sseldd 3604	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝑃 ∈ ((cls‘𝐽)‘{𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)}))
154		ngpxms 22405	. . . . . . . . . . . . . . . . 17 ⊢ (𝑈 ∈ NrmGrp → 𝑈 ∈ ∞MetSp)
155	2, 12	xmsxmet 22261	. . . . . . . . . . . . . . . . 17 ⊢ (𝑈 ∈ ∞MetSp → 𝐷 ∈ (∞Met‘𝑋))
156	22, 154, 155	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))
157	156	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝐷 ∈ (∞Met‘𝑋))
158	8	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝐴 ∈ 𝑋)
159	68	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (((𝐴𝐷𝑃) + 𝑆) / 2) ∈ ℝ)
160	159	rexrd 10089	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (((𝐴𝐷𝑃) + 𝑆) / 2) ∈ ℝ^*)
161		eqid 2622	. . . . . . . . . . . . . . . 16 ⊢ (MetOpen‘𝐷) = (MetOpen‘𝐷)
162		eqid 2622	. . . . . . . . . . . . . . . 16 ⊢ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} = {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)}
163	161, 162	blcld 22310	. . . . . . . . . . . . . . 15 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ (((𝐴𝐷𝑃) + 𝑆) / 2) ∈ ℝ^*) → {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ∈ (Clsd‘(MetOpen‘𝐷)))
164	157, 158, 160, 163	syl3anc 1326	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ∈ (Clsd‘(MetOpen‘𝐷)))
165	9, 2, 12	xmstopn 22256	. . . . . . . . . . . . . . . . 17 ⊢ (𝑈 ∈ ∞MetSp → 𝐽 = (MetOpen‘𝐷))
166	22, 154, 165	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐽 = (MetOpen‘𝐷))
167	166	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝐽 = (MetOpen‘𝐷))
168	167	fveq2d 6195	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (Clsd‘𝐽) = (Clsd‘(MetOpen‘𝐷)))
169	164, 168	eleqtrrd 2704	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ∈ (Clsd‘𝐽))
170		cldcls 20846	. . . . . . . . . . . . 13 ⊢ ({𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ∈ (Clsd‘𝐽) → ((cls‘𝐽)‘{𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)}) = {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)})
171	169, 170	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → ((cls‘𝐽)‘{𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)}) = {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)})
172	153, 171	eleqtrd 2703	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝑃 ∈ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)})
173		oveq2 6658	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑃 → (𝐴𝐷𝑦) = (𝐴𝐷𝑃))
174	173	breq1d 4663	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑃 → ((𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2) ↔ (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)))
175	174	elrab 3363	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ↔ (𝑃 ∈ 𝑋 ∧ (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)))
176	175	simprbi 480	. . . . . . . . . . 11 ⊢ (𝑃 ∈ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} → (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2))
177	172, 176	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2))
178	32, 34, 32	leadd2d 10622	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴𝐷𝑃) ≤ 𝑆 ↔ ((𝐴𝐷𝑃) + (𝐴𝐷𝑃)) ≤ ((𝐴𝐷𝑃) + 𝑆)))
179	32	recnd 10068	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴𝐷𝑃) ∈ ℂ)
180	179	2timesd 11275	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 · (𝐴𝐷𝑃)) = ((𝐴𝐷𝑃) + (𝐴𝐷𝑃)))
181	180	breq1d 4663	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · (𝐴𝐷𝑃)) ≤ ((𝐴𝐷𝑃) + 𝑆) ↔ ((𝐴𝐷𝑃) + (𝐴𝐷𝑃)) ≤ ((𝐴𝐷𝑃) + 𝑆)))
182		lemuldiv2 10904	. . . . . . . . . . . . . 14 ⊢ (((𝐴𝐷𝑃) ∈ ℝ ∧ ((𝐴𝐷𝑃) + 𝑆) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · (𝐴𝐷𝑃)) ≤ ((𝐴𝐷𝑃) + 𝑆) ↔ (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)))
183	79, 182	mp3an3 1413	. . . . . . . . . . . . 13 ⊢ (((𝐴𝐷𝑃) ∈ ℝ ∧ ((𝐴𝐷𝑃) + 𝑆) ∈ ℝ) → ((2 · (𝐴𝐷𝑃)) ≤ ((𝐴𝐷𝑃) + 𝑆) ↔ (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)))
184	32, 67, 183	syl2anc 693	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · (𝐴𝐷𝑃)) ≤ ((𝐴𝐷𝑃) + 𝑆) ↔ (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)))
185	178, 181, 184	3bitr2d 296	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴𝐷𝑃) ≤ 𝑆 ↔ (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)))
186	185	biimpar 502	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)) → (𝐴𝐷𝑃) ≤ 𝑆)
187	177, 186	syldan 487	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (𝐴𝐷𝑃) ≤ 𝑆)
188	187	ex 450	. . . . . . . 8 ⊢ (𝜑 → (𝑆 < (𝐴𝐷𝑃) → (𝐴𝐷𝑃) ≤ 𝑆))
189	49, 188	sylbird 250	. . . . . . 7 ⊢ (𝜑 → (¬ (𝐴𝐷𝑃) ≤ 𝑆 → (𝐴𝐷𝑃) ≤ 𝑆))
190	189	pm2.18d 124	. . . . . 6 ⊢ (𝜑 → (𝐴𝐷𝑃) ≤ 𝑆)
191	190	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝐴𝐷𝑃) ≤ 𝑆)
192	86	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑅 ⊆ ℝ)
193	92	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤)
194		simpr 477	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝑌)
195		fvex 6201	. . . . . . . . 9 ⊢ (𝑁‘(𝐴 − 𝑦)) ∈ V
196		eqid 2622	. . . . . . . . . 10 ⊢ (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦))) = (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))
197	196	elrnmpt1 5374	. . . . . . . . 9 ⊢ ((𝑦 ∈ 𝑌 ∧ (𝑁‘(𝐴 − 𝑦)) ∈ V) → (𝑁‘(𝐴 − 𝑦)) ∈ ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦))))
198	194, 195, 197	sylancl 694	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝑁‘(𝐴 − 𝑦)) ∈ ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦))))
199	198, 10	syl6eleqr 2712	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝑁‘(𝐴 − 𝑦)) ∈ 𝑅)
200		infrelb 11008	. . . . . . 7 ⊢ ((𝑅 ⊆ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ∧ (𝑁‘(𝐴 − 𝑦)) ∈ 𝑅) → inf(𝑅, ℝ, < ) ≤ (𝑁‘(𝐴 − 𝑦)))
201	192, 193, 199, 200	syl3anc 1326	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → inf(𝑅, ℝ, < ) ≤ (𝑁‘(𝐴 − 𝑦)))
202	11, 201	syl5eqbr 4688	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑆 ≤ (𝑁‘(𝐴 − 𝑦)))
203	33, 35, 48, 191, 202	letrd 10194	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝐴𝐷𝑃) ≤ (𝑁‘(𝐴 − 𝑦)))
204	27, 203	eqbrtrrd 4677	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝑁‘(𝐴 − 𝑃)) ≤ (𝑁‘(𝐴 − 𝑦)))
205	204	ralrimiva 2966	. 2 ⊢ (𝜑 → ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑃)) ≤ (𝑁‘(𝐴 − 𝑦)))
206		oveq2 6658	. . . . . 6 ⊢ (𝑥 = 𝑃 → (𝐴 − 𝑥) = (𝐴 − 𝑃))
207	206	fveq2d 6195	. . . . 5 ⊢ (𝑥 = 𝑃 → (𝑁‘(𝐴 − 𝑥)) = (𝑁‘(𝐴 − 𝑃)))
208	207	breq1d 4663	. . . 4 ⊢ (𝑥 = 𝑃 → ((𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)) ↔ (𝑁‘(𝐴 − 𝑃)) ≤ (𝑁‘(𝐴 − 𝑦))))
209	208	ralbidv 2986	. . 3 ⊢ (𝑥 = 𝑃 → (∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)) ↔ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑃)) ≤ (𝑁‘(𝐴 − 𝑦))))
210	209	rspcev 3309	. 2 ⊢ ((𝑃 ∈ 𝑌 ∧ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑃)) ≤ (𝑁‘(𝐴 − 𝑦))) → ∃𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))
211	16, 205, 210	syl2anc 693	1 ⊢ (𝜑 → ∃𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∧ wa 384 = wceq 1483 ∈ wcel 1990 ≠ wne 2794 ∀wral 2912 ∃wrex 2913 {crab 2916 Vcvv 3200 ∩ cin 3573 ⊆ wss 3574 ∅c0 3915 𝒫 cpw 4158 ∪ cuni 4436 class class class wbr 4653 ↦ cmpt 4729 × cxp 5112 ran crn 5115 ↾ cres 5116 ‘cfv 5888 (class class class)co 6650 infcinf 8347 ℝcr 9935 0cc0 9936 + caddc 9939 · cmul 9941 ℝ^*cxr 10073 < clt 10074 ≤ cle 10075 − cmin 10266 / cdiv 10684 2c2 11070 ℝ⁺crp 11832 ↑cexp 12860 Basecbs 15857 ↾_s cress 15858 distcds 15950 TopOpenctopn 16082 -_gcsg 17424 LModclmod 18863 LSubSpclss 18932 ∞Metcxmt 19731 Metcme 19732 fBascfbas 19734 filGencfg 19735 MetOpencmopn 19736 Clsdccld 20820 clsccl 20822 Filcfil 21649 fLim cflim 21738 ∞MetSpcxme 22122 MetSpcmt 22123 normcnm 22381 NrmGrpcngp 22382 ℂPreHilccph 22966 CMetSpccms 23129

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-inf2 8538 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014 ax-addf 10015 ax-mulf 10016

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-iin 4523 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-tpos 7352 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-oadd 7564 df-er 7742 df-map 7859 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-fi 8317 df-sup 8348 df-inf 8349 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-4 11081 df-5 11082 df-6 11083 df-7 11084 df-8 11085 df-9 11086 df-n0 11293 df-z 11378 df-dec 11494 df-uz 11688 df-q 11789 df-rp 11833 df-xneg 11946 df-xadd 11947 df-xmul 11948 df-ico 12181 df-icc 12182 df-fz 12327 df-seq 12802 df-exp 12861 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-struct 15859 df-ndx 15860 df-slot 15861 df-base 15863 df-sets 15864 df-ress 15865 df-plusg 15954 df-mulr 15955 df-starv 15956 df-sca 15957 df-vsca 15958 df-ip 15959 df-tset 15960 df-ple 15961 df-ds 15964 df-unif 15965 df-rest 16083 df-0g 16102 df-topgen 16104 df-mgm 17242 df-sgrp 17284 df-mnd 17295 df-mhm 17335 df-grp 17425 df-minusg 17426 df-sbg 17427 df-mulg 17541 df-subg 17591 df-ghm 17658 df-cmn 18195 df-abl 18196 df-mgp 18490 df-ur 18502 df-ring 18549 df-cring 18550 df-oppr 18623 df-dvdsr 18641 df-unit 18642 df-invr 18672 df-dvr 18683 df-rnghom 18715 df-drng 18749 df-subrg 18778 df-staf 18845 df-srng 18846 df-lmod 18865 df-lss 18933 df-lmhm 19022 df-lvec 19103 df-sra 19172 df-rgmod 19173 df-psmet 19738 df-xmet 19739 df-met 19740 df-bl 19741 df-mopn 19742 df-fbas 19743 df-fg 19744 df-cnfld 19747 df-phl 19971 df-top 20699 df-topon 20716 df-topsp 20737 df-bases 20750 df-cld 20823 df-ntr 20824 df-cls 20825 df-nei 20902 df-haus 21119 df-fil 21650 df-flim 21743 df-xms 22125 df-ms 22126 df-nm 22387 df-ngp 22388 df-nlm 22391 df-clm 22863 df-cph 22968 df-cfil 23053 df-cmet 23055 df-cms 23132

This theorem is referenced by: minveclem5 23204

W3C validator