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)