# Metamath Proof Explorer

## Theorem chtppilimlem2

Description: Lemma for chtppilim . (Contributed by Mario Carneiro, 22-Sep-2014)

Ref Expression
Hypotheses chtppilim.1 ${⊢}{\phi }\to {A}\in {ℝ}^{+}$
chtppilim.2 ${⊢}{\phi }\to {A}<1$
Assertion chtppilimlem2 ${⊢}{\phi }\to \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in \left[2,\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}\left({z}\le {x}\to {{A}}^{2}\underset{_}{\pi }\left({x}\right)\mathrm{log}{x}<\theta \left({x}\right)\right)$

### Proof

Step Hyp Ref Expression
1 chtppilim.1 ${⊢}{\phi }\to {A}\in {ℝ}^{+}$
2 chtppilim.2 ${⊢}{\phi }\to {A}<1$
3 simpr ${⊢}\left({\phi }\wedge {x}\in \left[2,\mathrm{+\infty }\right)\right)\to {x}\in \left[2,\mathrm{+\infty }\right)$
4 2re ${⊢}2\in ℝ$
5 elicopnf ${⊢}2\in ℝ\to \left({x}\in \left[2,\mathrm{+\infty }\right)↔\left({x}\in ℝ\wedge 2\le {x}\right)\right)$
6 4 5 ax-mp ${⊢}{x}\in \left[2,\mathrm{+\infty }\right)↔\left({x}\in ℝ\wedge 2\le {x}\right)$
7 3 6 sylib ${⊢}\left({\phi }\wedge {x}\in \left[2,\mathrm{+\infty }\right)\right)\to \left({x}\in ℝ\wedge 2\le {x}\right)$
8 7 simpld ${⊢}\left({\phi }\wedge {x}\in \left[2,\mathrm{+\infty }\right)\right)\to {x}\in ℝ$
9 0red ${⊢}\left({\phi }\wedge {x}\in \left[2,\mathrm{+\infty }\right)\right)\to 0\in ℝ$
10 4 a1i ${⊢}\left({\phi }\wedge {x}\in \left[2,\mathrm{+\infty }\right)\right)\to 2\in ℝ$
11 2pos ${⊢}0<2$
12 11 a1i ${⊢}\left({\phi }\wedge {x}\in \left[2,\mathrm{+\infty }\right)\right)\to 0<2$
13 7 simprd ${⊢}\left({\phi }\wedge {x}\in \left[2,\mathrm{+\infty }\right)\right)\to 2\le {x}$
14 9 10 8 12 13 ltletrd ${⊢}\left({\phi }\wedge {x}\in \left[2,\mathrm{+\infty }\right)\right)\to 0<{x}$
15 8 14 elrpd ${⊢}\left({\phi }\wedge {x}\in \left[2,\mathrm{+\infty }\right)\right)\to {x}\in {ℝ}^{+}$
16 1 rpred ${⊢}{\phi }\to {A}\in ℝ$
17 16 adantr ${⊢}\left({\phi }\wedge {x}\in \left[2,\mathrm{+\infty }\right)\right)\to {A}\in ℝ$
18 15 17 rpcxpcld ${⊢}\left({\phi }\wedge {x}\in \left[2,\mathrm{+\infty }\right)\right)\to {{x}}^{{A}}\in {ℝ}^{+}$
19 ppinncl ${⊢}\left({x}\in ℝ\wedge 2\le {x}\right)\to \underset{_}{\pi }\left({x}\right)\in ℕ$
20 7 19 syl ${⊢}\left({\phi }\wedge {x}\in \left[2,\mathrm{+\infty }\right)\right)\to \underset{_}{\pi }\left({x}\right)\in ℕ$
21 20 nnrpd ${⊢}\left({\phi }\wedge {x}\in \left[2,\mathrm{+\infty }\right)\right)\to \underset{_}{\pi }\left({x}\right)\in {ℝ}^{+}$
22 18 21 rpdivcld ${⊢}\left({\phi }\wedge {x}\in \left[2,\mathrm{+\infty }\right)\right)\to \frac{{{x}}^{{A}}}{\underset{_}{\pi }\left({x}\right)}\in {ℝ}^{+}$
23 22 ralrimiva ${⊢}{\phi }\to \forall {x}\in \left[2,\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}\frac{{{x}}^{{A}}}{\underset{_}{\pi }\left({x}\right)}\in {ℝ}^{+}$
24 1re ${⊢}1\in ℝ$
25 difrp ${⊢}\left({A}\in ℝ\wedge 1\in ℝ\right)\to \left({A}<1↔1-{A}\in {ℝ}^{+}\right)$
26 16 24 25 sylancl ${⊢}{\phi }\to \left({A}<1↔1-{A}\in {ℝ}^{+}\right)$
27 2 26 mpbid ${⊢}{\phi }\to 1-{A}\in {ℝ}^{+}$
28 ovexd ${⊢}{\phi }\to \left[2,\mathrm{+\infty }\right)\in \mathrm{V}$
29 24 a1i ${⊢}\left({\phi }\wedge {x}\in \left[2,\mathrm{+\infty }\right)\right)\to 1\in ℝ$
30 1lt2 ${⊢}1<2$
31 30 a1i ${⊢}\left({\phi }\wedge {x}\in \left[2,\mathrm{+\infty }\right)\right)\to 1<2$
32 29 10 8 31 13 ltletrd ${⊢}\left({\phi }\wedge {x}\in \left[2,\mathrm{+\infty }\right)\right)\to 1<{x}$
33 8 32 rplogcld ${⊢}\left({\phi }\wedge {x}\in \left[2,\mathrm{+\infty }\right)\right)\to \mathrm{log}{x}\in {ℝ}^{+}$
34 15 33 rpdivcld ${⊢}\left({\phi }\wedge {x}\in \left[2,\mathrm{+\infty }\right)\right)\to \frac{{x}}{\mathrm{log}{x}}\in {ℝ}^{+}$
35 34 21 rpdivcld ${⊢}\left({\phi }\wedge {x}\in \left[2,\mathrm{+\infty }\right)\right)\to \frac{\frac{{x}}{\mathrm{log}{x}}}{\underset{_}{\pi }\left({x}\right)}\in {ℝ}^{+}$
36 27 adantr ${⊢}\left({\phi }\wedge {x}\in \left[2,\mathrm{+\infty }\right)\right)\to 1-{A}\in {ℝ}^{+}$
37 36 rpred ${⊢}\left({\phi }\wedge {x}\in \left[2,\mathrm{+\infty }\right)\right)\to 1-{A}\in ℝ$
38 15 37 rpcxpcld ${⊢}\left({\phi }\wedge {x}\in \left[2,\mathrm{+\infty }\right)\right)\to {{x}}^{1-{A}}\in {ℝ}^{+}$
39 33 38 rpdivcld ${⊢}\left({\phi }\wedge {x}\in \left[2,\mathrm{+\infty }\right)\right)\to \frac{\mathrm{log}{x}}{{{x}}^{1-{A}}}\in {ℝ}^{+}$
40 eqidd ${⊢}{\phi }\to \left({x}\in \left[2,\mathrm{+\infty }\right)⟼\frac{\frac{{x}}{\mathrm{log}{x}}}{\underset{_}{\pi }\left({x}\right)}\right)=\left({x}\in \left[2,\mathrm{+\infty }\right)⟼\frac{\frac{{x}}{\mathrm{log}{x}}}{\underset{_}{\pi }\left({x}\right)}\right)$
41 eqidd ${⊢}{\phi }\to \left({x}\in \left[2,\mathrm{+\infty }\right)⟼\frac{\mathrm{log}{x}}{{{x}}^{1-{A}}}\right)=\left({x}\in \left[2,\mathrm{+\infty }\right)⟼\frac{\mathrm{log}{x}}{{{x}}^{1-{A}}}\right)$
42 28 35 39 40 41 offval2 ${⊢}{\phi }\to \left({x}\in \left[2,\mathrm{+\infty }\right)⟼\frac{\frac{{x}}{\mathrm{log}{x}}}{\underset{_}{\pi }\left({x}\right)}\right){×}_{f}\left({x}\in \left[2,\mathrm{+\infty }\right)⟼\frac{\mathrm{log}{x}}{{{x}}^{1-{A}}}\right)=\left({x}\in \left[2,\mathrm{+\infty }\right)⟼\left(\frac{\frac{{x}}{\mathrm{log}{x}}}{\underset{_}{\pi }\left({x}\right)}\right)\left(\frac{\mathrm{log}{x}}{{{x}}^{1-{A}}}\right)\right)$
43 34 rpcnd ${⊢}\left({\phi }\wedge {x}\in \left[2,\mathrm{+\infty }\right)\right)\to \frac{{x}}{\mathrm{log}{x}}\in ℂ$
44 39 rpcnd ${⊢}\left({\phi }\wedge {x}\in \left[2,\mathrm{+\infty }\right)\right)\to \frac{\mathrm{log}{x}}{{{x}}^{1-{A}}}\in ℂ$
45 21 rpcnne0d ${⊢}\left({\phi }\wedge {x}\in \left[2,\mathrm{+\infty }\right)\right)\to \left(\underset{_}{\pi }\left({x}\right)\in ℂ\wedge \underset{_}{\pi }\left({x}\right)\ne 0\right)$
46 div23 ${⊢}\left(\frac{{x}}{\mathrm{log}{x}}\in ℂ\wedge \frac{\mathrm{log}{x}}{{{x}}^{1-{A}}}\in ℂ\wedge \left(\underset{_}{\pi }\left({x}\right)\in ℂ\wedge \underset{_}{\pi }\left({x}\right)\ne 0\right)\right)\to \frac{\left(\frac{{x}}{\mathrm{log}{x}}\right)\left(\frac{\mathrm{log}{x}}{{{x}}^{1-{A}}}\right)}{\underset{_}{\pi }\left({x}\right)}=\left(\frac{\frac{{x}}{\mathrm{log}{x}}}{\underset{_}{\pi }\left({x}\right)}\right)\left(\frac{\mathrm{log}{x}}{{{x}}^{1-{A}}}\right)$
47 43 44 45 46 syl3anc ${⊢}\left({\phi }\wedge {x}\in \left[2,\mathrm{+\infty }\right)\right)\to \frac{\left(\frac{{x}}{\mathrm{log}{x}}\right)\left(\frac{\mathrm{log}{x}}{{{x}}^{1-{A}}}\right)}{\underset{_}{\pi }\left({x}\right)}=\left(\frac{\frac{{x}}{\mathrm{log}{x}}}{\underset{_}{\pi }\left({x}\right)}\right)\left(\frac{\mathrm{log}{x}}{{{x}}^{1-{A}}}\right)$
48 33 rpcnne0d ${⊢}\left({\phi }\wedge {x}\in \left[2,\mathrm{+\infty }\right)\right)\to \left(\mathrm{log}{x}\in ℂ\wedge \mathrm{log}{x}\ne 0\right)$
49 38 rpcnne0d ${⊢}\left({\phi }\wedge {x}\in \left[2,\mathrm{+\infty }\right)\right)\to \left({{x}}^{1-{A}}\in ℂ\wedge {{x}}^{1-{A}}\ne 0\right)$
50 8 recnd ${⊢}\left({\phi }\wedge {x}\in \left[2,\mathrm{+\infty }\right)\right)\to {x}\in ℂ$
51 dmdcan ${⊢}\left(\left(\mathrm{log}{x}\in ℂ\wedge \mathrm{log}{x}\ne 0\right)\wedge \left({{x}}^{1-{A}}\in ℂ\wedge {{x}}^{1-{A}}\ne 0\right)\wedge {x}\in ℂ\right)\to \left(\frac{\mathrm{log}{x}}{{{x}}^{1-{A}}}\right)\left(\frac{{x}}{\mathrm{log}{x}}\right)=\frac{{x}}{{{x}}^{1-{A}}}$
52 48 49 50 51 syl3anc ${⊢}\left({\phi }\wedge {x}\in \left[2,\mathrm{+\infty }\right)\right)\to \left(\frac{\mathrm{log}{x}}{{{x}}^{1-{A}}}\right)\left(\frac{{x}}{\mathrm{log}{x}}\right)=\frac{{x}}{{{x}}^{1-{A}}}$
53 43 44 mulcomd ${⊢}\left({\phi }\wedge {x}\in \left[2,\mathrm{+\infty }\right)\right)\to \left(\frac{{x}}{\mathrm{log}{x}}\right)\left(\frac{\mathrm{log}{x}}{{{x}}^{1-{A}}}\right)=\left(\frac{\mathrm{log}{x}}{{{x}}^{1-{A}}}\right)\left(\frac{{x}}{\mathrm{log}{x}}\right)$
54 15 rpcnne0d ${⊢}\left({\phi }\wedge {x}\in \left[2,\mathrm{+\infty }\right)\right)\to \left({x}\in ℂ\wedge {x}\ne 0\right)$
55 ax-1cn ${⊢}1\in ℂ$
56 55 a1i ${⊢}\left({\phi }\wedge {x}\in \left[2,\mathrm{+\infty }\right)\right)\to 1\in ℂ$
57 36 rpcnd ${⊢}\left({\phi }\wedge {x}\in \left[2,\mathrm{+\infty }\right)\right)\to 1-{A}\in ℂ$
58 cxpsub ${⊢}\left(\left({x}\in ℂ\wedge {x}\ne 0\right)\wedge 1\in ℂ\wedge 1-{A}\in ℂ\right)\to {{x}}^{1-\left(1-{A}\right)}=\frac{{{x}}^{1}}{{{x}}^{1-{A}}}$
59 54 56 57 58 syl3anc ${⊢}\left({\phi }\wedge {x}\in \left[2,\mathrm{+\infty }\right)\right)\to {{x}}^{1-\left(1-{A}\right)}=\frac{{{x}}^{1}}{{{x}}^{1-{A}}}$
60 17 recnd ${⊢}\left({\phi }\wedge {x}\in \left[2,\mathrm{+\infty }\right)\right)\to {A}\in ℂ$
61 nncan ${⊢}\left(1\in ℂ\wedge {A}\in ℂ\right)\to 1-\left(1-{A}\right)={A}$
62 55 60 61 sylancr ${⊢}\left({\phi }\wedge {x}\in \left[2,\mathrm{+\infty }\right)\right)\to 1-\left(1-{A}\right)={A}$
63 62 oveq2d ${⊢}\left({\phi }\wedge {x}\in \left[2,\mathrm{+\infty }\right)\right)\to {{x}}^{1-\left(1-{A}\right)}={{x}}^{{A}}$
64 59 63 eqtr3d ${⊢}\left({\phi }\wedge {x}\in \left[2,\mathrm{+\infty }\right)\right)\to \frac{{{x}}^{1}}{{{x}}^{1-{A}}}={{x}}^{{A}}$
65 50 cxp1d ${⊢}\left({\phi }\wedge {x}\in \left[2,\mathrm{+\infty }\right)\right)\to {{x}}^{1}={x}$
66 65 oveq1d ${⊢}\left({\phi }\wedge {x}\in \left[2,\mathrm{+\infty }\right)\right)\to \frac{{{x}}^{1}}{{{x}}^{1-{A}}}=\frac{{x}}{{{x}}^{1-{A}}}$
67 64 66 eqtr3d ${⊢}\left({\phi }\wedge {x}\in \left[2,\mathrm{+\infty }\right)\right)\to {{x}}^{{A}}=\frac{{x}}{{{x}}^{1-{A}}}$
68 52 53 67 3eqtr4d ${⊢}\left({\phi }\wedge {x}\in \left[2,\mathrm{+\infty }\right)\right)\to \left(\frac{{x}}{\mathrm{log}{x}}\right)\left(\frac{\mathrm{log}{x}}{{{x}}^{1-{A}}}\right)={{x}}^{{A}}$
69 68 oveq1d ${⊢}\left({\phi }\wedge {x}\in \left[2,\mathrm{+\infty }\right)\right)\to \frac{\left(\frac{{x}}{\mathrm{log}{x}}\right)\left(\frac{\mathrm{log}{x}}{{{x}}^{1-{A}}}\right)}{\underset{_}{\pi }\left({x}\right)}=\frac{{{x}}^{{A}}}{\underset{_}{\pi }\left({x}\right)}$
70 47 69 eqtr3d ${⊢}\left({\phi }\wedge {x}\in \left[2,\mathrm{+\infty }\right)\right)\to \left(\frac{\frac{{x}}{\mathrm{log}{x}}}{\underset{_}{\pi }\left({x}\right)}\right)\left(\frac{\mathrm{log}{x}}{{{x}}^{1-{A}}}\right)=\frac{{{x}}^{{A}}}{\underset{_}{\pi }\left({x}\right)}$
71 70 mpteq2dva ${⊢}{\phi }\to \left({x}\in \left[2,\mathrm{+\infty }\right)⟼\left(\frac{\frac{{x}}{\mathrm{log}{x}}}{\underset{_}{\pi }\left({x}\right)}\right)\left(\frac{\mathrm{log}{x}}{{{x}}^{1-{A}}}\right)\right)=\left({x}\in \left[2,\mathrm{+\infty }\right)⟼\frac{{{x}}^{{A}}}{\underset{_}{\pi }\left({x}\right)}\right)$
72 42 71 eqtrd ${⊢}{\phi }\to \left({x}\in \left[2,\mathrm{+\infty }\right)⟼\frac{\frac{{x}}{\mathrm{log}{x}}}{\underset{_}{\pi }\left({x}\right)}\right){×}_{f}\left({x}\in \left[2,\mathrm{+\infty }\right)⟼\frac{\mathrm{log}{x}}{{{x}}^{1-{A}}}\right)=\left({x}\in \left[2,\mathrm{+\infty }\right)⟼\frac{{{x}}^{{A}}}{\underset{_}{\pi }\left({x}\right)}\right)$
73 chebbnd1 ${⊢}\left({x}\in \left[2,\mathrm{+\infty }\right)⟼\frac{\frac{{x}}{\mathrm{log}{x}}}{\underset{_}{\pi }\left({x}\right)}\right)\in 𝑂\left(1\right)$
74 15 ex ${⊢}{\phi }\to \left({x}\in \left[2,\mathrm{+\infty }\right)\to {x}\in {ℝ}^{+}\right)$
75 74 ssrdv ${⊢}{\phi }\to \left[2,\mathrm{+\infty }\right)\subseteq {ℝ}^{+}$
76 cxploglim
77 27 76 syl
78 75 77 rlimres2
79 o1rlimmul
80 73 78 79 sylancr
81 72 80 eqbrtrrd
82 23 27 81 rlimi ${⊢}{\phi }\to \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in \left[2,\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}\left({z}\le {x}\to \left|\left(\frac{{{x}}^{{A}}}{\underset{_}{\pi }\left({x}\right)}\right)-0\right|<1-{A}\right)$
83 22 rpcnd ${⊢}\left({\phi }\wedge {x}\in \left[2,\mathrm{+\infty }\right)\right)\to \frac{{{x}}^{{A}}}{\underset{_}{\pi }\left({x}\right)}\in ℂ$
84 83 subid1d ${⊢}\left({\phi }\wedge {x}\in \left[2,\mathrm{+\infty }\right)\right)\to \left(\frac{{{x}}^{{A}}}{\underset{_}{\pi }\left({x}\right)}\right)-0=\frac{{{x}}^{{A}}}{\underset{_}{\pi }\left({x}\right)}$
85 84 fveq2d ${⊢}\left({\phi }\wedge {x}\in \left[2,\mathrm{+\infty }\right)\right)\to \left|\left(\frac{{{x}}^{{A}}}{\underset{_}{\pi }\left({x}\right)}\right)-0\right|=\left|\frac{{{x}}^{{A}}}{\underset{_}{\pi }\left({x}\right)}\right|$
86 22 rpred ${⊢}\left({\phi }\wedge {x}\in \left[2,\mathrm{+\infty }\right)\right)\to \frac{{{x}}^{{A}}}{\underset{_}{\pi }\left({x}\right)}\in ℝ$
87 22 rpge0d ${⊢}\left({\phi }\wedge {x}\in \left[2,\mathrm{+\infty }\right)\right)\to 0\le \frac{{{x}}^{{A}}}{\underset{_}{\pi }\left({x}\right)}$
88 86 87 absidd ${⊢}\left({\phi }\wedge {x}\in \left[2,\mathrm{+\infty }\right)\right)\to \left|\frac{{{x}}^{{A}}}{\underset{_}{\pi }\left({x}\right)}\right|=\frac{{{x}}^{{A}}}{\underset{_}{\pi }\left({x}\right)}$
89 85 88 eqtrd ${⊢}\left({\phi }\wedge {x}\in \left[2,\mathrm{+\infty }\right)\right)\to \left|\left(\frac{{{x}}^{{A}}}{\underset{_}{\pi }\left({x}\right)}\right)-0\right|=\frac{{{x}}^{{A}}}{\underset{_}{\pi }\left({x}\right)}$
90 89 breq1d ${⊢}\left({\phi }\wedge {x}\in \left[2,\mathrm{+\infty }\right)\right)\to \left(\left|\left(\frac{{{x}}^{{A}}}{\underset{_}{\pi }\left({x}\right)}\right)-0\right|<1-{A}↔\frac{{{x}}^{{A}}}{\underset{_}{\pi }\left({x}\right)}<1-{A}\right)$
91 1 adantr ${⊢}\left({\phi }\wedge \left({x}\in \left[2,\mathrm{+\infty }\right)\wedge \frac{{{x}}^{{A}}}{\underset{_}{\pi }\left({x}\right)}<1-{A}\right)\right)\to {A}\in {ℝ}^{+}$
92 2 adantr ${⊢}\left({\phi }\wedge \left({x}\in \left[2,\mathrm{+\infty }\right)\wedge \frac{{{x}}^{{A}}}{\underset{_}{\pi }\left({x}\right)}<1-{A}\right)\right)\to {A}<1$
93 simprl ${⊢}\left({\phi }\wedge \left({x}\in \left[2,\mathrm{+\infty }\right)\wedge \frac{{{x}}^{{A}}}{\underset{_}{\pi }\left({x}\right)}<1-{A}\right)\right)\to {x}\in \left[2,\mathrm{+\infty }\right)$
94 simprr ${⊢}\left({\phi }\wedge \left({x}\in \left[2,\mathrm{+\infty }\right)\wedge \frac{{{x}}^{{A}}}{\underset{_}{\pi }\left({x}\right)}<1-{A}\right)\right)\to \frac{{{x}}^{{A}}}{\underset{_}{\pi }\left({x}\right)}<1-{A}$
95 91 92 93 94 chtppilimlem1 ${⊢}\left({\phi }\wedge \left({x}\in \left[2,\mathrm{+\infty }\right)\wedge \frac{{{x}}^{{A}}}{\underset{_}{\pi }\left({x}\right)}<1-{A}\right)\right)\to {{A}}^{2}\underset{_}{\pi }\left({x}\right)\mathrm{log}{x}<\theta \left({x}\right)$
96 95 expr ${⊢}\left({\phi }\wedge {x}\in \left[2,\mathrm{+\infty }\right)\right)\to \left(\frac{{{x}}^{{A}}}{\underset{_}{\pi }\left({x}\right)}<1-{A}\to {{A}}^{2}\underset{_}{\pi }\left({x}\right)\mathrm{log}{x}<\theta \left({x}\right)\right)$
97 90 96 sylbid ${⊢}\left({\phi }\wedge {x}\in \left[2,\mathrm{+\infty }\right)\right)\to \left(\left|\left(\frac{{{x}}^{{A}}}{\underset{_}{\pi }\left({x}\right)}\right)-0\right|<1-{A}\to {{A}}^{2}\underset{_}{\pi }\left({x}\right)\mathrm{log}{x}<\theta \left({x}\right)\right)$
98 97 imim2d ${⊢}\left({\phi }\wedge {x}\in \left[2,\mathrm{+\infty }\right)\right)\to \left(\left({z}\le {x}\to \left|\left(\frac{{{x}}^{{A}}}{\underset{_}{\pi }\left({x}\right)}\right)-0\right|<1-{A}\right)\to \left({z}\le {x}\to {{A}}^{2}\underset{_}{\pi }\left({x}\right)\mathrm{log}{x}<\theta \left({x}\right)\right)\right)$
99 98 ralimdva ${⊢}{\phi }\to \left(\forall {x}\in \left[2,\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}\left({z}\le {x}\to \left|\left(\frac{{{x}}^{{A}}}{\underset{_}{\pi }\left({x}\right)}\right)-0\right|<1-{A}\right)\to \forall {x}\in \left[2,\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}\left({z}\le {x}\to {{A}}^{2}\underset{_}{\pi }\left({x}\right)\mathrm{log}{x}<\theta \left({x}\right)\right)\right)$
100 99 reximdv ${⊢}{\phi }\to \left(\exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in \left[2,\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}\left({z}\le {x}\to \left|\left(\frac{{{x}}^{{A}}}{\underset{_}{\pi }\left({x}\right)}\right)-0\right|<1-{A}\right)\to \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in \left[2,\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}\left({z}\le {x}\to {{A}}^{2}\underset{_}{\pi }\left({x}\right)\mathrm{log}{x}<\theta \left({x}\right)\right)\right)$
101 82 100 mpd ${⊢}{\phi }\to \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in \left[2,\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}\left({z}\le {x}\to {{A}}^{2}\underset{_}{\pi }\left({x}\right)\mathrm{log}{x}<\theta \left({x}\right)\right)$