This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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