Theorem pnt2

Description: The Prime Number Theorem, version 2: the first Chebyshev function tends asymptotically to x . (Contributed by Mario Carneiro, 1-Jun-2016)

	Ref	Expression
Assertion	pnt2	⊢ ( 𝑥 ∈ ℝ+ ↦ ( ( θ ‘ 𝑥 ) / 𝑥 ) ) ⇝𝑟 1

Proof

Step	Hyp	Ref	Expression
1		2re	⊢ 2 ∈ ℝ
2		elicopnf	⊢ ( 2 ∈ ℝ → ( 𝑥 ∈ ( 2 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 2 ≤ 𝑥 ) ) )
3	1 2	ax-mp	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 2 ≤ 𝑥 ) )
4		chprpcl	⊢ ( ( 𝑥 ∈ ℝ ∧ 2 ≤ 𝑥 ) → ( ψ ‘ 𝑥 ) ∈ ℝ+ )
5	3 4	sylbi	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( ψ ‘ 𝑥 ) ∈ ℝ+ )
6	3	simplbi	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → 𝑥 ∈ ℝ )
7		0red	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → 0 ∈ ℝ )
8	1	a1i	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → 2 ∈ ℝ )
9		2pos	⊢ 0 < 2
10	9	a1i	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → 0 < 2 )
11	3	simprbi	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → 2 ≤ 𝑥 )
12	7 8 6 10 11	ltletrd	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → 0 < 𝑥 )
13	6 12	elrpd	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → 𝑥 ∈ ℝ+ )
14	5 13	rpdivcld	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( ( ψ ‘ 𝑥 ) / 𝑥 ) ∈ ℝ+ )
15	14	adantl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( ψ ‘ 𝑥 ) / 𝑥 ) ∈ ℝ+ )
16		chtrpcl	⊢ ( ( 𝑥 ∈ ℝ ∧ 2 ≤ 𝑥 ) → ( θ ‘ 𝑥 ) ∈ ℝ+ )
17	3 16	sylbi	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( θ ‘ 𝑥 ) ∈ ℝ+ )
18	5 17	rpdivcld	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( ( ψ ‘ 𝑥 ) / ( θ ‘ 𝑥 ) ) ∈ ℝ+ )
19	18	adantl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( ψ ‘ 𝑥 ) / ( θ ‘ 𝑥 ) ) ∈ ℝ+ )
20	13	ssriv	⊢ ( 2 [,) +∞ ) ⊆ ℝ+
21	20	a1i	⊢ ( ⊤ → ( 2 [,) +∞ ) ⊆ ℝ+ )
22		pnt3	⊢ ( 𝑥 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑥 ) / 𝑥 ) ) ⇝𝑟 1
23	22	a1i	⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑥 ) / 𝑥 ) ) ⇝𝑟 1 )
24	21 23	rlimres2	⊢ ( ⊤ → ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( ψ ‘ 𝑥 ) / 𝑥 ) ) ⇝𝑟 1 )
25		chpchtlim	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( ψ ‘ 𝑥 ) / ( θ ‘ 𝑥 ) ) ) ⇝𝑟 1
26	25	a1i	⊢ ( ⊤ → ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( ψ ‘ 𝑥 ) / ( θ ‘ 𝑥 ) ) ) ⇝𝑟 1 )
27		ax-1ne0	⊢ 1 ≠ 0
28	27	a1i	⊢ ( ⊤ → 1 ≠ 0 )
29	19	rpne0d	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( ψ ‘ 𝑥 ) / ( θ ‘ 𝑥 ) ) ≠ 0 )
30	15 19 24 26 28 29	rlimdiv	⊢ ( ⊤ → ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) / ( ( ψ ‘ 𝑥 ) / ( θ ‘ 𝑥 ) ) ) ) ⇝𝑟 ( 1 / 1 ) )
31		rpre	⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ )
32		chpcl	⊢ ( 𝑥 ∈ ℝ → ( ψ ‘ 𝑥 ) ∈ ℝ )
33	31 32	syl	⊢ ( 𝑥 ∈ ℝ+ → ( ψ ‘ 𝑥 ) ∈ ℝ )
34	33	recnd	⊢ ( 𝑥 ∈ ℝ+ → ( ψ ‘ 𝑥 ) ∈ ℂ )
35	13 34	syl	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( ψ ‘ 𝑥 ) ∈ ℂ )
36	13	rpcnne0d	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) )
37	5	rpcnne0d	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( ( ψ ‘ 𝑥 ) ∈ ℂ ∧ ( ψ ‘ 𝑥 ) ≠ 0 ) )
38	17	rpcnne0d	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( ( θ ‘ 𝑥 ) ∈ ℂ ∧ ( θ ‘ 𝑥 ) ≠ 0 ) )
39		divdivdiv	⊢ ( ( ( ( ψ ‘ 𝑥 ) ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ) ∧ ( ( ( ψ ‘ 𝑥 ) ∈ ℂ ∧ ( ψ ‘ 𝑥 ) ≠ 0 ) ∧ ( ( θ ‘ 𝑥 ) ∈ ℂ ∧ ( θ ‘ 𝑥 ) ≠ 0 ) ) ) → ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) / ( ( ψ ‘ 𝑥 ) / ( θ ‘ 𝑥 ) ) ) = ( ( ( ψ ‘ 𝑥 ) · ( θ ‘ 𝑥 ) ) / ( 𝑥 · ( ψ ‘ 𝑥 ) ) ) )
40	35 36 37 38 39	syl22anc	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) / ( ( ψ ‘ 𝑥 ) / ( θ ‘ 𝑥 ) ) ) = ( ( ( ψ ‘ 𝑥 ) · ( θ ‘ 𝑥 ) ) / ( 𝑥 · ( ψ ‘ 𝑥 ) ) ) )
41	6	recnd	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → 𝑥 ∈ ℂ )
42	41 35	mulcomd	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( 𝑥 · ( ψ ‘ 𝑥 ) ) = ( ( ψ ‘ 𝑥 ) · 𝑥 ) )
43	42	oveq2d	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( ( ( ψ ‘ 𝑥 ) · ( θ ‘ 𝑥 ) ) / ( 𝑥 · ( ψ ‘ 𝑥 ) ) ) = ( ( ( ψ ‘ 𝑥 ) · ( θ ‘ 𝑥 ) ) / ( ( ψ ‘ 𝑥 ) · 𝑥 ) ) )
44		chtcl	⊢ ( 𝑥 ∈ ℝ → ( θ ‘ 𝑥 ) ∈ ℝ )
45	31 44	syl	⊢ ( 𝑥 ∈ ℝ+ → ( θ ‘ 𝑥 ) ∈ ℝ )
46	45	recnd	⊢ ( 𝑥 ∈ ℝ+ → ( θ ‘ 𝑥 ) ∈ ℂ )
47	13 46	syl	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( θ ‘ 𝑥 ) ∈ ℂ )
48		divcan5	⊢ ( ( ( θ ‘ 𝑥 ) ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ∧ ( ( ψ ‘ 𝑥 ) ∈ ℂ ∧ ( ψ ‘ 𝑥 ) ≠ 0 ) ) → ( ( ( ψ ‘ 𝑥 ) · ( θ ‘ 𝑥 ) ) / ( ( ψ ‘ 𝑥 ) · 𝑥 ) ) = ( ( θ ‘ 𝑥 ) / 𝑥 ) )
49	47 36 37 48	syl3anc	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( ( ( ψ ‘ 𝑥 ) · ( θ ‘ 𝑥 ) ) / ( ( ψ ‘ 𝑥 ) · 𝑥 ) ) = ( ( θ ‘ 𝑥 ) / 𝑥 ) )
50	40 43 49	3eqtrd	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) / ( ( ψ ‘ 𝑥 ) / ( θ ‘ 𝑥 ) ) ) = ( ( θ ‘ 𝑥 ) / 𝑥 ) )
51	50	mpteq2ia	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) / ( ( ψ ‘ 𝑥 ) / ( θ ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( θ ‘ 𝑥 ) / 𝑥 ) )
52		resmpt	⊢ ( ( 2 [,) +∞ ) ⊆ ℝ+ → ( ( 𝑥 ∈ ℝ+ ↦ ( ( θ ‘ 𝑥 ) / 𝑥 ) ) ↾ ( 2 [,) +∞ ) ) = ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( θ ‘ 𝑥 ) / 𝑥 ) ) )
53	20 52	ax-mp	⊢ ( ( 𝑥 ∈ ℝ+ ↦ ( ( θ ‘ 𝑥 ) / 𝑥 ) ) ↾ ( 2 [,) +∞ ) ) = ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( θ ‘ 𝑥 ) / 𝑥 ) )
54	51 53	eqtr4i	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) / ( ( ψ ‘ 𝑥 ) / ( θ ‘ 𝑥 ) ) ) ) = ( ( 𝑥 ∈ ℝ+ ↦ ( ( θ ‘ 𝑥 ) / 𝑥 ) ) ↾ ( 2 [,) +∞ ) )
55		1div1e1	⊢ ( 1 / 1 ) = 1
56	30 54 55	3brtr3g	⊢ ( ⊤ → ( ( 𝑥 ∈ ℝ+ ↦ ( ( θ ‘ 𝑥 ) / 𝑥 ) ) ↾ ( 2 [,) +∞ ) ) ⇝𝑟 1 )
57		rerpdivcl	⊢ ( ( ( θ ‘ 𝑥 ) ∈ ℝ ∧ 𝑥 ∈ ℝ+ ) → ( ( θ ‘ 𝑥 ) / 𝑥 ) ∈ ℝ )
58	45 57	mpancom	⊢ ( 𝑥 ∈ ℝ+ → ( ( θ ‘ 𝑥 ) / 𝑥 ) ∈ ℝ )
59	58	adantl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( θ ‘ 𝑥 ) / 𝑥 ) ∈ ℝ )
60	59	recnd	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( θ ‘ 𝑥 ) / 𝑥 ) ∈ ℂ )
61	60	fmpttd	⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( ( θ ‘ 𝑥 ) / 𝑥 ) ) : ℝ+ ⟶ ℂ )
62		rpssre	⊢ ℝ+ ⊆ ℝ
63	62	a1i	⊢ ( ⊤ → ℝ+ ⊆ ℝ )
64	1	a1i	⊢ ( ⊤ → 2 ∈ ℝ )
65	61 63 64	rlimresb	⊢ ( ⊤ → ( ( 𝑥 ∈ ℝ+ ↦ ( ( θ ‘ 𝑥 ) / 𝑥 ) ) ⇝𝑟 1 ↔ ( ( 𝑥 ∈ ℝ+ ↦ ( ( θ ‘ 𝑥 ) / 𝑥 ) ) ↾ ( 2 [,) +∞ ) ) ⇝𝑟 1 ) )
66	56 65	mpbird	⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( ( θ ‘ 𝑥 ) / 𝑥 ) ) ⇝𝑟 1 )
67	66	mptru	⊢ ( 𝑥 ∈ ℝ+ ↦ ( ( θ ‘ 𝑥 ) / 𝑥 ) ) ⇝𝑟 1