| 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 25464 |
. . 3
⊢ (𝜑 → 𝑃 ∈ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌)) |
| 15 | 14 | elin2d 4205 |
. 2
⊢ (𝜑 → 𝑃 ∈ 𝑌) |
| 16 | 11 | oveqi 7444 |
. . . . . . 7
⊢ (𝐴𝐷𝑃) = (𝐴((dist‘𝑈) ↾ (𝑋 × 𝑋))𝑃) |
| 17 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13 | minveclem4b 25465 |
. . . . . . . 8
⊢ (𝜑 → 𝑃 ∈ 𝑋) |
| 18 | 7, 17 | ovresd 7600 |
. . . . . . 7
⊢ (𝜑 → (𝐴((dist‘𝑈) ↾ (𝑋 × 𝑋))𝑃) = (𝐴(dist‘𝑈)𝑃)) |
| 19 | 16, 18 | eqtrid 2789 |
. . . . . 6
⊢ (𝜑 → (𝐴𝐷𝑃) = (𝐴(dist‘𝑈)𝑃)) |
| 20 | | cphngp 25207 |
. . . . . . . 8
⊢ (𝑈 ∈ ℂPreHil →
𝑈 ∈
NrmGrp) |
| 21 | 4, 20 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑈 ∈ NrmGrp) |
| 22 | | eqid 2737 |
. . . . . . . 8
⊢
(dist‘𝑈) =
(dist‘𝑈) |
| 23 | 3, 1, 2, 22 | ngpds 24617 |
. . . . . . 7
⊢ ((𝑈 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝐴(dist‘𝑈)𝑃) = (𝑁‘(𝐴 − 𝑃))) |
| 24 | 21, 7, 17, 23 | syl3anc 1373 |
. . . . . 6
⊢ (𝜑 → (𝐴(dist‘𝑈)𝑃) = (𝑁‘(𝐴 − 𝑃))) |
| 25 | 19, 24 | eqtrd 2777 |
. . . . 5
⊢ (𝜑 → (𝐴𝐷𝑃) = (𝑁‘(𝐴 − 𝑃))) |
| 26 | 25 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝐴𝐷𝑃) = (𝑁‘(𝐴 − 𝑃))) |
| 27 | | ngpms 24613 |
. . . . . . . 8
⊢ (𝑈 ∈ NrmGrp → 𝑈 ∈ MetSp) |
| 28 | 1, 11 | msmet 24467 |
. . . . . . . 8
⊢ (𝑈 ∈ MetSp → 𝐷 ∈ (Met‘𝑋)) |
| 29 | 21, 27, 28 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) |
| 30 | | metcl 24342 |
. . . . . . 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 25459 |
. . . . . 6
⊢ (𝜑 → 𝑆 ∈ ℝ) |
| 34 | 33 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑆 ∈ ℝ) |
| 35 | 21 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑈 ∈ NrmGrp) |
| 36 | | cphlmod 25208 |
. . . . . . . . 9
⊢ (𝑈 ∈ ℂPreHil →
𝑈 ∈
LMod) |
| 37 | 4, 36 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑈 ∈ LMod) |
| 38 | 37 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑈 ∈ LMod) |
| 39 | 7 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝐴 ∈ 𝑋) |
| 40 | | eqid 2737 |
. . . . . . . . . 10
⊢
(LSubSp‘𝑈) =
(LSubSp‘𝑈) |
| 41 | 1, 40 | lssss 20934 |
. . . . . . . . 9
⊢ (𝑌 ∈ (LSubSp‘𝑈) → 𝑌 ⊆ 𝑋) |
| 42 | 5, 41 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ⊆ 𝑋) |
| 43 | 42 | sselda 3983 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝑋) |
| 44 | 1, 2 | lmodvsubcl 20905 |
. . . . . . 7
⊢ ((𝑈 ∈ LMod ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐴 − 𝑦) ∈ 𝑋) |
| 45 | 38, 39, 43, 44 | syl3anc 1373 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝐴 − 𝑦) ∈ 𝑋) |
| 46 | 1, 3 | nmcl 24629 |
. . . . . 6
⊢ ((𝑈 ∈ NrmGrp ∧ (𝐴 − 𝑦) ∈ 𝑋) → (𝑁‘(𝐴 − 𝑦)) ∈ ℝ) |
| 47 | 35, 45, 46 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝑁‘(𝐴 − 𝑦)) ∈ ℝ) |
| 48 | 33, 31 | ltnled 11408 |
. . . . . . . 8
⊢ (𝜑 → (𝑆 < (𝐴𝐷𝑃) ↔ ¬ (𝐴𝐷𝑃) ≤ 𝑆)) |
| 49 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12 | minveclem3b 25462 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐹 ∈ (fBas‘𝑌)) |
| 50 | | fbsspw 23840 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐹 ∈ (fBas‘𝑌) → 𝐹 ⊆ 𝒫 𝑌) |
| 51 | 49, 50 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐹 ⊆ 𝒫 𝑌) |
| 52 | 42 | sspwd 4613 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝒫 𝑌 ⊆ 𝒫 𝑋) |
| 53 | 51, 52 | sstrd 3994 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐹 ⊆ 𝒫 𝑋) |
| 54 | 1 | fvexi 6920 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑋 ∈ V |
| 55 | 54 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑋 ∈ V) |
| 56 | | fbasweak 23873 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹 ∈ (fBas‘𝑌) ∧ 𝐹 ⊆ 𝒫 𝑋 ∧ 𝑋 ∈ V) → 𝐹 ∈ (fBas‘𝑋)) |
| 57 | 49, 53, 55, 56 | syl3anc 1373 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐹 ∈ (fBas‘𝑋)) |
| 58 | 57 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝐹 ∈ (fBas‘𝑋)) |
| 59 | | fgcl 23886 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ (fBas‘𝑋) → (𝑋filGen𝐹) ∈ (Fil‘𝑋)) |
| 60 | 58, 59 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (𝑋filGen𝐹) ∈ (Fil‘𝑋)) |
| 61 | | ssfg 23880 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∈ (fBas‘𝑋) → 𝐹 ⊆ (𝑋filGen𝐹)) |
| 62 | 58, 61 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝐹 ⊆ (𝑋filGen𝐹)) |
| 63 | | minvec.t |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑇 = (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2)) |
| 64 | 31, 33 | readdcld 11290 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → ((𝐴𝐷𝑃) + 𝑆) ∈ ℝ) |
| 65 | 64 | rehalfcld 12513 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (((𝐴𝐷𝑃) + 𝑆) / 2) ∈ ℝ) |
| 66 | 65 | resqcld 14165 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) ∈
ℝ) |
| 67 | 33 | resqcld 14165 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑆↑2) ∈ ℝ) |
| 68 | 66, 67 | resubcld 11691 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈ ℝ) |
| 69 | 68 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈ ℝ) |
| 70 | 33, 31, 33 | ltadd1d 11856 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝑆 < (𝐴𝐷𝑃) ↔ (𝑆 + 𝑆) < ((𝐴𝐷𝑃) + 𝑆))) |
| 71 | 33 | recnd 11289 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 𝑆 ∈ ℂ) |
| 72 | 71 | 2timesd 12509 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (2 · 𝑆) = (𝑆 + 𝑆)) |
| 73 | 72 | breq1d 5153 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ((2 · 𝑆) < ((𝐴𝐷𝑃) + 𝑆) ↔ (𝑆 + 𝑆) < ((𝐴𝐷𝑃) + 𝑆))) |
| 74 | | 2re 12340 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 2 ∈
ℝ |
| 75 | | 2pos 12369 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 0 <
2 |
| 76 | 74, 75 | pm3.2i 470 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (2 ∈
ℝ ∧ 0 < 2) |
| 77 | 76 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (2 ∈ ℝ ∧ 0
< 2)) |
| 78 | | ltmuldiv2 12142 |
. . . . . . . . . . . . . . . . . . . . . . . 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 25458 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤)) |
| 82 | 81 | simp3d 1145 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → ∀𝑤 ∈ 𝑅 0 ≤ 𝑤) |
| 83 | 81 | simp1d 1143 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → 𝑅 ⊆ ℝ) |
| 84 | 81 | simp2d 1144 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → 𝑅 ≠ ∅) |
| 85 | | 0re 11263 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 0 ∈
ℝ |
| 86 | | breq1 5146 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑥 = 0 → (𝑥 ≤ 𝑤 ↔ 0 ≤ 𝑤)) |
| 87 | 86 | ralbidv 3178 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑥 = 0 → (∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ↔ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤)) |
| 88 | 87 | rspcev 3622 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((0
∈ ℝ ∧ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤) → ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤) |
| 89 | 85, 82, 88 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤) |
| 90 | 85 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → 0 ∈
ℝ) |
| 91 | | infregelb 12252 |
. . . . . . . . . . . . . . . . . . . . . . . . . 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 5185 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 0 ≤ 𝑆) |
| 95 | | metge0 24355 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → 0 ≤ (𝐴𝐷𝑃)) |
| 96 | 29, 7, 17, 95 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 0 ≤ (𝐴𝐷𝑃)) |
| 97 | 31, 33, 96, 94 | addge0d 11839 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 0 ≤ ((𝐴𝐷𝑃) + 𝑆)) |
| 98 | | divge0 12137 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝐴𝐷𝑃) + 𝑆) ∈ ℝ ∧ 0 ≤ ((𝐴𝐷𝑃) + 𝑆)) ∧ (2 ∈ ℝ ∧ 0 < 2))
→ 0 ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)) |
| 99 | 64, 97, 77, 98 | syl21anc 838 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 0 ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)) |
| 100 | 33, 65, 94, 99 | lt2sqd 14295 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑆 < (((𝐴𝐷𝑃) + 𝑆) / 2) ↔ (𝑆↑2) < ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2))) |
| 101 | 67, 66 | posdifd 11850 |
. . . . . . . . . . . . . . . . . . . . . 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 13074 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈
ℝ+) |
| 105 | 63, 104 | eqeltrid 2845 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝑇 ∈
ℝ+) |
| 106 | 5 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝑌 ∈ (LSubSp‘𝑈)) |
| 107 | | rabexg 5337 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑌 ∈ (LSubSp‘𝑈) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ∈ V) |
| 108 | 106, 107 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ∈ V) |
| 109 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑟 ∈ ℝ+
↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}) = (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}) |
| 110 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑟 = 𝑇 → ((𝑆↑2) + 𝑟) = ((𝑆↑2) + 𝑇)) |
| 111 | 110 | breq2d 5155 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑟 = 𝑇 → (((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟) ↔ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇))) |
| 112 | 111 | rabbidv 3444 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑟 = 𝑇 → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)} = {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)}) |
| 113 | 109, 112 | elrnmpt1s 5970 |
. . . . . . . . . . . . . . . . . 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 2852 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ∈ 𝐹) |
| 116 | 62, 115 | sseldd 3984 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ∈ (𝑋filGen𝐹)) |
| 117 | | ssrab2 4080 |
. . . . . . . . . . . . . . . 16
⊢ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ⊆ 𝑋 |
| 118 | 117 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ⊆ 𝑋) |
| 119 | 63 | oveq2i 7442 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑆↑2) + 𝑇) = ((𝑆↑2) + (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2))) |
| 120 | 67 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → (𝑆↑2) ∈ ℝ) |
| 121 | 120 | recnd 11289 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → (𝑆↑2) ∈ ℂ) |
| 122 | 65 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → (((𝐴𝐷𝑃) + 𝑆) / 2) ∈ ℝ) |
| 123 | 122 | resqcld 14165 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) ∈
ℝ) |
| 124 | 123 | recnd 11289 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) ∈
ℂ) |
| 125 | 121, 124 | pncan3d 11623 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → ((𝑆↑2) + (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2))) = ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2)) |
| 126 | 119, 125 | eqtrid 2789 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → ((𝑆↑2) + 𝑇) = ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2)) |
| 127 | 126 | breq2d 5155 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → (((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇) ↔ ((𝐴𝐷𝑦)↑2) ≤ ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2))) |
| 128 | 29 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → 𝐷 ∈ (Met‘𝑋)) |
| 129 | 7 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → 𝐴 ∈ 𝑋) |
| 130 | 43 | adantlr 715 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝑋) |
| 131 | | metcl 24342 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐴𝐷𝑦) ∈ ℝ) |
| 132 | 128, 129,
130, 131 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → (𝐴𝐷𝑦) ∈ ℝ) |
| 133 | | metge0 24355 |
. . . . . . . . . . . . . . . . . . . 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 14296 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → ((𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2) ↔ ((𝐴𝐷𝑦)↑2) ≤ ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2))) |
| 137 | 127, 136 | bitr4d 282 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → (((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇) ↔ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2))) |
| 138 | 137 | rabbidva 3443 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} = {𝑦 ∈ 𝑌 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)}) |
| 139 | 42 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝑌 ⊆ 𝑋) |
| 140 | | rabss2 4078 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑌 ⊆ 𝑋 → {𝑦 ∈ 𝑌 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ⊆ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)}) |
| 141 | 139, 140 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑌 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ⊆ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)}) |
| 142 | 138, 141 | eqsstrd 4018 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ⊆ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)}) |
| 143 | | filss 23861 |
. . . . . . . . . . . . . . 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 23986 |
. . . . . . . . . . . . . 14
⊢ ({𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ∈ (𝑋filGen𝐹) → (𝐽 fLim (𝑋filGen𝐹)) ⊆ ((cls‘𝐽)‘{𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)})) |
| 146 | 144, 145 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (𝐽 fLim (𝑋filGen𝐹)) ⊆ ((cls‘𝐽)‘{𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)})) |
| 147 | 14 | elin1d 4204 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑃 ∈ (𝐽 fLim (𝑋filGen𝐹))) |
| 148 | 147 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝑃 ∈ (𝐽 fLim (𝑋filGen𝐹))) |
| 149 | 146, 148 | sseldd 3984 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝑃 ∈ ((cls‘𝐽)‘{𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)})) |
| 150 | | ngpxms 24614 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑈 ∈ NrmGrp → 𝑈 ∈
∞MetSp) |
| 151 | 1, 11 | xmsxmet 24466 |
. . . . . . . . . . . . . . . . 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 11311 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (((𝐴𝐷𝑃) + 𝑆) / 2) ∈
ℝ*) |
| 157 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢
(MetOpen‘𝐷) =
(MetOpen‘𝐷) |
| 158 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} = {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} |
| 159 | 157, 158 | blcld 24518 |
. . . . . . . . . . . . . . 15
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ (((𝐴𝐷𝑃) + 𝑆) / 2) ∈ ℝ*) →
{𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ∈
(Clsd‘(MetOpen‘𝐷))) |
| 160 | 153, 154,
156, 159 | syl3anc 1373 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ∈
(Clsd‘(MetOpen‘𝐷))) |
| 161 | 8, 1, 11 | xmstopn 24461 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑈 ∈ ∞MetSp →
𝐽 = (MetOpen‘𝐷)) |
| 162 | 21, 150, 161 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐽 = (MetOpen‘𝐷)) |
| 163 | 162 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝐽 = (MetOpen‘𝐷)) |
| 164 | 163 | fveq2d 6910 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (Clsd‘𝐽) = (Clsd‘(MetOpen‘𝐷))) |
| 165 | 160, 164 | eleqtrrd 2844 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ∈ (Clsd‘𝐽)) |
| 166 | | cldcls 23050 |
. . . . . . . . . . . . 13
⊢ ({𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ∈ (Clsd‘𝐽) → ((cls‘𝐽)‘{𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)}) = {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)}) |
| 167 | 165, 166 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → ((cls‘𝐽)‘{𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)}) = {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)}) |
| 168 | 149, 167 | eleqtrd 2843 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝑃 ∈ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)}) |
| 169 | | oveq2 7439 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑃 → (𝐴𝐷𝑦) = (𝐴𝐷𝑃)) |
| 170 | 169 | breq1d 5153 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑃 → ((𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2) ↔ (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2))) |
| 171 | 170 | elrab 3692 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ↔ (𝑃 ∈ 𝑋 ∧ (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2))) |
| 172 | 171 | simprbi 496 |
. . . . . . . . . . 11
⊢ (𝑃 ∈ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} → (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)) |
| 173 | 168, 172 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)) |
| 174 | 31, 33, 31 | leadd2d 11858 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐴𝐷𝑃) ≤ 𝑆 ↔ ((𝐴𝐷𝑃) + (𝐴𝐷𝑃)) ≤ ((𝐴𝐷𝑃) + 𝑆))) |
| 175 | 31 | recnd 11289 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴𝐷𝑃) ∈ ℂ) |
| 176 | 175 | 2timesd 12509 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (2 · (𝐴𝐷𝑃)) = ((𝐴𝐷𝑃) + (𝐴𝐷𝑃))) |
| 177 | 176 | breq1d 5153 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((2 · (𝐴𝐷𝑃)) ≤ ((𝐴𝐷𝑃) + 𝑆) ↔ ((𝐴𝐷𝑃) + (𝐴𝐷𝑃)) ≤ ((𝐴𝐷𝑃) + 𝑆))) |
| 178 | | lemuldiv2 12149 |
. . . . . . . . . . . . . 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 6919 |
. . . . . . . . 9
⊢ (𝑁‘(𝐴 − 𝑦)) ∈ V |
| 192 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦))) = (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦))) |
| 193 | 192 | elrnmpt1 5971 |
. . . . . . . . 9
⊢ ((𝑦 ∈ 𝑌 ∧ (𝑁‘(𝐴 − 𝑦)) ∈ V) → (𝑁‘(𝐴 − 𝑦)) ∈ ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))) |
| 194 | 190, 191,
193 | sylancl 586 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝑁‘(𝐴 − 𝑦)) ∈ ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))) |
| 195 | 194, 9 | eleqtrrdi 2852 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝑁‘(𝐴 − 𝑦)) ∈ 𝑅) |
| 196 | | infrelb 12253 |
. . . . . . 7
⊢ ((𝑅 ⊆ ℝ ∧
∃𝑥 ∈ ℝ
∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ∧ (𝑁‘(𝐴 − 𝑦)) ∈ 𝑅) → inf(𝑅, ℝ, < ) ≤ (𝑁‘(𝐴 − 𝑦))) |
| 197 | 188, 189,
195, 196 | syl3anc 1373 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → inf(𝑅, ℝ, < ) ≤ (𝑁‘(𝐴 − 𝑦))) |
| 198 | 10, 197 | eqbrtrid 5178 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑆 ≤ (𝑁‘(𝐴 − 𝑦))) |
| 199 | 32, 34, 47, 187, 198 | letrd 11418 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝐴𝐷𝑃) ≤ (𝑁‘(𝐴 − 𝑦))) |
| 200 | 26, 199 | eqbrtrrd 5167 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝑁‘(𝐴 − 𝑃)) ≤ (𝑁‘(𝐴 − 𝑦))) |
| 201 | 200 | ralrimiva 3146 |
. 2
⊢ (𝜑 → ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑃)) ≤ (𝑁‘(𝐴 − 𝑦))) |
| 202 | | oveq2 7439 |
. . . . . 6
⊢ (𝑥 = 𝑃 → (𝐴 − 𝑥) = (𝐴 − 𝑃)) |
| 203 | 202 | fveq2d 6910 |
. . . . 5
⊢ (𝑥 = 𝑃 → (𝑁‘(𝐴 − 𝑥)) = (𝑁‘(𝐴 − 𝑃))) |
| 204 | 203 | breq1d 5153 |
. . . 4
⊢ (𝑥 = 𝑃 → ((𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)) ↔ (𝑁‘(𝐴 − 𝑃)) ≤ (𝑁‘(𝐴 − 𝑦)))) |
| 205 | 204 | ralbidv 3178 |
. . 3
⊢ (𝑥 = 𝑃 → (∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)) ↔ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑃)) ≤ (𝑁‘(𝐴 − 𝑦)))) |
| 206 | 205 | rspcev 3622 |
. 2
⊢ ((𝑃 ∈ 𝑌 ∧ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑃)) ≤ (𝑁‘(𝐴 − 𝑦))) → ∃𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦))) |
| 207 | 15, 201, 206 | syl2anc 584 |
1
⊢ (𝜑 → ∃𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦))) |