Theorem chtleppi

Description: Upper bound on the theta function. (Contributed by Mario Carneiro, 22-Sep-2014)

	Ref	Expression
Assertion	chtleppi	⊢ ( 𝐴 ∈ ℝ+ → ( θ ‘ 𝐴 ) ≤ ( ( π ‘ 𝐴 ) · ( log ‘ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		rpre	⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ )
2		ppifi	⊢ ( 𝐴 ∈ ℝ → ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∈ Fin )
3	1 2	syl	⊢ ( 𝐴 ∈ ℝ+ → ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∈ Fin )
4		simpr	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) )
5	4	elin2d	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ℙ )
6		prmnn	⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℕ )
7	5 6	syl	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ℕ )
8	7	nnrpd	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ℝ+ )
9	8	relogcld	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( log ‘ 𝑝 ) ∈ ℝ )
10		relogcl	⊢ ( 𝐴 ∈ ℝ+ → ( log ‘ 𝐴 ) ∈ ℝ )
11	10	adantr	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( log ‘ 𝐴 ) ∈ ℝ )
12	4	elin1d	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ( 0 [,] 𝐴 ) )
13		0re	⊢ 0 ∈ ℝ
14		elicc2	⊢ ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝑝 ∈ ( 0 [,] 𝐴 ) ↔ ( 𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ 𝐴 ) ) )
15	13 1 14	sylancr	⊢ ( 𝐴 ∈ ℝ+ → ( 𝑝 ∈ ( 0 [,] 𝐴 ) ↔ ( 𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ 𝐴 ) ) )
16	15	biimpa	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑝 ∈ ( 0 [,] 𝐴 ) ) → ( 𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ 𝐴 ) )
17	12 16	syldan	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ 𝐴 ) )
18	17	simp3d	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ≤ 𝐴 )
19	8	reeflogd	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( exp ‘ ( log ‘ 𝑝 ) ) = 𝑝 )
20		reeflog	⊢ ( 𝐴 ∈ ℝ+ → ( exp ‘ ( log ‘ 𝐴 ) ) = 𝐴 )
21	20	adantr	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( exp ‘ ( log ‘ 𝐴 ) ) = 𝐴 )
22	18 19 21	3brtr4d	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( exp ‘ ( log ‘ 𝑝 ) ) ≤ ( exp ‘ ( log ‘ 𝐴 ) ) )
23		efle	⊢ ( ( ( log ‘ 𝑝 ) ∈ ℝ ∧ ( log ‘ 𝐴 ) ∈ ℝ ) → ( ( log ‘ 𝑝 ) ≤ ( log ‘ 𝐴 ) ↔ ( exp ‘ ( log ‘ 𝑝 ) ) ≤ ( exp ‘ ( log ‘ 𝐴 ) ) ) )
24	9 11 23	syl2anc	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( log ‘ 𝑝 ) ≤ ( log ‘ 𝐴 ) ↔ ( exp ‘ ( log ‘ 𝑝 ) ) ≤ ( exp ‘ ( log ‘ 𝐴 ) ) ) )
25	22 24	mpbird	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( log ‘ 𝑝 ) ≤ ( log ‘ 𝐴 ) )
26	3 9 11 25	fsumle	⊢ ( 𝐴 ∈ ℝ+ → Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( log ‘ 𝑝 ) ≤ Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( log ‘ 𝐴 ) )
27		chtval	⊢ ( 𝐴 ∈ ℝ → ( θ ‘ 𝐴 ) = Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( log ‘ 𝑝 ) )
28	1 27	syl	⊢ ( 𝐴 ∈ ℝ+ → ( θ ‘ 𝐴 ) = Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( log ‘ 𝑝 ) )
29		ppival	⊢ ( 𝐴 ∈ ℝ → ( π ‘ 𝐴 ) = ( ♯ ‘ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) )
30	1 29	syl	⊢ ( 𝐴 ∈ ℝ+ → ( π ‘ 𝐴 ) = ( ♯ ‘ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) )
31	30	oveq1d	⊢ ( 𝐴 ∈ ℝ+ → ( ( π ‘ 𝐴 ) · ( log ‘ 𝐴 ) ) = ( ( ♯ ‘ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) · ( log ‘ 𝐴 ) ) )
32	10	recnd	⊢ ( 𝐴 ∈ ℝ+ → ( log ‘ 𝐴 ) ∈ ℂ )
33		fsumconst	⊢ ( ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∈ Fin ∧ ( log ‘ 𝐴 ) ∈ ℂ ) → Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( log ‘ 𝐴 ) = ( ( ♯ ‘ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) · ( log ‘ 𝐴 ) ) )
34	3 32 33	syl2anc	⊢ ( 𝐴 ∈ ℝ+ → Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( log ‘ 𝐴 ) = ( ( ♯ ‘ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) · ( log ‘ 𝐴 ) ) )
35	31 34	eqtr4d	⊢ ( 𝐴 ∈ ℝ+ → ( ( π ‘ 𝐴 ) · ( log ‘ 𝐴 ) ) = Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( log ‘ 𝐴 ) )
36	26 28 35	3brtr4d	⊢ ( 𝐴 ∈ ℝ+ → ( θ ‘ 𝐴 ) ≤ ( ( π ‘ 𝐴 ) · ( log ‘ 𝐴 ) ) )