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 23960 |
. . 3
⊢ (𝜑 → 𝑃 ∈ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌)) |
15 | 14 | elin2d 4173 |
. 2
⊢ (𝜑 → 𝑃 ∈ 𝑌) |
16 | 11 | oveqi 7158 |
. . . . . . 7
⊢ (𝐴𝐷𝑃) = (𝐴((dist‘𝑈) ↾ (𝑋 × 𝑋))𝑃) |
17 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13 | minveclem4b 23961 |
. . . . . . . 8
⊢ (𝜑 → 𝑃 ∈ 𝑋) |
18 | 7, 17 | ovresd 7304 |
. . . . . . 7
⊢ (𝜑 → (𝐴((dist‘𝑈) ↾ (𝑋 × 𝑋))𝑃) = (𝐴(dist‘𝑈)𝑃)) |
19 | 16, 18 | syl5eq 2865 |
. . . . . 6
⊢ (𝜑 → (𝐴𝐷𝑃) = (𝐴(dist‘𝑈)𝑃)) |
20 | | cphngp 23704 |
. . . . . . . 8
⊢ (𝑈 ∈ ℂPreHil →
𝑈 ∈
NrmGrp) |
21 | 4, 20 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑈 ∈ NrmGrp) |
22 | | eqid 2818 |
. . . . . . . 8
⊢
(dist‘𝑈) =
(dist‘𝑈) |
23 | 3, 1, 2, 22 | ngpds 23140 |
. . . . . . 7
⊢ ((𝑈 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝐴(dist‘𝑈)𝑃) = (𝑁‘(𝐴 − 𝑃))) |
24 | 21, 7, 17, 23 | syl3anc 1363 |
. . . . . 6
⊢ (𝜑 → (𝐴(dist‘𝑈)𝑃) = (𝑁‘(𝐴 − 𝑃))) |
25 | 19, 24 | eqtrd 2853 |
. . . . 5
⊢ (𝜑 → (𝐴𝐷𝑃) = (𝑁‘(𝐴 − 𝑃))) |
26 | 25 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝐴𝐷𝑃) = (𝑁‘(𝐴 − 𝑃))) |
27 | | ngpms 23136 |
. . . . . . . 8
⊢ (𝑈 ∈ NrmGrp → 𝑈 ∈ MetSp) |
28 | 1, 11 | msmet 22994 |
. . . . . . . 8
⊢ (𝑈 ∈ MetSp → 𝐷 ∈ (Met‘𝑋)) |
29 | 21, 27, 28 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) |
30 | | metcl 22869 |
. . . . . . 7
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝐴𝐷𝑃) ∈ ℝ) |
31 | 29, 7, 17, 30 | syl3anc 1363 |
. . . . . 6
⊢ (𝜑 → (𝐴𝐷𝑃) ∈ ℝ) |
32 | 31 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝐴𝐷𝑃) ∈ ℝ) |
33 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | minveclem4c 23955 |
. . . . . 6
⊢ (𝜑 → 𝑆 ∈ ℝ) |
34 | 33 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑆 ∈ ℝ) |
35 | 21 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑈 ∈ NrmGrp) |
36 | | cphlmod 23705 |
. . . . . . . . 9
⊢ (𝑈 ∈ ℂPreHil →
𝑈 ∈
LMod) |
37 | 4, 36 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑈 ∈ LMod) |
38 | 37 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑈 ∈ LMod) |
39 | 7 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝐴 ∈ 𝑋) |
40 | | eqid 2818 |
. . . . . . . . . 10
⊢
(LSubSp‘𝑈) =
(LSubSp‘𝑈) |
41 | 1, 40 | lssss 19637 |
. . . . . . . . 9
⊢ (𝑌 ∈ (LSubSp‘𝑈) → 𝑌 ⊆ 𝑋) |
42 | 5, 41 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ⊆ 𝑋) |
43 | 42 | sselda 3964 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝑋) |
44 | 1, 2 | lmodvsubcl 19608 |
. . . . . . 7
⊢ ((𝑈 ∈ LMod ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐴 − 𝑦) ∈ 𝑋) |
45 | 38, 39, 43, 44 | syl3anc 1363 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝐴 − 𝑦) ∈ 𝑋) |
46 | 1, 3 | nmcl 23152 |
. . . . . 6
⊢ ((𝑈 ∈ NrmGrp ∧ (𝐴 − 𝑦) ∈ 𝑋) → (𝑁‘(𝐴 − 𝑦)) ∈ ℝ) |
47 | 35, 45, 46 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝑁‘(𝐴 − 𝑦)) ∈ ℝ) |
48 | 33, 31 | ltnled 10775 |
. . . . . . . 8
⊢ (𝜑 → (𝑆 < (𝐴𝐷𝑃) ↔ ¬ (𝐴𝐷𝑃) ≤ 𝑆)) |
49 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12 | minveclem3b 23958 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐹 ∈ (fBas‘𝑌)) |
50 | | fbsspw 22368 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐹 ∈ (fBas‘𝑌) → 𝐹 ⊆ 𝒫 𝑌) |
51 | 49, 50 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐹 ⊆ 𝒫 𝑌) |
52 | | sspwb 5332 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑌 ⊆ 𝑋 ↔ 𝒫 𝑌 ⊆ 𝒫 𝑋) |
53 | 42, 52 | sylib 219 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝒫 𝑌 ⊆ 𝒫 𝑋) |
54 | 51, 53 | sstrd 3974 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐹 ⊆ 𝒫 𝑋) |
55 | 1 | fvexi 6677 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑋 ∈ V |
56 | 55 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑋 ∈ V) |
57 | | fbasweak 22401 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹 ∈ (fBas‘𝑌) ∧ 𝐹 ⊆ 𝒫 𝑋 ∧ 𝑋 ∈ V) → 𝐹 ∈ (fBas‘𝑋)) |
58 | 49, 54, 56, 57 | syl3anc 1363 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐹 ∈ (fBas‘𝑋)) |
59 | 58 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝐹 ∈ (fBas‘𝑋)) |
60 | | fgcl 22414 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ (fBas‘𝑋) → (𝑋filGen𝐹) ∈ (Fil‘𝑋)) |
61 | 59, 60 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (𝑋filGen𝐹) ∈ (Fil‘𝑋)) |
62 | | ssfg 22408 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∈ (fBas‘𝑋) → 𝐹 ⊆ (𝑋filGen𝐹)) |
63 | 59, 62 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝐹 ⊆ (𝑋filGen𝐹)) |
64 | | minvec.t |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑇 = (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2)) |
65 | 31, 33 | readdcld 10658 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → ((𝐴𝐷𝑃) + 𝑆) ∈ ℝ) |
66 | 65 | rehalfcld 11872 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (((𝐴𝐷𝑃) + 𝑆) / 2) ∈ ℝ) |
67 | 66 | resqcld 13599 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) ∈
ℝ) |
68 | 33 | resqcld 13599 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑆↑2) ∈ ℝ) |
69 | 67, 68 | resubcld 11056 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈ ℝ) |
70 | 69 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈ ℝ) |
71 | 33, 31, 33 | ltadd1d 11221 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝑆 < (𝐴𝐷𝑃) ↔ (𝑆 + 𝑆) < ((𝐴𝐷𝑃) + 𝑆))) |
72 | 33 | recnd 10657 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 𝑆 ∈ ℂ) |
73 | 72 | 2timesd 11868 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (2 · 𝑆) = (𝑆 + 𝑆)) |
74 | 73 | breq1d 5067 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ((2 · 𝑆) < ((𝐴𝐷𝑃) + 𝑆) ↔ (𝑆 + 𝑆) < ((𝐴𝐷𝑃) + 𝑆))) |
75 | | 2re 11699 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 2 ∈
ℝ |
76 | | 2pos 11728 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 0 <
2 |
77 | 75, 76 | pm3.2i 471 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (2 ∈
ℝ ∧ 0 < 2) |
78 | 77 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (2 ∈ ℝ ∧ 0
< 2)) |
79 | | ltmuldiv2 11502 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑆 ∈ ℝ ∧ ((𝐴𝐷𝑃) + 𝑆) ∈ ℝ ∧ (2 ∈ ℝ
∧ 0 < 2)) → ((2 · 𝑆) < ((𝐴𝐷𝑃) + 𝑆) ↔ 𝑆 < (((𝐴𝐷𝑃) + 𝑆) / 2))) |
80 | 33, 65, 78, 79 | syl3anc 1363 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ((2 · 𝑆) < ((𝐴𝐷𝑃) + 𝑆) ↔ 𝑆 < (((𝐴𝐷𝑃) + 𝑆) / 2))) |
81 | 71, 74, 80 | 3bitr2d 308 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑆 < (𝐴𝐷𝑃) ↔ 𝑆 < (((𝐴𝐷𝑃) + 𝑆) / 2))) |
82 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | minveclem1 23954 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤)) |
83 | 82 | simp3d 1136 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → ∀𝑤 ∈ 𝑅 0 ≤ 𝑤) |
84 | 82 | simp1d 1134 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → 𝑅 ⊆ ℝ) |
85 | 82 | simp2d 1135 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → 𝑅 ≠ ∅) |
86 | | 0re 10631 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 0 ∈
ℝ |
87 | | breq1 5060 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑥 = 0 → (𝑥 ≤ 𝑤 ↔ 0 ≤ 𝑤)) |
88 | 87 | ralbidv 3194 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑥 = 0 → (∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ↔ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤)) |
89 | 88 | rspcev 3620 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((0
∈ ℝ ∧ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤) → ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤) |
90 | 86, 83, 89 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤) |
91 | 86 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → 0 ∈
ℝ) |
92 | | infregelb 11613 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤) ∧ 0 ∈ ℝ) → (0 ≤
inf(𝑅, ℝ, < )
↔ ∀𝑤 ∈
𝑅 0 ≤ 𝑤)) |
93 | 84, 85, 90, 91, 92 | syl31anc 1365 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (0 ≤ inf(𝑅, ℝ, < ) ↔
∀𝑤 ∈ 𝑅 0 ≤ 𝑤)) |
94 | 83, 93 | mpbird 258 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 0 ≤ inf(𝑅, ℝ, <
)) |
95 | 94, 10 | breqtrrdi 5099 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 0 ≤ 𝑆) |
96 | | metge0 22882 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → 0 ≤ (𝐴𝐷𝑃)) |
97 | 29, 7, 17, 96 | syl3anc 1363 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 0 ≤ (𝐴𝐷𝑃)) |
98 | 31, 33, 97, 95 | addge0d 11204 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 0 ≤ ((𝐴𝐷𝑃) + 𝑆)) |
99 | | divge0 11497 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝐴𝐷𝑃) + 𝑆) ∈ ℝ ∧ 0 ≤ ((𝐴𝐷𝑃) + 𝑆)) ∧ (2 ∈ ℝ ∧ 0 < 2))
→ 0 ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)) |
100 | 65, 98, 78, 99 | syl21anc 833 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 0 ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)) |
101 | 33, 66, 95, 100 | lt2sqd 13607 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑆 < (((𝐴𝐷𝑃) + 𝑆) / 2) ↔ (𝑆↑2) < ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2))) |
102 | 68, 67 | posdifd 11215 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((𝑆↑2) < ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) ↔ 0 < (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2)))) |
103 | 81, 101, 102 | 3bitrd 306 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑆 < (𝐴𝐷𝑃) ↔ 0 < (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2)))) |
104 | 103 | biimpa 477 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 0 < (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2))) |
105 | 70, 104 | elrpd 12416 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈
ℝ+) |
106 | 64, 105 | eqeltrid 2914 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝑇 ∈
ℝ+) |
107 | 5 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝑌 ∈ (LSubSp‘𝑈)) |
108 | | rabexg 5225 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑌 ∈ (LSubSp‘𝑈) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ∈ V) |
109 | 107, 108 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ∈ V) |
110 | | eqid 2818 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑟 ∈ ℝ+
↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}) = (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}) |
111 | | oveq2 7153 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑟 = 𝑇 → ((𝑆↑2) + 𝑟) = ((𝑆↑2) + 𝑇)) |
112 | 111 | breq2d 5069 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑟 = 𝑇 → (((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟) ↔ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇))) |
113 | 112 | rabbidv 3478 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑟 = 𝑇 → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)} = {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)}) |
114 | 110, 113 | elrnmpt1s 5822 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑇 ∈ ℝ+
∧ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ∈ V) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ∈ ran (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)})) |
115 | 106, 109,
114 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ∈ ran (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)})) |
116 | 115, 12 | eleqtrrdi 2921 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ∈ 𝐹) |
117 | 63, 116 | sseldd 3965 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ∈ (𝑋filGen𝐹)) |
118 | | ssrab2 4053 |
. . . . . . . . . . . . . . . 16
⊢ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ⊆ 𝑋 |
119 | 118 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ⊆ 𝑋) |
120 | 64 | oveq2i 7156 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑆↑2) + 𝑇) = ((𝑆↑2) + (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2))) |
121 | 68 | ad2antrr 722 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → (𝑆↑2) ∈ ℝ) |
122 | 121 | recnd 10657 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → (𝑆↑2) ∈ ℂ) |
123 | 66 | ad2antrr 722 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → (((𝐴𝐷𝑃) + 𝑆) / 2) ∈ ℝ) |
124 | 123 | resqcld 13599 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) ∈
ℝ) |
125 | 124 | recnd 10657 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) ∈
ℂ) |
126 | 122, 125 | pncan3d 10988 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → ((𝑆↑2) + (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2))) = ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2)) |
127 | 120, 126 | syl5eq 2865 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → ((𝑆↑2) + 𝑇) = ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2)) |
128 | 127 | breq2d 5069 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → (((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇) ↔ ((𝐴𝐷𝑦)↑2) ≤ ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2))) |
129 | 29 | ad2antrr 722 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → 𝐷 ∈ (Met‘𝑋)) |
130 | 7 | ad2antrr 722 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → 𝐴 ∈ 𝑋) |
131 | 43 | adantlr 711 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝑋) |
132 | | metcl 22869 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐴𝐷𝑦) ∈ ℝ) |
133 | 129, 130,
131, 132 | syl3anc 1363 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → (𝐴𝐷𝑦) ∈ ℝ) |
134 | | metge0 22882 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → 0 ≤ (𝐴𝐷𝑦)) |
135 | 129, 130,
131, 134 | syl3anc 1363 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → 0 ≤ (𝐴𝐷𝑦)) |
136 | 100 | ad2antrr 722 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → 0 ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)) |
137 | 133, 123,
135, 136 | le2sqd 13608 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → ((𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2) ↔ ((𝐴𝐷𝑦)↑2) ≤ ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2))) |
138 | 128, 137 | bitr4d 283 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → (((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇) ↔ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2))) |
139 | 138 | rabbidva 3476 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} = {𝑦 ∈ 𝑌 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)}) |
140 | 42 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝑌 ⊆ 𝑋) |
141 | | rabss2 4051 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑌 ⊆ 𝑋 → {𝑦 ∈ 𝑌 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ⊆ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)}) |
142 | 140, 141 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑌 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ⊆ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)}) |
143 | 139, 142 | eqsstrd 4002 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ⊆ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)}) |
144 | | filss 22389 |
. . . . . . . . . . . . . . 15
⊢ (((𝑋filGen𝐹) ∈ (Fil‘𝑋) ∧ ({𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ∈ (𝑋filGen𝐹) ∧ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ⊆ 𝑋 ∧ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ⊆ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)})) → {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ∈ (𝑋filGen𝐹)) |
145 | 61, 117, 119, 143, 144 | syl13anc 1364 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ∈ (𝑋filGen𝐹)) |
146 | | flimclsi 22514 |
. . . . . . . . . . . . . 14
⊢ ({𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ∈ (𝑋filGen𝐹) → (𝐽 fLim (𝑋filGen𝐹)) ⊆ ((cls‘𝐽)‘{𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)})) |
147 | 145, 146 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (𝐽 fLim (𝑋filGen𝐹)) ⊆ ((cls‘𝐽)‘{𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)})) |
148 | 14 | elin1d 4172 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑃 ∈ (𝐽 fLim (𝑋filGen𝐹))) |
149 | 148 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝑃 ∈ (𝐽 fLim (𝑋filGen𝐹))) |
150 | 147, 149 | sseldd 3965 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝑃 ∈ ((cls‘𝐽)‘{𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)})) |
151 | | ngpxms 23137 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑈 ∈ NrmGrp → 𝑈 ∈
∞MetSp) |
152 | 1, 11 | xmsxmet 22993 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑈 ∈ ∞MetSp →
𝐷 ∈
(∞Met‘𝑋)) |
153 | 21, 151, 152 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) |
154 | 153 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝐷 ∈ (∞Met‘𝑋)) |
155 | 7 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝐴 ∈ 𝑋) |
156 | 66 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (((𝐴𝐷𝑃) + 𝑆) / 2) ∈ ℝ) |
157 | 156 | rexrd 10679 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (((𝐴𝐷𝑃) + 𝑆) / 2) ∈
ℝ*) |
158 | | eqid 2818 |
. . . . . . . . . . . . . . . 16
⊢
(MetOpen‘𝐷) =
(MetOpen‘𝐷) |
159 | | eqid 2818 |
. . . . . . . . . . . . . . . 16
⊢ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} = {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} |
160 | 158, 159 | blcld 23042 |
. . . . . . . . . . . . . . 15
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ (((𝐴𝐷𝑃) + 𝑆) / 2) ∈ ℝ*) →
{𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ∈
(Clsd‘(MetOpen‘𝐷))) |
161 | 154, 155,
157, 160 | syl3anc 1363 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ∈
(Clsd‘(MetOpen‘𝐷))) |
162 | 8, 1, 11 | xmstopn 22988 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑈 ∈ ∞MetSp →
𝐽 = (MetOpen‘𝐷)) |
163 | 21, 151, 162 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐽 = (MetOpen‘𝐷)) |
164 | 163 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝐽 = (MetOpen‘𝐷)) |
165 | 164 | fveq2d 6667 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (Clsd‘𝐽) = (Clsd‘(MetOpen‘𝐷))) |
166 | 161, 165 | eleqtrrd 2913 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ∈ (Clsd‘𝐽)) |
167 | | cldcls 21578 |
. . . . . . . . . . . . 13
⊢ ({𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ∈ (Clsd‘𝐽) → ((cls‘𝐽)‘{𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)}) = {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)}) |
168 | 166, 167 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → ((cls‘𝐽)‘{𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)}) = {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)}) |
169 | 150, 168 | eleqtrd 2912 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝑃 ∈ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)}) |
170 | | oveq2 7153 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑃 → (𝐴𝐷𝑦) = (𝐴𝐷𝑃)) |
171 | 170 | breq1d 5067 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑃 → ((𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2) ↔ (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2))) |
172 | 171 | elrab 3677 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ↔ (𝑃 ∈ 𝑋 ∧ (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2))) |
173 | 172 | simprbi 497 |
. . . . . . . . . . 11
⊢ (𝑃 ∈ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} → (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)) |
174 | 169, 173 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)) |
175 | 31, 33, 31 | leadd2d 11223 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐴𝐷𝑃) ≤ 𝑆 ↔ ((𝐴𝐷𝑃) + (𝐴𝐷𝑃)) ≤ ((𝐴𝐷𝑃) + 𝑆))) |
176 | 31 | recnd 10657 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴𝐷𝑃) ∈ ℂ) |
177 | 176 | 2timesd 11868 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (2 · (𝐴𝐷𝑃)) = ((𝐴𝐷𝑃) + (𝐴𝐷𝑃))) |
178 | 177 | breq1d 5067 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((2 · (𝐴𝐷𝑃)) ≤ ((𝐴𝐷𝑃) + 𝑆) ↔ ((𝐴𝐷𝑃) + (𝐴𝐷𝑃)) ≤ ((𝐴𝐷𝑃) + 𝑆))) |
179 | | lemuldiv2 11509 |
. . . . . . . . . . . . . 14
⊢ (((𝐴𝐷𝑃) ∈ ℝ ∧ ((𝐴𝐷𝑃) + 𝑆) ∈ ℝ ∧ (2 ∈ ℝ
∧ 0 < 2)) → ((2 · (𝐴𝐷𝑃)) ≤ ((𝐴𝐷𝑃) + 𝑆) ↔ (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2))) |
180 | 77, 179 | mp3an3 1441 |
. . . . . . . . . . . . 13
⊢ (((𝐴𝐷𝑃) ∈ ℝ ∧ ((𝐴𝐷𝑃) + 𝑆) ∈ ℝ) → ((2 · (𝐴𝐷𝑃)) ≤ ((𝐴𝐷𝑃) + 𝑆) ↔ (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2))) |
181 | 31, 65, 180 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((2 · (𝐴𝐷𝑃)) ≤ ((𝐴𝐷𝑃) + 𝑆) ↔ (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2))) |
182 | 175, 178,
181 | 3bitr2d 308 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐴𝐷𝑃) ≤ 𝑆 ↔ (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2))) |
183 | 182 | biimpar 478 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)) → (𝐴𝐷𝑃) ≤ 𝑆) |
184 | 174, 183 | syldan 591 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (𝐴𝐷𝑃) ≤ 𝑆) |
185 | 184 | ex 413 |
. . . . . . . 8
⊢ (𝜑 → (𝑆 < (𝐴𝐷𝑃) → (𝐴𝐷𝑃) ≤ 𝑆)) |
186 | 48, 185 | sylbird 261 |
. . . . . . 7
⊢ (𝜑 → (¬ (𝐴𝐷𝑃) ≤ 𝑆 → (𝐴𝐷𝑃) ≤ 𝑆)) |
187 | 186 | pm2.18d 127 |
. . . . . 6
⊢ (𝜑 → (𝐴𝐷𝑃) ≤ 𝑆) |
188 | 187 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝐴𝐷𝑃) ≤ 𝑆) |
189 | 84 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑅 ⊆ ℝ) |
190 | 90 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤) |
191 | | simpr 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝑌) |
192 | | fvex 6676 |
. . . . . . . . 9
⊢ (𝑁‘(𝐴 − 𝑦)) ∈ V |
193 | | eqid 2818 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦))) = (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦))) |
194 | 193 | elrnmpt1 5823 |
. . . . . . . . 9
⊢ ((𝑦 ∈ 𝑌 ∧ (𝑁‘(𝐴 − 𝑦)) ∈ V) → (𝑁‘(𝐴 − 𝑦)) ∈ ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))) |
195 | 191, 192,
194 | sylancl 586 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝑁‘(𝐴 − 𝑦)) ∈ ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))) |
196 | 195, 9 | eleqtrrdi 2921 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝑁‘(𝐴 − 𝑦)) ∈ 𝑅) |
197 | | infrelb 11614 |
. . . . . . 7
⊢ ((𝑅 ⊆ ℝ ∧
∃𝑥 ∈ ℝ
∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ∧ (𝑁‘(𝐴 − 𝑦)) ∈ 𝑅) → inf(𝑅, ℝ, < ) ≤ (𝑁‘(𝐴 − 𝑦))) |
198 | 189, 190,
196, 197 | syl3anc 1363 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → inf(𝑅, ℝ, < ) ≤ (𝑁‘(𝐴 − 𝑦))) |
199 | 10, 198 | eqbrtrid 5092 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑆 ≤ (𝑁‘(𝐴 − 𝑦))) |
200 | 32, 34, 47, 188, 199 | letrd 10785 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝐴𝐷𝑃) ≤ (𝑁‘(𝐴 − 𝑦))) |
201 | 26, 200 | eqbrtrrd 5081 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝑁‘(𝐴 − 𝑃)) ≤ (𝑁‘(𝐴 − 𝑦))) |
202 | 201 | ralrimiva 3179 |
. 2
⊢ (𝜑 → ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑃)) ≤ (𝑁‘(𝐴 − 𝑦))) |
203 | | oveq2 7153 |
. . . . . 6
⊢ (𝑥 = 𝑃 → (𝐴 − 𝑥) = (𝐴 − 𝑃)) |
204 | 203 | fveq2d 6667 |
. . . . 5
⊢ (𝑥 = 𝑃 → (𝑁‘(𝐴 − 𝑥)) = (𝑁‘(𝐴 − 𝑃))) |
205 | 204 | breq1d 5067 |
. . . 4
⊢ (𝑥 = 𝑃 → ((𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)) ↔ (𝑁‘(𝐴 − 𝑃)) ≤ (𝑁‘(𝐴 − 𝑦)))) |
206 | 205 | ralbidv 3194 |
. . 3
⊢ (𝑥 = 𝑃 → (∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)) ↔ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑃)) ≤ (𝑁‘(𝐴 − 𝑦)))) |
207 | 206 | rspcev 3620 |
. 2
⊢ ((𝑃 ∈ 𝑌 ∧ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑃)) ≤ (𝑁‘(𝐴 − 𝑦))) → ∃𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦))) |
208 | 15, 202, 207 | syl2anc 584 |
1
⊢ (𝜑 → ∃𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦))) |