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 ‘ 𝐴 ) )