# 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

### Proof

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