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 24947 |
. . 3
β’ (π β π β ((π½ fLim (πfilGenπΉ)) β© π)) |
15 | 14 | elin2d 4200 |
. 2
β’ (π β π β π) |
16 | 11 | oveqi 7422 |
. . . . . . 7
β’ (π΄π·π) = (π΄((distβπ) βΎ (π Γ π))π) |
17 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13 | minveclem4b 24948 |
. . . . . . . 8
β’ (π β π β π) |
18 | 7, 17 | ovresd 7574 |
. . . . . . 7
β’ (π β (π΄((distβπ) βΎ (π Γ π))π) = (π΄(distβπ)π)) |
19 | 16, 18 | eqtrid 2785 |
. . . . . 6
β’ (π β (π΄π·π) = (π΄(distβπ)π)) |
20 | | cphngp 24690 |
. . . . . . . 8
β’ (π β βPreHil β
π β
NrmGrp) |
21 | 4, 20 | syl 17 |
. . . . . . 7
β’ (π β π β NrmGrp) |
22 | | eqid 2733 |
. . . . . . . 8
β’
(distβπ) =
(distβπ) |
23 | 3, 1, 2, 22 | ngpds 24113 |
. . . . . . 7
β’ ((π β NrmGrp β§ π΄ β π β§ π β π) β (π΄(distβπ)π) = (πβ(π΄ β π))) |
24 | 21, 7, 17, 23 | syl3anc 1372 |
. . . . . 6
β’ (π β (π΄(distβπ)π) = (πβ(π΄ β π))) |
25 | 19, 24 | eqtrd 2773 |
. . . . 5
β’ (π β (π΄π·π) = (πβ(π΄ β π))) |
26 | 25 | adantr 482 |
. . . 4
β’ ((π β§ π¦ β π) β (π΄π·π) = (πβ(π΄ β π))) |
27 | | ngpms 24109 |
. . . . . . . 8
β’ (π β NrmGrp β π β MetSp) |
28 | 1, 11 | msmet 23963 |
. . . . . . . 8
β’ (π β MetSp β π· β (Metβπ)) |
29 | 21, 27, 28 | 3syl 18 |
. . . . . . 7
β’ (π β π· β (Metβπ)) |
30 | | metcl 23838 |
. . . . . . 7
β’ ((π· β (Metβπ) β§ π΄ β π β§ π β π) β (π΄π·π) β β) |
31 | 29, 7, 17, 30 | syl3anc 1372 |
. . . . . 6
β’ (π β (π΄π·π) β β) |
32 | 31 | adantr 482 |
. . . . 5
β’ ((π β§ π¦ β π) β (π΄π·π) β β) |
33 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | minveclem4c 24942 |
. . . . . 6
β’ (π β π β β) |
34 | 33 | adantr 482 |
. . . . 5
β’ ((π β§ π¦ β π) β π β β) |
35 | 21 | adantr 482 |
. . . . . 6
β’ ((π β§ π¦ β π) β π β NrmGrp) |
36 | | cphlmod 24691 |
. . . . . . . . 9
β’ (π β βPreHil β
π β
LMod) |
37 | 4, 36 | syl 17 |
. . . . . . . 8
β’ (π β π β LMod) |
38 | 37 | adantr 482 |
. . . . . . 7
β’ ((π β§ π¦ β π) β π β LMod) |
39 | 7 | adantr 482 |
. . . . . . 7
β’ ((π β§ π¦ β π) β π΄ β π) |
40 | | eqid 2733 |
. . . . . . . . . 10
β’
(LSubSpβπ) =
(LSubSpβπ) |
41 | 1, 40 | lssss 20547 |
. . . . . . . . 9
β’ (π β (LSubSpβπ) β π β π) |
42 | 5, 41 | syl 17 |
. . . . . . . 8
β’ (π β π β π) |
43 | 42 | sselda 3983 |
. . . . . . 7
β’ ((π β§ π¦ β π) β π¦ β π) |
44 | 1, 2 | lmodvsubcl 20517 |
. . . . . . 7
β’ ((π β LMod β§ π΄ β π β§ π¦ β π) β (π΄ β π¦) β π) |
45 | 38, 39, 43, 44 | syl3anc 1372 |
. . . . . 6
β’ ((π β§ π¦ β π) β (π΄ β π¦) β π) |
46 | 1, 3 | nmcl 24125 |
. . . . . 6
β’ ((π β NrmGrp β§ (π΄ β π¦) β π) β (πβ(π΄ β π¦)) β β) |
47 | 35, 45, 46 | syl2anc 585 |
. . . . 5
β’ ((π β§ π¦ β π) β (πβ(π΄ β π¦)) β β) |
48 | 33, 31 | ltnled 11361 |
. . . . . . . 8
β’ (π β (π < (π΄π·π) β Β¬ (π΄π·π) β€ π)) |
49 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12 | minveclem3b 24945 |
. . . . . . . . . . . . . . . . . 18
β’ (π β πΉ β (fBasβπ)) |
50 | | fbsspw 23336 |
. . . . . . . . . . . . . . . . . . . 20
β’ (πΉ β (fBasβπ) β πΉ β π« π) |
51 | 49, 50 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β πΉ β π« π) |
52 | 42 | sspwd 4616 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π« π β π« π) |
53 | 51, 52 | sstrd 3993 |
. . . . . . . . . . . . . . . . . 18
β’ (π β πΉ β π« π) |
54 | 1 | fvexi 6906 |
. . . . . . . . . . . . . . . . . . 19
β’ π β V |
55 | 54 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π β V) |
56 | | fbasweak 23369 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΉ β (fBasβπ) β§ πΉ β π« π β§ π β V) β πΉ β (fBasβπ)) |
57 | 49, 53, 55, 56 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
β’ (π β πΉ β (fBasβπ)) |
58 | 57 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π < (π΄π·π)) β πΉ β (fBasβπ)) |
59 | | fgcl 23382 |
. . . . . . . . . . . . . . . 16
β’ (πΉ β (fBasβπ) β (πfilGenπΉ) β (Filβπ)) |
60 | 58, 59 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π < (π΄π·π)) β (πfilGenπΉ) β (Filβπ)) |
61 | | ssfg 23376 |
. . . . . . . . . . . . . . . . 17
β’ (πΉ β (fBasβπ) β πΉ β (πfilGenπΉ)) |
62 | 58, 61 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π < (π΄π·π)) β πΉ β (πfilGenπΉ)) |
63 | | minvec.t |
. . . . . . . . . . . . . . . . . . 19
β’ π = (((((π΄π·π) + π) / 2)β2) β (πβ2)) |
64 | 31, 33 | readdcld 11243 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β ((π΄π·π) + π) β β) |
65 | 64 | rehalfcld 12459 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (((π΄π·π) + π) / 2) β β) |
66 | 65 | resqcld 14090 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β ((((π΄π·π) + π) / 2)β2) β
β) |
67 | 33 | resqcld 14090 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (πβ2) β β) |
68 | 66, 67 | resubcld 11642 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (((((π΄π·π) + π) / 2)β2) β (πβ2)) β β) |
69 | 68 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π < (π΄π·π)) β (((((π΄π·π) + π) / 2)β2) β (πβ2)) β β) |
70 | 33, 31, 33 | ltadd1d 11807 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (π < (π΄π·π) β (π + π) < ((π΄π·π) + π))) |
71 | 33 | recnd 11242 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β π β β) |
72 | 71 | 2timesd 12455 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (2 Β· π) = (π + π)) |
73 | 72 | breq1d 5159 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β ((2 Β· π) < ((π΄π·π) + π) β (π + π) < ((π΄π·π) + π))) |
74 | | 2re 12286 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ 2 β
β |
75 | | 2pos 12315 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ 0 <
2 |
76 | 74, 75 | pm3.2i 472 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (2 β
β β§ 0 < 2) |
77 | 76 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (2 β β β§ 0
< 2)) |
78 | | ltmuldiv2 12088 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β β β§ ((π΄π·π) + π) β β β§ (2 β β
β§ 0 < 2)) β ((2 Β· π) < ((π΄π·π) + π) β π < (((π΄π·π) + π) / 2))) |
79 | 33, 64, 77, 78 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β ((2 Β· π) < ((π΄π·π) + π) β π < (((π΄π·π) + π) / 2))) |
80 | 70, 73, 79 | 3bitr2d 307 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (π < (π΄π·π) β π < (((π΄π·π) + π) / 2))) |
81 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | minveclem1 24941 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β (π
β β β§ π
β β
β§ βπ€ β π
0 β€ π€)) |
82 | 81 | simp3d 1145 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β βπ€ β π
0 β€ π€) |
83 | 81 | simp1d 1143 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β π
β β) |
84 | 81 | simp2d 1144 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β π
β β
) |
85 | | 0re 11216 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ 0 β
β |
86 | | breq1 5152 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π₯ = 0 β (π₯ β€ π€ β 0 β€ π€)) |
87 | 86 | ralbidv 3178 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π₯ = 0 β (βπ€ β π
π₯ β€ π€ β βπ€ β π
0 β€ π€)) |
88 | 87 | rspcev 3613 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((0
β β β§ βπ€ β π
0 β€ π€) β βπ₯ β β βπ€ β π
π₯ β€ π€) |
89 | 85, 82, 88 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β βπ₯ β β βπ€ β π
π₯ β€ π€) |
90 | 85 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β 0 β
β) |
91 | | infregelb 12198 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π
β β β§ π
β β
β§ βπ₯ β β βπ€ β π
π₯ β€ π€) β§ 0 β β) β (0 β€
inf(π
, β, < )
β βπ€ β
π
0 β€ π€)) |
92 | 83, 84, 89, 90, 91 | syl31anc 1374 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β (0 β€ inf(π
, β, < ) β
βπ€ β π
0 β€ π€)) |
93 | 82, 92 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β 0 β€ inf(π
, β, <
)) |
94 | 93, 10 | breqtrrdi 5191 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β 0 β€ π) |
95 | | metge0 23851 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π· β (Metβπ) β§ π΄ β π β§ π β π) β 0 β€ (π΄π·π)) |
96 | 29, 7, 17, 95 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β 0 β€ (π΄π·π)) |
97 | 31, 33, 96, 94 | addge0d 11790 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β 0 β€ ((π΄π·π) + π)) |
98 | | divge0 12083 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((π΄π·π) + π) β β β§ 0 β€ ((π΄π·π) + π)) β§ (2 β β β§ 0 < 2))
β 0 β€ (((π΄π·π) + π) / 2)) |
99 | 64, 97, 77, 98 | syl21anc 837 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β 0 β€ (((π΄π·π) + π) / 2)) |
100 | 33, 65, 94, 99 | lt2sqd 14219 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (π < (((π΄π·π) + π) / 2) β (πβ2) < ((((π΄π·π) + π) / 2)β2))) |
101 | 67, 66 | posdifd 11801 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β ((πβ2) < ((((π΄π·π) + π) / 2)β2) β 0 < (((((π΄π·π) + π) / 2)β2) β (πβ2)))) |
102 | 80, 100, 101 | 3bitrd 305 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (π < (π΄π·π) β 0 < (((((π΄π·π) + π) / 2)β2) β (πβ2)))) |
103 | 102 | biimpa 478 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π < (π΄π·π)) β 0 < (((((π΄π·π) + π) / 2)β2) β (πβ2))) |
104 | 69, 103 | elrpd 13013 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π < (π΄π·π)) β (((((π΄π·π) + π) / 2)β2) β (πβ2)) β
β+) |
105 | 63, 104 | eqeltrid 2838 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π < (π΄π·π)) β π β
β+) |
106 | 5 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π < (π΄π·π)) β π β (LSubSpβπ)) |
107 | | rabexg 5332 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (LSubSpβπ) β {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + π)} β V) |
108 | 106, 107 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π < (π΄π·π)) β {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + π)} β V) |
109 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β+
β¦ {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + π)}) = (π β β+ β¦ {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + π)}) |
110 | | oveq2 7417 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π β ((πβ2) + π) = ((πβ2) + π)) |
111 | 110 | breq2d 5161 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β (((π΄π·π¦)β2) β€ ((πβ2) + π) β ((π΄π·π¦)β2) β€ ((πβ2) + π))) |
112 | 111 | rabbidv 3441 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + π)} = {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + π)}) |
113 | 109, 112 | elrnmpt1s 5957 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β+
β§ {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + π)} β V) β {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + π)} β ran (π β β+ β¦ {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + π)})) |
114 | 105, 108,
113 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π < (π΄π·π)) β {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + π)} β ran (π β β+ β¦ {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + π)})) |
115 | 114, 12 | eleqtrrdi 2845 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π < (π΄π·π)) β {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + π)} β πΉ) |
116 | 62, 115 | sseldd 3984 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π < (π΄π·π)) β {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + π)} β (πfilGenπΉ)) |
117 | | ssrab2 4078 |
. . . . . . . . . . . . . . . 16
β’ {π¦ β π β£ (π΄π·π¦) β€ (((π΄π·π) + π) / 2)} β π |
118 | 117 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π < (π΄π·π)) β {π¦ β π β£ (π΄π·π¦) β€ (((π΄π·π) + π) / 2)} β π) |
119 | 63 | oveq2i 7420 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πβ2) + π) = ((πβ2) + (((((π΄π·π) + π) / 2)β2) β (πβ2))) |
120 | 67 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π < (π΄π·π)) β§ π¦ β π) β (πβ2) β β) |
121 | 120 | recnd 11242 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π < (π΄π·π)) β§ π¦ β π) β (πβ2) β β) |
122 | 65 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ π < (π΄π·π)) β§ π¦ β π) β (((π΄π·π) + π) / 2) β β) |
123 | 122 | resqcld 14090 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π < (π΄π·π)) β§ π¦ β π) β ((((π΄π·π) + π) / 2)β2) β
β) |
124 | 123 | recnd 11242 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π < (π΄π·π)) β§ π¦ β π) β ((((π΄π·π) + π) / 2)β2) β
β) |
125 | 121, 124 | pncan3d 11574 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π < (π΄π·π)) β§ π¦ β π) β ((πβ2) + (((((π΄π·π) + π) / 2)β2) β (πβ2))) = ((((π΄π·π) + π) / 2)β2)) |
126 | 119, 125 | eqtrid 2785 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π < (π΄π·π)) β§ π¦ β π) β ((πβ2) + π) = ((((π΄π·π) + π) / 2)β2)) |
127 | 126 | breq2d 5161 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π < (π΄π·π)) β§ π¦ β π) β (((π΄π·π¦)β2) β€ ((πβ2) + π) β ((π΄π·π¦)β2) β€ ((((π΄π·π) + π) / 2)β2))) |
128 | 29 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π < (π΄π·π)) β§ π¦ β π) β π· β (Metβπ)) |
129 | 7 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π < (π΄π·π)) β§ π¦ β π) β π΄ β π) |
130 | 43 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π < (π΄π·π)) β§ π¦ β π) β π¦ β π) |
131 | | metcl 23838 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π· β (Metβπ) β§ π΄ β π β§ π¦ β π) β (π΄π·π¦) β β) |
132 | 128, 129,
130, 131 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π < (π΄π·π)) β§ π¦ β π) β (π΄π·π¦) β β) |
133 | | metge0 23851 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π· β (Metβπ) β§ π΄ β π β§ π¦ β π) β 0 β€ (π΄π·π¦)) |
134 | 128, 129,
130, 133 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π < (π΄π·π)) β§ π¦ β π) β 0 β€ (π΄π·π¦)) |
135 | 99 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π < (π΄π·π)) β§ π¦ β π) β 0 β€ (((π΄π·π) + π) / 2)) |
136 | 132, 122,
134, 135 | le2sqd 14220 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π < (π΄π·π)) β§ π¦ β π) β ((π΄π·π¦) β€ (((π΄π·π) + π) / 2) β ((π΄π·π¦)β2) β€ ((((π΄π·π) + π) / 2)β2))) |
137 | 127, 136 | bitr4d 282 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π < (π΄π·π)) β§ π¦ β π) β (((π΄π·π¦)β2) β€ ((πβ2) + π) β (π΄π·π¦) β€ (((π΄π·π) + π) / 2))) |
138 | 137 | rabbidva 3440 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π < (π΄π·π)) β {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + π)} = {π¦ β π β£ (π΄π·π¦) β€ (((π΄π·π) + π) / 2)}) |
139 | 42 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π < (π΄π·π)) β π β π) |
140 | | rabss2 4076 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β {π¦ β π β£ (π΄π·π¦) β€ (((π΄π·π) + π) / 2)} β {π¦ β π β£ (π΄π·π¦) β€ (((π΄π·π) + π) / 2)}) |
141 | 139, 140 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π < (π΄π·π)) β {π¦ β π β£ (π΄π·π¦) β€ (((π΄π·π) + π) / 2)} β {π¦ β π β£ (π΄π·π¦) β€ (((π΄π·π) + π) / 2)}) |
142 | 138, 141 | eqsstrd 4021 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π < (π΄π·π)) β {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + π)} β {π¦ β π β£ (π΄π·π¦) β€ (((π΄π·π) + π) / 2)}) |
143 | | filss 23357 |
. . . . . . . . . . . . . . 15
β’ (((πfilGenπΉ) β (Filβπ) β§ ({π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + π)} β (πfilGenπΉ) β§ {π¦ β π β£ (π΄π·π¦) β€ (((π΄π·π) + π) / 2)} β π β§ {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + π)} β {π¦ β π β£ (π΄π·π¦) β€ (((π΄π·π) + π) / 2)})) β {π¦ β π β£ (π΄π·π¦) β€ (((π΄π·π) + π) / 2)} β (πfilGenπΉ)) |
144 | 60, 116, 118, 142, 143 | syl13anc 1373 |
. . . . . . . . . . . . . 14
β’ ((π β§ π < (π΄π·π)) β {π¦ β π β£ (π΄π·π¦) β€ (((π΄π·π) + π) / 2)} β (πfilGenπΉ)) |
145 | | flimclsi 23482 |
. . . . . . . . . . . . . 14
β’ ({π¦ β π β£ (π΄π·π¦) β€ (((π΄π·π) + π) / 2)} β (πfilGenπΉ) β (π½ fLim (πfilGenπΉ)) β ((clsβπ½)β{π¦ β π β£ (π΄π·π¦) β€ (((π΄π·π) + π) / 2)})) |
146 | 144, 145 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β§ π < (π΄π·π)) β (π½ fLim (πfilGenπΉ)) β ((clsβπ½)β{π¦ β π β£ (π΄π·π¦) β€ (((π΄π·π) + π) / 2)})) |
147 | 14 | elin1d 4199 |
. . . . . . . . . . . . . 14
β’ (π β π β (π½ fLim (πfilGenπΉ))) |
148 | 147 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π < (π΄π·π)) β π β (π½ fLim (πfilGenπΉ))) |
149 | 146, 148 | sseldd 3984 |
. . . . . . . . . . . 12
β’ ((π β§ π < (π΄π·π)) β π β ((clsβπ½)β{π¦ β π β£ (π΄π·π¦) β€ (((π΄π·π) + π) / 2)})) |
150 | | ngpxms 24110 |
. . . . . . . . . . . . . . . . 17
β’ (π β NrmGrp β π β
βMetSp) |
151 | 1, 11 | xmsxmet 23962 |
. . . . . . . . . . . . . . . . 17
β’ (π β βMetSp β
π· β
(βMetβπ)) |
152 | 21, 150, 151 | 3syl 18 |
. . . . . . . . . . . . . . . 16
β’ (π β π· β (βMetβπ)) |
153 | 152 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π < (π΄π·π)) β π· β (βMetβπ)) |
154 | 7 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π < (π΄π·π)) β π΄ β π) |
155 | 65 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π < (π΄π·π)) β (((π΄π·π) + π) / 2) β β) |
156 | 155 | rexrd 11264 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π < (π΄π·π)) β (((π΄π·π) + π) / 2) β
β*) |
157 | | eqid 2733 |
. . . . . . . . . . . . . . . 16
β’
(MetOpenβπ·) =
(MetOpenβπ·) |
158 | | eqid 2733 |
. . . . . . . . . . . . . . . 16
β’ {π¦ β π β£ (π΄π·π¦) β€ (((π΄π·π) + π) / 2)} = {π¦ β π β£ (π΄π·π¦) β€ (((π΄π·π) + π) / 2)} |
159 | 157, 158 | blcld 24014 |
. . . . . . . . . . . . . . 15
β’ ((π· β (βMetβπ) β§ π΄ β π β§ (((π΄π·π) + π) / 2) β β*) β
{π¦ β π β£ (π΄π·π¦) β€ (((π΄π·π) + π) / 2)} β
(Clsdβ(MetOpenβπ·))) |
160 | 153, 154,
156, 159 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ ((π β§ π < (π΄π·π)) β {π¦ β π β£ (π΄π·π¦) β€ (((π΄π·π) + π) / 2)} β
(Clsdβ(MetOpenβπ·))) |
161 | 8, 1, 11 | xmstopn 23957 |
. . . . . . . . . . . . . . . . 17
β’ (π β βMetSp β
π½ = (MetOpenβπ·)) |
162 | 21, 150, 161 | 3syl 18 |
. . . . . . . . . . . . . . . 16
β’ (π β π½ = (MetOpenβπ·)) |
163 | 162 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π < (π΄π·π)) β π½ = (MetOpenβπ·)) |
164 | 163 | fveq2d 6896 |
. . . . . . . . . . . . . 14
β’ ((π β§ π < (π΄π·π)) β (Clsdβπ½) = (Clsdβ(MetOpenβπ·))) |
165 | 160, 164 | eleqtrrd 2837 |
. . . . . . . . . . . . 13
β’ ((π β§ π < (π΄π·π)) β {π¦ β π β£ (π΄π·π¦) β€ (((π΄π·π) + π) / 2)} β (Clsdβπ½)) |
166 | | cldcls 22546 |
. . . . . . . . . . . . 13
β’ ({π¦ β π β£ (π΄π·π¦) β€ (((π΄π·π) + π) / 2)} β (Clsdβπ½) β ((clsβπ½)β{π¦ β π β£ (π΄π·π¦) β€ (((π΄π·π) + π) / 2)}) = {π¦ β π β£ (π΄π·π¦) β€ (((π΄π·π) + π) / 2)}) |
167 | 165, 166 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ π < (π΄π·π)) β ((clsβπ½)β{π¦ β π β£ (π΄π·π¦) β€ (((π΄π·π) + π) / 2)}) = {π¦ β π β£ (π΄π·π¦) β€ (((π΄π·π) + π) / 2)}) |
168 | 149, 167 | eleqtrd 2836 |
. . . . . . . . . . 11
β’ ((π β§ π < (π΄π·π)) β π β {π¦ β π β£ (π΄π·π¦) β€ (((π΄π·π) + π) / 2)}) |
169 | | oveq2 7417 |
. . . . . . . . . . . . . 14
β’ (π¦ = π β (π΄π·π¦) = (π΄π·π)) |
170 | 169 | breq1d 5159 |
. . . . . . . . . . . . 13
β’ (π¦ = π β ((π΄π·π¦) β€ (((π΄π·π) + π) / 2) β (π΄π·π) β€ (((π΄π·π) + π) / 2))) |
171 | 170 | elrab 3684 |
. . . . . . . . . . . 12
β’ (π β {π¦ β π β£ (π΄π·π¦) β€ (((π΄π·π) + π) / 2)} β (π β π β§ (π΄π·π) β€ (((π΄π·π) + π) / 2))) |
172 | 171 | simprbi 498 |
. . . . . . . . . . 11
β’ (π β {π¦ β π β£ (π΄π·π¦) β€ (((π΄π·π) + π) / 2)} β (π΄π·π) β€ (((π΄π·π) + π) / 2)) |
173 | 168, 172 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π < (π΄π·π)) β (π΄π·π) β€ (((π΄π·π) + π) / 2)) |
174 | 31, 33, 31 | leadd2d 11809 |
. . . . . . . . . . . 12
β’ (π β ((π΄π·π) β€ π β ((π΄π·π) + (π΄π·π)) β€ ((π΄π·π) + π))) |
175 | 31 | recnd 11242 |
. . . . . . . . . . . . . 14
β’ (π β (π΄π·π) β β) |
176 | 175 | 2timesd 12455 |
. . . . . . . . . . . . 13
β’ (π β (2 Β· (π΄π·π)) = ((π΄π·π) + (π΄π·π))) |
177 | 176 | breq1d 5159 |
. . . . . . . . . . . 12
β’ (π β ((2 Β· (π΄π·π)) β€ ((π΄π·π) + π) β ((π΄π·π) + (π΄π·π)) β€ ((π΄π·π) + π))) |
178 | | lemuldiv2 12095 |
. . . . . . . . . . . . . 14
β’ (((π΄π·π) β β β§ ((π΄π·π) + π) β β β§ (2 β β
β§ 0 < 2)) β ((2 Β· (π΄π·π)) β€ ((π΄π·π) + π) β (π΄π·π) β€ (((π΄π·π) + π) / 2))) |
179 | 76, 178 | mp3an3 1451 |
. . . . . . . . . . . . 13
β’ (((π΄π·π) β β β§ ((π΄π·π) + π) β β) β ((2 Β· (π΄π·π)) β€ ((π΄π·π) + π) β (π΄π·π) β€ (((π΄π·π) + π) / 2))) |
180 | 31, 64, 179 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π β ((2 Β· (π΄π·π)) β€ ((π΄π·π) + π) β (π΄π·π) β€ (((π΄π·π) + π) / 2))) |
181 | 174, 177,
180 | 3bitr2d 307 |
. . . . . . . . . . 11
β’ (π β ((π΄π·π) β€ π β (π΄π·π) β€ (((π΄π·π) + π) / 2))) |
182 | 181 | biimpar 479 |
. . . . . . . . . 10
β’ ((π β§ (π΄π·π) β€ (((π΄π·π) + π) / 2)) β (π΄π·π) β€ π) |
183 | 173, 182 | syldan 592 |
. . . . . . . . 9
β’ ((π β§ π < (π΄π·π)) β (π΄π·π) β€ π) |
184 | 183 | ex 414 |
. . . . . . . 8
β’ (π β (π < (π΄π·π) β (π΄π·π) β€ π)) |
185 | 48, 184 | sylbird 260 |
. . . . . . 7
β’ (π β (Β¬ (π΄π·π) β€ π β (π΄π·π) β€ π)) |
186 | 185 | pm2.18d 127 |
. . . . . 6
β’ (π β (π΄π·π) β€ π) |
187 | 186 | adantr 482 |
. . . . 5
β’ ((π β§ π¦ β π) β (π΄π·π) β€ π) |
188 | 83 | adantr 482 |
. . . . . . 7
β’ ((π β§ π¦ β π) β π
β β) |
189 | 89 | adantr 482 |
. . . . . . 7
β’ ((π β§ π¦ β π) β βπ₯ β β βπ€ β π
π₯ β€ π€) |
190 | | simpr 486 |
. . . . . . . . 9
β’ ((π β§ π¦ β π) β π¦ β π) |
191 | | fvex 6905 |
. . . . . . . . 9
β’ (πβ(π΄ β π¦)) β V |
192 | | eqid 2733 |
. . . . . . . . . 10
β’ (π¦ β π β¦ (πβ(π΄ β π¦))) = (π¦ β π β¦ (πβ(π΄ β π¦))) |
193 | 192 | elrnmpt1 5958 |
. . . . . . . . 9
β’ ((π¦ β π β§ (πβ(π΄ β π¦)) β V) β (πβ(π΄ β π¦)) β ran (π¦ β π β¦ (πβ(π΄ β π¦)))) |
194 | 190, 191,
193 | sylancl 587 |
. . . . . . . 8
β’ ((π β§ π¦ β π) β (πβ(π΄ β π¦)) β ran (π¦ β π β¦ (πβ(π΄ β π¦)))) |
195 | 194, 9 | eleqtrrdi 2845 |
. . . . . . 7
β’ ((π β§ π¦ β π) β (πβ(π΄ β π¦)) β π
) |
196 | | infrelb 12199 |
. . . . . . 7
β’ ((π
β β β§
βπ₯ β β
βπ€ β π
π₯ β€ π€ β§ (πβ(π΄ β π¦)) β π
) β inf(π
, β, < ) β€ (πβ(π΄ β π¦))) |
197 | 188, 189,
195, 196 | syl3anc 1372 |
. . . . . 6
β’ ((π β§ π¦ β π) β inf(π
, β, < ) β€ (πβ(π΄ β π¦))) |
198 | 10, 197 | eqbrtrid 5184 |
. . . . 5
β’ ((π β§ π¦ β π) β π β€ (πβ(π΄ β π¦))) |
199 | 32, 34, 47, 187, 198 | letrd 11371 |
. . . 4
β’ ((π β§ π¦ β π) β (π΄π·π) β€ (πβ(π΄ β π¦))) |
200 | 26, 199 | eqbrtrrd 5173 |
. . 3
β’ ((π β§ π¦ β π) β (πβ(π΄ β π)) β€ (πβ(π΄ β π¦))) |
201 | 200 | ralrimiva 3147 |
. 2
β’ (π β βπ¦ β π (πβ(π΄ β π)) β€ (πβ(π΄ β π¦))) |
202 | | oveq2 7417 |
. . . . . 6
β’ (π₯ = π β (π΄ β π₯) = (π΄ β π)) |
203 | 202 | fveq2d 6896 |
. . . . 5
β’ (π₯ = π β (πβ(π΄ β π₯)) = (πβ(π΄ β π))) |
204 | 203 | breq1d 5159 |
. . . 4
β’ (π₯ = π β ((πβ(π΄ β π₯)) β€ (πβ(π΄ β π¦)) β (πβ(π΄ β π)) β€ (πβ(π΄ β π¦)))) |
205 | 204 | ralbidv 3178 |
. . 3
β’ (π₯ = π β (βπ¦ β π (πβ(π΄ β π₯)) β€ (πβ(π΄ β π¦)) β βπ¦ β π (πβ(π΄ β π)) β€ (πβ(π΄ β π¦)))) |
206 | 205 | rspcev 3613 |
. 2
β’ ((π β π β§ βπ¦ β π (πβ(π΄ β π)) β€ (πβ(π΄ β π¦))) β βπ₯ β π βπ¦ β π (πβ(π΄ β π₯)) β€ (πβ(π΄ β π¦))) |
207 | 15, 201, 206 | syl2anc 585 |
1
β’ (π β βπ₯ β π βπ¦ β π (πβ(π΄ β π₯)) β€ (πβ(π΄ β π¦))) |