This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem vmalelog

Description: The von Mangoldt function is less than the natural log. (Contributed by Mario Carneiro, 7-Apr-2016)

Ref Expression
Assertion vmalelog 
|- ( A e. NN -> ( Lam ` A ) <_ ( log ` A ) )

Proof

Step Hyp Ref Expression
1 breq1 
 |-  ( ( Lam ` A ) = 0 -> ( ( Lam ` A ) <_ ( log ` A ) <-> 0 <_ ( log ` A ) ) )
2 isppw2 
 |-  ( A e. NN -> ( ( Lam ` A ) =/= 0 <-> E. p e. Prime E. k e. NN A = ( p ^ k ) ) )
3 prmnn 
 |-  ( p e. Prime -> p e. NN )
4 3 nnrpd 
 |-  ( p e. Prime -> p e. RR+ )
5 4 adantr 
 |-  ( ( p e. Prime /\ k e. NN ) -> p e. RR+ )
6 5 relogcld 
 |-  ( ( p e. Prime /\ k e. NN ) -> ( log ` p ) e. RR )
7 nnre 
 |-  ( k e. NN -> k e. RR )
8 7 adantl 
 |-  ( ( p e. Prime /\ k e. NN ) -> k e. RR )
9 log1 
 |-  ( log ` 1 ) = 0
10 3 adantr 
 |-  ( ( p e. Prime /\ k e. NN ) -> p e. NN )
11 10 nnge1d 
 |-  ( ( p e. Prime /\ k e. NN ) -> 1 <_ p )
12 1rp 
 |-  1 e. RR+
13 logleb 
 |-  ( ( 1 e. RR+ /\ p e. RR+ ) -> ( 1 <_ p <-> ( log ` 1 ) <_ ( log ` p ) ) )
14 12 5 13 sylancr 
 |-  ( ( p e. Prime /\ k e. NN ) -> ( 1 <_ p <-> ( log ` 1 ) <_ ( log ` p ) ) )
15 11 14 mpbid 
 |-  ( ( p e. Prime /\ k e. NN ) -> ( log ` 1 ) <_ ( log ` p ) )
16 9 15 eqbrtrrid 
 |-  ( ( p e. Prime /\ k e. NN ) -> 0 <_ ( log ` p ) )
17 nnge1 
 |-  ( k e. NN -> 1 <_ k )
18 17 adantl 
 |-  ( ( p e. Prime /\ k e. NN ) -> 1 <_ k )
19 6 8 16 18 lemulge12d 
 |-  ( ( p e. Prime /\ k e. NN ) -> ( log ` p ) <_ ( k x. ( log ` p ) ) )
20 vmappw 
 |-  ( ( p e. Prime /\ k e. NN ) -> ( Lam ` ( p ^ k ) ) = ( log ` p ) )
21 nnz 
 |-  ( k e. NN -> k e. ZZ )
22 relogexp 
 |-  ( ( p e. RR+ /\ k e. ZZ ) -> ( log ` ( p ^ k ) ) = ( k x. ( log ` p ) ) )
23 4 21 22 syl2an 
 |-  ( ( p e. Prime /\ k e. NN ) -> ( log ` ( p ^ k ) ) = ( k x. ( log ` p ) ) )
24 19 20 23 3brtr4d 
 |-  ( ( p e. Prime /\ k e. NN ) -> ( Lam ` ( p ^ k ) ) <_ ( log ` ( p ^ k ) ) )
25 fveq2 
 |-  ( A = ( p ^ k ) -> ( Lam ` A ) = ( Lam ` ( p ^ k ) ) )
26 fveq2 
 |-  ( A = ( p ^ k ) -> ( log ` A ) = ( log ` ( p ^ k ) ) )
27 25 26 breq12d 
 |-  ( A = ( p ^ k ) -> ( ( Lam ` A ) <_ ( log ` A ) <-> ( Lam ` ( p ^ k ) ) <_ ( log ` ( p ^ k ) ) ) )
28 24 27 syl5ibrcom 
 |-  ( ( p e. Prime /\ k e. NN ) -> ( A = ( p ^ k ) -> ( Lam ` A ) <_ ( log ` A ) ) )
29 28 rexlimivv 
 |-  ( E. p e. Prime E. k e. NN A = ( p ^ k ) -> ( Lam ` A ) <_ ( log ` A ) )
30 2 29 biimtrdi 
 |-  ( A e. NN -> ( ( Lam ` A ) =/= 0 -> ( Lam ` A ) <_ ( log ` A ) ) )
31 30 imp 
 |-  ( ( A e. NN /\ ( Lam ` A ) =/= 0 ) -> ( Lam ` A ) <_ ( log ` A ) )
32 nnge1 
 |-  ( A e. NN -> 1 <_ A )
33 nnrp 
 |-  ( A e. NN -> A e. RR+ )
34 logleb 
 |-  ( ( 1 e. RR+ /\ A e. RR+ ) -> ( 1 <_ A <-> ( log ` 1 ) <_ ( log ` A ) ) )
35 12 33 34 sylancr 
 |-  ( A e. NN -> ( 1 <_ A <-> ( log ` 1 ) <_ ( log ` A ) ) )
36 32 35 mpbid 
 |-  ( A e. NN -> ( log ` 1 ) <_ ( log ` A ) )
37 9 36 eqbrtrrid 
 |-  ( A e. NN -> 0 <_ ( log ` A ) )
38 1 31 37 pm2.61ne 
 |-  ( A e. NN -> ( Lam ` A ) <_ ( log ` A ) )