Theorem chtppilim 27712

Description: The θ function is asymptotic to π(𝑥)log(𝑥), so it is sufficient to prove θ(𝑥) / 𝑥 ⇝_𝑟 1 to establish the PNT. (Contributed by Mario Carneiro, 22-Sep-2014.)

Assertion

Ref	Expression
chtppilim	⊢ (𝑥 ∈ (2[,)+∞) ↦ ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥)))) ⇝𝑟 1

Proof of Theorem chtppilim

Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		halfre 12484	. . . . . . . . 9 ⊢ (1 / 2) ∈ ℝ
2		1re 11235	. . . . . . . . . 10 ⊢ 1 ∈ ℝ
3		rpre 13053	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℝ+ → 𝑦 ∈ ℝ)
4		resubcl 11549	. . . . . . . . . 10 ⊢ ((1 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (1 − 𝑦) ∈ ℝ)
5	2, 3, 4	sylancr 599	. . . . . . . . 9 ⊢ (𝑦 ∈ ℝ+ → (1 − 𝑦) ∈ ℝ)
6		ifcl 4531	. . . . . . . . 9 ⊢ (((1 / 2) ∈ ℝ ∧ (1 − 𝑦) ∈ ℝ) → if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦)) ∈ ℝ)
7	1, 5, 6	sylancr 599	. . . . . . . 8 ⊢ (𝑦 ∈ ℝ+ → if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦)) ∈ ℝ)
8		0red 11238	. . . . . . . . 9 ⊢ (𝑦 ∈ ℝ+ → 0 ∈ ℝ)
9	1	a1i 11	. . . . . . . . 9 ⊢ (𝑦 ∈ ℝ+ → (1 / 2) ∈ ℝ)
10		halfgt0 12486	. . . . . . . . . 10 ⊢ 0 < (1 / 2)
11	10	a1i 11	. . . . . . . . 9 ⊢ (𝑦 ∈ ℝ+ → 0 < (1 / 2))
12		max2 13241	. . . . . . . . . 10 ⊢ (((1 − 𝑦) ∈ ℝ ∧ (1 / 2) ∈ ℝ) → (1 / 2) ≤ if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦)))
13	5, 1, 12	sylancl 598	. . . . . . . . 9 ⊢ (𝑦 ∈ ℝ+ → (1 / 2) ≤ if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦)))
14	8, 9, 7, 11, 13	ltletrd 11397	. . . . . . . 8 ⊢ (𝑦 ∈ ℝ+ → 0 < if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦)))
15	7, 14	elrpd 13085	. . . . . . 7 ⊢ (𝑦 ∈ ℝ+ → if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦)) ∈ ℝ+)
16	15	rpsqrtcld 15501	. . . . . 6 ⊢ (𝑦 ∈ ℝ+ → (√‘if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦))) ∈ ℝ+)
17		halflt1 12488	. . . . . . . . 9 ⊢ (1 / 2) < 1
18		ltsubrp 13082	. . . . . . . . . 10 ⊢ ((1 ∈ ℝ ∧ 𝑦 ∈ ℝ+) → (1 − 𝑦) < 1)
19	2, 18	mpan 703	. . . . . . . . 9 ⊢ (𝑦 ∈ ℝ+ → (1 − 𝑦) < 1)
20		breq1 5110	. . . . . . . . . 10 ⊢ ((1 / 2) = if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦)) → ((1 / 2) < 1 ↔ if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦)) < 1))
21		breq1 5110	. . . . . . . . . 10 ⊢ ((1 − 𝑦) = if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦)) → ((1 − 𝑦) < 1 ↔ if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦)) < 1))
22	20, 21	ifboth 4525	. . . . . . . . 9 ⊢ (((1 / 2) < 1 ∧ (1 − 𝑦) < 1) → if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦)) < 1)
23	17, 19, 22	sylancr 599	. . . . . . . 8 ⊢ (𝑦 ∈ ℝ+ → if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦)) < 1)
24	15	rpge0d 13092	. . . . . . . . 9 ⊢ (𝑦 ∈ ℝ+ → 0 ≤ if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦)))
25	2	a1i 11	. . . . . . . . 9 ⊢ (𝑦 ∈ ℝ+ → 1 ∈ ℝ)
26		0le1 11764	. . . . . . . . . 10 ⊢ 0 ≤ 1
27	26	a1i 11	. . . . . . . . 9 ⊢ (𝑦 ∈ ℝ+ → 0 ≤ 1)
28	7, 24, 25, 27	sqrtltd 15517	. . . . . . . 8 ⊢ (𝑦 ∈ ℝ+ → (if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦)) < 1 ↔ (√‘if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦))) < (√‘1)))
29	23, 28	mpbid 235	. . . . . . 7 ⊢ (𝑦 ∈ ℝ+ → (√‘if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦))) < (√‘1))
30		sqrt1 15360	. . . . . . 7 ⊢ (√‘1) = 1
31	29, 30	breqtrdi 5150	. . . . . 6 ⊢ (𝑦 ∈ ℝ+ → (√‘if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦))) < 1)
32	16, 31	chtppilimlem2 27711	. . . . 5 ⊢ (𝑦 ∈ ℝ+ → ∃𝑧 ∈ ℝ ∀𝑥 ∈ (2[,)+∞)(𝑧 ≤ 𝑥 → (((√‘if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦)))↑2) · ((π‘𝑥) · (log‘𝑥))) < (θ‘𝑥)))
33	5	adantr 486	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℝ+ ∧ 𝑥 ∈ (2[,)+∞)) → (1 − 𝑦) ∈ ℝ)
34		max1 13239	. . . . . . . . . . 11 ⊢ (((1 − 𝑦) ∈ ℝ ∧ (1 / 2) ∈ ℝ) → (1 − 𝑦) ≤ if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦)))
35	33, 1, 34	sylancl 598	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℝ+ ∧ 𝑥 ∈ (2[,)+∞)) → (1 − 𝑦) ≤ if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦)))
36	7	adantr 486	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℝ+ ∧ 𝑥 ∈ (2[,)+∞)) → if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦)) ∈ ℝ)
37		2re 12342	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℝ
38		elicopnf 13500	. . . . . . . . . . . . . . . 16 ⊢ (2 ∈ ℝ → (𝑥 ∈ (2[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 2 ≤ 𝑥)))
39	37, 38	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (2[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 2 ≤ 𝑥))
40	39	simplbi 502	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (2[,)+∞) → 𝑥 ∈ ℝ)
41		chtcl 27346	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → (θ‘𝑥) ∈ ℝ)
42	40, 41	syl 18	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (2[,)+∞) → (θ‘𝑥) ∈ ℝ)
43		ppinncl 27411	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℝ ∧ 2 ≤ 𝑥) → (π‘𝑥) ∈ ℕ)
44	39, 43	sylbi 220	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (2[,)+∞) → (π‘𝑥) ∈ ℕ)
45	44	nnrpd 13086	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (2[,)+∞) → (π‘𝑥) ∈ ℝ+)
46	2	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (2[,)+∞) → 1 ∈ ℝ)
47	37	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (2[,)+∞) → 2 ∈ ℝ)
48		1lt2 12440	. . . . . . . . . . . . . . . . 17 ⊢ 1 < 2
49	48	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (2[,)+∞) → 1 < 2)
50	39	simprbi 503	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (2[,)+∞) → 2 ≤ 𝑥)
51	46, 47, 40, 49, 50	ltletrd 11397	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (2[,)+∞) → 1 < 𝑥)
52	40, 51	rplogcld 26867	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (2[,)+∞) → (log‘𝑥) ∈ ℝ+)
53	45, 52	rpmulcld 13104	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (2[,)+∞) → ((π‘𝑥) · (log‘𝑥)) ∈ ℝ+)
54	42, 53	rerpdivcld 13119	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (2[,)+∞) → ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))) ∈ ℝ)
55	54	adantl 487	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℝ+ ∧ 𝑥 ∈ (2[,)+∞)) → ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))) ∈ ℝ)
56		lelttr 11327	. . . . . . . . . . 11 ⊢ (((1 − 𝑦) ∈ ℝ ∧ if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦)) ∈ ℝ ∧ ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))) ∈ ℝ) → (((1 − 𝑦) ≤ if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦)) ∧ if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦)) < ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥)))) → (1 − 𝑦) < ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥)))))
57	33, 36, 55, 56	syl3anc 1398	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℝ+ ∧ 𝑥 ∈ (2[,)+∞)) → (((1 − 𝑦) ≤ if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦)) ∧ if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦)) < ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥)))) → (1 − 𝑦) < ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥)))))
58	35, 57	mpand 708	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℝ+ ∧ 𝑥 ∈ (2[,)+∞)) → (if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦)) < ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))) → (1 − 𝑦) < ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥)))))
59	7	recnd 11264	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℝ+ → if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦)) ∈ ℂ)
60	59	sqsqrtd 15531	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℝ+ → ((√‘if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦)))↑2) = if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦)))
61	60	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ ℝ+ ∧ 𝑥 ∈ (2[,)+∞)) → ((√‘if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦)))↑2) = if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦)))
62	61	oveq1d 7431	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℝ+ ∧ 𝑥 ∈ (2[,)+∞)) → (((√‘if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦)))↑2) · ((π‘𝑥) · (log‘𝑥))) = (if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦)) · ((π‘𝑥) · (log‘𝑥))))
63	62	breq1d 5117	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℝ+ ∧ 𝑥 ∈ (2[,)+∞)) → ((((√‘if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦)))↑2) · ((π‘𝑥) · (log‘𝑥))) < (θ‘𝑥) ↔ (if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦)) · ((π‘𝑥) · (log‘𝑥))) < (θ‘𝑥)))
64	42	adantl 487	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℝ+ ∧ 𝑥 ∈ (2[,)+∞)) → (θ‘𝑥) ∈ ℝ)
65	53	rpregt0d 13094	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (2[,)+∞) → (((π‘𝑥) · (log‘𝑥)) ∈ ℝ ∧ 0 < ((π‘𝑥) · (log‘𝑥))))
66	65	adantl 487	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℝ+ ∧ 𝑥 ∈ (2[,)+∞)) → (((π‘𝑥) · (log‘𝑥)) ∈ ℝ ∧ 0 < ((π‘𝑥) · (log‘𝑥))))
67		ltmuldiv 12115	. . . . . . . . . . 11 ⊢ ((if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦)) ∈ ℝ ∧ (θ‘𝑥) ∈ ℝ ∧ (((π‘𝑥) · (log‘𝑥)) ∈ ℝ ∧ 0 < ((π‘𝑥) · (log‘𝑥)))) → ((if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦)) · ((π‘𝑥) · (log‘𝑥))) < (θ‘𝑥) ↔ if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦)) < ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥)))))
68	36, 64, 66, 67	syl3anc 1398	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℝ+ ∧ 𝑥 ∈ (2[,)+∞)) → ((if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦)) · ((π‘𝑥) · (log‘𝑥))) < (θ‘𝑥) ↔ if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦)) < ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥)))))
69	63, 68	bitrd 282	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℝ+ ∧ 𝑥 ∈ (2[,)+∞)) → ((((√‘if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦)))↑2) · ((π‘𝑥) · (log‘𝑥))) < (θ‘𝑥) ↔ if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦)) < ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥)))))
70		0red 11238	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (2[,)+∞) → 0 ∈ ℝ)
71		2pos 12372	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 < 2
72	71	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (2[,)+∞) → 0 < 2)
73	70, 47, 40, 72, 50	ltletrd 11397	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (2[,)+∞) → 0 < 𝑥)
74	40, 73	elrpd 13085	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (2[,)+∞) → 𝑥 ∈ ℝ+)
75		chtleppi 27447	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℝ+ → (θ‘𝑥) ≤ ((π‘𝑥) · (log‘𝑥)))
76	74, 75	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (2[,)+∞) → (θ‘𝑥) ≤ ((π‘𝑥) · (log‘𝑥)))
77	53	rpcnd 13090	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (2[,)+∞) → ((π‘𝑥) · (log‘𝑥)) ∈ ℂ)
78	77	mulridd 11253	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (2[,)+∞) → (((π‘𝑥) · (log‘𝑥)) · 1) = ((π‘𝑥) · (log‘𝑥)))
79	76, 78	breqtrrd 5137	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (2[,)+∞) → (θ‘𝑥) ≤ (((π‘𝑥) · (log‘𝑥)) · 1))
80	42, 46, 53	ledivmuld 13141	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (2[,)+∞) → (((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))) ≤ 1 ↔ (θ‘𝑥) ≤ (((π‘𝑥) · (log‘𝑥)) · 1)))
81	79, 80	mpbird 260	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (2[,)+∞) → ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))) ≤ 1)
82	54, 46, 81	abssuble0d 15524	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (2[,)+∞) → (abs‘(((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))) − 1)) = (1 − ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥)))))
83	82	breq1d 5117	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (2[,)+∞) → ((abs‘(((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))) − 1)) < 𝑦 ↔ (1 − ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥)))) < 𝑦))
84	83	adantl 487	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℝ+ ∧ 𝑥 ∈ (2[,)+∞)) → ((abs‘(((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))) − 1)) < 𝑦 ↔ (1 − ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥)))) < 𝑦))
85	2	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℝ+ ∧ 𝑥 ∈ (2[,)+∞)) → 1 ∈ ℝ)
86	3	adantr 486	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℝ+ ∧ 𝑥 ∈ (2[,)+∞)) → 𝑦 ∈ ℝ)
87		ltsub23 11721	. . . . . . . . . . 11 ⊢ ((1 ∈ ℝ ∧ ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))) ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((1 − ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥)))) < 𝑦 ↔ (1 − 𝑦) < ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥)))))
88	85, 55, 86, 87	syl3anc 1398	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℝ+ ∧ 𝑥 ∈ (2[,)+∞)) → ((1 − ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥)))) < 𝑦 ↔ (1 − 𝑦) < ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥)))))
89	84, 88	bitrd 282	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℝ+ ∧ 𝑥 ∈ (2[,)+∞)) → ((abs‘(((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))) − 1)) < 𝑦 ↔ (1 − 𝑦) < ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥)))))
90	58, 69, 89	3imtr4d 297	. . . . . . . 8 ⊢ ((𝑦 ∈ ℝ+ ∧ 𝑥 ∈ (2[,)+∞)) → ((((√‘if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦)))↑2) · ((π‘𝑥) · (log‘𝑥))) < (θ‘𝑥) → (abs‘(((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))) − 1)) < 𝑦))
91	90	imim2d 58	. . . . . . 7 ⊢ ((𝑦 ∈ ℝ+ ∧ 𝑥 ∈ (2[,)+∞)) → ((𝑧 ≤ 𝑥 → (((√‘if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦)))↑2) · ((π‘𝑥) · (log‘𝑥))) < (θ‘𝑥)) → (𝑧 ≤ 𝑥 → (abs‘(((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))) − 1)) < 𝑦)))
92	91	ralimdva 3176	. . . . . 6 ⊢ (𝑦 ∈ ℝ+ → (∀𝑥 ∈ (2[,)+∞)(𝑧 ≤ 𝑥 → (((√‘if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦)))↑2) · ((π‘𝑥) · (log‘𝑥))) < (θ‘𝑥)) → ∀𝑥 ∈ (2[,)+∞)(𝑧 ≤ 𝑥 → (abs‘(((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))) − 1)) < 𝑦)))
93	92	reximdv 3179	. . . . 5 ⊢ (𝑦 ∈ ℝ+ → (∃𝑧 ∈ ℝ ∀𝑥 ∈ (2[,)+∞)(𝑧 ≤ 𝑥 → (((√‘if((1 − 𝑦) ≤ (1 / 2), (1 / 2), (1 − 𝑦)))↑2) · ((π‘𝑥) · (log‘𝑥))) < (θ‘𝑥)) → ∃𝑧 ∈ ℝ ∀𝑥 ∈ (2[,)+∞)(𝑧 ≤ 𝑥 → (abs‘(((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))) − 1)) < 𝑦)))
94	32, 93	mpd 16	. . . 4 ⊢ (𝑦 ∈ ℝ+ → ∃𝑧 ∈ ℝ ∀𝑥 ∈ (2[,)+∞)(𝑧 ≤ 𝑥 → (abs‘(((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))) − 1)) < 𝑦))
95	94	rgen 3080	. . 3 ⊢ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ ∀𝑥 ∈ (2[,)+∞)(𝑧 ≤ 𝑥 → (abs‘(((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))) − 1)) < 𝑦)
96	54	recnd 11264	. . . . . 6 ⊢ (𝑥 ∈ (2[,)+∞) → ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))) ∈ ℂ)
97	96	adantl 487	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ (2[,)+∞)) → ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))) ∈ ℂ)
98	97	ralrimiva 3156	. . . 4 ⊢ (⊤ → ∀𝑥 ∈ (2[,)+∞)((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))) ∈ ℂ)
99	40	ssriv 3938	. . . . 5 ⊢ (2[,)+∞) ⊆ ℝ
100	99	a1i 11	. . . 4 ⊢ (⊤ → (2[,)+∞) ⊆ ℝ)
101		1cnd 11229	. . . 4 ⊢ (⊤ → 1 ∈ ℂ)
102	98, 100, 101	rlim2 15585	. . 3 ⊢ (⊤ → ((𝑥 ∈ (2[,)+∞) ↦ ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥)))) ⇝𝑟 1 ↔ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ ∀𝑥 ∈ (2[,)+∞)(𝑧 ≤ 𝑥 → (abs‘(((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))) − 1)) < 𝑦)))
103	95, 102	mpbiri 261	. 2 ⊢ (⊤ → (𝑥 ∈ (2[,)+∞) ↦ ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥)))) ⇝𝑟 1)
104	103	mptru 1577	1 ⊢ (𝑥 ∈ (2[,)+∞) ↦ ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥)))) ⇝𝑟 1

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570  ⊤wtru 1571   ∈ wcel 2145  ∀wral 3078  ∃wrex 3088   ⊆ wss 3902  ifcif 4485   class class class wbr 5107   ↦ cmpt 5190  ‘cfv 6537  (class class class)co 7416  ℂcc 11125  ℝcr 11126  0cc0 11127  1c1 11128   · cmul 11132  +∞cpnf 11267   < clt 11270   ≤ cle 11271   − cmin 11468   / cdiv 11898  ℕcn 12260  2c2 12322  ℝ⁺crp 13044  [,)cico 13402  ↑cexp 14127  √csqrt 15322  abscabs 15323   ⇝_𝑟 crli 15574  logclog 26792  θccht 27328  πcppi 27331

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-rep 5236  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7739  ax-inf2 9623  ax-cnex 11183  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-mulcom 11191  ax-addass 11192  ax-mulass 11193  ax-distr 11194  ax-i2m1 11195  ax-1ne0 11196  ax-1rid 11197  ax-rnegex 11198  ax-rrecex 11199  ax-cnre 11200  ax-pre-lttri 11201  ax-pre-lttrn 11202  ax-pre-ltadd 11203  ax-pre-mulgt0 11204  ax-pre-sup 11205  ax-addf 11206

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-rmo 3367  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-tp 4592  df-op 4594  df-uni 4871  df-int 4911  df-iun 4956  df-iin 4957  df-br 5108  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-se 5613  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-isom 6546  df-riota 7373  df-ov 7419  df-oprab 7420  df-mpo 7421  df-of 7681  df-om 7866  df-1st 7989  df-2nd 7990  df-supp 8162  df-frecs 8283  df-wrecs 8314  df-recs 8363  df-rdg 8402  df-1o 8458  df-2o 8459  df-oadd 8462  df-er 8699  df-map 8831  df-pm 8832  df-ixp 8908  df-en 8956  df-dom 8957  df-sdom 8958  df-fin 8959  df-fsupp 9335  df-fi 9384  df-sup 9415  df-inf 9416  df-oi 9485  df-dju 9909  df-card 9947  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276  df-sub 11470  df-neg 11471  df-div 11899  df-nn 12261  df-2 12330  df-3 12331  df-4 12332  df-5 12333  df-6 12334  df-7 12335  df-8 12336  df-9 12337  df-n0 12532  df-xnn0 12605  df-z 12619  df-dec 12740  df-uz 12891  df-q 13001  df-rp 13045  df-xneg 13165  df-xadd 13166  df-xmul 13167  df-ioo 13404  df-ioc 13405  df-ico 13406  df-icc 13407  df-fz 13564  df-fzo 13712  df-fl 13855  df-mod 13933  df-seq 14068  df-exp 14128  df-fac 14340  df-bc 14369  df-hash 14397  df-shft 15142  df-cj 15188  df-re 15189  df-im 15190  df-sqrt 15324  df-abs 15325  df-limsup 15560  df-clim 15577  df-rlim 15578  df-o1 15579  df-lo1 15580  df-sum 15776  df-ef 16157  df-e 16158  df-sin 16159  df-cos 16160  df-pi 16162  df-dvds 16347  df-gcd 16589  df-prm 16766  df-pc 16933  df-struct 17243  df-sets 17260  df-slot 17278  df-ndx 17290  df-base 17306  df-ress 17327  df-plusg 17359  df-mulr 17360  df-starv 17361  df-sca 17362  df-vsca 17363  df-ip 17364  df-tset 17365  df-ple 17366  df-ds 17368  df-unif 17369  df-hom 17370  df-cco 17371  df-rest 17511  df-topn 17512  df-0g 17530  df-gsum 17531  df-topgen 17532  df-pt 17533  df-prds 17536  df-xrs 17592  df-qtop 17597  df-imas 17598  df-xps 17600  df-mre 17674  df-mrc 17675  df-acs 17677  df-mgm 18734  df-sgrp 18825  df-mnd 18841  df-submnd 18896  df-mulg 19195  df-cntz 19448  df-cmn 19913  df-psmet 21581  df-xmet 21582  df-met 21583  df-bl 21584  df-mopn 21585  df-fbas 21586  df-fg 21587  df-cnfld 21590  df-top 23123  df-topon 23140  df-topsp 23162  df-bases 23175  df-cld 23248  df-ntr 23249  df-cls 23250  df-nei 23327  df-lp 23365  df-perf 23366  df-cn 23456  df-cnp 23457  df-haus 23544  df-tx 23792  df-hmeo 23985  df-fil 24076  df-fm 24168  df-flim 24169  df-flf 24170  df-xms 24550  df-ms 24551  df-tms 24552  df-cncf 25110  df-limc 26098  df-dv 26099  df-log 26794  df-cxp 26795  df-cht 27334  df-ppi 27337

This theorem is used by:  chebbnd2  27714  chto1lb  27715  pnt  27851