Step |
Hyp |
Ref |
Expression |
1 |
|
vmadivsumb |
โข โ ๐ โ โ+ โ ๐ฆ โ ( 1 [,) +โ ) ( abs โ ( ฮฃ ๐ โ ( 1 ... ( โ โ ๐ฆ ) ) ( ( ฮ โ ๐ ) / ๐ ) โ ( log โ ๐ฆ ) ) ) โค ๐ |
2 |
|
simpl |
โข ( ( ๐ โ โ+ โง โ ๐ฆ โ ( 1 [,) +โ ) ( abs โ ( ฮฃ ๐ โ ( 1 ... ( โ โ ๐ฆ ) ) ( ( ฮ โ ๐ ) / ๐ ) โ ( log โ ๐ฆ ) ) ) โค ๐ ) โ ๐ โ โ+ ) |
3 |
|
simpr |
โข ( ( ๐ โ โ+ โง โ ๐ฆ โ ( 1 [,) +โ ) ( abs โ ( ฮฃ ๐ โ ( 1 ... ( โ โ ๐ฆ ) ) ( ( ฮ โ ๐ ) / ๐ ) โ ( log โ ๐ฆ ) ) ) โค ๐ ) โ โ ๐ฆ โ ( 1 [,) +โ ) ( abs โ ( ฮฃ ๐ โ ( 1 ... ( โ โ ๐ฆ ) ) ( ( ฮ โ ๐ ) / ๐ ) โ ( log โ ๐ฆ ) ) ) โค ๐ ) |
4 |
2 3
|
2vmadivsumlem |
โข ( ( ๐ โ โ+ โง โ ๐ฆ โ ( 1 [,) +โ ) ( abs โ ( ฮฃ ๐ โ ( 1 ... ( โ โ ๐ฆ ) ) ( ( ฮ โ ๐ ) / ๐ ) โ ( log โ ๐ฆ ) ) ) โค ๐ ) โ ( ๐ฅ โ ( 1 (,) +โ ) โฆ ( ( ฮฃ ๐ โ ( 1 ... ( โ โ ๐ฅ ) ) ( ( ( ฮ โ ๐ ) / ๐ ) ยท ฮฃ ๐ โ ( 1 ... ( โ โ ( ๐ฅ / ๐ ) ) ) ( ( ฮ โ ๐ ) / ๐ ) ) / ( log โ ๐ฅ ) ) โ ( ( log โ ๐ฅ ) / 2 ) ) ) โ ๐(1) ) |
5 |
4
|
rexlimiva |
โข ( โ ๐ โ โ+ โ ๐ฆ โ ( 1 [,) +โ ) ( abs โ ( ฮฃ ๐ โ ( 1 ... ( โ โ ๐ฆ ) ) ( ( ฮ โ ๐ ) / ๐ ) โ ( log โ ๐ฆ ) ) ) โค ๐ โ ( ๐ฅ โ ( 1 (,) +โ ) โฆ ( ( ฮฃ ๐ โ ( 1 ... ( โ โ ๐ฅ ) ) ( ( ( ฮ โ ๐ ) / ๐ ) ยท ฮฃ ๐ โ ( 1 ... ( โ โ ( ๐ฅ / ๐ ) ) ) ( ( ฮ โ ๐ ) / ๐ ) ) / ( log โ ๐ฅ ) ) โ ( ( log โ ๐ฅ ) / 2 ) ) ) โ ๐(1) ) |
6 |
1 5
|
ax-mp |
โข ( ๐ฅ โ ( 1 (,) +โ ) โฆ ( ( ฮฃ ๐ โ ( 1 ... ( โ โ ๐ฅ ) ) ( ( ( ฮ โ ๐ ) / ๐ ) ยท ฮฃ ๐ โ ( 1 ... ( โ โ ( ๐ฅ / ๐ ) ) ) ( ( ฮ โ ๐ ) / ๐ ) ) / ( log โ ๐ฅ ) ) โ ( ( log โ ๐ฅ ) / 2 ) ) ) โ ๐(1) |