This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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