Metamath Proof Explorer


Theorem chebbnd2

Description: The Chebyshev bound, part 2: The function ppi ( x ) is eventually upper bounded by a positive constant times x / log ( x ) . Alternatively stated, the function ppi ( x ) / ( x / log ( x ) ) is eventually bounded. (Contributed by Mario Carneiro, 22-Sep-2014)

Ref Expression
Assertion chebbnd2 ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( π𝑥 ) / ( 𝑥 / ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1)

Proof

Step Hyp Ref Expression
1 ovexd ( ⊤ → ( 2 [,) +∞ ) ∈ V )
2 ovexd ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( θ ‘ 𝑥 ) / 𝑥 ) ∈ V )
3 ovexd ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) / ( θ ‘ 𝑥 ) ) ∈ V )
4 eqidd ( ⊤ → ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( θ ‘ 𝑥 ) / 𝑥 ) ) = ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( θ ‘ 𝑥 ) / 𝑥 ) ) )
5 simpr ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → 𝑥 ∈ ( 2 [,) +∞ ) )
6 2re 2 ∈ ℝ
7 elicopnf ( 2 ∈ ℝ → ( 𝑥 ∈ ( 2 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 2 ≤ 𝑥 ) ) )
8 6 7 ax-mp ( 𝑥 ∈ ( 2 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 2 ≤ 𝑥 ) )
9 5 8 sylib ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( 𝑥 ∈ ℝ ∧ 2 ≤ 𝑥 ) )
10 chtrpcl ( ( 𝑥 ∈ ℝ ∧ 2 ≤ 𝑥 ) → ( θ ‘ 𝑥 ) ∈ ℝ+ )
11 9 10 syl ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( θ ‘ 𝑥 ) ∈ ℝ+ )
12 11 rpcnne0d ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( θ ‘ 𝑥 ) ∈ ℂ ∧ ( θ ‘ 𝑥 ) ≠ 0 ) )
13 ppinncl ( ( 𝑥 ∈ ℝ ∧ 2 ≤ 𝑥 ) → ( π𝑥 ) ∈ ℕ )
14 9 13 syl ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( π𝑥 ) ∈ ℕ )
15 14 nnrpd ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( π𝑥 ) ∈ ℝ+ )
16 9 simpld ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → 𝑥 ∈ ℝ )
17 1red ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → 1 ∈ ℝ )
18 6 a1i ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → 2 ∈ ℝ )
19 1lt2 1 < 2
20 19 a1i ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → 1 < 2 )
21 9 simprd ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → 2 ≤ 𝑥 )
22 17 18 16 20 21 ltletrd ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → 1 < 𝑥 )
23 16 22 rplogcld ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( log ‘ 𝑥 ) ∈ ℝ+ )
24 15 23 rpmulcld ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) ∈ ℝ+ )
25 24 rpcnne0d ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) ∈ ℂ ∧ ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) ≠ 0 ) )
26 recdiv ( ( ( ( θ ‘ 𝑥 ) ∈ ℂ ∧ ( θ ‘ 𝑥 ) ≠ 0 ) ∧ ( ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) ∈ ℂ ∧ ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) ≠ 0 ) ) → ( 1 / ( ( θ ‘ 𝑥 ) / ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) ) ) = ( ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) / ( θ ‘ 𝑥 ) ) )
27 12 25 26 syl2anc ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( 1 / ( ( θ ‘ 𝑥 ) / ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) ) ) = ( ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) / ( θ ‘ 𝑥 ) ) )
28 27 mpteq2dva ( ⊤ → ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( 1 / ( ( θ ‘ 𝑥 ) / ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) ) ) ) = ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) / ( θ ‘ 𝑥 ) ) ) )
29 1 2 3 4 28 offval2 ( ⊤ → ( ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( θ ‘ 𝑥 ) / 𝑥 ) ) ∘f · ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( 1 / ( ( θ ‘ 𝑥 ) / ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) ) ) ) ) = ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( ( θ ‘ 𝑥 ) / 𝑥 ) · ( ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) / ( θ ‘ 𝑥 ) ) ) ) )
30 0red ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → 0 ∈ ℝ )
31 2pos 0 < 2
32 31 a1i ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → 0 < 2 )
33 30 18 16 32 21 ltletrd ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → 0 < 𝑥 )
34 16 33 elrpd ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → 𝑥 ∈ ℝ+ )
35 34 rpcnne0d ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) )
36 24 rpcnd ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) ∈ ℂ )
37 dmdcan ( ( ( ( θ ‘ 𝑥 ) ∈ ℂ ∧ ( θ ‘ 𝑥 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ∧ ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) ∈ ℂ ) → ( ( ( θ ‘ 𝑥 ) / 𝑥 ) · ( ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) / ( θ ‘ 𝑥 ) ) ) = ( ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) / 𝑥 ) )
38 12 35 36 37 syl3anc ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( ( θ ‘ 𝑥 ) / 𝑥 ) · ( ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) / ( θ ‘ 𝑥 ) ) ) = ( ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) / 𝑥 ) )
39 15 rpcnd ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( π𝑥 ) ∈ ℂ )
40 23 rpcnne0d ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( log ‘ 𝑥 ) ∈ ℂ ∧ ( log ‘ 𝑥 ) ≠ 0 ) )
41 divdiv2 ( ( ( π𝑥 ) ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ∧ ( ( log ‘ 𝑥 ) ∈ ℂ ∧ ( log ‘ 𝑥 ) ≠ 0 ) ) → ( ( π𝑥 ) / ( 𝑥 / ( log ‘ 𝑥 ) ) ) = ( ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) / 𝑥 ) )
42 39 35 40 41 syl3anc ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( π𝑥 ) / ( 𝑥 / ( log ‘ 𝑥 ) ) ) = ( ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) / 𝑥 ) )
43 38 42 eqtr4d ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( ( θ ‘ 𝑥 ) / 𝑥 ) · ( ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) / ( θ ‘ 𝑥 ) ) ) = ( ( π𝑥 ) / ( 𝑥 / ( log ‘ 𝑥 ) ) ) )
44 43 mpteq2dva ( ⊤ → ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( ( θ ‘ 𝑥 ) / 𝑥 ) · ( ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) / ( θ ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( π𝑥 ) / ( 𝑥 / ( log ‘ 𝑥 ) ) ) ) )
45 29 44 eqtrd ( ⊤ → ( ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( θ ‘ 𝑥 ) / 𝑥 ) ) ∘f · ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( 1 / ( ( θ ‘ 𝑥 ) / ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) ) ) ) ) = ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( π𝑥 ) / ( 𝑥 / ( log ‘ 𝑥 ) ) ) ) )
46 34 ex ( ⊤ → ( 𝑥 ∈ ( 2 [,) +∞ ) → 𝑥 ∈ ℝ+ ) )
47 46 ssrdv ( ⊤ → ( 2 [,) +∞ ) ⊆ ℝ+ )
48 chto1ub ( 𝑥 ∈ ℝ+ ↦ ( ( θ ‘ 𝑥 ) / 𝑥 ) ) ∈ 𝑂(1)
49 48 a1i ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( ( θ ‘ 𝑥 ) / 𝑥 ) ) ∈ 𝑂(1) )
50 47 49 o1res2 ( ⊤ → ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( θ ‘ 𝑥 ) / 𝑥 ) ) ∈ 𝑂(1) )
51 ax-1cn 1 ∈ ℂ
52 51 a1i ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → 1 ∈ ℂ )
53 11 24 rpdivcld ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( θ ‘ 𝑥 ) / ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) ) ∈ ℝ+ )
54 53 rpcnd ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( θ ‘ 𝑥 ) / ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) ) ∈ ℂ )
55 pnfxr +∞ ∈ ℝ*
56 icossre ( ( 2 ∈ ℝ ∧ +∞ ∈ ℝ* ) → ( 2 [,) +∞ ) ⊆ ℝ )
57 6 55 56 mp2an ( 2 [,) +∞ ) ⊆ ℝ
58 rlimconst ( ( ( 2 [,) +∞ ) ⊆ ℝ ∧ 1 ∈ ℂ ) → ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ 1 ) ⇝𝑟 1 )
59 57 51 58 mp2an ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ 1 ) ⇝𝑟 1
60 59 a1i ( ⊤ → ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ 1 ) ⇝𝑟 1 )
61 chtppilim ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( θ ‘ 𝑥 ) / ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) ) ) ⇝𝑟 1
62 61 a1i ( ⊤ → ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( θ ‘ 𝑥 ) / ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) ) ) ⇝𝑟 1 )
63 ax-1ne0 1 ≠ 0
64 63 a1i ( ⊤ → 1 ≠ 0 )
65 53 rpne0d ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( θ ‘ 𝑥 ) / ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) ) ≠ 0 )
66 52 54 60 62 64 65 rlimdiv ( ⊤ → ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( 1 / ( ( θ ‘ 𝑥 ) / ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) ) ) ) ⇝𝑟 ( 1 / 1 ) )
67 rlimo1 ( ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( 1 / ( ( θ ‘ 𝑥 ) / ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) ) ) ) ⇝𝑟 ( 1 / 1 ) → ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( 1 / ( ( θ ‘ 𝑥 ) / ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) ) ) ) ∈ 𝑂(1) )
68 66 67 syl ( ⊤ → ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( 1 / ( ( θ ‘ 𝑥 ) / ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) ) ) ) ∈ 𝑂(1) )
69 o1mul ( ( ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( θ ‘ 𝑥 ) / 𝑥 ) ) ∈ 𝑂(1) ∧ ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( 1 / ( ( θ ‘ 𝑥 ) / ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) ) ) ) ∈ 𝑂(1) ) → ( ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( θ ‘ 𝑥 ) / 𝑥 ) ) ∘f · ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( 1 / ( ( θ ‘ 𝑥 ) / ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) ) ) ) ) ∈ 𝑂(1) )
70 50 68 69 syl2anc ( ⊤ → ( ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( θ ‘ 𝑥 ) / 𝑥 ) ) ∘f · ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( 1 / ( ( θ ‘ 𝑥 ) / ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) ) ) ) ) ∈ 𝑂(1) )
71 45 70 eqeltrrd ( ⊤ → ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( π𝑥 ) / ( 𝑥 / ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) )
72 71 mptru ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( π𝑥 ) / ( 𝑥 / ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1)