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 25485

Description: Lemma for minvec 25489. 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 25483	. . 3 ⊢ (𝜑 → 𝑃 ∈ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌))
15	14	elin2d 4228	. 2 ⊢ (𝜑 → 𝑃 ∈ 𝑌)
16	11	oveqi 7461	. . . . . . 7 ⊢ (𝐴𝐷𝑃) = (𝐴((dist‘𝑈) ↾ (𝑋 × 𝑋))𝑃)
17	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13	minveclem4b 25484	. . . . . . . 8 ⊢ (𝜑 → 𝑃 ∈ 𝑋)
18	7, 17	ovresd 7617	. . . . . . 7 ⊢ (𝜑 → (𝐴((dist‘𝑈) ↾ (𝑋 × 𝑋))𝑃) = (𝐴(dist‘𝑈)𝑃))
19	16, 18	eqtrid 2792	. . . . . 6 ⊢ (𝜑 → (𝐴𝐷𝑃) = (𝐴(dist‘𝑈)𝑃))
20		cphngp 25226	. . . . . . . 8 ⊢ (𝑈 ∈ ℂPreHil → 𝑈 ∈ NrmGrp)
21	4, 20	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑈 ∈ NrmGrp)
22		eqid 2740	. . . . . . . 8 ⊢ (dist‘𝑈) = (dist‘𝑈)
23	3, 1, 2, 22	ngpds 24638	. . . . . . 7 ⊢ ((𝑈 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝐴(dist‘𝑈)𝑃) = (𝑁‘(𝐴 − 𝑃)))
24	21, 7, 17, 23	syl3anc 1371	. . . . . 6 ⊢ (𝜑 → (𝐴(dist‘𝑈)𝑃) = (𝑁‘(𝐴 − 𝑃)))
25	19, 24	eqtrd 2780	. . . . 5 ⊢ (𝜑 → (𝐴𝐷𝑃) = (𝑁‘(𝐴 − 𝑃)))
26	25	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝐴𝐷𝑃) = (𝑁‘(𝐴 − 𝑃)))
27		ngpms 24634	. . . . . . . 8 ⊢ (𝑈 ∈ NrmGrp → 𝑈 ∈ MetSp)
28	1, 11	msmet 24488	. . . . . . . 8 ⊢ (𝑈 ∈ MetSp → 𝐷 ∈ (Met‘𝑋))
29	21, 27, 28	3syl 18	. . . . . . 7 ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋))
30		metcl 24363	. . . . . . 7 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝐴𝐷𝑃) ∈ ℝ)
31	29, 7, 17, 30	syl3anc 1371	. . . . . 6 ⊢ (𝜑 → (𝐴𝐷𝑃) ∈ ℝ)
32	31	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝐴𝐷𝑃) ∈ ℝ)
33	1, 2, 3, 4, 5, 6, 7, 8, 9, 10	minveclem4c 25478	. . . . . 6 ⊢ (𝜑 → 𝑆 ∈ ℝ)
34	33	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑆 ∈ ℝ)
35	21	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑈 ∈ NrmGrp)
36		cphlmod 25227	. . . . . . . . 9 ⊢ (𝑈 ∈ ℂPreHil → 𝑈 ∈ LMod)
37	4, 36	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑈 ∈ LMod)
38	37	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑈 ∈ LMod)
39	7	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝐴 ∈ 𝑋)
40		eqid 2740	. . . . . . . . . 10 ⊢ (LSubSp‘𝑈) = (LSubSp‘𝑈)
41	1, 40	lssss 20957	. . . . . . . . 9 ⊢ (𝑌 ∈ (LSubSp‘𝑈) → 𝑌 ⊆ 𝑋)
42	5, 41	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ⊆ 𝑋)
43	42	sselda 4008	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝑋)
44	1, 2	lmodvsubcl 20927	. . . . . . 7 ⊢ ((𝑈 ∈ LMod ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐴 − 𝑦) ∈ 𝑋)
45	38, 39, 43, 44	syl3anc 1371	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝐴 − 𝑦) ∈ 𝑋)
46	1, 3	nmcl 24650	. . . . . 6 ⊢ ((𝑈 ∈ NrmGrp ∧ (𝐴 − 𝑦) ∈ 𝑋) → (𝑁‘(𝐴 − 𝑦)) ∈ ℝ)
47	35, 45, 46	syl2anc 583	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝑁‘(𝐴 − 𝑦)) ∈ ℝ)
48	33, 31	ltnled 11437	. . . . . . . 8 ⊢ (𝜑 → (𝑆 < (𝐴𝐷𝑃) ↔ ¬ (𝐴𝐷𝑃) ≤ 𝑆))
49	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12	minveclem3b 25481	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐹 ∈ (fBas‘𝑌))
50		fbsspw 23861	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐹 ∈ (fBas‘𝑌) → 𝐹 ⊆ 𝒫 𝑌)
51	49, 50	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐹 ⊆ 𝒫 𝑌)
52	42	sspwd 4635	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝒫 𝑌 ⊆ 𝒫 𝑋)
53	51, 52	sstrd 4019	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐹 ⊆ 𝒫 𝑋)
54	1	fvexi 6934	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑋 ∈ V
55	54	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑋 ∈ V)
56		fbasweak 23894	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹 ∈ (fBas‘𝑌) ∧ 𝐹 ⊆ 𝒫 𝑋 ∧ 𝑋 ∈ V) → 𝐹 ∈ (fBas‘𝑋))
57	49, 53, 55, 56	syl3anc 1371	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐹 ∈ (fBas‘𝑋))
58	57	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝐹 ∈ (fBas‘𝑋))
59		fgcl 23907	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ (fBas‘𝑋) → (𝑋filGen𝐹) ∈ (Fil‘𝑋))
60	58, 59	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (𝑋filGen𝐹) ∈ (Fil‘𝑋))
61		ssfg 23901	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 ∈ (fBas‘𝑋) → 𝐹 ⊆ (𝑋filGen𝐹))
62	58, 61	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝐹 ⊆ (𝑋filGen𝐹))
63		minvec.t	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑇 = (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2))
64	31, 33	readdcld 11319	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((𝐴𝐷𝑃) + 𝑆) ∈ ℝ)
65	64	rehalfcld 12540	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (((𝐴𝐷𝑃) + 𝑆) / 2) ∈ ℝ)
66	65	resqcld 14175	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) ∈ ℝ)
67	33	resqcld 14175	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑆↑2) ∈ ℝ)
68	66, 67	resubcld 11718	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈ ℝ)
69	68	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈ ℝ)
70	33, 31, 33	ltadd1d 11883	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑆 < (𝐴𝐷𝑃) ↔ (𝑆 + 𝑆) < ((𝐴𝐷𝑃) + 𝑆)))
71	33	recnd 11318	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝑆 ∈ ℂ)
72	71	2timesd 12536	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (2 · 𝑆) = (𝑆 + 𝑆))
73	72	breq1d 5176	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((2 · 𝑆) < ((𝐴𝐷𝑃) + 𝑆) ↔ (𝑆 + 𝑆) < ((𝐴𝐷𝑃) + 𝑆)))
74		2re 12367	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 2 ∈ ℝ
75		2pos 12396	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 0 < 2
76	74, 75	pm3.2i 470	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (2 ∈ ℝ ∧ 0 < 2)
77	76	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (2 ∈ ℝ ∧ 0 < 2))
78		ltmuldiv2 12169	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑆 ∈ ℝ ∧ ((𝐴𝐷𝑃) + 𝑆) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · 𝑆) < ((𝐴𝐷𝑃) + 𝑆) ↔ 𝑆 < (((𝐴𝐷𝑃) + 𝑆) / 2)))
79	33, 64, 77, 78	syl3anc 1371	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((2 · 𝑆) < ((𝐴𝐷𝑃) + 𝑆) ↔ 𝑆 < (((𝐴𝐷𝑃) + 𝑆) / 2)))
80	70, 73, 79	3bitr2d 307	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑆 < (𝐴𝐷𝑃) ↔ 𝑆 < (((𝐴𝐷𝑃) + 𝑆) / 2)))
81	1, 2, 3, 4, 5, 6, 7, 8, 9	minveclem1 25477	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤))
82	81	simp3d 1144	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ∀𝑤 ∈ 𝑅 0 ≤ 𝑤)
83	81	simp1d 1142	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝑅 ⊆ ℝ)
84	81	simp2d 1143	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝑅 ≠ ∅)
85		0re 11292	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 0 ∈ ℝ
86		breq1 5169	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 = 0 → (𝑥 ≤ 𝑤 ↔ 0 ≤ 𝑤))
87	86	ralbidv 3184	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 = 0 → (∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ↔ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤))
88	87	rspcev 3635	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((0 ∈ ℝ ∧ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤) → ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤)
89	85, 82, 88	sylancr 586	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤)
90	85	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 0 ∈ ℝ)
91		infregelb 12279	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤) ∧ 0 ∈ ℝ) → (0 ≤ inf(𝑅, ℝ, < ) ↔ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤))
92	83, 84, 89, 90, 91	syl31anc 1373	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (0 ≤ inf(𝑅, ℝ, < ) ↔ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤))
93	82, 92	mpbird 257	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 0 ≤ inf(𝑅, ℝ, < ))
94	93, 10	breqtrrdi 5208	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 0 ≤ 𝑆)
95		metge0 24376	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → 0 ≤ (𝐴𝐷𝑃))
96	29, 7, 17, 95	syl3anc 1371	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 0 ≤ (𝐴𝐷𝑃))
97	31, 33, 96, 94	addge0d 11866	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 0 ≤ ((𝐴𝐷𝑃) + 𝑆))
98		divge0 12164	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐴𝐷𝑃) + 𝑆) ∈ ℝ ∧ 0 ≤ ((𝐴𝐷𝑃) + 𝑆)) ∧ (2 ∈ ℝ ∧ 0 < 2)) → 0 ≤ (((𝐴𝐷𝑃) + 𝑆) / 2))
99	64, 97, 77, 98	syl21anc 837	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 0 ≤ (((𝐴𝐷𝑃) + 𝑆) / 2))
100	33, 65, 94, 99	lt2sqd 14305	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑆 < (((𝐴𝐷𝑃) + 𝑆) / 2) ↔ (𝑆↑2) < ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2)))
101	67, 66	posdifd 11877	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((𝑆↑2) < ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) ↔ 0 < (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2))))
102	80, 100, 101	3bitrd 305	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑆 < (𝐴𝐷𝑃) ↔ 0 < (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2))))
103	102	biimpa 476	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 0 < (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2)))
104	69, 103	elrpd 13096	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈ ℝ⁺)
105	63, 104	eqeltrid 2848	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝑇 ∈ ℝ⁺)
106	5	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝑌 ∈ (LSubSp‘𝑈))
107		rabexg 5355	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑌 ∈ (LSubSp‘𝑈) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ∈ V)
108	106, 107	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ∈ V)
109		eqid 2740	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑟 ∈ ℝ⁺ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}) = (𝑟 ∈ ℝ⁺ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)})
110		oveq2 7456	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑟 = 𝑇 → ((𝑆↑2) + 𝑟) = ((𝑆↑2) + 𝑇))
111	110	breq2d 5178	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑟 = 𝑇 → (((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟) ↔ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)))
112	111	rabbidv 3451	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑟 = 𝑇 → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)} = {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)})
113	109, 112	elrnmpt1s 5982	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑇 ∈ ℝ⁺ ∧ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ∈ V) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ∈ ran (𝑟 ∈ ℝ⁺ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}))
114	105, 108, 113	syl2anc 583	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ∈ ran (𝑟 ∈ ℝ⁺ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}))
115	114, 12	eleqtrrdi 2855	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ∈ 𝐹)
116	62, 115	sseldd 4009	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ∈ (𝑋filGen𝐹))
117		ssrab2 4103	. . . . . . . . . . . . . . . 16 ⊢ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ⊆ 𝑋
118	117	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ⊆ 𝑋)
119	63	oveq2i 7459	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑆↑2) + 𝑇) = ((𝑆↑2) + (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2)))
120	67	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → (𝑆↑2) ∈ ℝ)
121	120	recnd 11318	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → (𝑆↑2) ∈ ℂ)
122	65	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → (((𝐴𝐷𝑃) + 𝑆) / 2) ∈ ℝ)
123	122	resqcld 14175	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) ∈ ℝ)
124	123	recnd 11318	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) ∈ ℂ)
125	121, 124	pncan3d 11650	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → ((𝑆↑2) + (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2))) = ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2))
126	119, 125	eqtrid 2792	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → ((𝑆↑2) + 𝑇) = ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2))
127	126	breq2d 5178	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → (((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇) ↔ ((𝐴𝐷𝑦)↑2) ≤ ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2)))
128	29	ad2antrr 725	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → 𝐷 ∈ (Met‘𝑋))
129	7	ad2antrr 725	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → 𝐴 ∈ 𝑋)
130	43	adantlr 714	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝑋)
131		metcl 24363	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐴𝐷𝑦) ∈ ℝ)
132	128, 129, 130, 131	syl3anc 1371	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → (𝐴𝐷𝑦) ∈ ℝ)
133		metge0 24376	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → 0 ≤ (𝐴𝐷𝑦))
134	128, 129, 130, 133	syl3anc 1371	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → 0 ≤ (𝐴𝐷𝑦))
135	99	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → 0 ≤ (((𝐴𝐷𝑃) + 𝑆) / 2))
136	132, 122, 134, 135	le2sqd 14306	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → ((𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2) ↔ ((𝐴𝐷𝑦)↑2) ≤ ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2)))
137	127, 136	bitr4d 282	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → (((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇) ↔ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)))
138	137	rabbidva 3450	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} = {𝑦 ∈ 𝑌 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)})
139	42	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝑌 ⊆ 𝑋)
140		rabss2 4101	. . . . . . . . . . . . . . . . 17 ⊢ (𝑌 ⊆ 𝑋 → {𝑦 ∈ 𝑌 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ⊆ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)})
141	139, 140	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑌 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ⊆ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)})
142	138, 141	eqsstrd 4047	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ⊆ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)})
143		filss 23882	. . . . . . . . . . . . . . 15 ⊢ (((𝑋filGen𝐹) ∈ (Fil‘𝑋) ∧ ({𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ∈ (𝑋filGen𝐹) ∧ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ⊆ 𝑋 ∧ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ⊆ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)})) → {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ∈ (𝑋filGen𝐹))
144	60, 116, 118, 142, 143	syl13anc 1372	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ∈ (𝑋filGen𝐹))
145		flimclsi 24007	. . . . . . . . . . . . . 14 ⊢ ({𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ∈ (𝑋filGen𝐹) → (𝐽 fLim (𝑋filGen𝐹)) ⊆ ((cls‘𝐽)‘{𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)}))
146	144, 145	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (𝐽 fLim (𝑋filGen𝐹)) ⊆ ((cls‘𝐽)‘{𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)}))
147	14	elin1d 4227	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑃 ∈ (𝐽 fLim (𝑋filGen𝐹)))
148	147	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝑃 ∈ (𝐽 fLim (𝑋filGen𝐹)))
149	146, 148	sseldd 4009	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝑃 ∈ ((cls‘𝐽)‘{𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)}))
150		ngpxms 24635	. . . . . . . . . . . . . . . . 17 ⊢ (𝑈 ∈ NrmGrp → 𝑈 ∈ ∞MetSp)
151	1, 11	xmsxmet 24487	. . . . . . . . . . . . . . . . 17 ⊢ (𝑈 ∈ ∞MetSp → 𝐷 ∈ (∞Met‘𝑋))
152	21, 150, 151	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))
153	152	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝐷 ∈ (∞Met‘𝑋))
154	7	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝐴 ∈ 𝑋)
155	65	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (((𝐴𝐷𝑃) + 𝑆) / 2) ∈ ℝ)
156	155	rexrd 11340	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (((𝐴𝐷𝑃) + 𝑆) / 2) ∈ ℝ^*)
157		eqid 2740	. . . . . . . . . . . . . . . 16 ⊢ (MetOpen‘𝐷) = (MetOpen‘𝐷)
158		eqid 2740	. . . . . . . . . . . . . . . 16 ⊢ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} = {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)}
159	157, 158	blcld 24539	. . . . . . . . . . . . . . 15 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ (((𝐴𝐷𝑃) + 𝑆) / 2) ∈ ℝ^*) → {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ∈ (Clsd‘(MetOpen‘𝐷)))
160	153, 154, 156, 159	syl3anc 1371	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ∈ (Clsd‘(MetOpen‘𝐷)))
161	8, 1, 11	xmstopn 24482	. . . . . . . . . . . . . . . . 17 ⊢ (𝑈 ∈ ∞MetSp → 𝐽 = (MetOpen‘𝐷))
162	21, 150, 161	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐽 = (MetOpen‘𝐷))
163	162	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝐽 = (MetOpen‘𝐷))
164	163	fveq2d 6924	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (Clsd‘𝐽) = (Clsd‘(MetOpen‘𝐷)))
165	160, 164	eleqtrrd 2847	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ∈ (Clsd‘𝐽))
166		cldcls 23071	. . . . . . . . . . . . 13 ⊢ ({𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ∈ (Clsd‘𝐽) → ((cls‘𝐽)‘{𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)}) = {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)})
167	165, 166	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → ((cls‘𝐽)‘{𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)}) = {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)})
168	149, 167	eleqtrd 2846	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝑃 ∈ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)})
169		oveq2 7456	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑃 → (𝐴𝐷𝑦) = (𝐴𝐷𝑃))
170	169	breq1d 5176	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑃 → ((𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2) ↔ (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)))
171	170	elrab 3708	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ↔ (𝑃 ∈ 𝑋 ∧ (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)))
172	171	simprbi 496	. . . . . . . . . . 11 ⊢ (𝑃 ∈ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} → (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2))
173	168, 172	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2))
174	31, 33, 31	leadd2d 11885	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴𝐷𝑃) ≤ 𝑆 ↔ ((𝐴𝐷𝑃) + (𝐴𝐷𝑃)) ≤ ((𝐴𝐷𝑃) + 𝑆)))
175	31	recnd 11318	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴𝐷𝑃) ∈ ℂ)
176	175	2timesd 12536	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 · (𝐴𝐷𝑃)) = ((𝐴𝐷𝑃) + (𝐴𝐷𝑃)))
177	176	breq1d 5176	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · (𝐴𝐷𝑃)) ≤ ((𝐴𝐷𝑃) + 𝑆) ↔ ((𝐴𝐷𝑃) + (𝐴𝐷𝑃)) ≤ ((𝐴𝐷𝑃) + 𝑆)))
178		lemuldiv2 12176	. . . . . . . . . . . . . 14 ⊢ (((𝐴𝐷𝑃) ∈ ℝ ∧ ((𝐴𝐷𝑃) + 𝑆) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · (𝐴𝐷𝑃)) ≤ ((𝐴𝐷𝑃) + 𝑆) ↔ (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)))
179	76, 178	mp3an3 1450	. . . . . . . . . . . . 13 ⊢ (((𝐴𝐷𝑃) ∈ ℝ ∧ ((𝐴𝐷𝑃) + 𝑆) ∈ ℝ) → ((2 · (𝐴𝐷𝑃)) ≤ ((𝐴𝐷𝑃) + 𝑆) ↔ (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)))
180	31, 64, 179	syl2anc 583	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · (𝐴𝐷𝑃)) ≤ ((𝐴𝐷𝑃) + 𝑆) ↔ (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)))
181	174, 177, 180	3bitr2d 307	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴𝐷𝑃) ≤ 𝑆 ↔ (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)))
182	181	biimpar 477	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)) → (𝐴𝐷𝑃) ≤ 𝑆)
183	173, 182	syldan 590	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (𝐴𝐷𝑃) ≤ 𝑆)
184	183	ex 412	. . . . . . . 8 ⊢ (𝜑 → (𝑆 < (𝐴𝐷𝑃) → (𝐴𝐷𝑃) ≤ 𝑆))
185	48, 184	sylbird 260	. . . . . . 7 ⊢ (𝜑 → (¬ (𝐴𝐷𝑃) ≤ 𝑆 → (𝐴𝐷𝑃) ≤ 𝑆))
186	185	pm2.18d 127	. . . . . 6 ⊢ (𝜑 → (𝐴𝐷𝑃) ≤ 𝑆)
187	186	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝐴𝐷𝑃) ≤ 𝑆)
188	83	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑅 ⊆ ℝ)
189	89	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤)
190		simpr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝑌)
191		fvex 6933	. . . . . . . . 9 ⊢ (𝑁‘(𝐴 − 𝑦)) ∈ V
192		eqid 2740	. . . . . . . . . 10 ⊢ (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦))) = (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))
193	192	elrnmpt1 5983	. . . . . . . . 9 ⊢ ((𝑦 ∈ 𝑌 ∧ (𝑁‘(𝐴 − 𝑦)) ∈ V) → (𝑁‘(𝐴 − 𝑦)) ∈ ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦))))
194	190, 191, 193	sylancl 585	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝑁‘(𝐴 − 𝑦)) ∈ ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦))))
195	194, 9	eleqtrrdi 2855	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝑁‘(𝐴 − 𝑦)) ∈ 𝑅)
196		infrelb 12280	. . . . . . 7 ⊢ ((𝑅 ⊆ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ∧ (𝑁‘(𝐴 − 𝑦)) ∈ 𝑅) → inf(𝑅, ℝ, < ) ≤ (𝑁‘(𝐴 − 𝑦)))
197	188, 189, 195, 196	syl3anc 1371	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → inf(𝑅, ℝ, < ) ≤ (𝑁‘(𝐴 − 𝑦)))
198	10, 197	eqbrtrid 5201	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑆 ≤ (𝑁‘(𝐴 − 𝑦)))
199	32, 34, 47, 187, 198	letrd 11447	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝐴𝐷𝑃) ≤ (𝑁‘(𝐴 − 𝑦)))
200	26, 199	eqbrtrrd 5190	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝑁‘(𝐴 − 𝑃)) ≤ (𝑁‘(𝐴 − 𝑦)))
201	200	ralrimiva 3152	. 2 ⊢ (𝜑 → ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑃)) ≤ (𝑁‘(𝐴 − 𝑦)))
202		oveq2 7456	. . . . . 6 ⊢ (𝑥 = 𝑃 → (𝐴 − 𝑥) = (𝐴 − 𝑃))
203	202	fveq2d 6924	. . . . 5 ⊢ (𝑥 = 𝑃 → (𝑁‘(𝐴 − 𝑥)) = (𝑁‘(𝐴 − 𝑃)))
204	203	breq1d 5176	. . . 4 ⊢ (𝑥 = 𝑃 → ((𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)) ↔ (𝑁‘(𝐴 − 𝑃)) ≤ (𝑁‘(𝐴 − 𝑦))))
205	204	ralbidv 3184	. . 3 ⊢ (𝑥 = 𝑃 → (∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)) ↔ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑃)) ≤ (𝑁‘(𝐴 − 𝑦))))
206	205	rspcev 3635	. 2 ⊢ ((𝑃 ∈ 𝑌 ∧ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑃)) ≤ (𝑁‘(𝐴 − 𝑦))) → ∃𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))
207	15, 201, 206	syl2anc 583	1 ⊢ (𝜑 → ∃𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1537 ∈ wcel 2108 ≠ wne 2946 ∀wral 3067 ∃wrex 3076 {crab 3443 Vcvv 3488 ⊆ wss 3976 ∅c0 4352 𝒫 cpw 4622 ∪ cuni 4931 class class class wbr 5166 ↦ cmpt 5249 × cxp 5698 ran crn 5701 ↾ cres 5702 ‘cfv 6573 (class class class)co 7448 infcinf 9510 ℝcr 11183 0cc0 11184 + caddc 11187 · cmul 11189 ℝ^*cxr 11323 < clt 11324 ≤ cle 11325 − cmin 11520 / cdiv 11947 2c2 12348 ℝ⁺crp 13057 ↑cexp 14112 Basecbs 17258 ↾_s cress 17287 distcds 17320 TopOpenctopn 17481 -_gcsg 18975 LModclmod 20880 LSubSpclss 20952 ∞Metcxmet 21372 Metcmet 21373 fBascfbas 21375 filGencfg 21376 MetOpencmopn 21377 Clsdccld 23045 clsccl 23047 Filcfil 23874 fLim cflim 23963 ∞MetSpcxms 24348 MetSpcms 24349 normcnm 24610 NrmGrpcngp 24611 ℂPreHilccph 25219 CMetSpccms 25385

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2158 ax-12 2178 ax-ext 2711 ax-rep 5303 ax-sep 5317 ax-nul 5324 ax-pow 5383 ax-pr 5447 ax-un 7770 ax-cnex 11240 ax-resscn 11241 ax-1cn 11242 ax-icn 11243 ax-addcl 11244 ax-addrcl 11245 ax-mulcl 11246 ax-mulrcl 11247 ax-mulcom 11248 ax-addass 11249 ax-mulass 11250 ax-distr 11251 ax-i2m1 11252 ax-1ne0 11253 ax-1rid 11254 ax-rnegex 11255 ax-rrecex 11256 ax-cnre 11257 ax-pre-lttri 11258 ax-pre-lttrn 11259 ax-pre-ltadd 11260 ax-pre-mulgt0 11261 ax-pre-sup 11262 ax-addf 11263 ax-mulf 11264

This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3or 1088 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2543 df-eu 2572 df-clab 2718 df-cleq 2732 df-clel 2819 df-nfc 2895 df-ne 2947 df-nel 3053 df-ral 3068 df-rex 3077 df-rmo 3388 df-reu 3389 df-rab 3444 df-v 3490 df-sbc 3805 df-csb 3922 df-dif 3979 df-un 3981 df-in 3983 df-ss 3993 df-pss 3996 df-nul 4353 df-if 4549 df-pw 4624 df-sn 4649 df-pr 4651 df-tp 4653 df-op 4655 df-uni 4932 df-int 4971 df-iun 5017 df-iin 5018 df-br 5167 df-opab 5229 df-mpt 5250 df-tr 5284 df-id 5593 df-eprel 5599 df-po 5607 df-so 5608 df-fr 5652 df-we 5654 df-xp 5706 df-rel 5707 df-cnv 5708 df-co 5709 df-dm 5710 df-rn 5711 df-res 5712 df-ima 5713 df-pred 6332 df-ord 6398 df-on 6399 df-lim 6400 df-suc 6401 df-iota 6525 df-fun 6575 df-fn 6576 df-f 6577 df-f1 6578 df-fo 6579 df-f1o 6580 df-fv 6581 df-riota 7404 df-ov 7451 df-oprab 7452 df-mpo 7453 df-om 7904 df-1st 8030 df-2nd 8031 df-tpos 8267 df-frecs 8322 df-wrecs 8353 df-recs 8427 df-rdg 8466 df-1o 8522 df-er 8763 df-map 8886 df-en 9004 df-dom 9005 df-sdom 9006 df-fin 9007 df-fi 9480 df-sup 9511 df-inf 9512 df-pnf 11326 df-mnf 11327 df-xr 11328 df-ltxr 11329 df-le 11330 df-sub 11522 df-neg 11523 df-div 11948 df-nn 12294 df-2 12356 df-3 12357 df-4 12358 df-5 12359 df-6 12360 df-7 12361 df-8 12362 df-9 12363 df-n0 12554 df-z 12640 df-dec 12759 df-uz 12904 df-q 13014 df-rp 13058 df-xneg 13175 df-xadd 13176 df-xmul 13177 df-ico 13413 df-icc 13414 df-fz 13568 df-seq 14053 df-exp 14113 df-cj 15148 df-re 15149 df-im 15150 df-sqrt 15284 df-abs 15285 df-struct 17194 df-sets 17211 df-slot 17229 df-ndx 17241 df-base 17259 df-ress 17288 df-plusg 17324 df-mulr 17325 df-starv 17326 df-sca 17327 df-vsca 17328 df-ip 17329 df-tset 17330 df-ple 17331 df-ds 17333 df-unif 17334 df-rest 17482 df-0g 17501 df-topgen 17503 df-mgm 18678 df-sgrp 18757 df-mnd 18773 df-mhm 18818 df-grp 18976 df-minusg 18977 df-sbg 18978 df-mulg 19108 df-subg 19163 df-ghm 19253 df-cmn 19824 df-abl 19825 df-mgp 20162 df-rng 20180 df-ur 20209 df-ring 20262 df-cring 20263 df-oppr 20360 df-dvdsr 20383 df-unit 20384 df-invr 20414 df-dvr 20427 df-rhm 20498 df-subrg 20597 df-drng 20753 df-staf 20862 df-srng 20863 df-lmod 20882 df-lss 20953 df-lmhm 21044 df-lvec 21125 df-sra 21195 df-rgmod 21196 df-psmet 21379 df-xmet 21380 df-met 21381 df-bl 21382 df-mopn 21383 df-fbas 21384 df-fg 21385 df-cnfld 21388 df-phl 21667 df-top 22921 df-topon 22938 df-topsp 22960 df-bases 22974 df-cld 23048 df-ntr 23049 df-cls 23050 df-nei 23127 df-haus 23344 df-fil 23875 df-flim 23968 df-xms 24351 df-ms 24352 df-nm 24616 df-ngp 24617 df-nlm 24620 df-clm 25115 df-cph 25221 df-cfil 25308 df-cmet 25310 df-cms 25388

This theorem is referenced by: minveclem5 25486

W3C validator