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 ∈ ℕ → Λ ⁡ A ≤ log ⁡ A

Proof

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