Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. . . . . . . . 9
β’ ((π β§ π β β+) β π β
β+) |
2 | | 2z 12542 |
. . . . . . . . 9
β’ 2 β
β€ |
3 | | rpexpcl 13993 |
. . . . . . . . 9
β’ ((π β β+
β§ 2 β β€) β (π β2) β
β+) |
4 | 1, 2, 3 | sylancl 587 |
. . . . . . . 8
β’ ((π β§ π β β+) β (π β2) β
β+) |
5 | 4 | rphalfcld 12976 |
. . . . . . 7
β’ ((π β§ π β β+) β ((π β2) / 2) β
β+) |
6 | | 4nn 12243 |
. . . . . . . 8
β’ 4 β
β |
7 | | nnrp 12933 |
. . . . . . . 8
β’ (4 β
β β 4 β β+) |
8 | 6, 7 | ax-mp 5 |
. . . . . . 7
β’ 4 β
β+ |
9 | | rpdivcl 12947 |
. . . . . . 7
β’ ((((π β2) / 2) β
β+ β§ 4 β β+) β (((π β2) / 2) / 4) β
β+) |
10 | 5, 8, 9 | sylancl 587 |
. . . . . 6
β’ ((π β§ π β β+) β (((π β2) / 2) / 4) β
β+) |
11 | | minvec.y |
. . . . . . . 8
β’ (π β π β (LSubSpβπ)) |
12 | 11 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β β+) β π β (LSubSpβπ)) |
13 | | rabexg 5293 |
. . . . . . 7
β’ (π β (LSubSpβπ) β {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + (((π β2) / 2) / 4))} β
V) |
14 | 12, 13 | syl 17 |
. . . . . 6
β’ ((π β§ π β β+) β {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + (((π β2) / 2) / 4))} β
V) |
15 | | eqid 2737 |
. . . . . . 7
β’ (π β β+
β¦ {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + π)}) = (π β β+ β¦ {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + π)}) |
16 | | oveq2 7370 |
. . . . . . . . 9
β’ (π = (((π β2) / 2) / 4) β ((πβ2) + π) = ((πβ2) + (((π β2) / 2) / 4))) |
17 | 16 | breq2d 5122 |
. . . . . . . 8
β’ (π = (((π β2) / 2) / 4) β (((π΄π·π¦)β2) β€ ((πβ2) + π) β ((π΄π·π¦)β2) β€ ((πβ2) + (((π β2) / 2) / 4)))) |
18 | 17 | rabbidv 3418 |
. . . . . . 7
β’ (π = (((π β2) / 2) / 4) β {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + π)} = {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + (((π β2) / 2) / 4))}) |
19 | 15, 18 | elrnmpt1s 5917 |
. . . . . 6
β’
(((((π β2) / 2)
/ 4) β β+ β§ {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + (((π β2) / 2) / 4))} β V) β {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + (((π β2) / 2) / 4))} β ran (π β β+
β¦ {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + π)})) |
20 | 10, 14, 19 | syl2anc 585 |
. . . . 5
β’ ((π β§ π β β+) β {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + (((π β2) / 2) / 4))} β ran (π β β+
β¦ {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + π)})) |
21 | | minvec.f |
. . . . 5
β’ πΉ = ran (π β β+ β¦ {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + π)}) |
22 | 20, 21 | eleqtrrdi 2849 |
. . . 4
β’ ((π β§ π β β+) β {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + (((π β2) / 2) / 4))} β πΉ) |
23 | | oveq2 7370 |
. . . . . . . . . 10
β’ (π¦ = π’ β (π΄π·π¦) = (π΄π·π’)) |
24 | 23 | oveq1d 7377 |
. . . . . . . . 9
β’ (π¦ = π’ β ((π΄π·π¦)β2) = ((π΄π·π’)β2)) |
25 | 24 | breq1d 5120 |
. . . . . . . 8
β’ (π¦ = π’ β (((π΄π·π¦)β2) β€ ((πβ2) + (((π β2) / 2) / 4)) β ((π΄π·π’)β2) β€ ((πβ2) + (((π β2) / 2) / 4)))) |
26 | 25 | elrab 3650 |
. . . . . . 7
β’ (π’ β {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + (((π β2) / 2) / 4))} β (π’ β π β§ ((π΄π·π’)β2) β€ ((πβ2) + (((π β2) / 2) / 4)))) |
27 | | oveq2 7370 |
. . . . . . . . . 10
β’ (π¦ = π£ β (π΄π·π¦) = (π΄π·π£)) |
28 | 27 | oveq1d 7377 |
. . . . . . . . 9
β’ (π¦ = π£ β ((π΄π·π¦)β2) = ((π΄π·π£)β2)) |
29 | 28 | breq1d 5120 |
. . . . . . . 8
β’ (π¦ = π£ β (((π΄π·π¦)β2) β€ ((πβ2) + (((π β2) / 2) / 4)) β ((π΄π·π£)β2) β€ ((πβ2) + (((π β2) / 2) / 4)))) |
30 | 29 | elrab 3650 |
. . . . . . 7
β’ (π£ β {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + (((π β2) / 2) / 4))} β (π£ β π β§ ((π΄π·π£)β2) β€ ((πβ2) + (((π β2) / 2) / 4)))) |
31 | 26, 30 | anbi12i 628 |
. . . . . 6
β’ ((π’ β {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + (((π β2) / 2) / 4))} β§ π£ β {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + (((π β2) / 2) / 4))}) β ((π’ β π β§ ((π΄π·π’)β2) β€ ((πβ2) + (((π β2) / 2) / 4))) β§ (π£ β π β§ ((π΄π·π£)β2) β€ ((πβ2) + (((π β2) / 2) / 4))))) |
32 | | simprll 778 |
. . . . . . . 8
β’ (((π β§ π β β+) β§ ((π’ β π β§ ((π΄π·π’)β2) β€ ((πβ2) + (((π β2) / 2) / 4))) β§ (π£ β π β§ ((π΄π·π£)β2) β€ ((πβ2) + (((π β2) / 2) / 4))))) β π’ β π) |
33 | | simprrl 780 |
. . . . . . . 8
β’ (((π β§ π β β+) β§ ((π’ β π β§ ((π΄π·π’)β2) β€ ((πβ2) + (((π β2) / 2) / 4))) β§ (π£ β π β§ ((π΄π·π£)β2) β€ ((πβ2) + (((π β2) / 2) / 4))))) β π£ β π) |
34 | 32, 33 | ovresd 7526 |
. . . . . . 7
β’ (((π β§ π β β+) β§ ((π’ β π β§ ((π΄π·π’)β2) β€ ((πβ2) + (((π β2) / 2) / 4))) β§ (π£ β π β§ ((π΄π·π£)β2) β€ ((πβ2) + (((π β2) / 2) / 4))))) β (π’(π· βΎ (π Γ π))π£) = (π’π·π£)) |
35 | | minvec.u |
. . . . . . . . . . . . 13
β’ (π β π β βPreHil) |
36 | | cphngp 24553 |
. . . . . . . . . . . . 13
β’ (π β βPreHil β
π β
NrmGrp) |
37 | | ngpms 23972 |
. . . . . . . . . . . . 13
β’ (π β NrmGrp β π β MetSp) |
38 | | minvec.x |
. . . . . . . . . . . . . 14
β’ π = (Baseβπ) |
39 | | minvec.d |
. . . . . . . . . . . . . 14
β’ π· = ((distβπ) βΎ (π Γ π)) |
40 | 38, 39 | msmet 23826 |
. . . . . . . . . . . . 13
β’ (π β MetSp β π· β (Metβπ)) |
41 | 35, 36, 37, 40 | 4syl 19 |
. . . . . . . . . . . 12
β’ (π β π· β (Metβπ)) |
42 | 41 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π β β+) β§ ((π’ β π β§ ((π΄π·π’)β2) β€ ((πβ2) + (((π β2) / 2) / 4))) β§ (π£ β π β§ ((π΄π·π£)β2) β€ ((πβ2) + (((π β2) / 2) / 4))))) β π· β (Metβπ)) |
43 | | eqid 2737 |
. . . . . . . . . . . . . . 15
β’
(LSubSpβπ) =
(LSubSpβπ) |
44 | 38, 43 | lssss 20413 |
. . . . . . . . . . . . . 14
β’ (π β (LSubSpβπ) β π β π) |
45 | 11, 44 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β π β π) |
46 | 45 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π β β+) β§ ((π’ β π β§ ((π΄π·π’)β2) β€ ((πβ2) + (((π β2) / 2) / 4))) β§ (π£ β π β§ ((π΄π·π£)β2) β€ ((πβ2) + (((π β2) / 2) / 4))))) β π β π) |
47 | 46, 32 | sseldd 3950 |
. . . . . . . . . . 11
β’ (((π β§ π β β+) β§ ((π’ β π β§ ((π΄π·π’)β2) β€ ((πβ2) + (((π β2) / 2) / 4))) β§ (π£ β π β§ ((π΄π·π£)β2) β€ ((πβ2) + (((π β2) / 2) / 4))))) β π’ β π) |
48 | 46, 33 | sseldd 3950 |
. . . . . . . . . . 11
β’ (((π β§ π β β+) β§ ((π’ β π β§ ((π΄π·π’)β2) β€ ((πβ2) + (((π β2) / 2) / 4))) β§ (π£ β π β§ ((π΄π·π£)β2) β€ ((πβ2) + (((π β2) / 2) / 4))))) β π£ β π) |
49 | | metcl 23701 |
. . . . . . . . . . 11
β’ ((π· β (Metβπ) β§ π’ β π β§ π£ β π) β (π’π·π£) β β) |
50 | 42, 47, 48, 49 | syl3anc 1372 |
. . . . . . . . . 10
β’ (((π β§ π β β+) β§ ((π’ β π β§ ((π΄π·π’)β2) β€ ((πβ2) + (((π β2) / 2) / 4))) β§ (π£ β π β§ ((π΄π·π£)β2) β€ ((πβ2) + (((π β2) / 2) / 4))))) β (π’π·π£) β β) |
51 | 50 | resqcld 14037 |
. . . . . . . . 9
β’ (((π β§ π β β+) β§ ((π’ β π β§ ((π΄π·π’)β2) β€ ((πβ2) + (((π β2) / 2) / 4))) β§ (π£ β π β§ ((π΄π·π£)β2) β€ ((πβ2) + (((π β2) / 2) / 4))))) β ((π’π·π£)β2) β β) |
52 | 5 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π β β+) β§ ((π’ β π β§ ((π΄π·π’)β2) β€ ((πβ2) + (((π β2) / 2) / 4))) β§ (π£ β π β§ ((π΄π·π£)β2) β€ ((πβ2) + (((π β2) / 2) / 4))))) β ((π β2) / 2) β
β+) |
53 | 52 | rpred 12964 |
. . . . . . . . 9
β’ (((π β§ π β β+) β§ ((π’ β π β§ ((π΄π·π’)β2) β€ ((πβ2) + (((π β2) / 2) / 4))) β§ (π£ β π β§ ((π΄π·π£)β2) β€ ((πβ2) + (((π β2) / 2) / 4))))) β ((π β2) / 2) β
β) |
54 | 4 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π β β+) β§ ((π’ β π β§ ((π΄π·π’)β2) β€ ((πβ2) + (((π β2) / 2) / 4))) β§ (π£ β π β§ ((π΄π·π£)β2) β€ ((πβ2) + (((π β2) / 2) / 4))))) β (π β2) β
β+) |
55 | 54 | rpred 12964 |
. . . . . . . . 9
β’ (((π β§ π β β+) β§ ((π’ β π β§ ((π΄π·π’)β2) β€ ((πβ2) + (((π β2) / 2) / 4))) β§ (π£ β π β§ ((π΄π·π£)β2) β€ ((πβ2) + (((π β2) / 2) / 4))))) β (π β2) β
β) |
56 | | minvec.m |
. . . . . . . . . . 11
β’ β =
(-gβπ) |
57 | | minvec.n |
. . . . . . . . . . 11
β’ π = (normβπ) |
58 | 35 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π β β+) β§ ((π’ β π β§ ((π΄π·π’)β2) β€ ((πβ2) + (((π β2) / 2) / 4))) β§ (π£ β π β§ ((π΄π·π£)β2) β€ ((πβ2) + (((π β2) / 2) / 4))))) β π β
βPreHil) |
59 | 11 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π β β+) β§ ((π’ β π β§ ((π΄π·π’)β2) β€ ((πβ2) + (((π β2) / 2) / 4))) β§ (π£ β π β§ ((π΄π·π£)β2) β€ ((πβ2) + (((π β2) / 2) / 4))))) β π β (LSubSpβπ)) |
60 | | minvec.w |
. . . . . . . . . . . 12
β’ (π β (π βΎs π) β CMetSp) |
61 | 60 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π β β+) β§ ((π’ β π β§ ((π΄π·π’)β2) β€ ((πβ2) + (((π β2) / 2) / 4))) β§ (π£ β π β§ ((π΄π·π£)β2) β€ ((πβ2) + (((π β2) / 2) / 4))))) β (π βΎs π) β
CMetSp) |
62 | | minvec.a |
. . . . . . . . . . . 12
β’ (π β π΄ β π) |
63 | 62 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π β β+) β§ ((π’ β π β§ ((π΄π·π’)β2) β€ ((πβ2) + (((π β2) / 2) / 4))) β§ (π£ β π β§ ((π΄π·π£)β2) β€ ((πβ2) + (((π β2) / 2) / 4))))) β π΄ β π) |
64 | | minvec.j |
. . . . . . . . . . 11
β’ π½ = (TopOpenβπ) |
65 | | minvec.r |
. . . . . . . . . . 11
β’ π
= ran (π¦ β π β¦ (πβ(π΄ β π¦))) |
66 | | minvec.s |
. . . . . . . . . . 11
β’ π = inf(π
, β, < ) |
67 | 10 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ π β β+) β§ ((π’ β π β§ ((π΄π·π’)β2) β€ ((πβ2) + (((π β2) / 2) / 4))) β§ (π£ β π β§ ((π΄π·π£)β2) β€ ((πβ2) + (((π β2) / 2) / 4))))) β (((π β2) / 2) / 4) β
β+) |
68 | 67 | rpred 12964 |
. . . . . . . . . . 11
β’ (((π β§ π β β+) β§ ((π’ β π β§ ((π΄π·π’)β2) β€ ((πβ2) + (((π β2) / 2) / 4))) β§ (π£ β π β§ ((π΄π·π£)β2) β€ ((πβ2) + (((π β2) / 2) / 4))))) β (((π β2) / 2) / 4) β
β) |
69 | 67 | rpge0d 12968 |
. . . . . . . . . . 11
β’ (((π β§ π β β+) β§ ((π’ β π β§ ((π΄π·π’)β2) β€ ((πβ2) + (((π β2) / 2) / 4))) β§ (π£ β π β§ ((π΄π·π£)β2) β€ ((πβ2) + (((π β2) / 2) / 4))))) β 0 β€ (((π β2) / 2) /
4)) |
70 | | simprlr 779 |
. . . . . . . . . . 11
β’ (((π β§ π β β+) β§ ((π’ β π β§ ((π΄π·π’)β2) β€ ((πβ2) + (((π β2) / 2) / 4))) β§ (π£ β π β§ ((π΄π·π£)β2) β€ ((πβ2) + (((π β2) / 2) / 4))))) β ((π΄π·π’)β2) β€ ((πβ2) + (((π β2) / 2) / 4))) |
71 | | simprrr 781 |
. . . . . . . . . . 11
β’ (((π β§ π β β+) β§ ((π’ β π β§ ((π΄π·π’)β2) β€ ((πβ2) + (((π β2) / 2) / 4))) β§ (π£ β π β§ ((π΄π·π£)β2) β€ ((πβ2) + (((π β2) / 2) / 4))))) β ((π΄π·π£)β2) β€ ((πβ2) + (((π β2) / 2) / 4))) |
72 | 38, 56, 57, 58, 59, 61, 63, 64, 65, 66, 39, 68, 69, 32, 33, 70, 71 | minveclem2 24806 |
. . . . . . . . . 10
β’ (((π β§ π β β+) β§ ((π’ β π β§ ((π΄π·π’)β2) β€ ((πβ2) + (((π β2) / 2) / 4))) β§ (π£ β π β§ ((π΄π·π£)β2) β€ ((πβ2) + (((π β2) / 2) / 4))))) β ((π’π·π£)β2) β€ (4 Β· (((π β2) / 2) /
4))) |
73 | 52 | rpcnd 12966 |
. . . . . . . . . . 11
β’ (((π β§ π β β+) β§ ((π’ β π β§ ((π΄π·π’)β2) β€ ((πβ2) + (((π β2) / 2) / 4))) β§ (π£ β π β§ ((π΄π·π£)β2) β€ ((πβ2) + (((π β2) / 2) / 4))))) β ((π β2) / 2) β
β) |
74 | | 4cn 12245 |
. . . . . . . . . . . 12
β’ 4 β
β |
75 | 74 | a1i 11 |
. . . . . . . . . . 11
β’ (((π β§ π β β+) β§ ((π’ β π β§ ((π΄π·π’)β2) β€ ((πβ2) + (((π β2) / 2) / 4))) β§ (π£ β π β§ ((π΄π·π£)β2) β€ ((πβ2) + (((π β2) / 2) / 4))))) β 4 β
β) |
76 | | 4ne0 12268 |
. . . . . . . . . . . 12
β’ 4 β
0 |
77 | 76 | a1i 11 |
. . . . . . . . . . 11
β’ (((π β§ π β β+) β§ ((π’ β π β§ ((π΄π·π’)β2) β€ ((πβ2) + (((π β2) / 2) / 4))) β§ (π£ β π β§ ((π΄π·π£)β2) β€ ((πβ2) + (((π β2) / 2) / 4))))) β 4 β
0) |
78 | 73, 75, 77 | divcan2d 11940 |
. . . . . . . . . 10
β’ (((π β§ π β β+) β§ ((π’ β π β§ ((π΄π·π’)β2) β€ ((πβ2) + (((π β2) / 2) / 4))) β§ (π£ β π β§ ((π΄π·π£)β2) β€ ((πβ2) + (((π β2) / 2) / 4))))) β (4 Β·
(((π β2) / 2) / 4)) =
((π β2) /
2)) |
79 | 72, 78 | breqtrd 5136 |
. . . . . . . . 9
β’ (((π β§ π β β+) β§ ((π’ β π β§ ((π΄π·π’)β2) β€ ((πβ2) + (((π β2) / 2) / 4))) β§ (π£ β π β§ ((π΄π·π£)β2) β€ ((πβ2) + (((π β2) / 2) / 4))))) β ((π’π·π£)β2) β€ ((π β2) / 2)) |
80 | | rphalflt 12951 |
. . . . . . . . . 10
β’ ((π β2) β
β+ β ((π β2) / 2) < (π β2)) |
81 | 54, 80 | syl 17 |
. . . . . . . . 9
β’ (((π β§ π β β+) β§ ((π’ β π β§ ((π΄π·π’)β2) β€ ((πβ2) + (((π β2) / 2) / 4))) β§ (π£ β π β§ ((π΄π·π£)β2) β€ ((πβ2) + (((π β2) / 2) / 4))))) β ((π β2) / 2) < (π β2)) |
82 | 51, 53, 55, 79, 81 | lelttrd 11320 |
. . . . . . . 8
β’ (((π β§ π β β+) β§ ((π’ β π β§ ((π΄π·π’)β2) β€ ((πβ2) + (((π β2) / 2) / 4))) β§ (π£ β π β§ ((π΄π·π£)β2) β€ ((πβ2) + (((π β2) / 2) / 4))))) β ((π’π·π£)β2) < (π β2)) |
83 | | rpre 12930 |
. . . . . . . . . 10
β’ (π β β+
β π β
β) |
84 | 83 | ad2antlr 726 |
. . . . . . . . 9
β’ (((π β§ π β β+) β§ ((π’ β π β§ ((π΄π·π’)β2) β€ ((πβ2) + (((π β2) / 2) / 4))) β§ (π£ β π β§ ((π΄π·π£)β2) β€ ((πβ2) + (((π β2) / 2) / 4))))) β π β
β) |
85 | | metge0 23714 |
. . . . . . . . . 10
β’ ((π· β (Metβπ) β§ π’ β π β§ π£ β π) β 0 β€ (π’π·π£)) |
86 | 42, 47, 48, 85 | syl3anc 1372 |
. . . . . . . . 9
β’ (((π β§ π β β+) β§ ((π’ β π β§ ((π΄π·π’)β2) β€ ((πβ2) + (((π β2) / 2) / 4))) β§ (π£ β π β§ ((π΄π·π£)β2) β€ ((πβ2) + (((π β2) / 2) / 4))))) β 0 β€ (π’π·π£)) |
87 | | rpge0 12935 |
. . . . . . . . . 10
β’ (π β β+
β 0 β€ π ) |
88 | 87 | ad2antlr 726 |
. . . . . . . . 9
β’ (((π β§ π β β+) β§ ((π’ β π β§ ((π΄π·π’)β2) β€ ((πβ2) + (((π β2) / 2) / 4))) β§ (π£ β π β§ ((π΄π·π£)β2) β€ ((πβ2) + (((π β2) / 2) / 4))))) β 0 β€ π ) |
89 | 50, 84, 86, 88 | lt2sqd 14166 |
. . . . . . . 8
β’ (((π β§ π β β+) β§ ((π’ β π β§ ((π΄π·π’)β2) β€ ((πβ2) + (((π β2) / 2) / 4))) β§ (π£ β π β§ ((π΄π·π£)β2) β€ ((πβ2) + (((π β2) / 2) / 4))))) β ((π’π·π£) < π β ((π’π·π£)β2) < (π β2))) |
90 | 82, 89 | mpbird 257 |
. . . . . . 7
β’ (((π β§ π β β+) β§ ((π’ β π β§ ((π΄π·π’)β2) β€ ((πβ2) + (((π β2) / 2) / 4))) β§ (π£ β π β§ ((π΄π·π£)β2) β€ ((πβ2) + (((π β2) / 2) / 4))))) β (π’π·π£) < π ) |
91 | 34, 90 | eqbrtrd 5132 |
. . . . . 6
β’ (((π β§ π β β+) β§ ((π’ β π β§ ((π΄π·π’)β2) β€ ((πβ2) + (((π β2) / 2) / 4))) β§ (π£ β π β§ ((π΄π·π£)β2) β€ ((πβ2) + (((π β2) / 2) / 4))))) β (π’(π· βΎ (π Γ π))π£) < π ) |
92 | 31, 91 | sylan2b 595 |
. . . . 5
β’ (((π β§ π β β+) β§ (π’ β {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + (((π β2) / 2) / 4))} β§ π£ β {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + (((π β2) / 2) / 4))})) β (π’(π· βΎ (π Γ π))π£) < π ) |
93 | 92 | ralrimivva 3198 |
. . . 4
β’ ((π β§ π β β+) β
βπ’ β {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + (((π β2) / 2) / 4))}βπ£ β {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + (((π β2) / 2) / 4))} (π’(π· βΎ (π Γ π))π£) < π ) |
94 | | raleq 3312 |
. . . . . 6
β’ (π€ = {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + (((π β2) / 2) / 4))} β (βπ£ β π€ (π’(π· βΎ (π Γ π))π£) < π β βπ£ β {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + (((π β2) / 2) / 4))} (π’(π· βΎ (π Γ π))π£) < π )) |
95 | 94 | raleqbi1dv 3310 |
. . . . 5
β’ (π€ = {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + (((π β2) / 2) / 4))} β (βπ’ β π€ βπ£ β π€ (π’(π· βΎ (π Γ π))π£) < π β βπ’ β {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + (((π β2) / 2) / 4))}βπ£ β {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + (((π β2) / 2) / 4))} (π’(π· βΎ (π Γ π))π£) < π )) |
96 | 95 | rspcev 3584 |
. . . 4
β’ (({π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + (((π β2) / 2) / 4))} β πΉ β§ βπ’ β {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + (((π β2) / 2) / 4))}βπ£ β {π¦ β π β£ ((π΄π·π¦)β2) β€ ((πβ2) + (((π β2) / 2) / 4))} (π’(π· βΎ (π Γ π))π£) < π ) β βπ€ β πΉ βπ’ β π€ βπ£ β π€ (π’(π· βΎ (π Γ π))π£) < π ) |
97 | 22, 93, 96 | syl2anc 585 |
. . 3
β’ ((π β§ π β β+) β
βπ€ β πΉ βπ’ β π€ βπ£ β π€ (π’(π· βΎ (π Γ π))π£) < π ) |
98 | 97 | ralrimiva 3144 |
. 2
β’ (π β βπ β β+ βπ€ β πΉ βπ’ β π€ βπ£ β π€ (π’(π· βΎ (π Γ π))π£) < π ) |
99 | 38, 56, 57, 35, 11, 60, 62, 64, 65, 66, 39 | minveclem3a 24807 |
. . . 4
β’ (π β (π· βΎ (π Γ π)) β (CMetβπ)) |
100 | | cmetmet 24666 |
. . . 4
β’ ((π· βΎ (π Γ π)) β (CMetβπ) β (π· βΎ (π Γ π)) β (Metβπ)) |
101 | | metxmet 23703 |
. . . 4
β’ ((π· βΎ (π Γ π)) β (Metβπ) β (π· βΎ (π Γ π)) β (βMetβπ)) |
102 | 99, 100, 101 | 3syl 18 |
. . 3
β’ (π β (π· βΎ (π Γ π)) β (βMetβπ)) |
103 | 38, 56, 57, 35, 11, 60, 62, 64, 65, 66, 39, 21 | minveclem3b 24808 |
. . 3
β’ (π β πΉ β (fBasβπ)) |
104 | | fgcfil 24651 |
. . 3
β’ (((π· βΎ (π Γ π)) β (βMetβπ) β§ πΉ β (fBasβπ)) β ((πfilGenπΉ) β (CauFilβ(π· βΎ (π Γ π))) β βπ β β+ βπ€ β πΉ βπ’ β π€ βπ£ β π€ (π’(π· βΎ (π Γ π))π£) < π )) |
105 | 102, 103,
104 | syl2anc 585 |
. 2
β’ (π β ((πfilGenπΉ) β (CauFilβ(π· βΎ (π Γ π))) β βπ β β+ βπ€ β πΉ βπ’ β π€ βπ£ β π€ (π’(π· βΎ (π Γ π))π£) < π )) |
106 | 98, 105 | mpbird 257 |
1
β’ (π β (πfilGenπΉ) β (CauFilβ(π· βΎ (π Γ π)))) |