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 ( 𝐴 ∈ ℕ → ( Λ ‘ 𝐴 ) ≤ ( log ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 breq1 ⊢ ( ( Λ ‘ 𝐴 ) = 0 → ( ( Λ ‘ 𝐴 ) ≤ ( log ‘ 𝐴 ) ↔ 0 ≤ ( log ‘ 𝐴 ) ) )
2 isppw2 ⊢ ( 𝐴 ∈ ℕ → ( ( Λ ‘ 𝐴 ) ≠ 0 ↔ ∃ 𝑝 ∈ ℙ ∃ 𝑘 ∈ ℕ 𝐴 = ( 𝑝 ↑ 𝑘 ) ) )
3 prmnn ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℕ )
4 3 nnrpd ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℝ+ )
5 4 adantr ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) → 𝑝 ∈ ℝ+ )
6 5 relogcld ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) → ( log ‘ 𝑝 ) ∈ ℝ )
7 nnre ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℝ )
8 7 adantl ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℝ )
9 log1 ⊢ ( log ‘ 1 ) = 0
10 3 adantr ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) → 𝑝 ∈ ℕ )
11 10 nnge1d ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) → 1 ≤ 𝑝 )
12 1rp ⊢ 1 ∈ ℝ+
13 logleb ⊢ ( ( 1 ∈ ℝ+ ∧ 𝑝 ∈ ℝ+ ) → ( 1 ≤ 𝑝 ↔ ( log ‘ 1 ) ≤ ( log ‘ 𝑝 ) ) )
14 12 5 13 sylancr ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) → ( 1 ≤ 𝑝 ↔ ( log ‘ 1 ) ≤ ( log ‘ 𝑝 ) ) )
15 11 14 mpbid ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) → ( log ‘ 1 ) ≤ ( log ‘ 𝑝 ) )
16 9 15 eqbrtrrid ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) → 0 ≤ ( log ‘ 𝑝 ) )
17 nnge1 ⊢ ( 𝑘 ∈ ℕ → 1 ≤ 𝑘 )
18 17 adantl ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) → 1 ≤ 𝑘 )
19 6 8 16 18 lemulge12d ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) → ( log ‘ 𝑝 ) ≤ ( 𝑘 · ( log ‘ 𝑝 ) ) )
20 vmappw ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) → ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) = ( log ‘ 𝑝 ) )
21 nnz ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℤ )
22 relogexp ⊢ ( ( 𝑝 ∈ ℝ+ ∧ 𝑘 ∈ ℤ ) → ( log ‘ ( 𝑝 ↑ 𝑘 ) ) = ( 𝑘 · ( log ‘ 𝑝 ) ) )
23 4 21 22 syl2an ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) → ( log ‘ ( 𝑝 ↑ 𝑘 ) ) = ( 𝑘 · ( log ‘ 𝑝 ) ) )
24 19 20 23 3brtr4d ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) → ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) ≤ ( log ‘ ( 𝑝 ↑ 𝑘 ) ) )
25 fveq2 ⊢ ( 𝐴 = ( 𝑝 ↑ 𝑘 ) → ( Λ ‘ 𝐴 ) = ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) )
26 fveq2 ⊢ ( 𝐴 = ( 𝑝 ↑ 𝑘 ) → ( log ‘ 𝐴 ) = ( log ‘ ( 𝑝 ↑ 𝑘 ) ) )
27 25 26 breq12d ⊢ ( 𝐴 = ( 𝑝 ↑ 𝑘 ) → ( ( Λ ‘ 𝐴 ) ≤ ( log ‘ 𝐴 ) ↔ ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) ≤ ( log ‘ ( 𝑝 ↑ 𝑘 ) ) ) )
28 24 27 syl5ibrcom ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) → ( 𝐴 = ( 𝑝 ↑ 𝑘 ) → ( Λ ‘ 𝐴 ) ≤ ( log ‘ 𝐴 ) ) )
29 28 rexlimivv ⊢ ( ∃ 𝑝 ∈ ℙ ∃ 𝑘 ∈ ℕ 𝐴 = ( 𝑝 ↑ 𝑘 ) → ( Λ ‘ 𝐴 ) ≤ ( log ‘ 𝐴 ) )
30 2 29 biimtrdi ⊢ ( 𝐴 ∈ ℕ → ( ( Λ ‘ 𝐴 ) ≠ 0 → ( Λ ‘ 𝐴 ) ≤ ( log ‘ 𝐴 ) ) )
31 30 imp ⊢ ( ( 𝐴 ∈ ℕ ∧ ( Λ ‘ 𝐴 ) ≠ 0 ) → ( Λ ‘ 𝐴 ) ≤ ( log ‘ 𝐴 ) )
32 nnge1 ⊢ ( 𝐴 ∈ ℕ → 1 ≤ 𝐴 )
33 nnrp ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℝ+ )
34 logleb ⊢ ( ( 1 ∈ ℝ+ ∧ 𝐴 ∈ ℝ+ ) → ( 1 ≤ 𝐴 ↔ ( log ‘ 1 ) ≤ ( log ‘ 𝐴 ) ) )
35 12 33 34 sylancr ⊢ ( 𝐴 ∈ ℕ → ( 1 ≤ 𝐴 ↔ ( log ‘ 1 ) ≤ ( log ‘ 𝐴 ) ) )
36 32 35 mpbid ⊢ ( 𝐴 ∈ ℕ → ( log ‘ 1 ) ≤ ( log ‘ 𝐴 ) )
37 9 36 eqbrtrrid ⊢ ( 𝐴 ∈ ℕ → 0 ≤ ( log ‘ 𝐴 ) )
38 1 31 37 pm2.61ne ⊢ ( 𝐴 ∈ ℕ → ( Λ ‘ 𝐴 ) ≤ ( log ‘ 𝐴 ) )