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 25591

Description: Lemma for minvec 25595. 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 25589	. . 3 ⊢ (𝜑 → 𝑃 ∈ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌))
15	14	elin2d 4158	. 2 ⊢ (𝜑 → 𝑃 ∈ 𝑌)
16	11	oveqi 7423	. . . . . . 7 ⊢ (𝐴𝐷𝑃) = (𝐴((dist‘𝑈) ↾ (𝑋 × 𝑋))𝑃)
17	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13	minveclem4b 25590	. . . . . . . 8 ⊢ (𝜑 → 𝑃 ∈ 𝑋)
18	7, 17	ovresd 7577	. . . . . . 7 ⊢ (𝜑 → (𝐴((dist‘𝑈) ↾ (𝑋 × 𝑋))𝑃) = (𝐴(dist‘𝑈)𝑃))
19	16, 18	eqtrid 2810	. . . . . 6 ⊢ (𝜑 → (𝐴𝐷𝑃) = (𝐴(dist‘𝑈)𝑃))
20		cphngp 25332	. . . . . . . 8 ⊢ (𝑈 ∈ ℂPreHil → 𝑈 ∈ NrmGrp)
21	4, 20	syl 18	. . . . . . 7 ⊢ (𝜑 → 𝑈 ∈ NrmGrp)
22		eqid 2763	. . . . . . . 8 ⊢ (dist‘𝑈) = (dist‘𝑈)
23	3, 1, 2, 22	ngpds 24761	. . . . . . 7 ⊢ ((𝑈 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝐴(dist‘𝑈)𝑃) = (𝑁‘(𝐴 − 𝑃)))
24	21, 7, 17, 23	syl3anc 1398	. . . . . 6 ⊢ (𝜑 → (𝐴(dist‘𝑈)𝑃) = (𝑁‘(𝐴 − 𝑃)))
25	19, 24	eqtrd 2798	. . . . 5 ⊢ (𝜑 → (𝐴𝐷𝑃) = (𝑁‘(𝐴 − 𝑃)))
26	25	adantr 485	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝐴𝐷𝑃) = (𝑁‘(𝐴 − 𝑃)))
27		ngpms 24757	. . . . . . . 8 ⊢ (𝑈 ∈ NrmGrp → 𝑈 ∈ MetSp)
28	1, 11	msmet 24614	. . . . . . . 8 ⊢ (𝑈 ∈ MetSp → 𝐷 ∈ (Met‘𝑋))
29	21, 27, 28	3syl 19	. . . . . . 7 ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋))
30		metcl 24489	. . . . . . 7 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝐴𝐷𝑃) ∈ ℝ)
31	29, 7, 17, 30	syl3anc 1398	. . . . . 6 ⊢ (𝜑 → (𝐴𝐷𝑃) ∈ ℝ)
32	31	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝐴𝐷𝑃) ∈ ℝ)
33	1, 2, 3, 4, 5, 6, 7, 8, 9, 10	minveclem4c 25584	. . . . . 6 ⊢ (𝜑 → 𝑆 ∈ ℝ)
34	33	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑆 ∈ ℝ)
35	21	adantr 485	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑈 ∈ NrmGrp)
36		cphlmod 25333	. . . . . . . . 9 ⊢ (𝑈 ∈ ℂPreHil → 𝑈 ∈ LMod)
37	4, 36	syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝑈 ∈ LMod)
38	37	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑈 ∈ LMod)
39	7	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝐴 ∈ 𝑋)
40		eqid 2763	. . . . . . . . . 10 ⊢ (LSubSp‘𝑈) = (LSubSp‘𝑈)
41	1, 40	lssss 21057	. . . . . . . . 9 ⊢ (𝑌 ∈ (LSubSp‘𝑈) → 𝑌 ⊆ 𝑋)
42	5, 41	syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ⊆ 𝑋)
43	42	sselda 3937	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝑋)
44	1, 2	lmodvsubcl 21028	. . . . . . 7 ⊢ ((𝑈 ∈ LMod ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐴 − 𝑦) ∈ 𝑋)
45	38, 39, 43, 44	syl3anc 1398	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝐴 − 𝑦) ∈ 𝑋)
46	1, 3	nmcl 24773	. . . . . 6 ⊢ ((𝑈 ∈ NrmGrp ∧ (𝐴 − 𝑦) ∈ 𝑋) → (𝑁‘(𝐴 − 𝑦)) ∈ ℝ)
47	35, 45, 46	syl2anc 595	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝑁‘(𝐴 − 𝑦)) ∈ ℝ)
48	33, 31	ltnled 11352	. . . . . . . 8 ⊢ (𝜑 → (𝑆 < (𝐴𝐷𝑃) ↔ ¬ (𝐴𝐷𝑃) ≤ 𝑆))
49	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12	minveclem3b 25587	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐹 ∈ (fBas‘𝑌))
50		fbsspw 23989	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐹 ∈ (fBas‘𝑌) → 𝐹 ⊆ 𝒫 𝑌)
51	49, 50	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐹 ⊆ 𝒫 𝑌)
52	42	sspwd 4575	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝒫 𝑌 ⊆ 𝒫 𝑋)
53	51, 52	sstrd 3947	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐹 ⊆ 𝒫 𝑋)
54	1	fvexi 6895	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑋 ∈ V
55	54	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑋 ∈ V)
56		fbasweak 24022	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹 ∈ (fBas‘𝑌) ∧ 𝐹 ⊆ 𝒫 𝑋 ∧ 𝑋 ∈ V) → 𝐹 ∈ (fBas‘𝑋))
57	49, 53, 55, 56	syl3anc 1398	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐹 ∈ (fBas‘𝑋))
58	57	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝐹 ∈ (fBas‘𝑋))
59		fgcl 24035	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ (fBas‘𝑋) → (𝑋filGen𝐹) ∈ (Fil‘𝑋))
60	58, 59	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (𝑋filGen𝐹) ∈ (Fil‘𝑋))
61		ssfg 24029	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 ∈ (fBas‘𝑋) → 𝐹 ⊆ (𝑋filGen𝐹))
62	58, 61	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝐹 ⊆ (𝑋filGen𝐹))
63		minvec.t	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑇 = (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2))
64	31, 33	readdcld 11233	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((𝐴𝐷𝑃) + 𝑆) ∈ ℝ)
65	64	rehalfcld 12486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (((𝐴𝐷𝑃) + 𝑆) / 2) ∈ ℝ)
66	65	resqcld 14157	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) ∈ ℝ)
67	33	resqcld 14157	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑆↑2) ∈ ℝ)
68	66, 67	resubcld 11637	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈ ℝ)
69	68	adantr 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈ ℝ)
70	33, 31, 33	ltadd1d 11802	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑆 < (𝐴𝐷𝑃) ↔ (𝑆 + 𝑆) < ((𝐴𝐷𝑃) + 𝑆)))
71	33	recnd 11232	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝑆 ∈ ℂ)
72	71	2timesd 12482	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (2 · 𝑆) = (𝑆 + 𝑆))
73	72	breq1d 5119	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((2 · 𝑆) < ((𝐴𝐷𝑃) + 𝑆) ↔ (𝑆 + 𝑆) < ((𝐴𝐷𝑃) + 𝑆)))
74		2re 12310	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 2 ∈ ℝ
75		2pos 12340	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 0 < 2
76	74, 75	pm3.2i 475	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (2 ∈ ℝ ∧ 0 < 2)
77	76	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (2 ∈ ℝ ∧ 0 < 2))
78		ltmuldiv2 12084	. . . . . . . . . . . . . . . . . . . . . . . 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 25583	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤))
82	81	simp3d 1162	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ∀𝑤 ∈ 𝑅 0 ≤ 𝑤)
83	81	simp1d 1160	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝑅 ⊆ ℝ)
84	81	simp2d 1161	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝑅 ≠ ∅)
85		0re 11205	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 0 ∈ ℝ
86		breq1 5112	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 = 0 → (𝑥 ≤ 𝑤 ↔ 0 ≤ 𝑤))
87	86	ralbidv 3188	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 = 0 → (∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ↔ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤))
88	87	rspcev 3581	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((0 ∈ ℝ ∧ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤) → ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤)
89	85, 82, 88	sylancr 598	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤)
90	85	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 0 ∈ ℝ)
91		infregelb 12194	. . . . . . . . . . . . . . . . . . . . . . . . . 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 5153	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 0 ≤ 𝑆)
95		metge0 24502	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → 0 ≤ (𝐴𝐷𝑃))
96	29, 7, 17, 95	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 0 ≤ (𝐴𝐷𝑃))
97	31, 33, 96, 94	addge0d 11785	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 0 ≤ ((𝐴𝐷𝑃) + 𝑆))
98		divge0 12079	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐴𝐷𝑃) + 𝑆) ∈ ℝ ∧ 0 ≤ ((𝐴𝐷𝑃) + 𝑆)) ∧ (2 ∈ ℝ ∧ 0 < 2)) → 0 ≤ (((𝐴𝐷𝑃) + 𝑆) / 2))
99	64, 97, 77, 98	syl21anc 850	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 0 ≤ (((𝐴𝐷𝑃) + 𝑆) / 2))
100	33, 65, 94, 99	lt2sqd 14288	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑆 < (((𝐴𝐷𝑃) + 𝑆) / 2) ↔ (𝑆↑2) < ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2)))
101	67, 66	posdifd 11796	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((𝑆↑2) < ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) ↔ 0 < (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2))))
102	80, 100, 101	3bitrd 308	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑆 < (𝐴𝐷𝑃) ↔ 0 < (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2))))
103	102	biimpa 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 0 < (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2)))
104	69, 103	elrpd 13052	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈ ℝ⁺)
105	63, 104	eqeltrid 2867	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝑇 ∈ ℝ⁺)
106	5	adantr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝑌 ∈ (LSubSp‘𝑈))
107		rabexg 5308	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑌 ∈ (LSubSp‘𝑈) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ∈ V)
108	106, 107	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ∈ V)
109		eqid 2763	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑟 ∈ ℝ⁺ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}) = (𝑟 ∈ ℝ⁺ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)})
110		oveq2 7418	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑟 = 𝑇 → ((𝑆↑2) + 𝑟) = ((𝑆↑2) + 𝑇))
111	110	breq2d 5121	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑟 = 𝑇 → (((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟) ↔ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)))
112	111	rabbidv 3423	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑟 = 𝑇 → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)} = {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)})
113	109, 112	elrnmpt1s 5949	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑇 ∈ ℝ⁺ ∧ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ∈ V) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ∈ ran (𝑟 ∈ ℝ⁺ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}))
114	105, 108, 113	syl2anc 595	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ∈ ran (𝑟 ∈ ℝ⁺ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}))
115	114, 12	eleqtrrdi 2874	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ∈ 𝐹)
116	62, 115	sseldd 3938	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ∈ (𝑋filGen𝐹))
117		ssrab2 4034	. . . . . . . . . . . . . . . 16 ⊢ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ⊆ 𝑋
118	117	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ⊆ 𝑋)
119	63	oveq2i 7421	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑆↑2) + 𝑇) = ((𝑆↑2) + (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2)))
120	67	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → (𝑆↑2) ∈ ℝ)
121	120	recnd 11232	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → (𝑆↑2) ∈ ℂ)
122	65	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → (((𝐴𝐷𝑃) + 𝑆) / 2) ∈ ℝ)
123	122	resqcld 14157	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) ∈ ℝ)
124	123	recnd 11232	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) ∈ ℂ)
125	121, 124	pncan3d 11567	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → ((𝑆↑2) + (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2))) = ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2))
126	119, 125	eqtrid 2810	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → ((𝑆↑2) + 𝑇) = ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2))
127	126	breq2d 5121	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → (((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇) ↔ ((𝐴𝐷𝑦)↑2) ≤ ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2)))
128	29	ad2antrr 738	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → 𝐷 ∈ (Met‘𝑋))
129	7	ad2antrr 738	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → 𝐴 ∈ 𝑋)
130	43	adantlr 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝑋)
131		metcl 24489	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐴𝐷𝑦) ∈ ℝ)
132	128, 129, 130, 131	syl3anc 1398	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → (𝐴𝐷𝑦) ∈ ℝ)
133		metge0 24502	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → 0 ≤ (𝐴𝐷𝑦))
134	128, 129, 130, 133	syl3anc 1398	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → 0 ≤ (𝐴𝐷𝑦))
135	99	ad2antrr 738	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → 0 ≤ (((𝐴𝐷𝑃) + 𝑆) / 2))
136	132, 122, 134, 135	le2sqd 14289	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → ((𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2) ↔ ((𝐴𝐷𝑦)↑2) ≤ ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2)))
137	127, 136	bitr4d 285	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → (((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇) ↔ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)))
138	137	rabbidva 3422	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} = {𝑦 ∈ 𝑌 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)})
139	42	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝑌 ⊆ 𝑋)
140		rabss2 4031	. . . . . . . . . . . . . . . . 17 ⊢ (𝑌 ⊆ 𝑋 → {𝑦 ∈ 𝑌 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ⊆ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)})
141	139, 140	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑌 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ⊆ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)})
142	138, 141	eqsstrd 3971	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ⊆ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)})
143		filss 24010	. . . . . . . . . . . . . . 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 24135	. . . . . . . . . . . . . 14 ⊢ ({𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ∈ (𝑋filGen𝐹) → (𝐽 fLim (𝑋filGen𝐹)) ⊆ ((cls‘𝐽)‘{𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)}))
146	144, 145	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (𝐽 fLim (𝑋filGen𝐹)) ⊆ ((cls‘𝐽)‘{𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)}))
147	14	elin1d 4157	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑃 ∈ (𝐽 fLim (𝑋filGen𝐹)))
148	147	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝑃 ∈ (𝐽 fLim (𝑋filGen𝐹)))
149	146, 148	sseldd 3938	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝑃 ∈ ((cls‘𝐽)‘{𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)}))
150		ngpxms 24758	. . . . . . . . . . . . . . . . 17 ⊢ (𝑈 ∈ NrmGrp → 𝑈 ∈ ∞MetSp)
151	1, 11	xmsxmet 24613	. . . . . . . . . . . . . . . . 17 ⊢ (𝑈 ∈ ∞MetSp → 𝐷 ∈ (∞Met‘𝑋))
152	21, 150, 151	3syl 19	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))
153	152	adantr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝐷 ∈ (∞Met‘𝑋))
154	7	adantr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝐴 ∈ 𝑋)
155	65	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (((𝐴𝐷𝑃) + 𝑆) / 2) ∈ ℝ)
156	155	rexrd 11254	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (((𝐴𝐷𝑃) + 𝑆) / 2) ∈ ℝ^*)
157		eqid 2763	. . . . . . . . . . . . . . . 16 ⊢ (MetOpen‘𝐷) = (MetOpen‘𝐷)
158		eqid 2763	. . . . . . . . . . . . . . . 16 ⊢ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} = {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)}
159	157, 158	blcld 24662	. . . . . . . . . . . . . . 15 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ (((𝐴𝐷𝑃) + 𝑆) / 2) ∈ ℝ^*) → {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ∈ (Clsd‘(MetOpen‘𝐷)))
160	153, 154, 156, 159	syl3anc 1398	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ∈ (Clsd‘(MetOpen‘𝐷)))
161	8, 1, 11	xmstopn 24608	. . . . . . . . . . . . . . . . 17 ⊢ (𝑈 ∈ ∞MetSp → 𝐽 = (MetOpen‘𝐷))
162	21, 150, 161	3syl 19	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐽 = (MetOpen‘𝐷))
163	162	adantr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝐽 = (MetOpen‘𝐷))
164	163	fveq2d 6885	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (Clsd‘𝐽) = (Clsd‘(MetOpen‘𝐷)))
165	160, 164	eleqtrrd 2866	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ∈ (Clsd‘𝐽))
166		cldcls 23199	. . . . . . . . . . . . 13 ⊢ ({𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ∈ (Clsd‘𝐽) → ((cls‘𝐽)‘{𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)}) = {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)})
167	165, 166	syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → ((cls‘𝐽)‘{𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)}) = {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)})
168	149, 167	eleqtrd 2865	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝑃 ∈ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)})
169		oveq2 7418	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑃 → (𝐴𝐷𝑦) = (𝐴𝐷𝑃))
170	169	breq1d 5119	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑃 → ((𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2) ↔ (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)))
171	170	elrab 3650	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ↔ (𝑃 ∈ 𝑋 ∧ (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)))
172	171	simprbi 502	. . . . . . . . . . 11 ⊢ (𝑃 ∈ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} → (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2))
173	168, 172	syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2))
174	31, 33, 31	leadd2d 11804	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴𝐷𝑃) ≤ 𝑆 ↔ ((𝐴𝐷𝑃) + (𝐴𝐷𝑃)) ≤ ((𝐴𝐷𝑃) + 𝑆)))
175	31	recnd 11232	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴𝐷𝑃) ∈ ℂ)
176	175	2timesd 12482	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 · (𝐴𝐷𝑃)) = ((𝐴𝐷𝑃) + (𝐴𝐷𝑃)))
177	176	breq1d 5119	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · (𝐴𝐷𝑃)) ≤ ((𝐴𝐷𝑃) + 𝑆) ↔ ((𝐴𝐷𝑃) + (𝐴𝐷𝑃)) ≤ ((𝐴𝐷𝑃) + 𝑆)))
178		lemuldiv2 12091	. . . . . . . . . . . . . 14 ⊢ (((𝐴𝐷𝑃) ∈ ℝ ∧ ((𝐴𝐷𝑃) + 𝑆) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · (𝐴𝐷𝑃)) ≤ ((𝐴𝐷𝑃) + 𝑆) ↔ (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)))
179	76, 178	mp3an3 1479	. . . . . . . . . . . . 13 ⊢ (((𝐴𝐷𝑃) ∈ ℝ ∧ ((𝐴𝐷𝑃) + 𝑆) ∈ ℝ) → ((2 · (𝐴𝐷𝑃)) ≤ ((𝐴𝐷𝑃) + 𝑆) ↔ (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)))
180	31, 64, 179	syl2anc 595	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · (𝐴𝐷𝑃)) ≤ ((𝐴𝐷𝑃) + 𝑆) ↔ (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)))
181	174, 177, 180	3bitr2d 310	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴𝐷𝑃) ≤ 𝑆 ↔ (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)))
182	181	biimpar 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)) → (𝐴𝐷𝑃) ≤ 𝑆)
183	173, 182	syldan 602	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (𝐴𝐷𝑃) ≤ 𝑆)
184	183	ex 417	. . . . . . . 8 ⊢ (𝜑 → (𝑆 < (𝐴𝐷𝑃) → (𝐴𝐷𝑃) ≤ 𝑆))
185	48, 184	sylbird 263	. . . . . . 7 ⊢ (𝜑 → (¬ (𝐴𝐷𝑃) ≤ 𝑆 → (𝐴𝐷𝑃) ≤ 𝑆))
186	185	pm2.18d 128	. . . . . 6 ⊢ (𝜑 → (𝐴𝐷𝑃) ≤ 𝑆)
187	186	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝐴𝐷𝑃) ≤ 𝑆)
188	83	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑅 ⊆ ℝ)
189	89	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤)
190		simpr 489	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝑌)
191		fvex 6894	. . . . . . . . 9 ⊢ (𝑁‘(𝐴 − 𝑦)) ∈ V
192		eqid 2763	. . . . . . . . . 10 ⊢ (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦))) = (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))
193	192	elrnmpt1 5950	. . . . . . . . 9 ⊢ ((𝑦 ∈ 𝑌 ∧ (𝑁‘(𝐴 − 𝑦)) ∈ V) → (𝑁‘(𝐴 − 𝑦)) ∈ ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦))))
194	190, 191, 193	sylancl 597	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝑁‘(𝐴 − 𝑦)) ∈ ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦))))
195	194, 9	eleqtrrdi 2874	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝑁‘(𝐴 − 𝑦)) ∈ 𝑅)
196		infrelb 12195	. . . . . . 7 ⊢ ((𝑅 ⊆ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ∧ (𝑁‘(𝐴 − 𝑦)) ∈ 𝑅) → inf(𝑅, ℝ, < ) ≤ (𝑁‘(𝐴 − 𝑦)))
197	188, 189, 195, 196	syl3anc 1398	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → inf(𝑅, ℝ, < ) ≤ (𝑁‘(𝐴 − 𝑦)))
198	10, 197	eqbrtrid 5146	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑆 ≤ (𝑁‘(𝐴 − 𝑦)))
199	32, 34, 47, 187, 198	letrd 11362	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝐴𝐷𝑃) ≤ (𝑁‘(𝐴 − 𝑦)))
200	26, 199	eqbrtrrd 5135	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝑁‘(𝐴 − 𝑃)) ≤ (𝑁‘(𝐴 − 𝑦)))
201	200	ralrimiva 3157	. 2 ⊢ (𝜑 → ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑃)) ≤ (𝑁‘(𝐴 − 𝑦)))
202		oveq2 7418	. . . . . 6 ⊢ (𝑥 = 𝑃 → (𝐴 − 𝑥) = (𝐴 − 𝑃))
203	202	fveq2d 6885	. . . . 5 ⊢ (𝑥 = 𝑃 → (𝑁‘(𝐴 − 𝑥)) = (𝑁‘(𝐴 − 𝑃)))
204	203	breq1d 5119	. . . 4 ⊢ (𝑥 = 𝑃 → ((𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)) ↔ (𝑁‘(𝐴 − 𝑃)) ≤ (𝑁‘(𝐴 − 𝑦))))
205	204	ralbidv 3188	. . 3 ⊢ (𝑥 = 𝑃 → (∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)) ↔ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑃)) ≤ (𝑁‘(𝐴 − 𝑦))))
206	205	rspcev 3581	. 2 ⊢ ((𝑃 ∈ 𝑌 ∧ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑃)) ≤ (𝑁‘(𝐴 − 𝑦))) → ∃𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))
207	15, 201, 206	syl2anc 595	1 ⊢ (𝜑 → ∃𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 = wceq 1570 ∈ wcel 2143 ≠ wne 2958 ∀wral 3079 ∃wrex 3089 {crab 3416 Vcvv 3455 ⊆ wss 3905 ∅c0 4286 𝒫 cpw 4562 ∪ cuni 4872 class class class wbr 5109 ↦ cmpt 5192 × cxp 5659 ran crn 5662 ↾ cres 5663 ‘cfv 6536 (class class class)co 7410 infcinf 9397 ℝcr 11094 0cc0 11095 + caddc 11098 · cmul 11100 ℝ^*cxr 11237 < clt 11238 ≤ cle 11239 − cmin 11436 / cdiv 11866 2c2 12290 ℝ⁺crp 13011 ↑cexp 14093 Basecbs 17264 ↾_s cress 17285 distcds 17314 TopOpenctopn 17469 -_gcsg 18997 LModclmod 20981 LSubSpclss 21052 ∞Metcxmet 21507 Metcmet 21508 fBascfbas 21510 filGencfg 21511 MetOpencmopn 21512 Clsdccld 23173 clsccl 23175 Filcfil 24002 fLim cflim 24091 ∞MetSpcxms 24474 MetSpcms 24475 normcnm 24733 NrmGrpcngp 24734 ℂPreHilccph 25325 CMetSpccms 25491

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-rep 5238 ax-sep 5257 ax-nul 5269 ax-pow 5336 ax-pr 5404 ax-un 7732 ax-cnex 11151 ax-resscn 11152 ax-1cn 11153 ax-icn 11154 ax-addcl 11155 ax-addrcl 11156 ax-mulcl 11157 ax-mulrcl 11158 ax-mulcom 11159 ax-addass 11160 ax-mulass 11161 ax-distr 11162 ax-i2m1 11163 ax-1ne0 11164 ax-1rid 11165 ax-rnegex 11166 ax-rrecex 11167 ax-cnre 11168 ax-pre-lttri 11169 ax-pre-lttrn 11170 ax-pre-ltadd 11171 ax-pre-mulgt0 11172 ax-pre-sup 11173 ax-addf 11174 ax-mulf 11175

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3457 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3925 df-nul 4287 df-if 4488 df-pw 4564 df-sn 4590 df-pr 4592 df-tp 4594 df-op 4596 df-uni 4873 df-int 4913 df-iun 4958 df-iin 4959 df-br 5110 df-opab 5174 df-mpt 5193 df-tr 5219 df-id 5556 df-eprel 5561 df-po 5569 df-so 5570 df-fr 5614 df-we 5616 df-xp 5667 df-rel 5668 df-cnv 5669 df-co 5670 df-dm 5671 df-rn 5672 df-res 5673 df-ima 5674 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-om 7859 df-1st 7982 df-2nd 7983 df-tpos 8218 df-frecs 8274 df-wrecs 8305 df-recs 8354 df-rdg 8393 df-1o 8449 df-er 8690 df-map 8822 df-en 8940 df-dom 8941 df-sdom 8942 df-fin 8943 df-fi 9367 df-sup 9398 df-inf 9399 df-pnf 11240 df-mnf 11241 df-xr 11242 df-ltxr 11243 df-le 11244 df-sub 11438 df-neg 11439 df-div 11867 df-nn 12229 df-2 12298 df-3 12299 df-4 12300 df-5 12301 df-6 12302 df-7 12303 df-8 12304 df-9 12305 df-n0 12500 df-z 12587 df-dec 12707 df-uz 12858 df-q 12968 df-rp 13012 df-xneg 13132 df-xadd 13133 df-xmul 13134 df-ico 13373 df-icc 13374 df-fz 13531 df-seq 14034 df-exp 14094 df-cj 15146 df-re 15147 df-im 15148 df-sqrt 15282 df-abs 15283 df-struct 17202 df-sets 17219 df-slot 17237 df-ndx 17249 df-base 17265 df-ress 17286 df-plusg 17318 df-mulr 17319 df-starv 17320 df-sca 17321 df-vsca 17322 df-ip 17323 df-tset 17324 df-ple 17325 df-ds 17327 df-unif 17328 df-rest 17470 df-0g 17489 df-topgen 17491 df-mgm 18693 df-sgrp 18772 df-mnd 18788 df-mhm 18836 df-grp 18998 df-minusg 18999 df-sbg 19000 df-mulg 19129 df-subg 19184 df-ghm 19279 df-cmn 19847 df-abl 19848 df-mgp 20212 df-rng 20226 df-ur 20259 df-ring 20312 df-cring 20313 df-oppr 20415 df-dvdsr 20435 df-unit 20436 df-invr 20466 df-dvr 20479 df-rhm 20550 df-subrg 20669 df-drng 20829 df-staf 20942 df-srng 20943 df-lmod 20983 df-lss 21053 df-lmhm 21143 df-lvec 21224 df-sra 21294 df-rgmod 21295 df-psmet 21514 df-xmet 21515 df-met 21516 df-bl 21517 df-mopn 21518 df-fbas 21519 df-fg 21520 df-cnfld 21523 df-phl 21776 df-top 23051 df-topon 23068 df-topsp 23090 df-bases 23103 df-cld 23176 df-ntr 23177 df-cls 23178 df-nei 23255 df-haus 23472 df-fil 24003 df-flim 24096 df-xms 24477 df-ms 24478 df-nm 24739 df-ngp 24740 df-nlm 24743 df-clm 25222 df-cph 25327 df-cfil 25414 df-cmet 25416 df-cms 25494

This theorem is referenced by: minveclem5 25592

W3C validator