Step |
Hyp |
Ref |
Expression |
1 |
|
minveco.x |
β’ π = ( BaseSet β π ) |
2 |
|
minveco.m |
β’ π = ( βπ£ β π ) |
3 |
|
minveco.n |
β’ π = ( normCV β π ) |
4 |
|
minveco.y |
β’ π = ( BaseSet β π ) |
5 |
|
minveco.u |
β’ ( π β π β CPreHilOLD ) |
6 |
|
minveco.w |
β’ ( π β π β ( ( SubSp β π ) β© CBan ) ) |
7 |
|
minveco.a |
β’ ( π β π΄ β π ) |
8 |
|
minveco.d |
β’ π· = ( IndMet β π ) |
9 |
|
minveco.j |
β’ π½ = ( MetOpen β π· ) |
10 |
|
minveco.r |
β’ π
= ran ( π¦ β π β¦ ( π β ( π΄ π π¦ ) ) ) |
11 |
|
minveco.s |
β’ π = inf ( π
, β , < ) |
12 |
|
minveco.f |
β’ ( π β πΉ : β βΆ π ) |
13 |
|
minveco.1 |
β’ ( ( π β§ π β β ) β ( ( π΄ π· ( πΉ β π ) ) β 2 ) β€ ( ( π β 2 ) + ( 1 / π ) ) ) |
14 |
|
minveco.t |
β’ π = ( 1 / ( ( ( ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + π ) / 2 ) β 2 ) β ( π β 2 ) ) ) |
15 |
|
phnv |
β’ ( π β CPreHilOLD β π β NrmCVec ) |
16 |
1 8
|
imsxmet |
β’ ( π β NrmCVec β π· β ( βMet β π ) ) |
17 |
5 15 16
|
3syl |
β’ ( π β π· β ( βMet β π ) ) |
18 |
9
|
methaus |
β’ ( π· β ( βMet β π ) β π½ β Haus ) |
19 |
|
lmfun |
β’ ( π½ β Haus β Fun ( βπ‘ β π½ ) ) |
20 |
17 18 19
|
3syl |
β’ ( π β Fun ( βπ‘ β π½ ) ) |
21 |
1 2 3 4 5 6 7 8 9 10 11 12 13
|
minvecolem4a |
β’ ( π β πΉ ( βπ‘ β ( MetOpen β ( π· βΎ ( π Γ π ) ) ) ) ( ( βπ‘ β ( MetOpen β ( π· βΎ ( π Γ π ) ) ) ) β πΉ ) ) |
22 |
|
eqid |
β’ ( π½ βΎt π ) = ( π½ βΎt π ) |
23 |
|
nnuz |
β’ β = ( β€β₯ β 1 ) |
24 |
4
|
fvexi |
β’ π β V |
25 |
24
|
a1i |
β’ ( π β π β V ) |
26 |
5 15
|
syl |
β’ ( π β π β NrmCVec ) |
27 |
9
|
mopntop |
β’ ( π· β ( βMet β π ) β π½ β Top ) |
28 |
26 16 27
|
3syl |
β’ ( π β π½ β Top ) |
29 |
|
elin |
β’ ( π β ( ( SubSp β π ) β© CBan ) β ( π β ( SubSp β π ) β§ π β CBan ) ) |
30 |
6 29
|
sylib |
β’ ( π β ( π β ( SubSp β π ) β§ π β CBan ) ) |
31 |
30
|
simpld |
β’ ( π β π β ( SubSp β π ) ) |
32 |
|
eqid |
β’ ( SubSp β π ) = ( SubSp β π ) |
33 |
1 4 32
|
sspba |
β’ ( ( π β NrmCVec β§ π β ( SubSp β π ) ) β π β π ) |
34 |
26 31 33
|
syl2anc |
β’ ( π β π β π ) |
35 |
|
xmetres2 |
β’ ( ( π· β ( βMet β π ) β§ π β π ) β ( π· βΎ ( π Γ π ) ) β ( βMet β π ) ) |
36 |
17 34 35
|
syl2anc |
β’ ( π β ( π· βΎ ( π Γ π ) ) β ( βMet β π ) ) |
37 |
|
eqid |
β’ ( MetOpen β ( π· βΎ ( π Γ π ) ) ) = ( MetOpen β ( π· βΎ ( π Γ π ) ) ) |
38 |
37
|
mopntopon |
β’ ( ( π· βΎ ( π Γ π ) ) β ( βMet β π ) β ( MetOpen β ( π· βΎ ( π Γ π ) ) ) β ( TopOn β π ) ) |
39 |
36 38
|
syl |
β’ ( π β ( MetOpen β ( π· βΎ ( π Γ π ) ) ) β ( TopOn β π ) ) |
40 |
|
lmcl |
β’ ( ( ( MetOpen β ( π· βΎ ( π Γ π ) ) ) β ( TopOn β π ) β§ πΉ ( βπ‘ β ( MetOpen β ( π· βΎ ( π Γ π ) ) ) ) ( ( βπ‘ β ( MetOpen β ( π· βΎ ( π Γ π ) ) ) ) β πΉ ) ) β ( ( βπ‘ β ( MetOpen β ( π· βΎ ( π Γ π ) ) ) ) β πΉ ) β π ) |
41 |
39 21 40
|
syl2anc |
β’ ( π β ( ( βπ‘ β ( MetOpen β ( π· βΎ ( π Γ π ) ) ) ) β πΉ ) β π ) |
42 |
|
1zzd |
β’ ( π β 1 β β€ ) |
43 |
22 23 25 28 41 42 12
|
lmss |
β’ ( π β ( πΉ ( βπ‘ β π½ ) ( ( βπ‘ β ( MetOpen β ( π· βΎ ( π Γ π ) ) ) ) β πΉ ) β πΉ ( βπ‘ β ( π½ βΎt π ) ) ( ( βπ‘ β ( MetOpen β ( π· βΎ ( π Γ π ) ) ) ) β πΉ ) ) ) |
44 |
|
eqid |
β’ ( π· βΎ ( π Γ π ) ) = ( π· βΎ ( π Γ π ) ) |
45 |
44 9 37
|
metrest |
β’ ( ( π· β ( βMet β π ) β§ π β π ) β ( π½ βΎt π ) = ( MetOpen β ( π· βΎ ( π Γ π ) ) ) ) |
46 |
17 34 45
|
syl2anc |
β’ ( π β ( π½ βΎt π ) = ( MetOpen β ( π· βΎ ( π Γ π ) ) ) ) |
47 |
46
|
fveq2d |
β’ ( π β ( βπ‘ β ( π½ βΎt π ) ) = ( βπ‘ β ( MetOpen β ( π· βΎ ( π Γ π ) ) ) ) ) |
48 |
47
|
breqd |
β’ ( π β ( πΉ ( βπ‘ β ( π½ βΎt π ) ) ( ( βπ‘ β ( MetOpen β ( π· βΎ ( π Γ π ) ) ) ) β πΉ ) β πΉ ( βπ‘ β ( MetOpen β ( π· βΎ ( π Γ π ) ) ) ) ( ( βπ‘ β ( MetOpen β ( π· βΎ ( π Γ π ) ) ) ) β πΉ ) ) ) |
49 |
43 48
|
bitrd |
β’ ( π β ( πΉ ( βπ‘ β π½ ) ( ( βπ‘ β ( MetOpen β ( π· βΎ ( π Γ π ) ) ) ) β πΉ ) β πΉ ( βπ‘ β ( MetOpen β ( π· βΎ ( π Γ π ) ) ) ) ( ( βπ‘ β ( MetOpen β ( π· βΎ ( π Γ π ) ) ) ) β πΉ ) ) ) |
50 |
21 49
|
mpbird |
β’ ( π β πΉ ( βπ‘ β π½ ) ( ( βπ‘ β ( MetOpen β ( π· βΎ ( π Γ π ) ) ) ) β πΉ ) ) |
51 |
|
funbrfv |
β’ ( Fun ( βπ‘ β π½ ) β ( πΉ ( βπ‘ β π½ ) ( ( βπ‘ β ( MetOpen β ( π· βΎ ( π Γ π ) ) ) ) β πΉ ) β ( ( βπ‘ β π½ ) β πΉ ) = ( ( βπ‘ β ( MetOpen β ( π· βΎ ( π Γ π ) ) ) ) β πΉ ) ) ) |
52 |
20 50 51
|
sylc |
β’ ( π β ( ( βπ‘ β π½ ) β πΉ ) = ( ( βπ‘ β ( MetOpen β ( π· βΎ ( π Γ π ) ) ) ) β πΉ ) ) |
53 |
52 41
|
eqeltrd |
β’ ( π β ( ( βπ‘ β π½ ) β πΉ ) β π ) |
54 |
1 2 3 4 5 6 7 8 9 10 11 12 13
|
minvecolem4b |
β’ ( π β ( ( βπ‘ β π½ ) β πΉ ) β π ) |
55 |
1 2 3 8
|
imsdval |
β’ ( ( π β NrmCVec β§ π΄ β π β§ ( ( βπ‘ β π½ ) β πΉ ) β π ) β ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) = ( π β ( π΄ π ( ( βπ‘ β π½ ) β πΉ ) ) ) ) |
56 |
26 7 54 55
|
syl3anc |
β’ ( π β ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) = ( π β ( π΄ π ( ( βπ‘ β π½ ) β πΉ ) ) ) ) |
57 |
56
|
adantr |
β’ ( ( π β§ π¦ β π ) β ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) = ( π β ( π΄ π ( ( βπ‘ β π½ ) β πΉ ) ) ) ) |
58 |
1 8
|
imsmet |
β’ ( π β NrmCVec β π· β ( Met β π ) ) |
59 |
5 15 58
|
3syl |
β’ ( π β π· β ( Met β π ) ) |
60 |
|
metcl |
β’ ( ( π· β ( Met β π ) β§ π΄ β π β§ ( ( βπ‘ β π½ ) β πΉ ) β π ) β ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) β β ) |
61 |
59 7 54 60
|
syl3anc |
β’ ( π β ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) β β ) |
62 |
61
|
adantr |
β’ ( ( π β§ π¦ β π ) β ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) β β ) |
63 |
1 2 3 4 5 6 7 8 9 10 11 12 13
|
minvecolem4c |
β’ ( π β π β β ) |
64 |
63
|
adantr |
β’ ( ( π β§ π¦ β π ) β π β β ) |
65 |
26
|
adantr |
β’ ( ( π β§ π¦ β π ) β π β NrmCVec ) |
66 |
7
|
adantr |
β’ ( ( π β§ π¦ β π ) β π΄ β π ) |
67 |
34
|
sselda |
β’ ( ( π β§ π¦ β π ) β π¦ β π ) |
68 |
1 2
|
nvmcl |
β’ ( ( π β NrmCVec β§ π΄ β π β§ π¦ β π ) β ( π΄ π π¦ ) β π ) |
69 |
65 66 67 68
|
syl3anc |
β’ ( ( π β§ π¦ β π ) β ( π΄ π π¦ ) β π ) |
70 |
1 3
|
nvcl |
β’ ( ( π β NrmCVec β§ ( π΄ π π¦ ) β π ) β ( π β ( π΄ π π¦ ) ) β β ) |
71 |
65 69 70
|
syl2anc |
β’ ( ( π β§ π¦ β π ) β ( π β ( π΄ π π¦ ) ) β β ) |
72 |
63 61
|
ltnled |
β’ ( π β ( π < ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) β Β¬ ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) β€ π ) ) |
73 |
|
eqid |
β’ ( β€β₯ β ( ( β β π ) + 1 ) ) = ( β€β₯ β ( ( β β π ) + 1 ) ) |
74 |
17
|
adantr |
β’ ( ( π β§ π < ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) ) β π· β ( βMet β π ) ) |
75 |
61 63
|
readdcld |
β’ ( π β ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + π ) β β ) |
76 |
75
|
rehalfcld |
β’ ( π β ( ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + π ) / 2 ) β β ) |
77 |
76
|
resqcld |
β’ ( π β ( ( ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + π ) / 2 ) β 2 ) β β ) |
78 |
63
|
resqcld |
β’ ( π β ( π β 2 ) β β ) |
79 |
77 78
|
resubcld |
β’ ( π β ( ( ( ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + π ) / 2 ) β 2 ) β ( π β 2 ) ) β β ) |
80 |
79
|
adantr |
β’ ( ( π β§ π < ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) ) β ( ( ( ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + π ) / 2 ) β 2 ) β ( π β 2 ) ) β β ) |
81 |
63 61 63
|
ltadd1d |
β’ ( π β ( π < ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) β ( π + π ) < ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + π ) ) ) |
82 |
63
|
recnd |
β’ ( π β π β β ) |
83 |
82
|
2timesd |
β’ ( π β ( 2 Β· π ) = ( π + π ) ) |
84 |
83
|
breq1d |
β’ ( π β ( ( 2 Β· π ) < ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + π ) β ( π + π ) < ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + π ) ) ) |
85 |
|
2re |
β’ 2 β β |
86 |
|
2pos |
β’ 0 < 2 |
87 |
85 86
|
pm3.2i |
β’ ( 2 β β β§ 0 < 2 ) |
88 |
87
|
a1i |
β’ ( π β ( 2 β β β§ 0 < 2 ) ) |
89 |
|
ltmuldiv2 |
β’ ( ( π β β β§ ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + π ) β β β§ ( 2 β β β§ 0 < 2 ) ) β ( ( 2 Β· π ) < ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + π ) β π < ( ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + π ) / 2 ) ) ) |
90 |
63 75 88 89
|
syl3anc |
β’ ( π β ( ( 2 Β· π ) < ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + π ) β π < ( ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + π ) / 2 ) ) ) |
91 |
81 84 90
|
3bitr2d |
β’ ( π β ( π < ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) β π < ( ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + π ) / 2 ) ) ) |
92 |
1 2 3 4 5 6 7 8 9 10
|
minvecolem1 |
β’ ( π β ( π
β β β§ π
β β
β§ β π€ β π
0 β€ π€ ) ) |
93 |
92
|
simp3d |
β’ ( π β β π€ β π
0 β€ π€ ) |
94 |
92
|
simp1d |
β’ ( π β π
β β ) |
95 |
92
|
simp2d |
β’ ( π β π
β β
) |
96 |
|
0re |
β’ 0 β β |
97 |
|
breq1 |
β’ ( π₯ = 0 β ( π₯ β€ π€ β 0 β€ π€ ) ) |
98 |
97
|
ralbidv |
β’ ( π₯ = 0 β ( β π€ β π
π₯ β€ π€ β β π€ β π
0 β€ π€ ) ) |
99 |
98
|
rspcev |
β’ ( ( 0 β β β§ β π€ β π
0 β€ π€ ) β β π₯ β β β π€ β π
π₯ β€ π€ ) |
100 |
96 93 99
|
sylancr |
β’ ( π β β π₯ β β β π€ β π
π₯ β€ π€ ) |
101 |
96
|
a1i |
β’ ( π β 0 β β ) |
102 |
|
infregelb |
β’ ( ( ( π
β β β§ π
β β
β§ β π₯ β β β π€ β π
π₯ β€ π€ ) β§ 0 β β ) β ( 0 β€ inf ( π
, β , < ) β β π€ β π
0 β€ π€ ) ) |
103 |
94 95 100 101 102
|
syl31anc |
β’ ( π β ( 0 β€ inf ( π
, β , < ) β β π€ β π
0 β€ π€ ) ) |
104 |
93 103
|
mpbird |
β’ ( π β 0 β€ inf ( π
, β , < ) ) |
105 |
104 11
|
breqtrrdi |
β’ ( π β 0 β€ π ) |
106 |
|
metge0 |
β’ ( ( π· β ( Met β π ) β§ π΄ β π β§ ( ( βπ‘ β π½ ) β πΉ ) β π ) β 0 β€ ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) ) |
107 |
59 7 54 106
|
syl3anc |
β’ ( π β 0 β€ ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) ) |
108 |
61 63 107 105
|
addge0d |
β’ ( π β 0 β€ ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + π ) ) |
109 |
|
divge0 |
β’ ( ( ( ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + π ) β β β§ 0 β€ ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + π ) ) β§ ( 2 β β β§ 0 < 2 ) ) β 0 β€ ( ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + π ) / 2 ) ) |
110 |
75 108 88 109
|
syl21anc |
β’ ( π β 0 β€ ( ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + π ) / 2 ) ) |
111 |
63 76 105 110
|
lt2sqd |
β’ ( π β ( π < ( ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + π ) / 2 ) β ( π β 2 ) < ( ( ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + π ) / 2 ) β 2 ) ) ) |
112 |
78 77
|
posdifd |
β’ ( π β ( ( π β 2 ) < ( ( ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + π ) / 2 ) β 2 ) β 0 < ( ( ( ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + π ) / 2 ) β 2 ) β ( π β 2 ) ) ) ) |
113 |
91 111 112
|
3bitrd |
β’ ( π β ( π < ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) β 0 < ( ( ( ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + π ) / 2 ) β 2 ) β ( π β 2 ) ) ) ) |
114 |
113
|
biimpa |
β’ ( ( π β§ π < ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) ) β 0 < ( ( ( ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + π ) / 2 ) β 2 ) β ( π β 2 ) ) ) |
115 |
80 114
|
elrpd |
β’ ( ( π β§ π < ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) ) β ( ( ( ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + π ) / 2 ) β 2 ) β ( π β 2 ) ) β β+ ) |
116 |
115
|
rpreccld |
β’ ( ( π β§ π < ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) ) β ( 1 / ( ( ( ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + π ) / 2 ) β 2 ) β ( π β 2 ) ) ) β β+ ) |
117 |
14 116
|
eqeltrid |
β’ ( ( π β§ π < ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) ) β π β β+ ) |
118 |
117
|
rprege0d |
β’ ( ( π β§ π < ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) ) β ( π β β β§ 0 β€ π ) ) |
119 |
|
flge0nn0 |
β’ ( ( π β β β§ 0 β€ π ) β ( β β π ) β β0 ) |
120 |
|
nn0p1nn |
β’ ( ( β β π ) β β0 β ( ( β β π ) + 1 ) β β ) |
121 |
118 119 120
|
3syl |
β’ ( ( π β§ π < ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) ) β ( ( β β π ) + 1 ) β β ) |
122 |
121
|
nnzd |
β’ ( ( π β§ π < ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) ) β ( ( β β π ) + 1 ) β β€ ) |
123 |
50 52
|
breqtrrd |
β’ ( π β πΉ ( βπ‘ β π½ ) ( ( βπ‘ β π½ ) β πΉ ) ) |
124 |
123
|
adantr |
β’ ( ( π β§ π < ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) ) β πΉ ( βπ‘ β π½ ) ( ( βπ‘ β π½ ) β πΉ ) ) |
125 |
7
|
adantr |
β’ ( ( π β§ π < ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) ) β π΄ β π ) |
126 |
76
|
adantr |
β’ ( ( π β§ π < ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) ) β ( ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + π ) / 2 ) β β ) |
127 |
126
|
rexrd |
β’ ( ( π β§ π < ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) ) β ( ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + π ) / 2 ) β β* ) |
128 |
|
simpll |
β’ ( ( ( π β§ π < ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) ) β§ π β ( β€β₯ β ( ( β β π ) + 1 ) ) ) β π ) |
129 |
|
eluznn |
β’ ( ( ( ( β β π ) + 1 ) β β β§ π β ( β€β₯ β ( ( β β π ) + 1 ) ) ) β π β β ) |
130 |
121 129
|
sylan |
β’ ( ( ( π β§ π < ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) ) β§ π β ( β€β₯ β ( ( β β π ) + 1 ) ) ) β π β β ) |
131 |
59
|
adantr |
β’ ( ( π β§ π β β ) β π· β ( Met β π ) ) |
132 |
7
|
adantr |
β’ ( ( π β§ π β β ) β π΄ β π ) |
133 |
12 34
|
fssd |
β’ ( π β πΉ : β βΆ π ) |
134 |
133
|
ffvelcdmda |
β’ ( ( π β§ π β β ) β ( πΉ β π ) β π ) |
135 |
|
metcl |
β’ ( ( π· β ( Met β π ) β§ π΄ β π β§ ( πΉ β π ) β π ) β ( π΄ π· ( πΉ β π ) ) β β ) |
136 |
131 132 134 135
|
syl3anc |
β’ ( ( π β§ π β β ) β ( π΄ π· ( πΉ β π ) ) β β ) |
137 |
128 130 136
|
syl2anc |
β’ ( ( ( π β§ π < ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) ) β§ π β ( β€β₯ β ( ( β β π ) + 1 ) ) ) β ( π΄ π· ( πΉ β π ) ) β β ) |
138 |
137
|
resqcld |
β’ ( ( ( π β§ π < ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) ) β§ π β ( β€β₯ β ( ( β β π ) + 1 ) ) ) β ( ( π΄ π· ( πΉ β π ) ) β 2 ) β β ) |
139 |
63
|
ad2antrr |
β’ ( ( ( π β§ π < ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) ) β§ π β ( β€β₯ β ( ( β β π ) + 1 ) ) ) β π β β ) |
140 |
139
|
resqcld |
β’ ( ( ( π β§ π < ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) ) β§ π β ( β€β₯ β ( ( β β π ) + 1 ) ) ) β ( π β 2 ) β β ) |
141 |
130
|
nnrecred |
β’ ( ( ( π β§ π < ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) ) β§ π β ( β€β₯ β ( ( β β π ) + 1 ) ) ) β ( 1 / π ) β β ) |
142 |
140 141
|
readdcld |
β’ ( ( ( π β§ π < ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) ) β§ π β ( β€β₯ β ( ( β β π ) + 1 ) ) ) β ( ( π β 2 ) + ( 1 / π ) ) β β ) |
143 |
77
|
ad2antrr |
β’ ( ( ( π β§ π < ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) ) β§ π β ( β€β₯ β ( ( β β π ) + 1 ) ) ) β ( ( ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + π ) / 2 ) β 2 ) β β ) |
144 |
128 130 13
|
syl2anc |
β’ ( ( ( π β§ π < ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) ) β§ π β ( β€β₯ β ( ( β β π ) + 1 ) ) ) β ( ( π΄ π· ( πΉ β π ) ) β 2 ) β€ ( ( π β 2 ) + ( 1 / π ) ) ) |
145 |
117
|
adantr |
β’ ( ( ( π β§ π < ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) ) β§ π β ( β€β₯ β ( ( β β π ) + 1 ) ) ) β π β β+ ) |
146 |
145
|
rpred |
β’ ( ( ( π β§ π < ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) ) β§ π β ( β€β₯ β ( ( β β π ) + 1 ) ) ) β π β β ) |
147 |
|
reflcl |
β’ ( π β β β ( β β π ) β β ) |
148 |
|
peano2re |
β’ ( ( β β π ) β β β ( ( β β π ) + 1 ) β β ) |
149 |
146 147 148
|
3syl |
β’ ( ( ( π β§ π < ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) ) β§ π β ( β€β₯ β ( ( β β π ) + 1 ) ) ) β ( ( β β π ) + 1 ) β β ) |
150 |
130
|
nnred |
β’ ( ( ( π β§ π < ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) ) β§ π β ( β€β₯ β ( ( β β π ) + 1 ) ) ) β π β β ) |
151 |
|
fllep1 |
β’ ( π β β β π β€ ( ( β β π ) + 1 ) ) |
152 |
146 151
|
syl |
β’ ( ( ( π β§ π < ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) ) β§ π β ( β€β₯ β ( ( β β π ) + 1 ) ) ) β π β€ ( ( β β π ) + 1 ) ) |
153 |
|
eluzle |
β’ ( π β ( β€β₯ β ( ( β β π ) + 1 ) ) β ( ( β β π ) + 1 ) β€ π ) |
154 |
153
|
adantl |
β’ ( ( ( π β§ π < ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) ) β§ π β ( β€β₯ β ( ( β β π ) + 1 ) ) ) β ( ( β β π ) + 1 ) β€ π ) |
155 |
146 149 150 152 154
|
letrd |
β’ ( ( ( π β§ π < ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) ) β§ π β ( β€β₯ β ( ( β β π ) + 1 ) ) ) β π β€ π ) |
156 |
14 155
|
eqbrtrrid |
β’ ( ( ( π β§ π < ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) ) β§ π β ( β€β₯ β ( ( β β π ) + 1 ) ) ) β ( 1 / ( ( ( ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + π ) / 2 ) β 2 ) β ( π β 2 ) ) ) β€ π ) |
157 |
|
1red |
β’ ( ( ( π β§ π < ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) ) β§ π β ( β€β₯ β ( ( β β π ) + 1 ) ) ) β 1 β β ) |
158 |
79
|
ad2antrr |
β’ ( ( ( π β§ π < ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) ) β§ π β ( β€β₯ β ( ( β β π ) + 1 ) ) ) β ( ( ( ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + π ) / 2 ) β 2 ) β ( π β 2 ) ) β β ) |
159 |
114
|
adantr |
β’ ( ( ( π β§ π < ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) ) β§ π β ( β€β₯ β ( ( β β π ) + 1 ) ) ) β 0 < ( ( ( ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + π ) / 2 ) β 2 ) β ( π β 2 ) ) ) |
160 |
130
|
nngt0d |
β’ ( ( ( π β§ π < ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) ) β§ π β ( β€β₯ β ( ( β β π ) + 1 ) ) ) β 0 < π ) |
161 |
|
lediv23 |
β’ ( ( 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 |
β’ ( ( ( π β§ π < ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) ) β§ π β ( β€β₯ β ( ( β β π ) + 1 ) ) ) β ( ( 1 / ( ( ( ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + π ) / 2 ) β 2 ) β ( π β 2 ) ) ) β€ π β ( 1 / π ) β€ ( ( ( ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + π ) / 2 ) β 2 ) β ( π β 2 ) ) ) ) |
163 |
156 162
|
mpbid |
β’ ( ( ( π β§ π < ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) ) β§ π β ( β€β₯ β ( ( β β π ) + 1 ) ) ) β ( 1 / π ) β€ ( ( ( ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + π ) / 2 ) β 2 ) β ( π β 2 ) ) ) |
164 |
140 141 143
|
leaddsub2d |
β’ ( ( ( π β§ π < ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) ) β§ π β ( β€β₯ β ( ( β β π ) + 1 ) ) ) β ( ( ( π β 2 ) + ( 1 / π ) ) β€ ( ( ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + π ) / 2 ) β 2 ) β ( 1 / π ) β€ ( ( ( ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + π ) / 2 ) β 2 ) β ( π β 2 ) ) ) ) |
165 |
163 164
|
mpbird |
β’ ( ( ( π β§ π < ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) ) β§ π β ( β€β₯ β ( ( β β π ) + 1 ) ) ) β ( ( π β 2 ) + ( 1 / π ) ) β€ ( ( ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + π ) / 2 ) β 2 ) ) |
166 |
138 142 143 144 165
|
letrd |
β’ ( ( ( π β§ π < ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) ) β§ π β ( β€β₯ β ( ( β β π ) + 1 ) ) ) β ( ( π΄ π· ( πΉ β π ) ) β 2 ) β€ ( ( ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + π ) / 2 ) β 2 ) ) |
167 |
76
|
ad2antrr |
β’ ( ( ( π β§ π < ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) ) β§ π β ( β€β₯ β ( ( β β π ) + 1 ) ) ) β ( ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + π ) / 2 ) β β ) |
168 |
|
metge0 |
β’ ( ( π· β ( Met β π ) β§ π΄ β π β§ ( πΉ β π ) β π ) β 0 β€ ( π΄ π· ( πΉ β π ) ) ) |
169 |
131 132 134 168
|
syl3anc |
β’ ( ( π β§ π β β ) β 0 β€ ( π΄ π· ( πΉ β π ) ) ) |
170 |
128 130 169
|
syl2anc |
β’ ( ( ( π β§ π < ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) ) β§ π β ( β€β₯ β ( ( β β π ) + 1 ) ) ) β 0 β€ ( π΄ π· ( πΉ β π ) ) ) |
171 |
110
|
ad2antrr |
β’ ( ( ( π β§ π < ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) ) β§ π β ( β€β₯ β ( ( β β π ) + 1 ) ) ) β 0 β€ ( ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + π ) / 2 ) ) |
172 |
137 167 170 171
|
le2sqd |
β’ ( ( ( π β§ π < ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) ) β§ π β ( β€β₯ β ( ( β β π ) + 1 ) ) ) β ( ( π΄ π· ( πΉ β π ) ) β€ ( ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + π ) / 2 ) β ( ( π΄ π· ( πΉ β π ) ) β 2 ) β€ ( ( ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + π ) / 2 ) β 2 ) ) ) |
173 |
166 172
|
mpbird |
β’ ( ( ( π β§ π < ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) ) β§ π β ( β€β₯ β ( ( β β π ) + 1 ) ) ) β ( π΄ π· ( πΉ β π ) ) β€ ( ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + π ) / 2 ) ) |
174 |
73 9 74 122 124 125 127 173
|
lmle |
β’ ( ( π β§ π < ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) ) β ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) β€ ( ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + π ) / 2 ) ) |
175 |
61 63 61
|
leadd2d |
β’ ( π β ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) β€ π β ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) ) β€ ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + π ) ) ) |
176 |
61
|
recnd |
β’ ( π β ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) β β ) |
177 |
176
|
2timesd |
β’ ( π β ( 2 Β· ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) ) = ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) ) ) |
178 |
177
|
breq1d |
β’ ( π β ( ( 2 Β· ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) ) β€ ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + π ) β ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) ) β€ ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + π ) ) ) |
179 |
|
lemuldiv2 |
β’ ( ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) β β β§ ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + π ) β β β§ ( 2 β β β§ 0 < 2 ) ) β ( ( 2 Β· ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) ) β€ ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + π ) β ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) β€ ( ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + π ) / 2 ) ) ) |
180 |
87 179
|
mp3an3 |
β’ ( ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) β β β§ ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + π ) β β ) β ( ( 2 Β· ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) ) β€ ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + π ) β ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) β€ ( ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + π ) / 2 ) ) ) |
181 |
61 75 180
|
syl2anc |
β’ ( π β ( ( 2 Β· ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) ) β€ ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + π ) β ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) β€ ( ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + π ) / 2 ) ) ) |
182 |
175 178 181
|
3bitr2d |
β’ ( π β ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) β€ π β ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) β€ ( ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + π ) / 2 ) ) ) |
183 |
182
|
biimpar |
β’ ( ( π β§ ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) β€ ( ( ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) + π ) / 2 ) ) β ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) β€ π ) |
184 |
174 183
|
syldan |
β’ ( ( π β§ π < ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) ) β ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) β€ π ) |
185 |
184
|
ex |
β’ ( π β ( π < ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) β ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) β€ π ) ) |
186 |
72 185
|
sylbird |
β’ ( π β ( Β¬ ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) β€ π β ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) β€ π ) ) |
187 |
186
|
pm2.18d |
β’ ( π β ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) β€ π ) |
188 |
187
|
adantr |
β’ ( ( π β§ π¦ β π ) β ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) β€ π ) |
189 |
94
|
adantr |
β’ ( ( π β§ π¦ β π ) β π
β β ) |
190 |
100
|
adantr |
β’ ( ( π β§ π¦ β π ) β β π₯ β β β π€ β π
π₯ β€ π€ ) |
191 |
|
simpr |
β’ ( ( π β§ π¦ β π ) β π¦ β π ) |
192 |
|
fvex |
β’ ( π β ( π΄ π π¦ ) ) β V |
193 |
|
eqid |
β’ ( π¦ β π β¦ ( π β ( π΄ π π¦ ) ) ) = ( π¦ β π β¦ ( π β ( π΄ π π¦ ) ) ) |
194 |
193
|
elrnmpt1 |
β’ ( ( π¦ β π β§ ( π β ( π΄ π π¦ ) ) β V ) β ( π β ( π΄ π π¦ ) ) β ran ( π¦ β π β¦ ( π β ( π΄ π π¦ ) ) ) ) |
195 |
191 192 194
|
sylancl |
β’ ( ( π β§ π¦ β π ) β ( π β ( π΄ π π¦ ) ) β ran ( π¦ β π β¦ ( π β ( π΄ π π¦ ) ) ) ) |
196 |
195 10
|
eleqtrrdi |
β’ ( ( π β§ π¦ β π ) β ( π β ( π΄ π π¦ ) ) β π
) |
197 |
|
infrelb |
β’ ( ( π
β β β§ β π₯ β β β π€ β π
π₯ β€ π€ β§ ( π β ( π΄ π π¦ ) ) β π
) β inf ( π
, β , < ) β€ ( π β ( π΄ π π¦ ) ) ) |
198 |
189 190 196 197
|
syl3anc |
β’ ( ( π β§ π¦ β π ) β inf ( π
, β , < ) β€ ( π β ( π΄ π π¦ ) ) ) |
199 |
11 198
|
eqbrtrid |
β’ ( ( π β§ π¦ β π ) β π β€ ( π β ( π΄ π π¦ ) ) ) |
200 |
62 64 71 188 199
|
letrd |
β’ ( ( π β§ π¦ β π ) β ( π΄ π· ( ( βπ‘ β π½ ) β πΉ ) ) β€ ( π β ( π΄ π π¦ ) ) ) |
201 |
57 200
|
eqbrtrrd |
β’ ( ( π β§ π¦ β π ) β ( π β ( π΄ π ( ( βπ‘ β π½ ) β πΉ ) ) ) β€ ( π β ( π΄ π π¦ ) ) ) |
202 |
201
|
ralrimiva |
β’ ( π β β π¦ β π ( π β ( π΄ π ( ( βπ‘ β π½ ) β πΉ ) ) ) β€ ( π β ( π΄ π π¦ ) ) ) |
203 |
|
oveq2 |
β’ ( π₯ = ( ( βπ‘ β π½ ) β πΉ ) β ( π΄ π π₯ ) = ( π΄ π ( ( βπ‘ β π½ ) β πΉ ) ) ) |
204 |
203
|
fveq2d |
β’ ( π₯ = ( ( βπ‘ β π½ ) β πΉ ) β ( π β ( π΄ π π₯ ) ) = ( π β ( π΄ π ( ( βπ‘ β π½ ) β πΉ ) ) ) ) |
205 |
204
|
breq1d |
β’ ( π₯ = ( ( βπ‘ β π½ ) β πΉ ) β ( ( π β ( π΄ π π₯ ) ) β€ ( π β ( π΄ π π¦ ) ) β ( π β ( π΄ π ( ( βπ‘ β π½ ) β πΉ ) ) ) β€ ( π β ( π΄ π π¦ ) ) ) ) |
206 |
205
|
ralbidv |
β’ ( π₯ = ( ( βπ‘ β π½ ) β πΉ ) β ( β π¦ β π ( π β ( π΄ π π₯ ) ) β€ ( π β ( π΄ π π¦ ) ) β β π¦ β π ( π β ( π΄ π ( ( βπ‘ β π½ ) β πΉ ) ) ) β€ ( π β ( π΄ π π¦ ) ) ) ) |
207 |
206
|
rspcev |
β’ ( ( ( ( βπ‘ β π½ ) β πΉ ) β π β§ β π¦ β π ( π β ( π΄ π ( ( βπ‘ β π½ ) β πΉ ) ) ) β€ ( π β ( π΄ π π¦ ) ) ) β β π₯ β π β π¦ β π ( π β ( π΄ π π₯ ) ) β€ ( π β ( π΄ π π¦ ) ) ) |
208 |
53 202 207
|
syl2anc |
β’ ( π β β π₯ β π β π¦ β π ( π β ( π΄ π π₯ ) ) β€ ( π β ( π΄ π π¦ ) ) ) |