Theorem chpchtlim

Description: The psi and theta functions are asymptotic to each other, so is sufficient to prove either theta ( x ) / x ~>r 1 or psi ( x ) / x ~>r 1 to establish the PNT. (Contributed by Mario Carneiro, 8-Apr-2016)

	Ref	Expression
Assertion	chpchtlim	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( ψ ‘ 𝑥 ) / ( θ ‘ 𝑥 ) ) ) ⇝𝑟 1

Proof

Step	Hyp	Ref	Expression
1		1red	⊢ ( ⊤ → 1 ∈ ℝ )
2		1red	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → 1 ∈ ℝ )
3		2re	⊢ 2 ∈ ℝ
4		elicopnf	⊢ ( 2 ∈ ℝ → ( 𝑥 ∈ ( 2 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 2 ≤ 𝑥 ) ) )
5	3 4	ax-mp	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 2 ≤ 𝑥 ) )
6	5	simplbi	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → 𝑥 ∈ ℝ )
7	6	adantl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → 𝑥 ∈ ℝ )
8		0red	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → 0 ∈ ℝ )
9	3	a1i	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → 2 ∈ ℝ )
10		2pos	⊢ 0 < 2
11	10	a1i	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → 0 < 2 )
12	5	simprbi	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → 2 ≤ 𝑥 )
13	8 9 6 11 12	ltletrd	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → 0 < 𝑥 )
14	6 13	elrpd	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → 𝑥 ∈ ℝ+ )
15	14	adantl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → 𝑥 ∈ ℝ+ )
16	15	rpge0d	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → 0 ≤ 𝑥 )
17	7 16	resqrtcld	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( √ ‘ 𝑥 ) ∈ ℝ )
18	15	relogcld	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( log ‘ 𝑥 ) ∈ ℝ )
19	17 18	remulcld	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( √ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ∈ ℝ )
20	12	adantl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → 2 ≤ 𝑥 )
21		chtrpcl	⊢ ( ( 𝑥 ∈ ℝ ∧ 2 ≤ 𝑥 ) → ( θ ‘ 𝑥 ) ∈ ℝ+ )
22	7 20 21	syl2anc	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( θ ‘ 𝑥 ) ∈ ℝ+ )
23	19 22	rerpdivcld	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( ( √ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) / ( θ ‘ 𝑥 ) ) ∈ ℝ )
24	6	ssriv	⊢ ( 2 [,) +∞ ) ⊆ ℝ
25	1	recnd	⊢ ( ⊤ → 1 ∈ ℂ )
26		rlimconst	⊢ ( ( ( 2 [,) +∞ ) ⊆ ℝ ∧ 1 ∈ ℂ ) → ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ 1 ) ⇝𝑟 1 )
27	24 25 26	sylancr	⊢ ( ⊤ → ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ 1 ) ⇝𝑟 1 )
28		ovexd	⊢ ( ⊤ → ( 2 [,) +∞ ) ∈ V )
29	7 22	rerpdivcld	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( 𝑥 / ( θ ‘ 𝑥 ) ) ∈ ℝ )
30		ovexd	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( ( √ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) / 𝑥 ) ∈ V )
31		eqidd	⊢ ( ⊤ → ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( 𝑥 / ( θ ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( 𝑥 / ( θ ‘ 𝑥 ) ) ) )
32	7	recnd	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → 𝑥 ∈ ℂ )
33		cxpsqrt	⊢ ( 𝑥 ∈ ℂ → ( 𝑥 ↑𝑐 ( 1 / 2 ) ) = ( √ ‘ 𝑥 ) )
34	32 33	syl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( 𝑥 ↑𝑐 ( 1 / 2 ) ) = ( √ ‘ 𝑥 ) )
35	34	oveq2d	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( log ‘ 𝑥 ) / ( 𝑥 ↑𝑐 ( 1 / 2 ) ) ) = ( ( log ‘ 𝑥 ) / ( √ ‘ 𝑥 ) ) )
36	18	recnd	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( log ‘ 𝑥 ) ∈ ℂ )
37	15	rpsqrtcld	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( √ ‘ 𝑥 ) ∈ ℝ+ )
38	37	rpcnne0d	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( √ ‘ 𝑥 ) ∈ ℂ ∧ ( √ ‘ 𝑥 ) ≠ 0 ) )
39		divcan5	⊢ ( ( ( log ‘ 𝑥 ) ∈ ℂ ∧ ( ( √ ‘ 𝑥 ) ∈ ℂ ∧ ( √ ‘ 𝑥 ) ≠ 0 ) ∧ ( ( √ ‘ 𝑥 ) ∈ ℂ ∧ ( √ ‘ 𝑥 ) ≠ 0 ) ) → ( ( ( √ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) / ( ( √ ‘ 𝑥 ) · ( √ ‘ 𝑥 ) ) ) = ( ( log ‘ 𝑥 ) / ( √ ‘ 𝑥 ) ) )
40	36 38 38 39	syl3anc	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( ( √ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) / ( ( √ ‘ 𝑥 ) · ( √ ‘ 𝑥 ) ) ) = ( ( log ‘ 𝑥 ) / ( √ ‘ 𝑥 ) ) )
41		remsqsqrt	⊢ ( ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) → ( ( √ ‘ 𝑥 ) · ( √ ‘ 𝑥 ) ) = 𝑥 )
42	7 16 41	syl2anc	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( √ ‘ 𝑥 ) · ( √ ‘ 𝑥 ) ) = 𝑥 )
43	42	oveq2d	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( ( √ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) / ( ( √ ‘ 𝑥 ) · ( √ ‘ 𝑥 ) ) ) = ( ( ( √ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) / 𝑥 ) )
44	35 40 43	3eqtr2d	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( log ‘ 𝑥 ) / ( 𝑥 ↑𝑐 ( 1 / 2 ) ) ) = ( ( ( √ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) / 𝑥 ) )
45	44	mpteq2dva	⊢ ( ⊤ → ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( log ‘ 𝑥 ) / ( 𝑥 ↑𝑐 ( 1 / 2 ) ) ) ) = ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( ( √ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) / 𝑥 ) ) )
46	28 29 30 31 45	offval2	⊢ ( ⊤ → ( ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( 𝑥 / ( θ ‘ 𝑥 ) ) ) ∘f · ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( log ‘ 𝑥 ) / ( 𝑥 ↑𝑐 ( 1 / 2 ) ) ) ) ) = ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( 𝑥 / ( θ ‘ 𝑥 ) ) · ( ( ( √ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) / 𝑥 ) ) ) )
47	15	rpne0d	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → 𝑥 ≠ 0 )
48	22	rpcnne0d	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( θ ‘ 𝑥 ) ∈ ℂ ∧ ( θ ‘ 𝑥 ) ≠ 0 ) )
49	19	recnd	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( √ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ∈ ℂ )
50		dmdcan	⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ∧ ( ( θ ‘ 𝑥 ) ∈ ℂ ∧ ( θ ‘ 𝑥 ) ≠ 0 ) ∧ ( ( √ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ∈ ℂ ) → ( ( 𝑥 / ( θ ‘ 𝑥 ) ) · ( ( ( √ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) / 𝑥 ) ) = ( ( ( √ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) / ( θ ‘ 𝑥 ) ) )
51	32 47 48 49 50	syl211anc	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( 𝑥 / ( θ ‘ 𝑥 ) ) · ( ( ( √ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) / 𝑥 ) ) = ( ( ( √ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) / ( θ ‘ 𝑥 ) ) )
52	51	mpteq2dva	⊢ ( ⊤ → ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( 𝑥 / ( θ ‘ 𝑥 ) ) · ( ( ( √ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) / 𝑥 ) ) ) = ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( ( √ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) / ( θ ‘ 𝑥 ) ) ) )
53	46 52	eqtrd	⊢ ( ⊤ → ( ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( 𝑥 / ( θ ‘ 𝑥 ) ) ) ∘f · ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( log ‘ 𝑥 ) / ( 𝑥 ↑𝑐 ( 1 / 2 ) ) ) ) ) = ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( ( √ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) / ( θ ‘ 𝑥 ) ) ) )
54		chto1lb	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( 𝑥 / ( θ ‘ 𝑥 ) ) ) ∈ 𝑂(1)
55	14	ssriv	⊢ ( 2 [,) +∞ ) ⊆ ℝ+
56	55	a1i	⊢ ( ⊤ → ( 2 [,) +∞ ) ⊆ ℝ+ )
57		1rp	⊢ 1 ∈ ℝ+
58		rphalfcl	⊢ ( 1 ∈ ℝ+ → ( 1 / 2 ) ∈ ℝ+ )
59	57 58	ax-mp	⊢ ( 1 / 2 ) ∈ ℝ+
60		cxploglim	⊢ ( ( 1 / 2 ) ∈ ℝ+ → ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ 𝑥 ) / ( 𝑥 ↑𝑐 ( 1 / 2 ) ) ) ) ⇝𝑟 0 )
61	59 60	ax-mp	⊢ ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ 𝑥 ) / ( 𝑥 ↑𝑐 ( 1 / 2 ) ) ) ) ⇝𝑟 0
62	61	a1i	⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ 𝑥 ) / ( 𝑥 ↑𝑐 ( 1 / 2 ) ) ) ) ⇝𝑟 0 )
63	56 62	rlimres2	⊢ ( ⊤ → ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( log ‘ 𝑥 ) / ( 𝑥 ↑𝑐 ( 1 / 2 ) ) ) ) ⇝𝑟 0 )
64		o1rlimmul	⊢ ( ( ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( 𝑥 / ( θ ‘ 𝑥 ) ) ) ∈ 𝑂(1) ∧ ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( log ‘ 𝑥 ) / ( 𝑥 ↑𝑐 ( 1 / 2 ) ) ) ) ⇝𝑟 0 ) → ( ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( 𝑥 / ( θ ‘ 𝑥 ) ) ) ∘f · ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( log ‘ 𝑥 ) / ( 𝑥 ↑𝑐 ( 1 / 2 ) ) ) ) ) ⇝𝑟 0 )
65	54 63 64	sylancr	⊢ ( ⊤ → ( ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( 𝑥 / ( θ ‘ 𝑥 ) ) ) ∘f · ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( log ‘ 𝑥 ) / ( 𝑥 ↑𝑐 ( 1 / 2 ) ) ) ) ) ⇝𝑟 0 )
66	53 65	eqbrtrrd	⊢ ( ⊤ → ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( ( √ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) / ( θ ‘ 𝑥 ) ) ) ⇝𝑟 0 )
67	2 23 27 66	rlimadd	⊢ ( ⊤ → ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( 1 + ( ( ( √ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) / ( θ ‘ 𝑥 ) ) ) ) ⇝𝑟 ( 1 + 0 ) )
68		1p0e1	⊢ ( 1 + 0 ) = 1
69	67 68	breqtrdi	⊢ ( ⊤ → ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( 1 + ( ( ( √ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) / ( θ ‘ 𝑥 ) ) ) ) ⇝𝑟 1 )
70		1re	⊢ 1 ∈ ℝ
71		readdcl	⊢ ( ( 1 ∈ ℝ ∧ ( ( ( √ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) / ( θ ‘ 𝑥 ) ) ∈ ℝ ) → ( 1 + ( ( ( √ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) / ( θ ‘ 𝑥 ) ) ) ∈ ℝ )
72	70 23 71	sylancr	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( 1 + ( ( ( √ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) / ( θ ‘ 𝑥 ) ) ) ∈ ℝ )
73		chpcl	⊢ ( 𝑥 ∈ ℝ → ( ψ ‘ 𝑥 ) ∈ ℝ )
74	7 73	syl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ψ ‘ 𝑥 ) ∈ ℝ )
75	74 22	rerpdivcld	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( ψ ‘ 𝑥 ) / ( θ ‘ 𝑥 ) ) ∈ ℝ )
76		chtcl	⊢ ( 𝑥 ∈ ℝ → ( θ ‘ 𝑥 ) ∈ ℝ )
77	7 76	syl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( θ ‘ 𝑥 ) ∈ ℝ )
78	77 19	readdcld	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( θ ‘ 𝑥 ) + ( ( √ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ∈ ℝ )
79	3	a1i	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → 2 ∈ ℝ )
80		1le2	⊢ 1 ≤ 2
81	80	a1i	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → 1 ≤ 2 )
82	2 79 7 81 20	letrd	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → 1 ≤ 𝑥 )
83		chpub	⊢ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) → ( ψ ‘ 𝑥 ) ≤ ( ( θ ‘ 𝑥 ) + ( ( √ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) )
84	7 82 83	syl2anc	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ψ ‘ 𝑥 ) ≤ ( ( θ ‘ 𝑥 ) + ( ( √ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) )
85	74 78 22 84	lediv1dd	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( ψ ‘ 𝑥 ) / ( θ ‘ 𝑥 ) ) ≤ ( ( ( θ ‘ 𝑥 ) + ( ( √ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) / ( θ ‘ 𝑥 ) ) )
86	22	rpcnd	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( θ ‘ 𝑥 ) ∈ ℂ )
87		divdir	⊢ ( ( ( θ ‘ 𝑥 ) ∈ ℂ ∧ ( ( √ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ∈ ℂ ∧ ( ( θ ‘ 𝑥 ) ∈ ℂ ∧ ( θ ‘ 𝑥 ) ≠ 0 ) ) → ( ( ( θ ‘ 𝑥 ) + ( ( √ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) / ( θ ‘ 𝑥 ) ) = ( ( ( θ ‘ 𝑥 ) / ( θ ‘ 𝑥 ) ) + ( ( ( √ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) / ( θ ‘ 𝑥 ) ) ) )
88	86 49 48 87	syl3anc	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( ( θ ‘ 𝑥 ) + ( ( √ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) / ( θ ‘ 𝑥 ) ) = ( ( ( θ ‘ 𝑥 ) / ( θ ‘ 𝑥 ) ) + ( ( ( √ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) / ( θ ‘ 𝑥 ) ) ) )
89		divid	⊢ ( ( ( θ ‘ 𝑥 ) ∈ ℂ ∧ ( θ ‘ 𝑥 ) ≠ 0 ) → ( ( θ ‘ 𝑥 ) / ( θ ‘ 𝑥 ) ) = 1 )
90	48 89	syl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( θ ‘ 𝑥 ) / ( θ ‘ 𝑥 ) ) = 1 )
91	90	oveq1d	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( ( θ ‘ 𝑥 ) / ( θ ‘ 𝑥 ) ) + ( ( ( √ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) / ( θ ‘ 𝑥 ) ) ) = ( 1 + ( ( ( √ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) / ( θ ‘ 𝑥 ) ) ) )
92	88 91	eqtrd	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( ( θ ‘ 𝑥 ) + ( ( √ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) / ( θ ‘ 𝑥 ) ) = ( 1 + ( ( ( √ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) / ( θ ‘ 𝑥 ) ) ) )
93	85 92	breqtrd	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( ψ ‘ 𝑥 ) / ( θ ‘ 𝑥 ) ) ≤ ( 1 + ( ( ( √ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) / ( θ ‘ 𝑥 ) ) ) )
94	93	adantrr	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ( 2 [,) +∞ ) ∧ 1 ≤ 𝑥 ) ) → ( ( ψ ‘ 𝑥 ) / ( θ ‘ 𝑥 ) ) ≤ ( 1 + ( ( ( √ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) / ( θ ‘ 𝑥 ) ) ) )
95	86	mullidd	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( 1 · ( θ ‘ 𝑥 ) ) = ( θ ‘ 𝑥 ) )
96		chtlepsi	⊢ ( 𝑥 ∈ ℝ → ( θ ‘ 𝑥 ) ≤ ( ψ ‘ 𝑥 ) )
97	7 96	syl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( θ ‘ 𝑥 ) ≤ ( ψ ‘ 𝑥 ) )
98	95 97	eqbrtrd	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( 1 · ( θ ‘ 𝑥 ) ) ≤ ( ψ ‘ 𝑥 ) )
99	2 74 22	lemuldivd	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( 1 · ( θ ‘ 𝑥 ) ) ≤ ( ψ ‘ 𝑥 ) ↔ 1 ≤ ( ( ψ ‘ 𝑥 ) / ( θ ‘ 𝑥 ) ) ) )
100	98 99	mpbid	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → 1 ≤ ( ( ψ ‘ 𝑥 ) / ( θ ‘ 𝑥 ) ) )
101	100	adantrr	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ( 2 [,) +∞ ) ∧ 1 ≤ 𝑥 ) ) → 1 ≤ ( ( ψ ‘ 𝑥 ) / ( θ ‘ 𝑥 ) ) )
102	1 1 69 72 75 94 101	rlimsqz2	⊢ ( ⊤ → ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( ψ ‘ 𝑥 ) / ( θ ‘ 𝑥 ) ) ) ⇝𝑟 1 )
103	102	mptru	⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( ψ ‘ 𝑥 ) / ( θ ‘ 𝑥 ) ) ) ⇝𝑟 1