Metamath Proof Explorer


Theorem 2vmadivsum

Description: The sum sum_ m n <_ x , Lam ( m ) Lam ( n ) / m n is asymptotic to log ^ 2 ( x ) / 2 + O ( log x ) . (Contributed by Mario Carneiro, 30-May-2016)

Ref Expression
Assertion 2vmadivsum ( ๐‘ฅ โˆˆ ( 1 (,) +โˆž ) โ†ฆ ( ( ฮฃ ๐‘› โˆˆ ( 1 ... ( โŒŠ โ€˜ ๐‘ฅ ) ) ( ( ( ฮ› โ€˜ ๐‘› ) / ๐‘› ) ยท ฮฃ ๐‘š โˆˆ ( 1 ... ( โŒŠ โ€˜ ( ๐‘ฅ / ๐‘› ) ) ) ( ( ฮ› โ€˜ ๐‘š ) / ๐‘š ) ) / ( log โ€˜ ๐‘ฅ ) ) โˆ’ ( ( log โ€˜ ๐‘ฅ ) / 2 ) ) ) โˆˆ ๐‘‚(1)

Proof

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)