# 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}\in ℕ\to \Lambda \left({A}\right)\le \mathrm{log}{A}$

### Proof

Step Hyp Ref Expression
1 breq1 ${⊢}\Lambda \left({A}\right)=0\to \left(\Lambda \left({A}\right)\le \mathrm{log}{A}↔0\le \mathrm{log}{A}\right)$
2 isppw2 ${⊢}{A}\in ℕ\to \left(\Lambda \left({A}\right)\ne 0↔\exists {p}\in ℙ\phantom{\rule{.4em}{0ex}}\exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{A}={{p}}^{{k}}\right)$
3 prmnn ${⊢}{p}\in ℙ\to {p}\in ℕ$
4 3 nnrpd ${⊢}{p}\in ℙ\to {p}\in {ℝ}^{+}$
5 4 adantr ${⊢}\left({p}\in ℙ\wedge {k}\in ℕ\right)\to {p}\in {ℝ}^{+}$
6 5 relogcld ${⊢}\left({p}\in ℙ\wedge {k}\in ℕ\right)\to \mathrm{log}{p}\in ℝ$
7 nnre ${⊢}{k}\in ℕ\to {k}\in ℝ$
8 7 adantl ${⊢}\left({p}\in ℙ\wedge {k}\in ℕ\right)\to {k}\in ℝ$
9 log1 ${⊢}\mathrm{log}1=0$
10 3 adantr ${⊢}\left({p}\in ℙ\wedge {k}\in ℕ\right)\to {p}\in ℕ$
11 10 nnge1d ${⊢}\left({p}\in ℙ\wedge {k}\in ℕ\right)\to 1\le {p}$
12 1rp ${⊢}1\in {ℝ}^{+}$
13 logleb ${⊢}\left(1\in {ℝ}^{+}\wedge {p}\in {ℝ}^{+}\right)\to \left(1\le {p}↔\mathrm{log}1\le \mathrm{log}{p}\right)$
14 12 5 13 sylancr ${⊢}\left({p}\in ℙ\wedge {k}\in ℕ\right)\to \left(1\le {p}↔\mathrm{log}1\le \mathrm{log}{p}\right)$
15 11 14 mpbid ${⊢}\left({p}\in ℙ\wedge {k}\in ℕ\right)\to \mathrm{log}1\le \mathrm{log}{p}$
16 9 15 eqbrtrrid ${⊢}\left({p}\in ℙ\wedge {k}\in ℕ\right)\to 0\le \mathrm{log}{p}$
17 nnge1 ${⊢}{k}\in ℕ\to 1\le {k}$
18 17 adantl ${⊢}\left({p}\in ℙ\wedge {k}\in ℕ\right)\to 1\le {k}$
19 6 8 16 18 lemulge12d ${⊢}\left({p}\in ℙ\wedge {k}\in ℕ\right)\to \mathrm{log}{p}\le {k}\mathrm{log}{p}$
20 vmappw ${⊢}\left({p}\in ℙ\wedge {k}\in ℕ\right)\to \Lambda \left({{p}}^{{k}}\right)=\mathrm{log}{p}$
21 nnz ${⊢}{k}\in ℕ\to {k}\in ℤ$
22 relogexp ${⊢}\left({p}\in {ℝ}^{+}\wedge {k}\in ℤ\right)\to \mathrm{log}{{p}}^{{k}}={k}\mathrm{log}{p}$
23 4 21 22 syl2an ${⊢}\left({p}\in ℙ\wedge {k}\in ℕ\right)\to \mathrm{log}{{p}}^{{k}}={k}\mathrm{log}{p}$
24 19 20 23 3brtr4d ${⊢}\left({p}\in ℙ\wedge {k}\in ℕ\right)\to \Lambda \left({{p}}^{{k}}\right)\le \mathrm{log}{{p}}^{{k}}$
25 fveq2 ${⊢}{A}={{p}}^{{k}}\to \Lambda \left({A}\right)=\Lambda \left({{p}}^{{k}}\right)$
26 fveq2 ${⊢}{A}={{p}}^{{k}}\to \mathrm{log}{A}=\mathrm{log}{{p}}^{{k}}$
27 25 26 breq12d ${⊢}{A}={{p}}^{{k}}\to \left(\Lambda \left({A}\right)\le \mathrm{log}{A}↔\Lambda \left({{p}}^{{k}}\right)\le \mathrm{log}{{p}}^{{k}}\right)$
28 24 27 syl5ibrcom ${⊢}\left({p}\in ℙ\wedge {k}\in ℕ\right)\to \left({A}={{p}}^{{k}}\to \Lambda \left({A}\right)\le \mathrm{log}{A}\right)$
29 28 rexlimivv ${⊢}\exists {p}\in ℙ\phantom{\rule{.4em}{0ex}}\exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{A}={{p}}^{{k}}\to \Lambda \left({A}\right)\le \mathrm{log}{A}$
30 2 29 syl6bi ${⊢}{A}\in ℕ\to \left(\Lambda \left({A}\right)\ne 0\to \Lambda \left({A}\right)\le \mathrm{log}{A}\right)$
31 30 imp ${⊢}\left({A}\in ℕ\wedge \Lambda \left({A}\right)\ne 0\right)\to \Lambda \left({A}\right)\le \mathrm{log}{A}$
32 nnge1 ${⊢}{A}\in ℕ\to 1\le {A}$
33 nnrp ${⊢}{A}\in ℕ\to {A}\in {ℝ}^{+}$
34 logleb ${⊢}\left(1\in {ℝ}^{+}\wedge {A}\in {ℝ}^{+}\right)\to \left(1\le {A}↔\mathrm{log}1\le \mathrm{log}{A}\right)$
35 12 33 34 sylancr ${⊢}{A}\in ℕ\to \left(1\le {A}↔\mathrm{log}1\le \mathrm{log}{A}\right)$
36 32 35 mpbid ${⊢}{A}\in ℕ\to \mathrm{log}1\le \mathrm{log}{A}$
37 9 36 eqbrtrrid ${⊢}{A}\in ℕ\to 0\le \mathrm{log}{A}$
38 1 31 37 pm2.61ne ${⊢}{A}\in ℕ\to \Lambda \left({A}\right)\le \mathrm{log}{A}$