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 24594 |
. . 3
⊢ (𝜑 → 𝑃 ∈ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌)) |
15 | 14 | elin2d 4133 |
. 2
⊢ (𝜑 → 𝑃 ∈ 𝑌) |
16 | 11 | oveqi 7288 |
. . . . . . 7
⊢ (𝐴𝐷𝑃) = (𝐴((dist‘𝑈) ↾ (𝑋 × 𝑋))𝑃) |
17 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13 | minveclem4b 24595 |
. . . . . . . 8
⊢ (𝜑 → 𝑃 ∈ 𝑋) |
18 | 7, 17 | ovresd 7439 |
. . . . . . 7
⊢ (𝜑 → (𝐴((dist‘𝑈) ↾ (𝑋 × 𝑋))𝑃) = (𝐴(dist‘𝑈)𝑃)) |
19 | 16, 18 | eqtrid 2790 |
. . . . . 6
⊢ (𝜑 → (𝐴𝐷𝑃) = (𝐴(dist‘𝑈)𝑃)) |
20 | | cphngp 24337 |
. . . . . . . 8
⊢ (𝑈 ∈ ℂPreHil →
𝑈 ∈
NrmGrp) |
21 | 4, 20 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑈 ∈ NrmGrp) |
22 | | eqid 2738 |
. . . . . . . 8
⊢
(dist‘𝑈) =
(dist‘𝑈) |
23 | 3, 1, 2, 22 | ngpds 23760 |
. . . . . . 7
⊢ ((𝑈 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝐴(dist‘𝑈)𝑃) = (𝑁‘(𝐴 − 𝑃))) |
24 | 21, 7, 17, 23 | syl3anc 1370 |
. . . . . 6
⊢ (𝜑 → (𝐴(dist‘𝑈)𝑃) = (𝑁‘(𝐴 − 𝑃))) |
25 | 19, 24 | eqtrd 2778 |
. . . . 5
⊢ (𝜑 → (𝐴𝐷𝑃) = (𝑁‘(𝐴 − 𝑃))) |
26 | 25 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝐴𝐷𝑃) = (𝑁‘(𝐴 − 𝑃))) |
27 | | ngpms 23756 |
. . . . . . . 8
⊢ (𝑈 ∈ NrmGrp → 𝑈 ∈ MetSp) |
28 | 1, 11 | msmet 23610 |
. . . . . . . 8
⊢ (𝑈 ∈ MetSp → 𝐷 ∈ (Met‘𝑋)) |
29 | 21, 27, 28 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) |
30 | | metcl 23485 |
. . . . . . 7
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝐴𝐷𝑃) ∈ ℝ) |
31 | 29, 7, 17, 30 | syl3anc 1370 |
. . . . . 6
⊢ (𝜑 → (𝐴𝐷𝑃) ∈ ℝ) |
32 | 31 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝐴𝐷𝑃) ∈ ℝ) |
33 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | minveclem4c 24589 |
. . . . . 6
⊢ (𝜑 → 𝑆 ∈ ℝ) |
34 | 33 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑆 ∈ ℝ) |
35 | 21 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑈 ∈ NrmGrp) |
36 | | cphlmod 24338 |
. . . . . . . . 9
⊢ (𝑈 ∈ ℂPreHil →
𝑈 ∈
LMod) |
37 | 4, 36 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑈 ∈ LMod) |
38 | 37 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑈 ∈ LMod) |
39 | 7 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝐴 ∈ 𝑋) |
40 | | eqid 2738 |
. . . . . . . . . 10
⊢
(LSubSp‘𝑈) =
(LSubSp‘𝑈) |
41 | 1, 40 | lssss 20198 |
. . . . . . . . 9
⊢ (𝑌 ∈ (LSubSp‘𝑈) → 𝑌 ⊆ 𝑋) |
42 | 5, 41 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ⊆ 𝑋) |
43 | 42 | sselda 3921 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝑋) |
44 | 1, 2 | lmodvsubcl 20168 |
. . . . . . 7
⊢ ((𝑈 ∈ LMod ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐴 − 𝑦) ∈ 𝑋) |
45 | 38, 39, 43, 44 | syl3anc 1370 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝐴 − 𝑦) ∈ 𝑋) |
46 | 1, 3 | nmcl 23772 |
. . . . . 6
⊢ ((𝑈 ∈ NrmGrp ∧ (𝐴 − 𝑦) ∈ 𝑋) → (𝑁‘(𝐴 − 𝑦)) ∈ ℝ) |
47 | 35, 45, 46 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝑁‘(𝐴 − 𝑦)) ∈ ℝ) |
48 | 33, 31 | ltnled 11122 |
. . . . . . . 8
⊢ (𝜑 → (𝑆 < (𝐴𝐷𝑃) ↔ ¬ (𝐴𝐷𝑃) ≤ 𝑆)) |
49 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12 | minveclem3b 24592 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐹 ∈ (fBas‘𝑌)) |
50 | | fbsspw 22983 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐹 ∈ (fBas‘𝑌) → 𝐹 ⊆ 𝒫 𝑌) |
51 | 49, 50 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐹 ⊆ 𝒫 𝑌) |
52 | 42 | sspwd 4548 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝒫 𝑌 ⊆ 𝒫 𝑋) |
53 | 51, 52 | sstrd 3931 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐹 ⊆ 𝒫 𝑋) |
54 | 1 | fvexi 6788 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑋 ∈ V |
55 | 54 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑋 ∈ V) |
56 | | fbasweak 23016 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹 ∈ (fBas‘𝑌) ∧ 𝐹 ⊆ 𝒫 𝑋 ∧ 𝑋 ∈ V) → 𝐹 ∈ (fBas‘𝑋)) |
57 | 49, 53, 55, 56 | syl3anc 1370 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐹 ∈ (fBas‘𝑋)) |
58 | 57 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝐹 ∈ (fBas‘𝑋)) |
59 | | fgcl 23029 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ (fBas‘𝑋) → (𝑋filGen𝐹) ∈ (Fil‘𝑋)) |
60 | 58, 59 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (𝑋filGen𝐹) ∈ (Fil‘𝑋)) |
61 | | ssfg 23023 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∈ (fBas‘𝑋) → 𝐹 ⊆ (𝑋filGen𝐹)) |
62 | 58, 61 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝐹 ⊆ (𝑋filGen𝐹)) |
63 | | minvec.t |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑇 = (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2)) |
64 | 31, 33 | readdcld 11004 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → ((𝐴𝐷𝑃) + 𝑆) ∈ ℝ) |
65 | 64 | rehalfcld 12220 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (((𝐴𝐷𝑃) + 𝑆) / 2) ∈ ℝ) |
66 | 65 | resqcld 13965 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) ∈
ℝ) |
67 | 33 | resqcld 13965 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑆↑2) ∈ ℝ) |
68 | 66, 67 | resubcld 11403 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈ ℝ) |
69 | 68 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈ ℝ) |
70 | 33, 31, 33 | ltadd1d 11568 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝑆 < (𝐴𝐷𝑃) ↔ (𝑆 + 𝑆) < ((𝐴𝐷𝑃) + 𝑆))) |
71 | 33 | recnd 11003 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 𝑆 ∈ ℂ) |
72 | 71 | 2timesd 12216 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (2 · 𝑆) = (𝑆 + 𝑆)) |
73 | 72 | breq1d 5084 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ((2 · 𝑆) < ((𝐴𝐷𝑃) + 𝑆) ↔ (𝑆 + 𝑆) < ((𝐴𝐷𝑃) + 𝑆))) |
74 | | 2re 12047 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 2 ∈
ℝ |
75 | | 2pos 12076 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 0 <
2 |
76 | 74, 75 | pm3.2i 471 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (2 ∈
ℝ ∧ 0 < 2) |
77 | 76 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (2 ∈ ℝ ∧ 0
< 2)) |
78 | | ltmuldiv2 11849 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑆 ∈ ℝ ∧ ((𝐴𝐷𝑃) + 𝑆) ∈ ℝ ∧ (2 ∈ ℝ
∧ 0 < 2)) → ((2 · 𝑆) < ((𝐴𝐷𝑃) + 𝑆) ↔ 𝑆 < (((𝐴𝐷𝑃) + 𝑆) / 2))) |
79 | 33, 64, 77, 78 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ((2 · 𝑆) < ((𝐴𝐷𝑃) + 𝑆) ↔ 𝑆 < (((𝐴𝐷𝑃) + 𝑆) / 2))) |
80 | 70, 73, 79 | 3bitr2d 307 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑆 < (𝐴𝐷𝑃) ↔ 𝑆 < (((𝐴𝐷𝑃) + 𝑆) / 2))) |
81 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | minveclem1 24588 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤)) |
82 | 81 | simp3d 1143 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → ∀𝑤 ∈ 𝑅 0 ≤ 𝑤) |
83 | 81 | simp1d 1141 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → 𝑅 ⊆ ℝ) |
84 | 81 | simp2d 1142 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → 𝑅 ≠ ∅) |
85 | | 0re 10977 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 0 ∈
ℝ |
86 | | breq1 5077 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑥 = 0 → (𝑥 ≤ 𝑤 ↔ 0 ≤ 𝑤)) |
87 | 86 | ralbidv 3112 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑥 = 0 → (∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ↔ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤)) |
88 | 87 | rspcev 3561 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((0
∈ ℝ ∧ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤) → ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤) |
89 | 85, 82, 88 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤) |
90 | 85 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → 0 ∈
ℝ) |
91 | | infregelb 11959 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤) ∧ 0 ∈ ℝ) → (0 ≤
inf(𝑅, ℝ, < )
↔ ∀𝑤 ∈
𝑅 0 ≤ 𝑤)) |
92 | 83, 84, 89, 90, 91 | syl31anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (0 ≤ inf(𝑅, ℝ, < ) ↔
∀𝑤 ∈ 𝑅 0 ≤ 𝑤)) |
93 | 82, 92 | mpbird 256 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 0 ≤ inf(𝑅, ℝ, <
)) |
94 | 93, 10 | breqtrrdi 5116 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 0 ≤ 𝑆) |
95 | | metge0 23498 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → 0 ≤ (𝐴𝐷𝑃)) |
96 | 29, 7, 17, 95 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 0 ≤ (𝐴𝐷𝑃)) |
97 | 31, 33, 96, 94 | addge0d 11551 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 0 ≤ ((𝐴𝐷𝑃) + 𝑆)) |
98 | | divge0 11844 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝐴𝐷𝑃) + 𝑆) ∈ ℝ ∧ 0 ≤ ((𝐴𝐷𝑃) + 𝑆)) ∧ (2 ∈ ℝ ∧ 0 < 2))
→ 0 ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)) |
99 | 64, 97, 77, 98 | syl21anc 835 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 0 ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)) |
100 | 33, 65, 94, 99 | lt2sqd 13973 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑆 < (((𝐴𝐷𝑃) + 𝑆) / 2) ↔ (𝑆↑2) < ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2))) |
101 | 67, 66 | posdifd 11562 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((𝑆↑2) < ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) ↔ 0 < (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2)))) |
102 | 80, 100, 101 | 3bitrd 305 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑆 < (𝐴𝐷𝑃) ↔ 0 < (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2)))) |
103 | 102 | biimpa 477 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 0 < (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2))) |
104 | 69, 103 | elrpd 12769 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈
ℝ+) |
105 | 63, 104 | eqeltrid 2843 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝑇 ∈
ℝ+) |
106 | 5 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝑌 ∈ (LSubSp‘𝑈)) |
107 | | rabexg 5255 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑌 ∈ (LSubSp‘𝑈) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ∈ V) |
108 | 106, 107 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ∈ V) |
109 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑟 ∈ ℝ+
↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}) = (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}) |
110 | | oveq2 7283 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑟 = 𝑇 → ((𝑆↑2) + 𝑟) = ((𝑆↑2) + 𝑇)) |
111 | 110 | breq2d 5086 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑟 = 𝑇 → (((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟) ↔ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇))) |
112 | 111 | rabbidv 3414 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑟 = 𝑇 → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)} = {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)}) |
113 | 109, 112 | elrnmpt1s 5866 |
. . . . . . . . . . . . . . . . . 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 2850 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ∈ 𝐹) |
116 | 62, 115 | sseldd 3922 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ∈ (𝑋filGen𝐹)) |
117 | | ssrab2 4013 |
. . . . . . . . . . . . . . . 16
⊢ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ⊆ 𝑋 |
118 | 117 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ⊆ 𝑋) |
119 | 63 | oveq2i 7286 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑆↑2) + 𝑇) = ((𝑆↑2) + (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2))) |
120 | 67 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → (𝑆↑2) ∈ ℝ) |
121 | 120 | recnd 11003 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → (𝑆↑2) ∈ ℂ) |
122 | 65 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → (((𝐴𝐷𝑃) + 𝑆) / 2) ∈ ℝ) |
123 | 122 | resqcld 13965 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) ∈
ℝ) |
124 | 123 | recnd 11003 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) ∈
ℂ) |
125 | 121, 124 | pncan3d 11335 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → ((𝑆↑2) + (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2))) = ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2)) |
126 | 119, 125 | eqtrid 2790 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → ((𝑆↑2) + 𝑇) = ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2)) |
127 | 126 | breq2d 5086 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → (((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇) ↔ ((𝐴𝐷𝑦)↑2) ≤ ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2))) |
128 | 29 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → 𝐷 ∈ (Met‘𝑋)) |
129 | 7 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → 𝐴 ∈ 𝑋) |
130 | 43 | adantlr 712 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝑋) |
131 | | metcl 23485 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐴𝐷𝑦) ∈ ℝ) |
132 | 128, 129,
130, 131 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → (𝐴𝐷𝑦) ∈ ℝ) |
133 | | metge0 23498 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → 0 ≤ (𝐴𝐷𝑦)) |
134 | 128, 129,
130, 133 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → 0 ≤ (𝐴𝐷𝑦)) |
135 | 99 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → 0 ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)) |
136 | 132, 122,
134, 135 | le2sqd 13974 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → ((𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2) ↔ ((𝐴𝐷𝑦)↑2) ≤ ((((𝐴𝐷𝑃) + 𝑆) / 2)↑2))) |
137 | 127, 136 | bitr4d 281 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) ∧ 𝑦 ∈ 𝑌) → (((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇) ↔ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2))) |
138 | 137 | rabbidva 3413 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} = {𝑦 ∈ 𝑌 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)}) |
139 | 42 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝑌 ⊆ 𝑋) |
140 | | rabss2 4011 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑌 ⊆ 𝑋 → {𝑦 ∈ 𝑌 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ⊆ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)}) |
141 | 139, 140 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑌 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ⊆ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)}) |
142 | 138, 141 | eqsstrd 3959 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ⊆ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)}) |
143 | | filss 23004 |
. . . . . . . . . . . . . . 15
⊢ (((𝑋filGen𝐹) ∈ (Fil‘𝑋) ∧ ({𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ∈ (𝑋filGen𝐹) ∧ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ⊆ 𝑋 ∧ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑇)} ⊆ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)})) → {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ∈ (𝑋filGen𝐹)) |
144 | 60, 116, 118, 142, 143 | syl13anc 1371 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ∈ (𝑋filGen𝐹)) |
145 | | flimclsi 23129 |
. . . . . . . . . . . . . 14
⊢ ({𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ∈ (𝑋filGen𝐹) → (𝐽 fLim (𝑋filGen𝐹)) ⊆ ((cls‘𝐽)‘{𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)})) |
146 | 144, 145 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (𝐽 fLim (𝑋filGen𝐹)) ⊆ ((cls‘𝐽)‘{𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)})) |
147 | 14 | elin1d 4132 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑃 ∈ (𝐽 fLim (𝑋filGen𝐹))) |
148 | 147 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝑃 ∈ (𝐽 fLim (𝑋filGen𝐹))) |
149 | 146, 148 | sseldd 3922 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝑃 ∈ ((cls‘𝐽)‘{𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)})) |
150 | | ngpxms 23757 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑈 ∈ NrmGrp → 𝑈 ∈
∞MetSp) |
151 | 1, 11 | xmsxmet 23609 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑈 ∈ ∞MetSp →
𝐷 ∈
(∞Met‘𝑋)) |
152 | 21, 150, 151 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) |
153 | 152 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝐷 ∈ (∞Met‘𝑋)) |
154 | 7 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝐴 ∈ 𝑋) |
155 | 65 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (((𝐴𝐷𝑃) + 𝑆) / 2) ∈ ℝ) |
156 | 155 | rexrd 11025 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (((𝐴𝐷𝑃) + 𝑆) / 2) ∈
ℝ*) |
157 | | eqid 2738 |
. . . . . . . . . . . . . . . 16
⊢
(MetOpen‘𝐷) =
(MetOpen‘𝐷) |
158 | | eqid 2738 |
. . . . . . . . . . . . . . . 16
⊢ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} = {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} |
159 | 157, 158 | blcld 23661 |
. . . . . . . . . . . . . . 15
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ (((𝐴𝐷𝑃) + 𝑆) / 2) ∈ ℝ*) →
{𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ∈
(Clsd‘(MetOpen‘𝐷))) |
160 | 153, 154,
156, 159 | syl3anc 1370 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ∈
(Clsd‘(MetOpen‘𝐷))) |
161 | 8, 1, 11 | xmstopn 23604 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑈 ∈ ∞MetSp →
𝐽 = (MetOpen‘𝐷)) |
162 | 21, 150, 161 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐽 = (MetOpen‘𝐷)) |
163 | 162 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝐽 = (MetOpen‘𝐷)) |
164 | 163 | fveq2d 6778 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (Clsd‘𝐽) = (Clsd‘(MetOpen‘𝐷))) |
165 | 160, 164 | eleqtrrd 2842 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ∈ (Clsd‘𝐽)) |
166 | | cldcls 22193 |
. . . . . . . . . . . . 13
⊢ ({𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ∈ (Clsd‘𝐽) → ((cls‘𝐽)‘{𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)}) = {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)}) |
167 | 165, 166 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → ((cls‘𝐽)‘{𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)}) = {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)}) |
168 | 149, 167 | eleqtrd 2841 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → 𝑃 ∈ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)}) |
169 | | oveq2 7283 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑃 → (𝐴𝐷𝑦) = (𝐴𝐷𝑃)) |
170 | 169 | breq1d 5084 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑃 → ((𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2) ↔ (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2))) |
171 | 170 | elrab 3624 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} ↔ (𝑃 ∈ 𝑋 ∧ (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2))) |
172 | 171 | simprbi 497 |
. . . . . . . . . . 11
⊢ (𝑃 ∈ {𝑦 ∈ 𝑋 ∣ (𝐴𝐷𝑦) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)} → (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)) |
173 | 168, 172 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)) |
174 | 31, 33, 31 | leadd2d 11570 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐴𝐷𝑃) ≤ 𝑆 ↔ ((𝐴𝐷𝑃) + (𝐴𝐷𝑃)) ≤ ((𝐴𝐷𝑃) + 𝑆))) |
175 | 31 | recnd 11003 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴𝐷𝑃) ∈ ℂ) |
176 | 175 | 2timesd 12216 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (2 · (𝐴𝐷𝑃)) = ((𝐴𝐷𝑃) + (𝐴𝐷𝑃))) |
177 | 176 | breq1d 5084 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((2 · (𝐴𝐷𝑃)) ≤ ((𝐴𝐷𝑃) + 𝑆) ↔ ((𝐴𝐷𝑃) + (𝐴𝐷𝑃)) ≤ ((𝐴𝐷𝑃) + 𝑆))) |
178 | | lemuldiv2 11856 |
. . . . . . . . . . . . . 14
⊢ (((𝐴𝐷𝑃) ∈ ℝ ∧ ((𝐴𝐷𝑃) + 𝑆) ∈ ℝ ∧ (2 ∈ ℝ
∧ 0 < 2)) → ((2 · (𝐴𝐷𝑃)) ≤ ((𝐴𝐷𝑃) + 𝑆) ↔ (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2))) |
179 | 76, 178 | mp3an3 1449 |
. . . . . . . . . . . . 13
⊢ (((𝐴𝐷𝑃) ∈ ℝ ∧ ((𝐴𝐷𝑃) + 𝑆) ∈ ℝ) → ((2 · (𝐴𝐷𝑃)) ≤ ((𝐴𝐷𝑃) + 𝑆) ↔ (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2))) |
180 | 31, 64, 179 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((2 · (𝐴𝐷𝑃)) ≤ ((𝐴𝐷𝑃) + 𝑆) ↔ (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2))) |
181 | 174, 177,
180 | 3bitr2d 307 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐴𝐷𝑃) ≤ 𝑆 ↔ (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2))) |
182 | 181 | biimpar 478 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐴𝐷𝑃) ≤ (((𝐴𝐷𝑃) + 𝑆) / 2)) → (𝐴𝐷𝑃) ≤ 𝑆) |
183 | 173, 182 | syldan 591 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑆 < (𝐴𝐷𝑃)) → (𝐴𝐷𝑃) ≤ 𝑆) |
184 | 183 | ex 413 |
. . . . . . . 8
⊢ (𝜑 → (𝑆 < (𝐴𝐷𝑃) → (𝐴𝐷𝑃) ≤ 𝑆)) |
185 | 48, 184 | sylbird 259 |
. . . . . . 7
⊢ (𝜑 → (¬ (𝐴𝐷𝑃) ≤ 𝑆 → (𝐴𝐷𝑃) ≤ 𝑆)) |
186 | 185 | pm2.18d 127 |
. . . . . 6
⊢ (𝜑 → (𝐴𝐷𝑃) ≤ 𝑆) |
187 | 186 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝐴𝐷𝑃) ≤ 𝑆) |
188 | 83 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑅 ⊆ ℝ) |
189 | 89 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤) |
190 | | simpr 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝑌) |
191 | | fvex 6787 |
. . . . . . . . 9
⊢ (𝑁‘(𝐴 − 𝑦)) ∈ V |
192 | | eqid 2738 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦))) = (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦))) |
193 | 192 | elrnmpt1 5867 |
. . . . . . . . 9
⊢ ((𝑦 ∈ 𝑌 ∧ (𝑁‘(𝐴 − 𝑦)) ∈ V) → (𝑁‘(𝐴 − 𝑦)) ∈ ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))) |
194 | 190, 191,
193 | sylancl 586 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝑁‘(𝐴 − 𝑦)) ∈ ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))) |
195 | 194, 9 | eleqtrrdi 2850 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝑁‘(𝐴 − 𝑦)) ∈ 𝑅) |
196 | | infrelb 11960 |
. . . . . . 7
⊢ ((𝑅 ⊆ ℝ ∧
∃𝑥 ∈ ℝ
∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ∧ (𝑁‘(𝐴 − 𝑦)) ∈ 𝑅) → inf(𝑅, ℝ, < ) ≤ (𝑁‘(𝐴 − 𝑦))) |
197 | 188, 189,
195, 196 | syl3anc 1370 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → inf(𝑅, ℝ, < ) ≤ (𝑁‘(𝐴 − 𝑦))) |
198 | 10, 197 | eqbrtrid 5109 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑆 ≤ (𝑁‘(𝐴 − 𝑦))) |
199 | 32, 34, 47, 187, 198 | letrd 11132 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝐴𝐷𝑃) ≤ (𝑁‘(𝐴 − 𝑦))) |
200 | 26, 199 | eqbrtrrd 5098 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝑁‘(𝐴 − 𝑃)) ≤ (𝑁‘(𝐴 − 𝑦))) |
201 | 200 | ralrimiva 3103 |
. 2
⊢ (𝜑 → ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑃)) ≤ (𝑁‘(𝐴 − 𝑦))) |
202 | | oveq2 7283 |
. . . . . 6
⊢ (𝑥 = 𝑃 → (𝐴 − 𝑥) = (𝐴 − 𝑃)) |
203 | 202 | fveq2d 6778 |
. . . . 5
⊢ (𝑥 = 𝑃 → (𝑁‘(𝐴 − 𝑥)) = (𝑁‘(𝐴 − 𝑃))) |
204 | 203 | breq1d 5084 |
. . . 4
⊢ (𝑥 = 𝑃 → ((𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)) ↔ (𝑁‘(𝐴 − 𝑃)) ≤ (𝑁‘(𝐴 − 𝑦)))) |
205 | 204 | ralbidv 3112 |
. . 3
⊢ (𝑥 = 𝑃 → (∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)) ↔ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑃)) ≤ (𝑁‘(𝐴 − 𝑦)))) |
206 | 205 | rspcev 3561 |
. 2
⊢ ((𝑃 ∈ 𝑌 ∧ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑃)) ≤ (𝑁‘(𝐴 − 𝑦))) → ∃𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦))) |
207 | 15, 201, 206 | syl2anc 584 |
1
⊢ (𝜑 → ∃𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦))) |