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 25332

Description: Lemma for minvec 25336. 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 25330	. . 3 ⊢ (𝜑 → 𝑃 ∈ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌))
15	14	elin2d 4168	. 2 ⊢ (𝜑 → 𝑃 ∈ 𝑌)
16	11	oveqi 7400	. . . . . . 7 ⊢ (𝐴𝐷𝑃) = (𝐴((dist‘𝑈) ↾ (𝑋 × 𝑋))𝑃)
17	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13	minveclem4b 25331	. . . . . . . 8 ⊢ (𝜑 → 𝑃 ∈ 𝑋)
18	7, 17	ovresd 7556	. . . . . . 7 ⊢ (𝜑 → (𝐴((dist‘𝑈) ↾ (𝑋 × 𝑋))𝑃) = (𝐴(dist‘𝑈)𝑃))
19	16, 18	eqtrid 2776	. . . . . 6 ⊢ (𝜑 → (𝐴𝐷𝑃) = (𝐴(dist‘𝑈)𝑃))
20		cphngp 25073	. . . . . . . 8 ⊢ (𝑈 ∈ ℂPreHil → 𝑈 ∈ NrmGrp)
21	4, 20	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑈 ∈ NrmGrp)
22		eqid 2729	. . . . . . . 8 ⊢ (dist‘𝑈) = (dist‘𝑈)
23	3, 1, 2, 22	ngpds 24492	. . . . . . 7 ⊢ ((𝑈 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝐴(dist‘𝑈)𝑃) = (𝑁‘(𝐴 − 𝑃)))
24	21, 7, 17, 23	syl3anc 1373	. . . . . 6 ⊢ (𝜑 → (𝐴(dist‘𝑈)𝑃) = (𝑁‘(𝐴 − 𝑃)))
25	19, 24	eqtrd 2764	. . . . 5 ⊢ (𝜑 → (𝐴𝐷𝑃) = (𝑁‘(𝐴 − 𝑃)))
26	25	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝐴𝐷𝑃) = (𝑁‘(𝐴 − 𝑃)))
27		ngpms 24488	. . . . . . . 8 ⊢ (𝑈 ∈ NrmGrp → 𝑈 ∈ MetSp)
28	1, 11	msmet 24345	. . . . . . . 8 ⊢ (𝑈 ∈ MetSp → 𝐷 ∈ (Met‘𝑋))
29	21, 27, 28	3syl 18	. . . . . . 7 ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋))
30		metcl 24220	. . . . . . 7 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝐴𝐷𝑃) ∈ ℝ)
31	29, 7, 17, 30	syl3anc 1373	. . . . . 6 ⊢ (𝜑 → (𝐴𝐷𝑃) ∈ ℝ)
32	31	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝐴𝐷𝑃) ∈ ℝ)
33	1, 2, 3, 4, 5, 6, 7, 8, 9, 10	minveclem4c 25325	. . . . . 6 ⊢ (𝜑 → 𝑆 ∈ ℝ)
34	33	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑆 ∈ ℝ)
35	21	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑈 ∈ NrmGrp)
36		cphlmod 25074	. . . . . . . . 9 ⊢ (𝑈 ∈ ℂPreHil → 𝑈 ∈ LMod)
37	4, 36	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑈 ∈ LMod)
38	37	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑈 ∈ LMod)
39	7	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝐴 ∈ 𝑋)
40		eqid 2729	. . . . . . . . . 10 ⊢ (LSubSp‘𝑈) = (LSubSp‘𝑈)
41	1, 40	lssss 20842	. . . . . . . . 9 ⊢ (𝑌 ∈ (LSubSp‘𝑈) → 𝑌 ⊆ 𝑋)
42	5, 41	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ⊆ 𝑋)
43	42	sselda 3946	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝑋)
44	1, 2	lmodvsubcl 20813	. . . . . . 7 ⊢ ((𝑈 ∈ LMod ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐴 − 𝑦) ∈ 𝑋)
45	38, 39, 43, 44	syl3anc 1373	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝐴 − 𝑦) ∈ 𝑋)
46	1, 3	nmcl 24504	. . . . . 6 ⊢ ((𝑈 ∈ NrmGrp ∧ (𝐴 − 𝑦) ∈ 𝑋) → (𝑁‘(𝐴 − 𝑦)) ∈ ℝ)
47	35, 45, 46	syl2anc 584	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝑁‘(𝐴 − 𝑦)) ∈ ℝ)
48	33, 31	ltnled 11321	. . . . . . . 8 ⊢ (𝜑 → (𝑆 < (𝐴𝐷𝑃) ↔ ¬ (𝐴𝐷𝑃) ≤ 𝑆))
49	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12	minveclem3b 25328	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐹 ∈ (fBas‘𝑌))
50		fbsspw 23719	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐹 ∈ (fBas‘𝑌) → 𝐹 ⊆ 𝒫 𝑌)
51	49, 50	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐹 ⊆ 𝒫 𝑌)
52	42	sspwd 4576	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝒫 𝑌 ⊆ 𝒫 𝑋)
53	51, 52	sstrd 3957	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐹 ⊆ 𝒫 𝑋)
54	1	fvexi 6872	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑋 ∈ V
55	54	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑋 ∈ V)
56		fbasweak 23752	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹 ∈ (fBas‘𝑌) ∧ 𝐹 ⊆ 𝒫 𝑋 ∧ 𝑋 ∈ V) → 𝐹 ∈ (fBas‘𝑋))
57	49, 53, 55, 56	syl3anc 1373	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐹 ∈ (fBas‘𝑋))
58	57	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝐹 ∈ (fBas‘𝑋))
59		fgcl 23765	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ (fBas‘𝑋) → (𝑋filGen𝐹) ∈ (Fil‘𝑋))
60	58, 59	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (𝑋filGen𝐹) ∈ (Fil‘𝑋))
61		ssfg 23759	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 ∈ (fBas‘𝑋) → 𝐹 ⊆ (𝑋filGen𝐹))
62	58, 61	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝐹 ⊆ (𝑋filGen𝐹))
63		minvec.t	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑇 = (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2))
64	31, 33	readdcld 11203	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((𝐴𝐷𝑃) + 𝑆) ∈ ℝ)
65	64	rehalfcld 12429	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (((𝐴𝐷𝑃) + 𝑆) / 2) ∈ ℝ)
66	65	resqcld 14090	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) ∈ ℝ)
67	33	resqcld 14090	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑆↑2) ∈ ℝ)
68	66, 67	resubcld 11606	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈ ℝ)
69	68	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈ ℝ)
70	33, 31, 33	ltadd1d 11771	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑆 < (𝐴𝐷𝑃) ↔ (𝑆 + 𝑆) < ((𝐴𝐷𝑃) + 𝑆)))
71	33	recnd 11202	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝑆 ∈ ℂ)
72	71	2timesd 12425	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (2 · 𝑆) = (𝑆 + 𝑆))
73	72	breq1d 5117	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((2 · 𝑆) < ((𝐴𝐷𝑃) + 𝑆) ↔ (𝑆 + 𝑆) < ((𝐴𝐷𝑃) + 𝑆)))
74		2re 12260	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 2 ∈ ℝ
75		2pos 12289	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 0 < 2
76	74, 75	pm3.2i 470	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (2 ∈ ℝ ∧ 0 < 2)
77	76	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (2 ∈ ℝ ∧ 0 < 2))
78		ltmuldiv2 12057	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑆 ∈ ℝ ∧ ((𝐴𝐷𝑃) + 𝑆) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · 𝑆) < ((𝐴𝐷𝑃) + 𝑆) ↔ 𝑆 < (((𝐴𝐷𝑃) + 𝑆) / 2)))
79	33, 64, 77, 78	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((2 · 𝑆) < ((𝐴𝐷𝑃) + 𝑆) ↔ 𝑆 < (((𝐴𝐷𝑃) + 𝑆) / 2)))
80	70, 73, 79	3bitr2d 307	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑆 < (𝐴𝐷𝑃) ↔ 𝑆 < (((𝐴𝐷𝑃) + 𝑆) / 2)))
81	1, 2, 3, 4, 5, 6, 7, 8, 9	minveclem1 25324	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤))
82	81	simp3d 1144	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ∀𝑤 ∈ 𝑅 0 ≤ 𝑤)
83	81	simp1d 1142	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝑅 ⊆ ℝ)
84	81	simp2d 1143	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝑅 ≠ ∅)
85		0re 11176	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 0 ∈ ℝ
86		breq1 5110	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 = 0 → (𝑥 ≤ 𝑤 ↔ 0 ≤ 𝑤))
87	86	ralbidv 3156	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 = 0 → (∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ↔ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤))
88	87	rspcev 3588	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((0 ∈ ℝ ∧ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤) → ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤)
89	85, 82, 88	sylancr 587	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤)
90	85	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 0 ∈ ℝ)
91		infregelb 12167	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤) ∧ 0 ∈ ℝ) → (0 ≤ inf(𝑅, ℝ, < ) ↔ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤))
92	83, 84, 89, 90, 91	syl31anc 1375	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (0 ≤ inf(𝑅, ℝ, < ) ↔ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤))
93	82, 92	mpbird 257	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 0 ≤ inf(𝑅, ℝ, < ))
94	93, 10	breqtrrdi 5149	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 0 ≤ 𝑆)
95		metge0 24233	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → 0 ≤ (𝐴𝐷𝑃))
96	29, 7, 17, 95	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 0 ≤ (𝐴𝐷𝑃))
97	31, 33, 96, 94	addge0d 11754	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 0 ≤ ((𝐴𝐷𝑃) + 𝑆))
98		divge0 12052	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐴𝐷𝑃) + 𝑆) ∈ ℝ ∧ 0 ≤ ((𝐴𝐷𝑃) + 𝑆)) ∧ (2 ∈ ℝ ∧ 0 < 2)) → 0 ≤ (((𝐴𝐷𝑃) + 𝑆) / 2))
99	64, 97, 77, 98	syl21anc 837	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 0 ≤ (((𝐴𝐷𝑃) + 𝑆) / 2))
100	33, 65, 94, 99	lt2sqd 14221	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑆 < (((𝐴𝐷𝑃) + 𝑆) / 2) ↔ (𝑆↑2) < ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2)))
101	67, 66	posdifd 11765	. . . . . . . . . . . . . . . . . . . . . 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 12992	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈ ℝ⁺)
105	63, 104	eqeltrid 2832	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝑇 ∈ ℝ⁺)
106	5	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝑌 ∈ (LSubSp‘𝑈))
107		rabexg 5292	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑌 ∈ (LSubSp‘𝑈) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ∈ V)
108	106, 107	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ∈ V)
109		eqid 2729	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑟 ∈ ℝ⁺ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}) = (𝑟 ∈ ℝ⁺ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)})
110		oveq2 7395	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑟 = 𝑇 → ((𝑆↑2) + 𝑟) = ((𝑆↑2) + 𝑇))
111	110	breq2d 5119	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑟 = 𝑇 → (((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟) ↔ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)))
112	111	rabbidv 3413	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑟 = 𝑇 → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)} = {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)})
113	109, 112	elrnmpt1s 5923	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑇 ∈ ℝ⁺ ∧ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ∈ V) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ∈ ran (𝑟 ∈ ℝ⁺ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}))
114	105, 108, 113	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ∈ ran (𝑟 ∈ ℝ⁺ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}))
115	114, 12	eleqtrrdi 2839	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ∈ 𝐹)
116	62, 115	sseldd 3947	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ∈ (𝑋filGen𝐹))
117		ssrab2 4043	. . . . . . . . . . . . . . . 16 ⊢ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ⊆ 𝑋
118	117	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ⊆ 𝑋)
119	63	oveq2i 7398	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑆↑2) + 𝑇) = ((𝑆↑2) + (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2)))
120	67	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → (𝑆↑2) ∈ ℝ)
121	120	recnd 11202	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → (𝑆↑2) ∈ ℂ)
122	65	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → (((𝐴𝐷𝑃) + 𝑆) / 2) ∈ ℝ)
123	122	resqcld 14090	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) ∈ ℝ)
124	123	recnd 11202	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) ∈ ℂ)
125	121, 124	pncan3d 11536	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → ((𝑆↑2) + (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2))) = ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2))
126	119, 125	eqtrid 2776	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → ((𝑆↑2) + 𝑇) = ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2))
127	126	breq2d 5119	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → (((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇) ↔ ((𝐴𝐷𝑦)↑2) ≤ ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2)))
128	29	ad2antrr 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → 𝐷 ∈ (Met‘𝑋))
129	7	ad2antrr 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → 𝐴 ∈ 𝑋)
130	43	adantlr 715	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝑋)
131		metcl 24220	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐴𝐷𝑦) ∈ ℝ)
132	128, 129, 130, 131	syl3anc 1373	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → (𝐴𝐷𝑦) ∈ ℝ)
133		metge0 24233	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → 0 ≤ (𝐴𝐷𝑦))
134	128, 129, 130, 133	syl3anc 1373	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → 0 ≤ (𝐴𝐷𝑦))
135	99	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → 0 ≤ (((𝐴𝐷𝑃) + 𝑆) / 2))
136	132, 122, 134, 135	le2sqd 14222	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → ((𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2) ↔ ((𝐴𝐷𝑦)↑2) ≤ ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2)))
137	127, 136	bitr4d 282	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → (((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇) ↔ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)))
138	137	rabbidva 3412	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} = {𝑦 ∈ 𝑌 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)})
139	42	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝑌 ⊆ 𝑋)
140		rabss2 4041	. . . . . . . . . . . . . . . . 17 ⊢ (𝑌 ⊆ 𝑋 → {𝑦 ∈ 𝑌 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ⊆ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)})
141	139, 140	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑌 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ⊆ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)})
142	138, 141	eqsstrd 3981	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ⊆ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)})
143		filss 23740	. . . . . . . . . . . . . . 15 ⊢ (((𝑋filGen𝐹) ∈ (Fil‘𝑋) ∧ ({𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ∈ (𝑋filGen𝐹) ∧ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ⊆ 𝑋 ∧ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ⊆ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)})) → {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ∈ (𝑋filGen𝐹))
144	60, 116, 118, 142, 143	syl13anc 1374	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ∈ (𝑋filGen𝐹))
145		flimclsi 23865	. . . . . . . . . . . . . 14 ⊢ ({𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ∈ (𝑋filGen𝐹) → (𝐽 fLim (𝑋filGen𝐹)) ⊆ ((cls‘𝐽)‘{𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)}))
146	144, 145	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (𝐽 fLim (𝑋filGen𝐹)) ⊆ ((cls‘𝐽)‘{𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)}))
147	14	elin1d 4167	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑃 ∈ (𝐽 fLim (𝑋filGen𝐹)))
148	147	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝑃 ∈ (𝐽 fLim (𝑋filGen𝐹)))
149	146, 148	sseldd 3947	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝑃 ∈ ((cls‘𝐽)‘{𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)}))
150		ngpxms 24489	. . . . . . . . . . . . . . . . 17 ⊢ (𝑈 ∈ NrmGrp → 𝑈 ∈ ∞MetSp)
151	1, 11	xmsxmet 24344	. . . . . . . . . . . . . . . . 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 11224	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (((𝐴𝐷𝑃) + 𝑆) / 2) ∈ ℝ^*)
157		eqid 2729	. . . . . . . . . . . . . . . 16 ⊢ (MetOpen‘𝐷) = (MetOpen‘𝐷)
158		eqid 2729	. . . . . . . . . . . . . . . 16 ⊢ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} = {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)}
159	157, 158	blcld 24393	. . . . . . . . . . . . . . 15 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ (((𝐴𝐷𝑃) + 𝑆) / 2) ∈ ℝ^*) → {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ∈ (Clsd‘(MetOpen‘𝐷)))
160	153, 154, 156, 159	syl3anc 1373	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ∈ (Clsd‘(MetOpen‘𝐷)))
161	8, 1, 11	xmstopn 24339	. . . . . . . . . . . . . . . . 17 ⊢ (𝑈 ∈ ∞MetSp → 𝐽 = (MetOpen‘𝐷))
162	21, 150, 161	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐽 = (MetOpen‘𝐷))
163	162	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝐽 = (MetOpen‘𝐷))
164	163	fveq2d 6862	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (Clsd‘𝐽) = (Clsd‘(MetOpen‘𝐷)))
165	160, 164	eleqtrrd 2831	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ∈ (Clsd‘𝐽))
166		cldcls 22929	. . . . . . . . . . . . 13 ⊢ ({𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ∈ (Clsd‘𝐽) → ((cls‘𝐽)‘{𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)}) = {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)})
167	165, 166	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → ((cls‘𝐽)‘{𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)}) = {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)})
168	149, 167	eleqtrd 2830	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝑃 ∈ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)})
169		oveq2 7395	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑃 → (𝐴𝐷𝑦) = (𝐴𝐷𝑃))
170	169	breq1d 5117	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑃 → ((𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2) ↔ (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)))
171	170	elrab 3659	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ↔ (𝑃 ∈ 𝑋 ∧ (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)))
172	171	simprbi 496	. . . . . . . . . . 11 ⊢ (𝑃 ∈ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} → (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2))
173	168, 172	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2))
174	31, 33, 31	leadd2d 11773	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴𝐷𝑃) ≤ 𝑆 ↔ ((𝐴𝐷𝑃) + (𝐴𝐷𝑃)) ≤ ((𝐴𝐷𝑃) + 𝑆)))
175	31	recnd 11202	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴𝐷𝑃) ∈ ℂ)
176	175	2timesd 12425	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 · (𝐴𝐷𝑃)) = ((𝐴𝐷𝑃) + (𝐴𝐷𝑃)))
177	176	breq1d 5117	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · (𝐴𝐷𝑃)) ≤ ((𝐴𝐷𝑃) + 𝑆) ↔ ((𝐴𝐷𝑃) + (𝐴𝐷𝑃)) ≤ ((𝐴𝐷𝑃) + 𝑆)))
178		lemuldiv2 12064	. . . . . . . . . . . . . 14 ⊢ (((𝐴𝐷𝑃) ∈ ℝ ∧ ((𝐴𝐷𝑃) + 𝑆) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · (𝐴𝐷𝑃)) ≤ ((𝐴𝐷𝑃) + 𝑆) ↔ (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)))
179	76, 178	mp3an3 1452	. . . . . . . . . . . . 13 ⊢ (((𝐴𝐷𝑃) ∈ ℝ ∧ ((𝐴𝐷𝑃) + 𝑆) ∈ ℝ) → ((2 · (𝐴𝐷𝑃)) ≤ ((𝐴𝐷𝑃) + 𝑆) ↔ (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)))
180	31, 64, 179	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · (𝐴𝐷𝑃)) ≤ ((𝐴𝐷𝑃) + 𝑆) ↔ (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)))
181	174, 177, 180	3bitr2d 307	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴𝐷𝑃) ≤ 𝑆 ↔ (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)))
182	181	biimpar 477	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)) → (𝐴𝐷𝑃) ≤ 𝑆)
183	173, 182	syldan 591	. . . . . . . . 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 6871	. . . . . . . . 9 ⊢ (𝑁‘(𝐴 − 𝑦)) ∈ V
192		eqid 2729	. . . . . . . . . 10 ⊢ (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦))) = (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))
193	192	elrnmpt1 5924	. . . . . . . . 9 ⊢ ((𝑦 ∈ 𝑌 ∧ (𝑁‘(𝐴 − 𝑦)) ∈ V) → (𝑁‘(𝐴 − 𝑦)) ∈ ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦))))
194	190, 191, 193	sylancl 586	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝑁‘(𝐴 − 𝑦)) ∈ ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦))))
195	194, 9	eleqtrrdi 2839	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝑁‘(𝐴 − 𝑦)) ∈ 𝑅)
196		infrelb 12168	. . . . . . 7 ⊢ ((𝑅 ⊆ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ∧ (𝑁‘(𝐴 − 𝑦)) ∈ 𝑅) → inf(𝑅, ℝ, < ) ≤ (𝑁‘(𝐴 − 𝑦)))
197	188, 189, 195, 196	syl3anc 1373	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → inf(𝑅, ℝ, < ) ≤ (𝑁‘(𝐴 − 𝑦)))
198	10, 197	eqbrtrid 5142	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑆 ≤ (𝑁‘(𝐴 − 𝑦)))
199	32, 34, 47, 187, 198	letrd 11331	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝐴𝐷𝑃) ≤ (𝑁‘(𝐴 − 𝑦)))
200	26, 199	eqbrtrrd 5131	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝑁‘(𝐴 − 𝑃)) ≤ (𝑁‘(𝐴 − 𝑦)))
201	200	ralrimiva 3125	. 2 ⊢ (𝜑 → ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑃)) ≤ (𝑁‘(𝐴 − 𝑦)))
202		oveq2 7395	. . . . . 6 ⊢ (𝑥 = 𝑃 → (𝐴 − 𝑥) = (𝐴 − 𝑃))
203	202	fveq2d 6862	. . . . 5 ⊢ (𝑥 = 𝑃 → (𝑁‘(𝐴 − 𝑥)) = (𝑁‘(𝐴 − 𝑃)))
204	203	breq1d 5117	. . . 4 ⊢ (𝑥 = 𝑃 → ((𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)) ↔ (𝑁‘(𝐴 − 𝑃)) ≤ (𝑁‘(𝐴 − 𝑦))))
205	204	ralbidv 3156	. . 3 ⊢ (𝑥 = 𝑃 → (∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)) ↔ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑃)) ≤ (𝑁‘(𝐴 − 𝑦))))
206	205	rspcev 3588	. 2 ⊢ ((𝑃 ∈ 𝑌 ∧ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑃)) ≤ (𝑁‘(𝐴 − 𝑦))) → ∃𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))
207	15, 201, 206	syl2anc 584	1 ⊢ (𝜑 → ∃𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 ∈ wcel 2109 ≠ wne 2925 ∀wral 3044 ∃wrex 3053 {crab 3405 Vcvv 3447 ⊆ wss 3914 ∅c0 4296 𝒫 cpw 4563 ∪ cuni 4871 class class class wbr 5107 ↦ cmpt 5188 × cxp 5636 ran crn 5639 ↾ cres 5640 ‘cfv 6511 (class class class)co 7387 infcinf 9392 ℝcr 11067 0cc0 11068 + caddc 11071 · cmul 11073 ℝ^*cxr 11207 < clt 11208 ≤ cle 11209 − cmin 11405 / cdiv 11835 2c2 12241 ℝ⁺crp 12951 ↑cexp 14026 Basecbs 17179 ↾_s cress 17200 distcds 17229 TopOpenctopn 17384 -_gcsg 18867 LModclmod 20766 LSubSpclss 20837 ∞Metcxmet 21249 Metcmet 21250 fBascfbas 21252 filGencfg 21253 MetOpencmopn 21254 Clsdccld 22903 clsccl 22905 Filcfil 23732 fLim cflim 23821 ∞MetSpcxms 24205 MetSpcms 24206 normcnm 24464 NrmGrpcngp 24465 ℂPreHilccph 25066 CMetSpccms 25232

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5234 ax-sep 5251 ax-nul 5261 ax-pow 5320 ax-pr 5387 ax-un 7711 ax-cnex 11124 ax-resscn 11125 ax-1cn 11126 ax-icn 11127 ax-addcl 11128 ax-addrcl 11129 ax-mulcl 11130 ax-mulrcl 11131 ax-mulcom 11132 ax-addass 11133 ax-mulass 11134 ax-distr 11135 ax-i2m1 11136 ax-1ne0 11137 ax-1rid 11138 ax-rnegex 11139 ax-rrecex 11140 ax-cnre 11141 ax-pre-lttri 11142 ax-pre-lttrn 11143 ax-pre-ltadd 11144 ax-pre-mulgt0 11145 ax-pre-sup 11146 ax-addf 11147 ax-mulf 11148

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3354 df-reu 3355 df-rab 3406 df-v 3449 df-sbc 3754 df-csb 3863 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-pss 3934 df-nul 4297 df-if 4489 df-pw 4565 df-sn 4590 df-pr 4592 df-tp 4594 df-op 4596 df-uni 4872 df-int 4911 df-iun 4957 df-iin 4958 df-br 5108 df-opab 5170 df-mpt 5189 df-tr 5215 df-id 5533 df-eprel 5538 df-po 5546 df-so 5547 df-fr 5591 df-we 5593 df-xp 5644 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-rn 5649 df-res 5650 df-ima 5651 df-pred 6274 df-ord 6335 df-on 6336 df-lim 6337 df-suc 6338 df-iota 6464 df-fun 6513 df-fn 6514 df-f 6515 df-f1 6516 df-fo 6517 df-f1o 6518 df-fv 6519 df-riota 7344 df-ov 7390 df-oprab 7391 df-mpo 7392 df-om 7843 df-1st 7968 df-2nd 7969 df-tpos 8205 df-frecs 8260 df-wrecs 8291 df-recs 8340 df-rdg 8378 df-1o 8434 df-er 8671 df-map 8801 df-en 8919 df-dom 8920 df-sdom 8921 df-fin 8922 df-fi 9362 df-sup 9393 df-inf 9394 df-pnf 11210 df-mnf 11211 df-xr 11212 df-ltxr 11213 df-le 11214 df-sub 11407 df-neg 11408 df-div 11836 df-nn 12187 df-2 12249 df-3 12250 df-4 12251 df-5 12252 df-6 12253 df-7 12254 df-8 12255 df-9 12256 df-n0 12443 df-z 12530 df-dec 12650 df-uz 12794 df-q 12908 df-rp 12952 df-xneg 13072 df-xadd 13073 df-xmul 13074 df-ico 13312 df-icc 13313 df-fz 13469 df-seq 13967 df-exp 14027 df-cj 15065 df-re 15066 df-im 15067 df-sqrt 15201 df-abs 15202 df-struct 17117 df-sets 17134 df-slot 17152 df-ndx 17164 df-base 17180 df-ress 17201 df-plusg 17233 df-mulr 17234 df-starv 17235 df-sca 17236 df-vsca 17237 df-ip 17238 df-tset 17239 df-ple 17240 df-ds 17242 df-unif 17243 df-rest 17385 df-0g 17404 df-topgen 17406 df-mgm 18567 df-sgrp 18646 df-mnd 18662 df-mhm 18710 df-grp 18868 df-minusg 18869 df-sbg 18870 df-mulg 19000 df-subg 19055 df-ghm 19145 df-cmn 19712 df-abl 19713 df-mgp 20050 df-rng 20062 df-ur 20091 df-ring 20144 df-cring 20145 df-oppr 20246 df-dvdsr 20266 df-unit 20267 df-invr 20297 df-dvr 20310 df-rhm 20381 df-subrg 20479 df-drng 20640 df-staf 20748 df-srng 20749 df-lmod 20768 df-lss 20838 df-lmhm 20929 df-lvec 21010 df-sra 21080 df-rgmod 21081 df-psmet 21256 df-xmet 21257 df-met 21258 df-bl 21259 df-mopn 21260 df-fbas 21261 df-fg 21262 df-cnfld 21265 df-phl 21535 df-top 22781 df-topon 22798 df-topsp 22820 df-bases 22833 df-cld 22906 df-ntr 22907 df-cls 22908 df-nei 22985 df-haus 23202 df-fil 23733 df-flim 23826 df-xms 24208 df-ms 24209 df-nm 24470 df-ngp 24471 df-nlm 24474 df-clm 24963 df-cph 25068 df-cfil 25155 df-cmet 25157 df-cms 25235

This theorem is referenced by: minveclem5 25333

W3C validator