Theorem chtppilim

Description: The theta function is asymptotic to ppi ( x ) log ( x ) , so it is sufficient to prove theta ( x ) / x ~>r 1 to establish the PNT. (Contributed by Mario Carneiro, 22-Sep-2014)

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

Proof

Step	Hyp	Ref	Expression
1		halfre	⊢ ( 1 / 2 ) ∈ ℝ
2		1re	⊢ 1 ∈ ℝ
3		rpre	⊢ ( 𝑦 ∈ ℝ+ → 𝑦 ∈ ℝ )
4		resubcl	⊢ ( ( 1 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 1 − 𝑦 ) ∈ ℝ )
5	2 3 4	sylancr	⊢ ( 𝑦 ∈ ℝ+ → ( 1 − 𝑦 ) ∈ ℝ )
6		ifcl	⊢ ( ( ( 1 / 2 ) ∈ ℝ ∧ ( 1 − 𝑦 ) ∈ ℝ ) → if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) ∈ ℝ )
7	1 5 6	sylancr	⊢ ( 𝑦 ∈ ℝ+ → if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) ∈ ℝ )
8		0red	⊢ ( 𝑦 ∈ ℝ+ → 0 ∈ ℝ )
9	1	a1i	⊢ ( 𝑦 ∈ ℝ+ → ( 1 / 2 ) ∈ ℝ )
10		halfgt0	⊢ 0 < ( 1 / 2 )
11	10	a1i	⊢ ( 𝑦 ∈ ℝ+ → 0 < ( 1 / 2 ) )
12		max2	⊢ ( ( ( 1 − 𝑦 ) ∈ ℝ ∧ ( 1 / 2 ) ∈ ℝ ) → ( 1 / 2 ) ≤ if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) )
13	5 1 12	sylancl	⊢ ( 𝑦 ∈ ℝ+ → ( 1 / 2 ) ≤ if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) )
14	8 9 7 11 13	ltletrd	⊢ ( 𝑦 ∈ ℝ+ → 0 < if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) )
15	7 14	elrpd	⊢ ( 𝑦 ∈ ℝ+ → if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) ∈ ℝ+ )
16	15	rpsqrtcld	⊢ ( 𝑦 ∈ ℝ+ → ( √ ‘ if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) ) ∈ ℝ+ )
17		halflt1	⊢ ( 1 / 2 ) < 1
18		ltsubrp	⊢ ( ( 1 ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) → ( 1 − 𝑦 ) < 1 )
19	2 18	mpan	⊢ ( 𝑦 ∈ ℝ+ → ( 1 − 𝑦 ) < 1 )
20		breq1	⊢ ( ( 1 / 2 ) = if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) → ( ( 1 / 2 ) < 1 ↔ if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) < 1 ) )
21		breq1	⊢ ( ( 1 − 𝑦 ) = if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) → ( ( 1 − 𝑦 ) < 1 ↔ if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) < 1 ) )
22	20 21	ifboth	⊢ ( ( ( 1 / 2 ) < 1 ∧ ( 1 − 𝑦 ) < 1 ) → if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) < 1 )
23	17 19 22	sylancr	⊢ ( 𝑦 ∈ ℝ+ → if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) < 1 )
24	15	rpge0d	⊢ ( 𝑦 ∈ ℝ+ → 0 ≤ if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) )
25	2	a1i	⊢ ( 𝑦 ∈ ℝ+ → 1 ∈ ℝ )
26		0le1	⊢ 0 ≤ 1
27	26	a1i	⊢ ( 𝑦 ∈ ℝ+ → 0 ≤ 1 )
28	7 24 25 27	sqrtltd	⊢ ( 𝑦 ∈ ℝ+ → ( if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) < 1 ↔ ( √ ‘ if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) ) < ( √ ‘ 1 ) ) )
29	23 28	mpbid	⊢ ( 𝑦 ∈ ℝ+ → ( √ ‘ if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) ) < ( √ ‘ 1 ) )
30		sqrt1	⊢ ( √ ‘ 1 ) = 1
31	29 30	breqtrdi	⊢ ( 𝑦 ∈ ℝ+ → ( √ ‘ if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) ) < 1 )
32	16 31	chtppilimlem2	⊢ ( 𝑦 ∈ ℝ+ → ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ ( 2 [,) +∞ ) ( 𝑧 ≤ 𝑥 → ( ( ( √ ‘ if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) ) ↑ 2 ) · ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) < ( θ ‘ 𝑥 ) ) )
33	5	adantr	⊢ ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( 1 − 𝑦 ) ∈ ℝ )
34		max1	⊢ ( ( ( 1 − 𝑦 ) ∈ ℝ ∧ ( 1 / 2 ) ∈ ℝ ) → ( 1 − 𝑦 ) ≤ if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) )
35	33 1 34	sylancl	⊢ ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( 1 − 𝑦 ) ≤ if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) )
36	7	adantr	⊢ ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) ∈ ℝ )
37		2re	⊢ 2 ∈ ℝ
38		elicopnf	⊢ ( 2 ∈ ℝ → ( 𝑥 ∈ ( 2 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 2 ≤ 𝑥 ) ) )
39	37 38	ax-mp	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 2 ≤ 𝑥 ) )
40	39	simplbi	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → 𝑥 ∈ ℝ )
41		chtcl	⊢ ( 𝑥 ∈ ℝ → ( θ ‘ 𝑥 ) ∈ ℝ )
42	40 41	syl	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( θ ‘ 𝑥 ) ∈ ℝ )
43		ppinncl	⊢ ( ( 𝑥 ∈ ℝ ∧ 2 ≤ 𝑥 ) → ( π ‘ 𝑥 ) ∈ ℕ )
44	39 43	sylbi	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( π ‘ 𝑥 ) ∈ ℕ )
45	44	nnrpd	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( π ‘ 𝑥 ) ∈ ℝ+ )
46	2	a1i	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → 1 ∈ ℝ )
47	37	a1i	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → 2 ∈ ℝ )
48		1lt2	⊢ 1 < 2
49	48	a1i	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → 1 < 2 )
50	39	simprbi	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → 2 ≤ 𝑥 )
51	46 47 40 49 50	ltletrd	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → 1 < 𝑥 )
52	40 51	rplogcld	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( log ‘ 𝑥 ) ∈ ℝ+ )
53	45 52	rpmulcld	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ∈ ℝ+ )
54	42 53	rerpdivcld	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ∈ ℝ )
55	54	adantl	⊢ ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ∈ ℝ )
56		lelttr	⊢ ( ( ( 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	⊢ ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( ( 1 − 𝑦 ) ≤ if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) ∧ if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) < ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ) → ( 1 − 𝑦 ) < ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ) )
58	35 57	mpand	⊢ ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) < ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) → ( 1 − 𝑦 ) < ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ) )
59	7	recnd	⊢ ( 𝑦 ∈ ℝ+ → if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) ∈ ℂ )
60	59	sqsqrtd	⊢ ( 𝑦 ∈ ℝ+ → ( ( √ ‘ if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) ) ↑ 2 ) = if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) )
61	60	adantr	⊢ ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( √ ‘ if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) ) ↑ 2 ) = if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) )
62	61	oveq1d	⊢ ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( ( √ ‘ if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) ) ↑ 2 ) · ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) = ( if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) · ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) )
63	62	breq1d	⊢ ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( ( ( √ ‘ if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) ) ↑ 2 ) · ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) < ( θ ‘ 𝑥 ) ↔ ( if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) · ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) < ( θ ‘ 𝑥 ) ) )
64	42	adantl	⊢ ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( θ ‘ 𝑥 ) ∈ ℝ )
65	53	rpregt0d	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ∈ ℝ ∧ 0 < ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) )
66	65	adantl	⊢ ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ∈ ℝ ∧ 0 < ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) )
67		ltmuldiv	⊢ ( ( 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	⊢ ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) · ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) < ( θ ‘ 𝑥 ) ↔ if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) < ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ) )
69	63 68	bitrd	⊢ ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( ( ( √ ‘ if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) ) ↑ 2 ) · ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) < ( θ ‘ 𝑥 ) ↔ if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) < ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ) )
70		0red	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → 0 ∈ ℝ )
71		2pos	⊢ 0 < 2
72	71	a1i	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → 0 < 2 )
73	70 47 40 72 50	ltletrd	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → 0 < 𝑥 )
74	40 73	elrpd	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → 𝑥 ∈ ℝ+ )
75		chtleppi	⊢ ( 𝑥 ∈ ℝ+ → ( θ ‘ 𝑥 ) ≤ ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) )
76	74 75	syl	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( θ ‘ 𝑥 ) ≤ ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) )
77	53	rpcnd	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ∈ ℂ )
78	77	mulridd	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) · 1 ) = ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) )
79	76 78	breqtrrd	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( θ ‘ 𝑥 ) ≤ ( ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) · 1 ) )
80	42 46 53	ledivmuld	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ≤ 1 ↔ ( θ ‘ 𝑥 ) ≤ ( ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) · 1 ) ) )
81	79 80	mpbird	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ≤ 1 )
82	54 46 81	abssuble0d	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( abs ‘ ( ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) − 1 ) ) = ( 1 − ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ) )
83	82	breq1d	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( ( abs ‘ ( ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) − 1 ) ) < 𝑦 ↔ ( 1 − ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ) < 𝑦 ) )
84	83	adantl	⊢ ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( abs ‘ ( ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) − 1 ) ) < 𝑦 ↔ ( 1 − ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ) < 𝑦 ) )
85	2	a1i	⊢ ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → 1 ∈ ℝ )
86	3	adantr	⊢ ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → 𝑦 ∈ ℝ )
87		ltsub23	⊢ ( ( 1 ∈ ℝ ∧ ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( 1 − ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ) < 𝑦 ↔ ( 1 − 𝑦 ) < ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ) )
88	85 55 86 87	syl3anc	⊢ ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( 1 − ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ) < 𝑦 ↔ ( 1 − 𝑦 ) < ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ) )
89	84 88	bitrd	⊢ ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( abs ‘ ( ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) − 1 ) ) < 𝑦 ↔ ( 1 − 𝑦 ) < ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ) )
90	58 69 89	3imtr4d	⊢ ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( ( ( √ ‘ if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) ) ↑ 2 ) · ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) < ( θ ‘ 𝑥 ) → ( abs ‘ ( ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) − 1 ) ) < 𝑦 ) )
91	90	imim2d	⊢ ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( 𝑧 ≤ 𝑥 → ( ( ( √ ‘ if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) ) ↑ 2 ) · ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) < ( θ ‘ 𝑥 ) ) → ( 𝑧 ≤ 𝑥 → ( abs ‘ ( ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) − 1 ) ) < 𝑦 ) ) )
92	91	ralimdva	⊢ ( 𝑦 ∈ ℝ+ → ( ∀ 𝑥 ∈ ( 2 [,) +∞ ) ( 𝑧 ≤ 𝑥 → ( ( ( √ ‘ if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) ) ↑ 2 ) · ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) < ( θ ‘ 𝑥 ) ) → ∀ 𝑥 ∈ ( 2 [,) +∞ ) ( 𝑧 ≤ 𝑥 → ( abs ‘ ( ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) − 1 ) ) < 𝑦 ) ) )
93	92	reximdv	⊢ ( 𝑦 ∈ ℝ+ → ( ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ ( 2 [,) +∞ ) ( 𝑧 ≤ 𝑥 → ( ( ( √ ‘ if ( ( 1 − 𝑦 ) ≤ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 − 𝑦 ) ) ) ↑ 2 ) · ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) < ( θ ‘ 𝑥 ) ) → ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ ( 2 [,) +∞ ) ( 𝑧 ≤ 𝑥 → ( abs ‘ ( ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) − 1 ) ) < 𝑦 ) ) )
94	32 93	mpd	⊢ ( 𝑦 ∈ ℝ+ → ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ ( 2 [,) +∞ ) ( 𝑧 ≤ 𝑥 → ( abs ‘ ( ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) − 1 ) ) < 𝑦 ) )
95	94	rgen	⊢ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ ( 2 [,) +∞ ) ( 𝑧 ≤ 𝑥 → ( abs ‘ ( ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) − 1 ) ) < 𝑦 )
96	54	recnd	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ∈ ℂ )
97	96	adantl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ∈ ℂ )
98	97	ralrimiva	⊢ ( ⊤ → ∀ 𝑥 ∈ ( 2 [,) +∞ ) ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ∈ ℂ )
99	40	ssriv	⊢ ( 2 [,) +∞ ) ⊆ ℝ
100	99	a1i	⊢ ( ⊤ → ( 2 [,) +∞ ) ⊆ ℝ )
101		1cnd	⊢ ( ⊤ → 1 ∈ ℂ )
102	98 100 101	rlim2	⊢ ( ⊤ → ( ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ) ⇝𝑟 1 ↔ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ ( 2 [,) +∞ ) ( 𝑧 ≤ 𝑥 → ( abs ‘ ( ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) − 1 ) ) < 𝑦 ) ) )
103	95 102	mpbiri	⊢ ( ⊤ → ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ) ⇝𝑟 1 )
104	103	mptru	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ) ⇝𝑟 1