Step | Hyp | Ref
| Expression |
1 | | minveco.u |
. . . . . 6
β’ (π β π β
CPreHilOLD) |
2 | | phnv 29798 |
. . . . . 6
β’ (π β CPreHilOLD
β π β
NrmCVec) |
3 | | minveco.x |
. . . . . . 7
β’ π = (BaseSetβπ) |
4 | | minveco.d |
. . . . . . 7
β’ π· = (IndMetβπ) |
5 | 3, 4 | imsxmet 29676 |
. . . . . 6
β’ (π β NrmCVec β π· β (βMetβπ)) |
6 | 1, 2, 5 | 3syl 18 |
. . . . 5
β’ (π β π· β (βMetβπ)) |
7 | | minveco.j |
. . . . . 6
β’ π½ = (MetOpenβπ·) |
8 | 7 | methaus 23892 |
. . . . 5
β’ (π· β (βMetβπ) β π½ β Haus) |
9 | | lmfun 22748 |
. . . . 5
β’ (π½ β Haus β Fun
(βπ‘βπ½)) |
10 | 6, 8, 9 | 3syl 18 |
. . . 4
β’ (π β Fun
(βπ‘βπ½)) |
11 | | minveco.m |
. . . . . 6
β’ π = ( βπ£
βπ) |
12 | | minveco.n |
. . . . . 6
β’ π =
(normCVβπ) |
13 | | minveco.y |
. . . . . 6
β’ π = (BaseSetβπ) |
14 | | minveco.w |
. . . . . 6
β’ (π β π β ((SubSpβπ) β© CBan)) |
15 | | minveco.a |
. . . . . 6
β’ (π β π΄ β π) |
16 | | minveco.r |
. . . . . 6
β’ π
= ran (π¦ β π β¦ (πβ(π΄ππ¦))) |
17 | | minveco.s |
. . . . . 6
β’ π = inf(π
, β, < ) |
18 | | minveco.f |
. . . . . 6
β’ (π β πΉ:ββΆπ) |
19 | | minveco.1 |
. . . . . 6
β’ ((π β§ π β β) β ((π΄π·(πΉβπ))β2) β€ ((πβ2) + (1 / π))) |
20 | 3, 11, 12, 13, 1, 14, 15, 4, 7, 16, 17, 18, 19 | minvecolem4a 29861 |
. . . . 5
β’ (π β πΉ(βπ‘β(MetOpenβ(π· βΎ (π Γ π))))((βπ‘β(MetOpenβ(π· βΎ (π Γ π))))βπΉ)) |
21 | | eqid 2733 |
. . . . . . 7
β’ (π½ βΎt π) = (π½ βΎt π) |
22 | | nnuz 12811 |
. . . . . . 7
β’ β =
(β€β₯β1) |
23 | 13 | fvexi 6857 |
. . . . . . . 8
β’ π β V |
24 | 23 | a1i 11 |
. . . . . . 7
β’ (π β π β V) |
25 | 1, 2 | syl 17 |
. . . . . . . 8
β’ (π β π β NrmCVec) |
26 | 7 | mopntop 23809 |
. . . . . . . 8
β’ (π· β (βMetβπ) β π½ β Top) |
27 | 25, 5, 26 | 3syl 18 |
. . . . . . 7
β’ (π β π½ β Top) |
28 | | elin 3927 |
. . . . . . . . . . . . 13
β’ (π β ((SubSpβπ) β© CBan) β (π β (SubSpβπ) β§ π β CBan)) |
29 | 14, 28 | sylib 217 |
. . . . . . . . . . . 12
β’ (π β (π β (SubSpβπ) β§ π β CBan)) |
30 | 29 | simpld 496 |
. . . . . . . . . . 11
β’ (π β π β (SubSpβπ)) |
31 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(SubSpβπ) =
(SubSpβπ) |
32 | 3, 13, 31 | sspba 29711 |
. . . . . . . . . . 11
β’ ((π β NrmCVec β§ π β (SubSpβπ)) β π β π) |
33 | 25, 30, 32 | syl2anc 585 |
. . . . . . . . . 10
β’ (π β π β π) |
34 | | xmetres2 23730 |
. . . . . . . . . 10
β’ ((π· β (βMetβπ) β§ π β π) β (π· βΎ (π Γ π)) β (βMetβπ)) |
35 | 6, 33, 34 | syl2anc 585 |
. . . . . . . . 9
β’ (π β (π· βΎ (π Γ π)) β (βMetβπ)) |
36 | | eqid 2733 |
. . . . . . . . . 10
β’
(MetOpenβ(π·
βΎ (π Γ π))) = (MetOpenβ(π· βΎ (π Γ π))) |
37 | 36 | mopntopon 23808 |
. . . . . . . . 9
β’ ((π· βΎ (π Γ π)) β (βMetβπ) β (MetOpenβ(π· βΎ (π Γ π))) β (TopOnβπ)) |
38 | 35, 37 | syl 17 |
. . . . . . . 8
β’ (π β (MetOpenβ(π· βΎ (π Γ π))) β (TopOnβπ)) |
39 | | lmcl 22664 |
. . . . . . . 8
β’
(((MetOpenβ(π·
βΎ (π Γ π))) β (TopOnβπ) β§ πΉ(βπ‘β(MetOpenβ(π· βΎ (π Γ π))))((βπ‘β(MetOpenβ(π· βΎ (π Γ π))))βπΉ)) β
((βπ‘β(MetOpenβ(π· βΎ (π Γ π))))βπΉ) β π) |
40 | 38, 20, 39 | syl2anc 585 |
. . . . . . 7
β’ (π β
((βπ‘β(MetOpenβ(π· βΎ (π Γ π))))βπΉ) β π) |
41 | | 1zzd 12539 |
. . . . . . 7
β’ (π β 1 β
β€) |
42 | 21, 22, 24, 27, 40, 41, 18 | lmss 22665 |
. . . . . 6
β’ (π β (πΉ(βπ‘βπ½)((βπ‘β(MetOpenβ(π· βΎ (π Γ π))))βπΉ) β πΉ(βπ‘β(π½ βΎt π))((βπ‘β(MetOpenβ(π· βΎ (π Γ π))))βπΉ))) |
43 | | eqid 2733 |
. . . . . . . . . 10
β’ (π· βΎ (π Γ π)) = (π· βΎ (π Γ π)) |
44 | 43, 7, 36 | metrest 23896 |
. . . . . . . . 9
β’ ((π· β (βMetβπ) β§ π β π) β (π½ βΎt π) = (MetOpenβ(π· βΎ (π Γ π)))) |
45 | 6, 33, 44 | syl2anc 585 |
. . . . . . . 8
β’ (π β (π½ βΎt π) = (MetOpenβ(π· βΎ (π Γ π)))) |
46 | 45 | fveq2d 6847 |
. . . . . . 7
β’ (π β
(βπ‘β(π½ βΎt π)) =
(βπ‘β(MetOpenβ(π· βΎ (π Γ π))))) |
47 | 46 | breqd 5117 |
. . . . . 6
β’ (π β (πΉ(βπ‘β(π½ βΎt π))((βπ‘β(MetOpenβ(π· βΎ (π Γ π))))βπΉ) β πΉ(βπ‘β(MetOpenβ(π· βΎ (π Γ π))))((βπ‘β(MetOpenβ(π· βΎ (π Γ π))))βπΉ))) |
48 | 42, 47 | bitrd 279 |
. . . . 5
β’ (π β (πΉ(βπ‘βπ½)((βπ‘β(MetOpenβ(π· βΎ (π Γ π))))βπΉ) β πΉ(βπ‘β(MetOpenβ(π· βΎ (π Γ π))))((βπ‘β(MetOpenβ(π· βΎ (π Γ π))))βπΉ))) |
49 | 20, 48 | mpbird 257 |
. . . 4
β’ (π β πΉ(βπ‘βπ½)((βπ‘β(MetOpenβ(π· βΎ (π Γ π))))βπΉ)) |
50 | | funbrfv 6894 |
. . . 4
β’ (Fun
(βπ‘βπ½) β (πΉ(βπ‘βπ½)((βπ‘β(MetOpenβ(π· βΎ (π Γ π))))βπΉ) β ((βπ‘βπ½)βπΉ) =
((βπ‘β(MetOpenβ(π· βΎ (π Γ π))))βπΉ))) |
51 | 10, 49, 50 | sylc 65 |
. . 3
β’ (π β
((βπ‘βπ½)βπΉ) =
((βπ‘β(MetOpenβ(π· βΎ (π Γ π))))βπΉ)) |
52 | 51, 40 | eqeltrd 2834 |
. 2
β’ (π β
((βπ‘βπ½)βπΉ) β π) |
53 | 3, 11, 12, 13, 1, 14, 15, 4, 7, 16, 17, 18, 19 | minvecolem4b 29862 |
. . . . . 6
β’ (π β
((βπ‘βπ½)βπΉ) β π) |
54 | 3, 11, 12, 4 | imsdval 29670 |
. . . . . 6
β’ ((π β NrmCVec β§ π΄ β π β§
((βπ‘βπ½)βπΉ) β π) β (π΄π·((βπ‘βπ½)βπΉ)) = (πβ(π΄π((βπ‘βπ½)βπΉ)))) |
55 | 25, 15, 53, 54 | syl3anc 1372 |
. . . . 5
β’ (π β (π΄π·((βπ‘βπ½)βπΉ)) = (πβ(π΄π((βπ‘βπ½)βπΉ)))) |
56 | 55 | adantr 482 |
. . . 4
β’ ((π β§ π¦ β π) β (π΄π·((βπ‘βπ½)βπΉ)) = (πβ(π΄π((βπ‘βπ½)βπΉ)))) |
57 | 3, 4 | imsmet 29675 |
. . . . . . . 8
β’ (π β NrmCVec β π· β (Metβπ)) |
58 | 1, 2, 57 | 3syl 18 |
. . . . . . 7
β’ (π β π· β (Metβπ)) |
59 | | metcl 23701 |
. . . . . . 7
β’ ((π· β (Metβπ) β§ π΄ β π β§
((βπ‘βπ½)βπΉ) β π) β (π΄π·((βπ‘βπ½)βπΉ)) β β) |
60 | 58, 15, 53, 59 | syl3anc 1372 |
. . . . . 6
β’ (π β (π΄π·((βπ‘βπ½)βπΉ)) β β) |
61 | 60 | adantr 482 |
. . . . 5
β’ ((π β§ π¦ β π) β (π΄π·((βπ‘βπ½)βπΉ)) β β) |
62 | 3, 11, 12, 13, 1, 14, 15, 4, 7, 16, 17, 18, 19 | minvecolem4c 29863 |
. . . . . 6
β’ (π β π β β) |
63 | 62 | adantr 482 |
. . . . 5
β’ ((π β§ π¦ β π) β π β β) |
64 | 25 | adantr 482 |
. . . . . 6
β’ ((π β§ π¦ β π) β π β NrmCVec) |
65 | 15 | adantr 482 |
. . . . . . 7
β’ ((π β§ π¦ β π) β π΄ β π) |
66 | 33 | sselda 3945 |
. . . . . . 7
β’ ((π β§ π¦ β π) β π¦ β π) |
67 | 3, 11 | nvmcl 29630 |
. . . . . . 7
β’ ((π β NrmCVec β§ π΄ β π β§ π¦ β π) β (π΄ππ¦) β π) |
68 | 64, 65, 66, 67 | syl3anc 1372 |
. . . . . 6
β’ ((π β§ π¦ β π) β (π΄ππ¦) β π) |
69 | 3, 12 | nvcl 29645 |
. . . . . 6
β’ ((π β NrmCVec β§ (π΄ππ¦) β π) β (πβ(π΄ππ¦)) β β) |
70 | 64, 68, 69 | syl2anc 585 |
. . . . 5
β’ ((π β§ π¦ β π) β (πβ(π΄ππ¦)) β β) |
71 | 62, 60 | ltnled 11307 |
. . . . . . . 8
β’ (π β (π < (π΄π·((βπ‘βπ½)βπΉ)) β Β¬ (π΄π·((βπ‘βπ½)βπΉ)) β€ π)) |
72 | | eqid 2733 |
. . . . . . . . . . 11
β’
(β€β₯β((ββπ) + 1)) =
(β€β₯β((ββπ) + 1)) |
73 | 6 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π < (π΄π·((βπ‘βπ½)βπΉ))) β π· β (βMetβπ)) |
74 | | minveco.t |
. . . . . . . . . . . . . . 15
β’ π = (1 / (((((π΄π·((βπ‘βπ½)βπΉ)) + π) / 2)β2) β (πβ2))) |
75 | 60, 62 | readdcld 11189 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β ((π΄π·((βπ‘βπ½)βπΉ)) + π) β β) |
76 | 75 | rehalfcld 12405 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (((π΄π·((βπ‘βπ½)βπΉ)) + π) / 2) β β) |
77 | 76 | resqcld 14036 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β ((((π΄π·((βπ‘βπ½)βπΉ)) + π) / 2)β2) β
β) |
78 | 62 | resqcld 14036 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (πβ2) β β) |
79 | 77, 78 | resubcld 11588 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (((((π΄π·((βπ‘βπ½)βπΉ)) + π) / 2)β2) β (πβ2)) β β) |
80 | 79 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π < (π΄π·((βπ‘βπ½)βπΉ))) β (((((π΄π·((βπ‘βπ½)βπΉ)) + π) / 2)β2) β (πβ2)) β β) |
81 | 62, 60, 62 | ltadd1d 11753 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (π < (π΄π·((βπ‘βπ½)βπΉ)) β (π + π) < ((π΄π·((βπ‘βπ½)βπΉ)) + π))) |
82 | 62 | recnd 11188 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β π β β) |
83 | 82 | 2timesd 12401 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (2 Β· π) = (π + π)) |
84 | 83 | breq1d 5116 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β ((2 Β· π) < ((π΄π·((βπ‘βπ½)βπΉ)) + π) β (π + π) < ((π΄π·((βπ‘βπ½)βπΉ)) + π))) |
85 | | 2re 12232 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ 2 β
β |
86 | | 2pos 12261 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ 0 <
2 |
87 | 85, 86 | pm3.2i 472 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (2 β
β β§ 0 < 2) |
88 | 87 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (2 β β β§ 0
< 2)) |
89 | | ltmuldiv2 12034 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β β β§ ((π΄π·((βπ‘βπ½)βπΉ)) + π) β β β§ (2 β β
β§ 0 < 2)) β ((2 Β· π) < ((π΄π·((βπ‘βπ½)βπΉ)) + π) β π < (((π΄π·((βπ‘βπ½)βπΉ)) + π) / 2))) |
90 | 62, 75, 88, 89 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β ((2 Β· π) < ((π΄π·((βπ‘βπ½)βπΉ)) + π) β π < (((π΄π·((βπ‘βπ½)βπΉ)) + π) / 2))) |
91 | 81, 84, 90 | 3bitr2d 307 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (π < (π΄π·((βπ‘βπ½)βπΉ)) β π < (((π΄π·((βπ‘βπ½)βπΉ)) + π) / 2))) |
92 | 3, 11, 12, 13, 1, 14, 15, 4, 7, 16 | minvecolem1 29858 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (π
β β β§ π
β β
β§ βπ€ β π
0 β€ π€)) |
93 | 92 | simp3d 1145 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β βπ€ β π
0 β€ π€) |
94 | 92 | simp1d 1143 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β π
β β) |
95 | 92 | simp2d 1144 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β π
β β
) |
96 | | 0re 11162 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ 0 β
β |
97 | | breq1 5109 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π₯ = 0 β (π₯ β€ π€ β 0 β€ π€)) |
98 | 97 | ralbidv 3171 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π₯ = 0 β (βπ€ β π
π₯ β€ π€ β βπ€ β π
0 β€ π€)) |
99 | 98 | rspcev 3580 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((0
β β β§ βπ€ β π
0 β€ π€) β βπ₯ β β βπ€ β π
π₯ β€ π€) |
100 | 96, 93, 99 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β βπ₯ β β βπ€ β π
π₯ β€ π€) |
101 | 96 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β 0 β
β) |
102 | | infregelb 12144 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π
β β β§ π
β β
β§ βπ₯ β β βπ€ β π
π₯ β€ π€) β§ 0 β β) β (0 β€
inf(π
, β, < )
β βπ€ β
π
0 β€ π€)) |
103 | 94, 95, 100, 101, 102 | syl31anc 1374 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (0 β€ inf(π
, β, < ) β
βπ€ β π
0 β€ π€)) |
104 | 93, 103 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β 0 β€ inf(π
, β, <
)) |
105 | 104, 17 | breqtrrdi 5148 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β 0 β€ π) |
106 | | metge0 23714 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π· β (Metβπ) β§ π΄ β π β§
((βπ‘βπ½)βπΉ) β π) β 0 β€ (π΄π·((βπ‘βπ½)βπΉ))) |
107 | 58, 15, 53, 106 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β 0 β€ (π΄π·((βπ‘βπ½)βπΉ))) |
108 | 60, 62, 107, 105 | addge0d 11736 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β 0 β€ ((π΄π·((βπ‘βπ½)βπΉ)) + π)) |
109 | | divge0 12029 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π΄π·((βπ‘βπ½)βπΉ)) + π) β β β§ 0 β€ ((π΄π·((βπ‘βπ½)βπΉ)) + π)) β§ (2 β β β§ 0 < 2))
β 0 β€ (((π΄π·((βπ‘βπ½)βπΉ)) + π) / 2)) |
110 | 75, 108, 88, 109 | syl21anc 837 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β 0 β€ (((π΄π·((βπ‘βπ½)βπΉ)) + π) / 2)) |
111 | 62, 76, 105, 110 | lt2sqd 14165 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (π < (((π΄π·((βπ‘βπ½)βπΉ)) + π) / 2) β (πβ2) < ((((π΄π·((βπ‘βπ½)βπΉ)) + π) / 2)β2))) |
112 | 78, 77 | posdifd 11747 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β ((πβ2) < ((((π΄π·((βπ‘βπ½)βπΉ)) + π) / 2)β2) β 0 < (((((π΄π·((βπ‘βπ½)βπΉ)) + π) / 2)β2) β (πβ2)))) |
113 | 91, 111, 112 | 3bitrd 305 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π < (π΄π·((βπ‘βπ½)βπΉ)) β 0 < (((((π΄π·((βπ‘βπ½)βπΉ)) + π) / 2)β2) β (πβ2)))) |
114 | 113 | biimpa 478 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π < (π΄π·((βπ‘βπ½)βπΉ))) β 0 < (((((π΄π·((βπ‘βπ½)βπΉ)) + π) / 2)β2) β (πβ2))) |
115 | 80, 114 | elrpd 12959 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π < (π΄π·((βπ‘βπ½)βπΉ))) β (((((π΄π·((βπ‘βπ½)βπΉ)) + π) / 2)β2) β (πβ2)) β
β+) |
116 | 115 | rpreccld 12972 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π < (π΄π·((βπ‘βπ½)βπΉ))) β (1 / (((((π΄π·((βπ‘βπ½)βπΉ)) + π) / 2)β2) β (πβ2))) β
β+) |
117 | 74, 116 | eqeltrid 2838 |
. . . . . . . . . . . . . 14
β’ ((π β§ π < (π΄π·((βπ‘βπ½)βπΉ))) β π β
β+) |
118 | 117 | rprege0d 12969 |
. . . . . . . . . . . . 13
β’ ((π β§ π < (π΄π·((βπ‘βπ½)βπΉ))) β (π β β β§ 0 β€ π)) |
119 | | flge0nn0 13731 |
. . . . . . . . . . . . 13
β’ ((π β β β§ 0 β€
π) β
(ββπ) β
β0) |
120 | | nn0p1nn 12457 |
. . . . . . . . . . . . 13
β’
((ββπ)
β β0 β ((ββπ) + 1) β β) |
121 | 118, 119,
120 | 3syl 18 |
. . . . . . . . . . . 12
β’ ((π β§ π < (π΄π·((βπ‘βπ½)βπΉ))) β ((ββπ) + 1) β β) |
122 | 121 | nnzd 12531 |
. . . . . . . . . . 11
β’ ((π β§ π < (π΄π·((βπ‘βπ½)βπΉ))) β ((ββπ) + 1) β β€) |
123 | 49, 51 | breqtrrd 5134 |
. . . . . . . . . . . 12
β’ (π β πΉ(βπ‘βπ½)((βπ‘βπ½)βπΉ)) |
124 | 123 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π < (π΄π·((βπ‘βπ½)βπΉ))) β πΉ(βπ‘βπ½)((βπ‘βπ½)βπΉ)) |
125 | 15 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π < (π΄π·((βπ‘βπ½)βπΉ))) β π΄ β π) |
126 | 76 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π < (π΄π·((βπ‘βπ½)βπΉ))) β (((π΄π·((βπ‘βπ½)βπΉ)) + π) / 2) β β) |
127 | 126 | rexrd 11210 |
. . . . . . . . . . 11
β’ ((π β§ π < (π΄π·((βπ‘βπ½)βπΉ))) β (((π΄π·((βπ‘βπ½)βπΉ)) + π) / 2) β
β*) |
128 | | simpll 766 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π < (π΄π·((βπ‘βπ½)βπΉ))) β§ π β
(β€β₯β((ββπ) + 1))) β π) |
129 | | eluznn 12848 |
. . . . . . . . . . . . . . . 16
β’
((((ββπ)
+ 1) β β β§ π
β (β€β₯β((ββπ) + 1))) β π β β) |
130 | 121, 129 | sylan 581 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π < (π΄π·((βπ‘βπ½)βπΉ))) β§ π β
(β€β₯β((ββπ) + 1))) β π β β) |
131 | 58 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β π· β (Metβπ)) |
132 | 15 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β π΄ β π) |
133 | 18, 33 | fssd 6687 |
. . . . . . . . . . . . . . . . 17
β’ (π β πΉ:ββΆπ) |
134 | 133 | ffvelcdmda 7036 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β (πΉβπ) β π) |
135 | | metcl 23701 |
. . . . . . . . . . . . . . . 16
β’ ((π· β (Metβπ) β§ π΄ β π β§ (πΉβπ) β π) β (π΄π·(πΉβπ)) β β) |
136 | 131, 132,
134, 135 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β (π΄π·(πΉβπ)) β β) |
137 | 128, 130,
136 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (((π β§ π < (π΄π·((βπ‘βπ½)βπΉ))) β§ π β
(β€β₯β((ββπ) + 1))) β (π΄π·(πΉβπ)) β β) |
138 | 137 | resqcld 14036 |
. . . . . . . . . . . . 13
β’ (((π β§ π < (π΄π·((βπ‘βπ½)βπΉ))) β§ π β
(β€β₯β((ββπ) + 1))) β ((π΄π·(πΉβπ))β2) β β) |
139 | 62 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π < (π΄π·((βπ‘βπ½)βπΉ))) β§ π β
(β€β₯β((ββπ) + 1))) β π β β) |
140 | 139 | resqcld 14036 |
. . . . . . . . . . . . . 14
β’ (((π β§ π < (π΄π·((βπ‘βπ½)βπΉ))) β§ π β
(β€β₯β((ββπ) + 1))) β (πβ2) β β) |
141 | 130 | nnrecred 12209 |
. . . . . . . . . . . . . 14
β’ (((π β§ π < (π΄π·((βπ‘βπ½)βπΉ))) β§ π β
(β€β₯β((ββπ) + 1))) β (1 / π) β β) |
142 | 140, 141 | readdcld 11189 |
. . . . . . . . . . . . 13
β’ (((π β§ π < (π΄π·((βπ‘βπ½)βπΉ))) β§ π β
(β€β₯β((ββπ) + 1))) β ((πβ2) + (1 / π)) β β) |
143 | 77 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ π < (π΄π·((βπ‘βπ½)βπΉ))) β§ π β
(β€β₯β((ββπ) + 1))) β ((((π΄π·((βπ‘βπ½)βπΉ)) + π) / 2)β2) β
β) |
144 | 128, 130,
19 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (((π β§ π < (π΄π·((βπ‘βπ½)βπΉ))) β§ π β
(β€β₯β((ββπ) + 1))) β ((π΄π·(πΉβπ))β2) β€ ((πβ2) + (1 / π))) |
145 | 117 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π < (π΄π·((βπ‘βπ½)βπΉ))) β§ π β
(β€β₯β((ββπ) + 1))) β π β
β+) |
146 | 145 | rpred 12962 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π < (π΄π·((βπ‘βπ½)βπΉ))) β§ π β
(β€β₯β((ββπ) + 1))) β π β β) |
147 | | reflcl 13707 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β β
(ββπ) β
β) |
148 | | peano2re 11333 |
. . . . . . . . . . . . . . . . . 18
β’
((ββπ)
β β β ((ββπ) + 1) β β) |
149 | 146, 147,
148 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π < (π΄π·((βπ‘βπ½)βπΉ))) β§ π β
(β€β₯β((ββπ) + 1))) β ((ββπ) + 1) β
β) |
150 | 130 | nnred 12173 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π < (π΄π·((βπ‘βπ½)βπΉ))) β§ π β
(β€β₯β((ββπ) + 1))) β π β β) |
151 | | fllep1 13712 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β β π β€ ((ββπ) + 1)) |
152 | 146, 151 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π < (π΄π·((βπ‘βπ½)βπΉ))) β§ π β
(β€β₯β((ββπ) + 1))) β π β€ ((ββπ) + 1)) |
153 | | eluzle 12781 |
. . . . . . . . . . . . . . . . . 18
β’ (π β
(β€β₯β((ββπ) + 1)) β ((ββπ) + 1) β€ π) |
154 | 153 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π < (π΄π·((βπ‘βπ½)βπΉ))) β§ π β
(β€β₯β((ββπ) + 1))) β ((ββπ) + 1) β€ π) |
155 | 146, 149,
150, 152, 154 | letrd 11317 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π < (π΄π·((βπ‘βπ½)βπΉ))) β§ π β
(β€β₯β((ββπ) + 1))) β π β€ π) |
156 | 74, 155 | eqbrtrrid 5142 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π < (π΄π·((βπ‘βπ½)βπΉ))) β§ π β
(β€β₯β((ββπ) + 1))) β (1 / (((((π΄π·((βπ‘βπ½)βπΉ)) + π) / 2)β2) β (πβ2))) β€ π) |
157 | | 1red 11161 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π < (π΄π·((βπ‘βπ½)βπΉ))) β§ π β
(β€β₯β((ββπ) + 1))) β 1 β
β) |
158 | 79 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π < (π΄π·((βπ‘βπ½)βπΉ))) β§ π β
(β€β₯β((ββπ) + 1))) β (((((π΄π·((βπ‘βπ½)βπΉ)) + π) / 2)β2) β (πβ2)) β β) |
159 | 114 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π < (π΄π·((βπ‘βπ½)βπΉ))) β§ π β
(β€β₯β((ββπ) + 1))) β 0 < (((((π΄π·((βπ‘βπ½)βπΉ)) + π) / 2)β2) β (πβ2))) |
160 | 130 | nngt0d 12207 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π < (π΄π·((βπ‘βπ½)βπΉ))) β§ π β
(β€β₯β((ββπ) + 1))) β 0 < π) |
161 | | lediv23 12052 |
. . . . . . . . . . . . . . . 16
β’ ((1
β β β§ ((((((π΄π·((βπ‘βπ½)βπΉ)) + π) / 2)β2) β (πβ2)) β β β§ 0 <
(((((π΄π·((βπ‘βπ½)βπΉ)) + π) / 2)β2) β (πβ2))) β§ (π β β β§ 0 < π)) β ((1 / (((((π΄π·((βπ‘βπ½)βπΉ)) + π) / 2)β2) β (πβ2))) β€ π β (1 / π) β€ (((((π΄π·((βπ‘βπ½)βπΉ)) + π) / 2)β2) β (πβ2)))) |
162 | 157, 158,
159, 150, 160, 161 | syl122anc 1380 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π < (π΄π·((βπ‘βπ½)βπΉ))) β§ π β
(β€β₯β((ββπ) + 1))) β ((1 / (((((π΄π·((βπ‘βπ½)βπΉ)) + π) / 2)β2) β (πβ2))) β€ π β (1 / π) β€ (((((π΄π·((βπ‘βπ½)βπΉ)) + π) / 2)β2) β (πβ2)))) |
163 | 156, 162 | mpbid 231 |
. . . . . . . . . . . . . 14
β’ (((π β§ π < (π΄π·((βπ‘βπ½)βπΉ))) β§ π β
(β€β₯β((ββπ) + 1))) β (1 / π) β€ (((((π΄π·((βπ‘βπ½)βπΉ)) + π) / 2)β2) β (πβ2))) |
164 | 140, 141,
143 | leaddsub2d 11762 |
. . . . . . . . . . . . . 14
β’ (((π β§ π < (π΄π·((βπ‘βπ½)βπΉ))) β§ π β
(β€β₯β((ββπ) + 1))) β (((πβ2) + (1 / π)) β€ ((((π΄π·((βπ‘βπ½)βπΉ)) + π) / 2)β2) β (1 / π) β€ (((((π΄π·((βπ‘βπ½)βπΉ)) + π) / 2)β2) β (πβ2)))) |
165 | 163, 164 | mpbird 257 |
. . . . . . . . . . . . 13
β’ (((π β§ π < (π΄π·((βπ‘βπ½)βπΉ))) β§ π β
(β€β₯β((ββπ) + 1))) β ((πβ2) + (1 / π)) β€ ((((π΄π·((βπ‘βπ½)βπΉ)) + π) / 2)β2)) |
166 | 138, 142,
143, 144, 165 | letrd 11317 |
. . . . . . . . . . . 12
β’ (((π β§ π < (π΄π·((βπ‘βπ½)βπΉ))) β§ π β
(β€β₯β((ββπ) + 1))) β ((π΄π·(πΉβπ))β2) β€ ((((π΄π·((βπ‘βπ½)βπΉ)) + π) / 2)β2)) |
167 | 76 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ π < (π΄π·((βπ‘βπ½)βπΉ))) β§ π β
(β€β₯β((ββπ) + 1))) β (((π΄π·((βπ‘βπ½)βπΉ)) + π) / 2) β β) |
168 | | metge0 23714 |
. . . . . . . . . . . . . . 15
β’ ((π· β (Metβπ) β§ π΄ β π β§ (πΉβπ) β π) β 0 β€ (π΄π·(πΉβπ))) |
169 | 131, 132,
134, 168 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β 0 β€ (π΄π·(πΉβπ))) |
170 | 128, 130,
169 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (((π β§ π < (π΄π·((βπ‘βπ½)βπΉ))) β§ π β
(β€β₯β((ββπ) + 1))) β 0 β€ (π΄π·(πΉβπ))) |
171 | 110 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ π < (π΄π·((βπ‘βπ½)βπΉ))) β§ π β
(β€β₯β((ββπ) + 1))) β 0 β€ (((π΄π·((βπ‘βπ½)βπΉ)) + π) / 2)) |
172 | 137, 167,
170, 171 | le2sqd 14166 |
. . . . . . . . . . . 12
β’ (((π β§ π < (π΄π·((βπ‘βπ½)βπΉ))) β§ π β
(β€β₯β((ββπ) + 1))) β ((π΄π·(πΉβπ)) β€ (((π΄π·((βπ‘βπ½)βπΉ)) + π) / 2) β ((π΄π·(πΉβπ))β2) β€ ((((π΄π·((βπ‘βπ½)βπΉ)) + π) / 2)β2))) |
173 | 166, 172 | mpbird 257 |
. . . . . . . . . . 11
β’ (((π β§ π < (π΄π·((βπ‘βπ½)βπΉ))) β§ π β
(β€β₯β((ββπ) + 1))) β (π΄π·(πΉβπ)) β€ (((π΄π·((βπ‘βπ½)βπΉ)) + π) / 2)) |
174 | 72, 7, 73, 122, 124, 125, 127, 173 | lmle 24681 |
. . . . . . . . . 10
β’ ((π β§ π < (π΄π·((βπ‘βπ½)βπΉ))) β (π΄π·((βπ‘βπ½)βπΉ)) β€ (((π΄π·((βπ‘βπ½)βπΉ)) + π) / 2)) |
175 | 60, 62, 60 | leadd2d 11755 |
. . . . . . . . . . . 12
β’ (π β ((π΄π·((βπ‘βπ½)βπΉ)) β€ π β ((π΄π·((βπ‘βπ½)βπΉ)) + (π΄π·((βπ‘βπ½)βπΉ))) β€ ((π΄π·((βπ‘βπ½)βπΉ)) + π))) |
176 | 60 | recnd 11188 |
. . . . . . . . . . . . . 14
β’ (π β (π΄π·((βπ‘βπ½)βπΉ)) β β) |
177 | 176 | 2timesd 12401 |
. . . . . . . . . . . . 13
β’ (π β (2 Β· (π΄π·((βπ‘βπ½)βπΉ))) = ((π΄π·((βπ‘βπ½)βπΉ)) + (π΄π·((βπ‘βπ½)βπΉ)))) |
178 | 177 | breq1d 5116 |
. . . . . . . . . . . 12
β’ (π β ((2 Β· (π΄π·((βπ‘βπ½)βπΉ))) β€ ((π΄π·((βπ‘βπ½)βπΉ)) + π) β ((π΄π·((βπ‘βπ½)βπΉ)) + (π΄π·((βπ‘βπ½)βπΉ))) β€ ((π΄π·((βπ‘βπ½)βπΉ)) + π))) |
179 | | lemuldiv2 12041 |
. . . . . . . . . . . . . 14
β’ (((π΄π·((βπ‘βπ½)βπΉ)) β β β§ ((π΄π·((βπ‘βπ½)βπΉ)) + π) β β β§ (2 β β
β§ 0 < 2)) β ((2 Β· (π΄π·((βπ‘βπ½)βπΉ))) β€ ((π΄π·((βπ‘βπ½)βπΉ)) + π) β (π΄π·((βπ‘βπ½)βπΉ)) β€ (((π΄π·((βπ‘βπ½)βπΉ)) + π) / 2))) |
180 | 87, 179 | mp3an3 1451 |
. . . . . . . . . . . . 13
β’ (((π΄π·((βπ‘βπ½)βπΉ)) β β β§ ((π΄π·((βπ‘βπ½)βπΉ)) + π) β β) β ((2 Β· (π΄π·((βπ‘βπ½)βπΉ))) β€ ((π΄π·((βπ‘βπ½)βπΉ)) + π) β (π΄π·((βπ‘βπ½)βπΉ)) β€ (((π΄π·((βπ‘βπ½)βπΉ)) + π) / 2))) |
181 | 60, 75, 180 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π β ((2 Β· (π΄π·((βπ‘βπ½)βπΉ))) β€ ((π΄π·((βπ‘βπ½)βπΉ)) + π) β (π΄π·((βπ‘βπ½)βπΉ)) β€ (((π΄π·((βπ‘βπ½)βπΉ)) + π) / 2))) |
182 | 175, 178,
181 | 3bitr2d 307 |
. . . . . . . . . . 11
β’ (π β ((π΄π·((βπ‘βπ½)βπΉ)) β€ π β (π΄π·((βπ‘βπ½)βπΉ)) β€ (((π΄π·((βπ‘βπ½)βπΉ)) + π) / 2))) |
183 | 182 | biimpar 479 |
. . . . . . . . . 10
β’ ((π β§ (π΄π·((βπ‘βπ½)βπΉ)) β€ (((π΄π·((βπ‘βπ½)βπΉ)) + π) / 2)) β (π΄π·((βπ‘βπ½)βπΉ)) β€ π) |
184 | 174, 183 | syldan 592 |
. . . . . . . . 9
β’ ((π β§ π < (π΄π·((βπ‘βπ½)βπΉ))) β (π΄π·((βπ‘βπ½)βπΉ)) β€ π) |
185 | 184 | ex 414 |
. . . . . . . 8
β’ (π β (π < (π΄π·((βπ‘βπ½)βπΉ)) β (π΄π·((βπ‘βπ½)βπΉ)) β€ π)) |
186 | 71, 185 | sylbird 260 |
. . . . . . 7
β’ (π β (Β¬ (π΄π·((βπ‘βπ½)βπΉ)) β€ π β (π΄π·((βπ‘βπ½)βπΉ)) β€ π)) |
187 | 186 | pm2.18d 127 |
. . . . . 6
β’ (π β (π΄π·((βπ‘βπ½)βπΉ)) β€ π) |
188 | 187 | adantr 482 |
. . . . 5
β’ ((π β§ π¦ β π) β (π΄π·((βπ‘βπ½)βπΉ)) β€ π) |
189 | 94 | adantr 482 |
. . . . . . 7
β’ ((π β§ π¦ β π) β π
β β) |
190 | 100 | adantr 482 |
. . . . . . 7
β’ ((π β§ π¦ β π) β βπ₯ β β βπ€ β π
π₯ β€ π€) |
191 | | simpr 486 |
. . . . . . . . 9
β’ ((π β§ π¦ β π) β π¦ β π) |
192 | | fvex 6856 |
. . . . . . . . 9
β’ (πβ(π΄ππ¦)) β V |
193 | | eqid 2733 |
. . . . . . . . . 10
β’ (π¦ β π β¦ (πβ(π΄ππ¦))) = (π¦ β π β¦ (πβ(π΄ππ¦))) |
194 | 193 | elrnmpt1 5914 |
. . . . . . . . 9
β’ ((π¦ β π β§ (πβ(π΄ππ¦)) β V) β (πβ(π΄ππ¦)) β ran (π¦ β π β¦ (πβ(π΄ππ¦)))) |
195 | 191, 192,
194 | sylancl 587 |
. . . . . . . 8
β’ ((π β§ π¦ β π) β (πβ(π΄ππ¦)) β ran (π¦ β π β¦ (πβ(π΄ππ¦)))) |
196 | 195, 16 | eleqtrrdi 2845 |
. . . . . . 7
β’ ((π β§ π¦ β π) β (πβ(π΄ππ¦)) β π
) |
197 | | infrelb 12145 |
. . . . . . 7
β’ ((π
β β β§
βπ₯ β β
βπ€ β π
π₯ β€ π€ β§ (πβ(π΄ππ¦)) β π
) β inf(π
, β, < ) β€ (πβ(π΄ππ¦))) |
198 | 189, 190,
196, 197 | syl3anc 1372 |
. . . . . 6
β’ ((π β§ π¦ β π) β inf(π
, β, < ) β€ (πβ(π΄ππ¦))) |
199 | 17, 198 | eqbrtrid 5141 |
. . . . 5
β’ ((π β§ π¦ β π) β π β€ (πβ(π΄ππ¦))) |
200 | 61, 63, 70, 188, 199 | letrd 11317 |
. . . 4
β’ ((π β§ π¦ β π) β (π΄π·((βπ‘βπ½)βπΉ)) β€ (πβ(π΄ππ¦))) |
201 | 56, 200 | eqbrtrrd 5130 |
. . 3
β’ ((π β§ π¦ β π) β (πβ(π΄π((βπ‘βπ½)βπΉ))) β€ (πβ(π΄ππ¦))) |
202 | 201 | ralrimiva 3140 |
. 2
β’ (π β βπ¦ β π (πβ(π΄π((βπ‘βπ½)βπΉ))) β€ (πβ(π΄ππ¦))) |
203 | | oveq2 7366 |
. . . . . 6
β’ (π₯ =
((βπ‘βπ½)βπΉ) β (π΄ππ₯) = (π΄π((βπ‘βπ½)βπΉ))) |
204 | 203 | fveq2d 6847 |
. . . . 5
β’ (π₯ =
((βπ‘βπ½)βπΉ) β (πβ(π΄ππ₯)) = (πβ(π΄π((βπ‘βπ½)βπΉ)))) |
205 | 204 | breq1d 5116 |
. . . 4
β’ (π₯ =
((βπ‘βπ½)βπΉ) β ((πβ(π΄ππ₯)) β€ (πβ(π΄ππ¦)) β (πβ(π΄π((βπ‘βπ½)βπΉ))) β€ (πβ(π΄ππ¦)))) |
206 | 205 | ralbidv 3171 |
. . 3
β’ (π₯ =
((βπ‘βπ½)βπΉ) β (βπ¦ β π (πβ(π΄ππ₯)) β€ (πβ(π΄ππ¦)) β βπ¦ β π (πβ(π΄π((βπ‘βπ½)βπΉ))) β€ (πβ(π΄ππ¦)))) |
207 | 206 | rspcev 3580 |
. 2
β’
((((βπ‘βπ½)βπΉ) β π β§ βπ¦ β π (πβ(π΄π((βπ‘βπ½)βπΉ))) β€ (πβ(π΄ππ¦))) β βπ₯ β π βπ¦ β π (πβ(π΄ππ₯)) β€ (πβ(π΄ππ¦))) |
208 | 52, 202, 207 | syl2anc 585 |
1
β’ (π β βπ₯ β π βπ¦ β π (πβ(π΄ππ₯)) β€ (πβ(π΄ππ¦))) |