Step | Hyp | Ref
| Expression |
1 | | 4re 12242 |
. . . . . . 7
β’ 4 β
β |
2 | | 4pos 12265 |
. . . . . . 7
β’ 0 <
4 |
3 | 1, 2 | elrpii 12923 |
. . . . . 6
β’ 4 β
β+ |
4 | | simpr 486 |
. . . . . . 7
β’ ((π β§ π₯ β β+) β π₯ β
β+) |
5 | | 2z 12540 |
. . . . . . 7
β’ 2 β
β€ |
6 | | rpexpcl 13992 |
. . . . . . 7
β’ ((π₯ β β+
β§ 2 β β€) β (π₯β2) β
β+) |
7 | 4, 5, 6 | sylancl 587 |
. . . . . 6
β’ ((π β§ π₯ β β+) β (π₯β2) β
β+) |
8 | | rpdivcl 12945 |
. . . . . 6
β’ ((4
β β+ β§ (π₯β2) β β+) β
(4 / (π₯β2)) β
β+) |
9 | 3, 7, 8 | sylancr 588 |
. . . . 5
β’ ((π β§ π₯ β β+) β (4 /
(π₯β2)) β
β+) |
10 | | rprege0 12935 |
. . . . 5
β’ ((4 /
(π₯β2)) β
β+ β ((4 / (π₯β2)) β β β§ 0 β€ (4 /
(π₯β2)))) |
11 | | flge0nn0 13731 |
. . . . 5
β’ (((4 /
(π₯β2)) β β
β§ 0 β€ (4 / (π₯β2))) β (ββ(4 / (π₯β2))) β
β0) |
12 | | nn0p1nn 12457 |
. . . . 5
β’
((ββ(4 / (π₯β2))) β β0 β
((ββ(4 / (π₯β2))) + 1) β
β) |
13 | 9, 10, 11, 12 | 4syl 19 |
. . . 4
β’ ((π β§ π₯ β β+) β
((ββ(4 / (π₯β2))) + 1) β
β) |
14 | | minveco.u |
. . . . . . . . . . 11
β’ (π β π β
CPreHilOLD) |
15 | | phnv 29798 |
. . . . . . . . . . 11
β’ (π β CPreHilOLD
β π β
NrmCVec) |
16 | | minveco.x |
. . . . . . . . . . . 12
β’ π = (BaseSetβπ) |
17 | | minveco.d |
. . . . . . . . . . . 12
β’ π· = (IndMetβπ) |
18 | 16, 17 | imsmet 29675 |
. . . . . . . . . . 11
β’ (π β NrmCVec β π· β (Metβπ)) |
19 | 14, 15, 18 | 3syl 18 |
. . . . . . . . . 10
β’ (π β π· β (Metβπ)) |
20 | 19 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(4 / (π₯β2))) + 1))) β π· β (Metβπ)) |
21 | 14, 15 | syl 17 |
. . . . . . . . . . . 12
β’ (π β π β NrmCVec) |
22 | | inss1 4189 |
. . . . . . . . . . . . 13
β’
((SubSpβπ)
β© CBan) β (SubSpβπ) |
23 | | minveco.w |
. . . . . . . . . . . . 13
β’ (π β π β ((SubSpβπ) β© CBan)) |
24 | 22, 23 | sselid 3943 |
. . . . . . . . . . . 12
β’ (π β π β (SubSpβπ)) |
25 | | minveco.y |
. . . . . . . . . . . . 13
β’ π = (BaseSetβπ) |
26 | | eqid 2733 |
. . . . . . . . . . . . 13
β’
(SubSpβπ) =
(SubSpβπ) |
27 | 16, 25, 26 | sspba 29711 |
. . . . . . . . . . . 12
β’ ((π β NrmCVec β§ π β (SubSpβπ)) β π β π) |
28 | 21, 24, 27 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β π β π) |
29 | 28 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(4 / (π₯β2))) + 1))) β π β π) |
30 | | minveco.f |
. . . . . . . . . . . 12
β’ (π β πΉ:ββΆπ) |
31 | 30 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(4 / (π₯β2))) + 1))) β πΉ:ββΆπ) |
32 | 13 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(4 / (π₯β2))) + 1))) β ((ββ(4 /
(π₯β2))) + 1) β
β) |
33 | 31, 32 | ffvelcdmd 7037 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(4 / (π₯β2))) + 1))) β (πΉβ((ββ(4 / (π₯β2))) + 1)) β π) |
34 | 29, 33 | sseldd 3946 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(4 / (π₯β2))) + 1))) β (πΉβ((ββ(4 / (π₯β2))) + 1)) β π) |
35 | | eluznn 12848 |
. . . . . . . . . . . 12
β’
((((ββ(4 / (π₯β2))) + 1) β β β§ π β
(β€β₯β((ββ(4 / (π₯β2))) + 1))) β π β β) |
36 | 13, 35 | sylan 581 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(4 / (π₯β2))) + 1))) β π β β) |
37 | 31, 36 | ffvelcdmd 7037 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(4 / (π₯β2))) + 1))) β (πΉβπ) β π) |
38 | 29, 37 | sseldd 3946 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(4 / (π₯β2))) + 1))) β (πΉβπ) β π) |
39 | | metcl 23701 |
. . . . . . . . 9
β’ ((π· β (Metβπ) β§ (πΉβ((ββ(4 / (π₯β2))) + 1)) β π β§ (πΉβπ) β π) β ((πΉβ((ββ(4 / (π₯β2))) + 1))π·(πΉβπ)) β β) |
40 | 20, 34, 38, 39 | syl3anc 1372 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(4 / (π₯β2))) + 1))) β ((πΉβ((ββ(4 / (π₯β2))) + 1))π·(πΉβπ)) β β) |
41 | 40 | resqcld 14036 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(4 / (π₯β2))) + 1))) β (((πΉβ((ββ(4 / (π₯β2))) + 1))π·(πΉβπ))β2) β β) |
42 | 32 | nnrpd 12960 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(4 / (π₯β2))) + 1))) β ((ββ(4 /
(π₯β2))) + 1) β
β+) |
43 | 42 | rpreccld 12972 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(4 / (π₯β2))) + 1))) β (1 /
((ββ(4 / (π₯β2))) + 1)) β
β+) |
44 | | rpmulcl 12943 |
. . . . . . . . 9
β’ ((4
β β+ β§ (1 / ((ββ(4 / (π₯β2))) + 1)) β β+)
β (4 Β· (1 / ((ββ(4 / (π₯β2))) + 1))) β
β+) |
45 | 3, 43, 44 | sylancr 588 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(4 / (π₯β2))) + 1))) β (4 Β· (1 /
((ββ(4 / (π₯β2))) + 1))) β
β+) |
46 | 45 | rpred 12962 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(4 / (π₯β2))) + 1))) β (4 Β· (1 /
((ββ(4 / (π₯β2))) + 1))) β
β) |
47 | 7 | adantr 482 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(4 / (π₯β2))) + 1))) β (π₯β2) β
β+) |
48 | 47 | rpred 12962 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(4 / (π₯β2))) + 1))) β (π₯β2) β β) |
49 | | minveco.m |
. . . . . . . 8
β’ π = ( βπ£
βπ) |
50 | | minveco.n |
. . . . . . . 8
β’ π =
(normCVβπ) |
51 | 14 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(4 / (π₯β2))) + 1))) β π β
CPreHilOLD) |
52 | 23 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(4 / (π₯β2))) + 1))) β π β ((SubSpβπ) β© CBan)) |
53 | | minveco.a |
. . . . . . . . 9
β’ (π β π΄ β π) |
54 | 53 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(4 / (π₯β2))) + 1))) β π΄ β π) |
55 | | minveco.j |
. . . . . . . 8
β’ π½ = (MetOpenβπ·) |
56 | | minveco.r |
. . . . . . . 8
β’ π
= ran (π¦ β π β¦ (πβ(π΄ππ¦))) |
57 | | minveco.s |
. . . . . . . 8
β’ π = inf(π
, β, < ) |
58 | 13 | nnrpd 12960 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β β+) β
((ββ(4 / (π₯β2))) + 1) β
β+) |
59 | 58 | rpreccld 12972 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β+) β (1 /
((ββ(4 / (π₯β2))) + 1)) β
β+) |
60 | 59 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(4 / (π₯β2))) + 1))) β (1 /
((ββ(4 / (π₯β2))) + 1)) β
β+) |
61 | 60 | rpred 12962 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(4 / (π₯β2))) + 1))) β (1 /
((ββ(4 / (π₯β2))) + 1)) β
β) |
62 | 60 | rpge0d 12966 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(4 / (π₯β2))) + 1))) β 0 β€ (1 /
((ββ(4 / (π₯β2))) + 1))) |
63 | 30 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β+) β πΉ:ββΆπ) |
64 | 63 | ffvelcdmda 7036 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ π β β) β (πΉβπ) β π) |
65 | 36, 64 | syldan 592 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(4 / (π₯β2))) + 1))) β (πΉβπ) β π) |
66 | | fveq2 6843 |
. . . . . . . . . . . 12
β’ (π = ((ββ(4 / (π₯β2))) + 1) β (πΉβπ) = (πΉβ((ββ(4 / (π₯β2))) +
1))) |
67 | 66 | oveq2d 7374 |
. . . . . . . . . . 11
β’ (π = ((ββ(4 / (π₯β2))) + 1) β (π΄π·(πΉβπ)) = (π΄π·(πΉβ((ββ(4 / (π₯β2))) +
1)))) |
68 | 67 | oveq1d 7373 |
. . . . . . . . . 10
β’ (π = ((ββ(4 / (π₯β2))) + 1) β ((π΄π·(πΉβπ))β2) = ((π΄π·(πΉβ((ββ(4 / (π₯β2))) +
1)))β2)) |
69 | | oveq2 7366 |
. . . . . . . . . . 11
β’ (π = ((ββ(4 / (π₯β2))) + 1) β (1 /
π) = (1 /
((ββ(4 / (π₯β2))) + 1))) |
70 | 69 | oveq2d 7374 |
. . . . . . . . . 10
β’ (π = ((ββ(4 / (π₯β2))) + 1) β ((πβ2) + (1 / π)) = ((πβ2) + (1 / ((ββ(4 / (π₯β2))) +
1)))) |
71 | 68, 70 | breq12d 5119 |
. . . . . . . . 9
β’ (π = ((ββ(4 / (π₯β2))) + 1) β (((π΄π·(πΉβπ))β2) β€ ((πβ2) + (1 / π)) β ((π΄π·(πΉβ((ββ(4 / (π₯β2))) + 1)))β2) β€
((πβ2) + (1 /
((ββ(4 / (π₯β2))) + 1))))) |
72 | | minveco.1 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β ((π΄π·(πΉβπ))β2) β€ ((πβ2) + (1 / π))) |
73 | 72 | ralrimiva 3140 |
. . . . . . . . . 10
β’ (π β βπ β β ((π΄π·(πΉβπ))β2) β€ ((πβ2) + (1 / π))) |
74 | 73 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(4 / (π₯β2))) + 1))) β βπ β β ((π΄π·(πΉβπ))β2) β€ ((πβ2) + (1 / π))) |
75 | 71, 74, 32 | rspcdva 3581 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(4 / (π₯β2))) + 1))) β ((π΄π·(πΉβ((ββ(4 / (π₯β2))) + 1)))β2) β€
((πβ2) + (1 /
((ββ(4 / (π₯β2))) + 1)))) |
76 | 29, 65 | sseldd 3946 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(4 / (π₯β2))) + 1))) β (πΉβπ) β π) |
77 | | metcl 23701 |
. . . . . . . . . . 11
β’ ((π· β (Metβπ) β§ π΄ β π β§ (πΉβπ) β π) β (π΄π·(πΉβπ)) β β) |
78 | 20, 54, 76, 77 | syl3anc 1372 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(4 / (π₯β2))) + 1))) β (π΄π·(πΉβπ)) β β) |
79 | 78 | resqcld 14036 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(4 / (π₯β2))) + 1))) β ((π΄π·(πΉβπ))β2) β β) |
80 | 16, 49, 50, 25, 14, 23, 53, 17, 55, 56 | minvecolem1 29858 |
. . . . . . . . . . . . . 14
β’ (π β (π
β β β§ π
β β
β§ βπ€ β π
0 β€ π€)) |
81 | | 0re 11162 |
. . . . . . . . . . . . . . . 16
β’ 0 β
β |
82 | | breq1 5109 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = 0 β (π₯ β€ π€ β 0 β€ π€)) |
83 | 82 | ralbidv 3171 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = 0 β (βπ€ β π
π₯ β€ π€ β βπ€ β π
0 β€ π€)) |
84 | 83 | rspcev 3580 |
. . . . . . . . . . . . . . . 16
β’ ((0
β β β§ βπ€ β π
0 β€ π€) β βπ₯ β β βπ€ β π
π₯ β€ π€) |
85 | 81, 84 | mpan 689 |
. . . . . . . . . . . . . . 15
β’
(βπ€ β
π
0 β€ π€ β βπ₯ β β βπ€ β π
π₯ β€ π€) |
86 | 85 | 3anim3i 1155 |
. . . . . . . . . . . . . 14
β’ ((π
β β β§ π
β β
β§
βπ€ β π
0 β€ π€) β (π
β β β§ π
β β
β§ βπ₯ β β βπ€ β π
π₯ β€ π€)) |
87 | | infrecl 12142 |
. . . . . . . . . . . . . 14
β’ ((π
β β β§ π
β β
β§ βπ₯ β β βπ€ β π
π₯ β€ π€) β inf(π
, β, < ) β
β) |
88 | 80, 86, 87 | 3syl 18 |
. . . . . . . . . . . . 13
β’ (π β inf(π
, β, < ) β
β) |
89 | 57, 88 | eqeltrid 2838 |
. . . . . . . . . . . 12
β’ (π β π β β) |
90 | 89 | resqcld 14036 |
. . . . . . . . . . 11
β’ (π β (πβ2) β β) |
91 | 90 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(4 / (π₯β2))) + 1))) β (πβ2) β β) |
92 | 36 | nnrecred 12209 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(4 / (π₯β2))) + 1))) β (1 / π) β
β) |
93 | 91, 92 | readdcld 11189 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(4 / (π₯β2))) + 1))) β ((πβ2) + (1 / π)) β β) |
94 | 91, 61 | readdcld 11189 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(4 / (π₯β2))) + 1))) β ((πβ2) + (1 / ((ββ(4 / (π₯β2))) + 1))) β
β) |
95 | 72 | adantlr 714 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β β) β ((π΄π·(πΉβπ))β2) β€ ((πβ2) + (1 / π))) |
96 | 36, 95 | syldan 592 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(4 / (π₯β2))) + 1))) β ((π΄π·(πΉβπ))β2) β€ ((πβ2) + (1 / π))) |
97 | | eluzle 12781 |
. . . . . . . . . . . 12
β’ (π β
(β€β₯β((ββ(4 / (π₯β2))) + 1)) β ((ββ(4 /
(π₯β2))) + 1) β€
π) |
98 | 97 | adantl 483 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(4 / (π₯β2))) + 1))) β ((ββ(4 /
(π₯β2))) + 1) β€
π) |
99 | 42 | rpregt0d 12968 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(4 / (π₯β2))) + 1))) β (((ββ(4
/ (π₯β2))) + 1) β
β β§ 0 < ((ββ(4 / (π₯β2))) + 1))) |
100 | | nnre 12165 |
. . . . . . . . . . . . . 14
β’ (π β β β π β
β) |
101 | | nngt0 12189 |
. . . . . . . . . . . . . 14
β’ (π β β β 0 <
π) |
102 | 100, 101 | jca 513 |
. . . . . . . . . . . . 13
β’ (π β β β (π β β β§ 0 <
π)) |
103 | 36, 102 | syl 17 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(4 / (π₯β2))) + 1))) β (π β β β§ 0 < π)) |
104 | | lerec 12043 |
. . . . . . . . . . . 12
β’
(((((ββ(4 / (π₯β2))) + 1) β β β§ 0 <
((ββ(4 / (π₯β2))) + 1)) β§ (π β β β§ 0 < π)) β (((ββ(4 /
(π₯β2))) + 1) β€
π β (1 / π) β€ (1 / ((ββ(4 /
(π₯β2))) +
1)))) |
105 | 99, 103, 104 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(4 / (π₯β2))) + 1))) β (((ββ(4
/ (π₯β2))) + 1) β€
π β (1 / π) β€ (1 / ((ββ(4 /
(π₯β2))) +
1)))) |
106 | 98, 105 | mpbid 231 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(4 / (π₯β2))) + 1))) β (1 / π) β€ (1 / ((ββ(4 /
(π₯β2))) +
1))) |
107 | 92, 61, 91, 106 | leadd2dd 11775 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(4 / (π₯β2))) + 1))) β ((πβ2) + (1 / π)) β€ ((πβ2) + (1 / ((ββ(4 / (π₯β2))) +
1)))) |
108 | 79, 93, 94, 96, 107 | letrd 11317 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(4 / (π₯β2))) + 1))) β ((π΄π·(πΉβπ))β2) β€ ((πβ2) + (1 / ((ββ(4 / (π₯β2))) +
1)))) |
109 | 16, 49, 50, 25, 51, 52, 54, 17, 55, 56, 57, 61, 62, 33, 65, 75, 108 | minvecolem2 29859 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(4 / (π₯β2))) + 1))) β (((πΉβ((ββ(4 / (π₯β2))) + 1))π·(πΉβπ))β2) β€ (4 Β· (1 /
((ββ(4 / (π₯β2))) + 1)))) |
110 | | rpdivcl 12945 |
. . . . . . . . . 10
β’ (((π₯β2) β
β+ β§ 4 β β+) β ((π₯β2) / 4) β
β+) |
111 | 47, 3, 110 | sylancl 587 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(4 / (π₯β2))) + 1))) β ((π₯β2) / 4) β
β+) |
112 | | rpcnne0 12938 |
. . . . . . . . . . . 12
β’ ((π₯β2) β
β+ β ((π₯β2) β β β§ (π₯β2) β
0)) |
113 | 47, 112 | syl 17 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(4 / (π₯β2))) + 1))) β ((π₯β2) β β β§ (π₯β2) β
0)) |
114 | | rpcnne0 12938 |
. . . . . . . . . . . 12
β’ (4 β
β+ β (4 β β β§ 4 β 0)) |
115 | 3, 114 | ax-mp 5 |
. . . . . . . . . . 11
β’ (4 β
β β§ 4 β 0) |
116 | | recdiv 11866 |
. . . . . . . . . . 11
β’ ((((π₯β2) β β β§
(π₯β2) β 0) β§ (4
β β β§ 4 β 0)) β (1 / ((π₯β2) / 4)) = (4 / (π₯β2))) |
117 | 113, 115,
116 | sylancl 587 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(4 / (π₯β2))) + 1))) β (1 / ((π₯β2) / 4)) = (4 / (π₯β2))) |
118 | 9 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(4 / (π₯β2))) + 1))) β (4 / (π₯β2)) β
β+) |
119 | 118 | rpred 12962 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(4 / (π₯β2))) + 1))) β (4 / (π₯β2)) β
β) |
120 | | flltp1 13711 |
. . . . . . . . . . 11
β’ ((4 /
(π₯β2)) β β
β (4 / (π₯β2))
< ((ββ(4 / (π₯β2))) + 1)) |
121 | 119, 120 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(4 / (π₯β2))) + 1))) β (4 / (π₯β2)) <
((ββ(4 / (π₯β2))) + 1)) |
122 | 117, 121 | eqbrtrd 5128 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(4 / (π₯β2))) + 1))) β (1 / ((π₯β2) / 4)) <
((ββ(4 / (π₯β2))) + 1)) |
123 | 111, 42, 122 | ltrec1d 12982 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(4 / (π₯β2))) + 1))) β (1 /
((ββ(4 / (π₯β2))) + 1)) < ((π₯β2) / 4)) |
124 | 1, 2 | pm3.2i 472 |
. . . . . . . . . 10
β’ (4 β
β β§ 0 < 4) |
125 | | ltmuldiv2 12034 |
. . . . . . . . . 10
β’ (((1 /
((ββ(4 / (π₯β2))) + 1)) β β β§ (π₯β2) β β β§ (4
β β β§ 0 < 4)) β ((4 Β· (1 / ((ββ(4 /
(π₯β2))) + 1))) <
(π₯β2) β (1 /
((ββ(4 / (π₯β2))) + 1)) < ((π₯β2) / 4))) |
126 | 124, 125 | mp3an3 1451 |
. . . . . . . . 9
β’ (((1 /
((ββ(4 / (π₯β2))) + 1)) β β β§ (π₯β2) β β) β
((4 Β· (1 / ((ββ(4 / (π₯β2))) + 1))) < (π₯β2) β (1 / ((ββ(4 /
(π₯β2))) + 1)) <
((π₯β2) /
4))) |
127 | 61, 48, 126 | syl2anc 585 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(4 / (π₯β2))) + 1))) β ((4 Β· (1 /
((ββ(4 / (π₯β2))) + 1))) < (π₯β2) β (1 / ((ββ(4 /
(π₯β2))) + 1)) <
((π₯β2) /
4))) |
128 | 123, 127 | mpbird 257 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(4 / (π₯β2))) + 1))) β (4 Β· (1 /
((ββ(4 / (π₯β2))) + 1))) < (π₯β2)) |
129 | 41, 46, 48, 109, 128 | lelttrd 11318 |
. . . . . 6
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(4 / (π₯β2))) + 1))) β (((πΉβ((ββ(4 / (π₯β2))) + 1))π·(πΉβπ))β2) < (π₯β2)) |
130 | | metge0 23714 |
. . . . . . . 8
β’ ((π· β (Metβπ) β§ (πΉβ((ββ(4 / (π₯β2))) + 1)) β π β§ (πΉβπ) β π) β 0 β€ ((πΉβ((ββ(4 / (π₯β2))) + 1))π·(πΉβπ))) |
131 | 20, 34, 38, 130 | syl3anc 1372 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(4 / (π₯β2))) + 1))) β 0 β€ ((πΉβ((ββ(4 /
(π₯β2))) + 1))π·(πΉβπ))) |
132 | | rprege0 12935 |
. . . . . . . 8
β’ (π₯ β β+
β (π₯ β β
β§ 0 β€ π₯)) |
133 | 132 | ad2antlr 726 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(4 / (π₯β2))) + 1))) β (π₯ β β β§ 0 β€ π₯)) |
134 | | lt2sq 14044 |
. . . . . . 7
β’
(((((πΉβ((ββ(4 / (π₯β2))) + 1))π·(πΉβπ)) β β β§ 0 β€ ((πΉβ((ββ(4 /
(π₯β2))) + 1))π·(πΉβπ))) β§ (π₯ β β β§ 0 β€ π₯)) β (((πΉβ((ββ(4 / (π₯β2))) + 1))π·(πΉβπ)) < π₯ β (((πΉβ((ββ(4 / (π₯β2))) + 1))π·(πΉβπ))β2) < (π₯β2))) |
135 | 40, 131, 133, 134 | syl21anc 837 |
. . . . . 6
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(4 / (π₯β2))) + 1))) β (((πΉβ((ββ(4 / (π₯β2))) + 1))π·(πΉβπ)) < π₯ β (((πΉβ((ββ(4 / (π₯β2))) + 1))π·(πΉβπ))β2) < (π₯β2))) |
136 | 129, 135 | mpbird 257 |
. . . . 5
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(4 / (π₯β2))) + 1))) β ((πΉβ((ββ(4 / (π₯β2))) + 1))π·(πΉβπ)) < π₯) |
137 | 136 | ralrimiva 3140 |
. . . 4
β’ ((π β§ π₯ β β+) β
βπ β
(β€β₯β((ββ(4 / (π₯β2))) + 1))((πΉβ((ββ(4 / (π₯β2))) + 1))π·(πΉβπ)) < π₯) |
138 | | fveq2 6843 |
. . . . . 6
β’ (π = ((ββ(4 / (π₯β2))) + 1) β
(β€β₯βπ) =
(β€β₯β((ββ(4 / (π₯β2))) + 1))) |
139 | | fveq2 6843 |
. . . . . . . 8
β’ (π = ((ββ(4 / (π₯β2))) + 1) β (πΉβπ) = (πΉβ((ββ(4 / (π₯β2))) +
1))) |
140 | 139 | oveq1d 7373 |
. . . . . . 7
β’ (π = ((ββ(4 / (π₯β2))) + 1) β ((πΉβπ)π·(πΉβπ)) = ((πΉβ((ββ(4 / (π₯β2))) + 1))π·(πΉβπ))) |
141 | 140 | breq1d 5116 |
. . . . . 6
β’ (π = ((ββ(4 / (π₯β2))) + 1) β (((πΉβπ)π·(πΉβπ)) < π₯ β ((πΉβ((ββ(4 / (π₯β2))) + 1))π·(πΉβπ)) < π₯)) |
142 | 138, 141 | raleqbidv 3318 |
. . . . 5
β’ (π = ((ββ(4 / (π₯β2))) + 1) β
(βπ β
(β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯ β βπ β
(β€β₯β((ββ(4 / (π₯β2))) + 1))((πΉβ((ββ(4 / (π₯β2))) + 1))π·(πΉβπ)) < π₯)) |
143 | 142 | rspcev 3580 |
. . . 4
β’
((((ββ(4 / (π₯β2))) + 1) β β β§
βπ β
(β€β₯β((ββ(4 / (π₯β2))) + 1))((πΉβ((ββ(4 / (π₯β2))) + 1))π·(πΉβπ)) < π₯) β βπ β β βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯) |
144 | 13, 137, 143 | syl2anc 585 |
. . 3
β’ ((π β§ π₯ β β+) β
βπ β β
βπ β
(β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯) |
145 | 144 | ralrimiva 3140 |
. 2
β’ (π β βπ₯ β β+ βπ β β βπ β
(β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯) |
146 | | nnuz 12811 |
. . 3
β’ β =
(β€β₯β1) |
147 | 16, 17 | imsxmet 29676 |
. . . 4
β’ (π β NrmCVec β π· β (βMetβπ)) |
148 | 14, 15, 147 | 3syl 18 |
. . 3
β’ (π β π· β (βMetβπ)) |
149 | | 1zzd 12539 |
. . 3
β’ (π β 1 β
β€) |
150 | | eqidd 2734 |
. . 3
β’ ((π β§ π β β) β (πΉβπ) = (πΉβπ)) |
151 | | eqidd 2734 |
. . 3
β’ ((π β§ π β β) β (πΉβπ) = (πΉβπ)) |
152 | 30, 28 | fssd 6687 |
. . 3
β’ (π β πΉ:ββΆπ) |
153 | 146, 148,
149, 150, 151, 152 | iscauf 24660 |
. 2
β’ (π β (πΉ β (Cauβπ·) β βπ₯ β β+ βπ β β βπ β
(β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯)) |
154 | 145, 153 | mpbird 257 |
1
β’ (π β πΉ β (Cauβπ·)) |