Metamath Proof Explorer


Theorem chto1lb

Description: The theta function is lower bounded by a linear term. Corollary of chebbnd1 . (Contributed by Mario Carneiro, 8-Apr-2016)

Ref Expression
Assertion chto1lb x2+∞xθx𝑂1

Proof

Step Hyp Ref Expression
1 ovexd 2+∞V
2 2re 2
3 elicopnf 2x2+∞x2x
4 2 3 ax-mp x2+∞x2x
5 4 biimpi x2+∞x2x
6 5 simpld x2+∞x
7 0red x2+∞0
8 2 a1i x2+∞2
9 2pos 0<2
10 9 a1i x2+∞0<2
11 5 simprd x2+∞2x
12 7 8 6 10 11 ltletrd x2+∞0<x
13 6 12 elrpd x2+∞x+
14 ppinncl x2xπ_x
15 14 nnrpd x2xπ_x+
16 5 15 syl x2+∞π_x+
17 1red x2+∞1
18 1lt2 1<2
19 18 a1i x2+∞1<2
20 17 8 6 19 11 ltletrd x2+∞1<x
21 6 20 rplogcld x2+∞logx+
22 16 21 rpmulcld x2+∞π_xlogx+
23 13 22 rpdivcld x2+∞xπ_xlogx+
24 23 rpcnd x2+∞xπ_xlogx
25 24 adantl x2+∞xπ_xlogx
26 chtrpcl x2xθx+
27 5 26 syl x2+∞θx+
28 22 27 rpdivcld x2+∞π_xlogxθx+
29 28 rpcnd x2+∞π_xlogxθx
30 29 adantl x2+∞π_xlogxθx
31 6 recnd x2+∞x
32 21 rpcnd x2+∞logx
33 16 rpcnd x2+∞π_x
34 21 rpne0d x2+∞logx0
35 16 rpne0d x2+∞π_x0
36 31 32 33 34 35 divdiv1d x2+∞xlogxπ_x=xlogxπ_x
37 32 33 mulcomd x2+∞logxπ_x=π_xlogx
38 37 oveq2d x2+∞xlogxπ_x=xπ_xlogx
39 36 38 eqtrd x2+∞xlogxπ_x=xπ_xlogx
40 39 mpteq2ia x2+∞xlogxπ_x=x2+∞xπ_xlogx
41 40 a1i x2+∞xlogxπ_x=x2+∞xπ_xlogx
42 27 rpcnd x2+∞θx
43 22 rpcnd x2+∞π_xlogx
44 27 rpne0d x2+∞θx0
45 22 rpne0d x2+∞π_xlogx0
46 42 43 44 45 recdivd x2+∞1θxπ_xlogx=π_xlogxθx
47 46 mpteq2ia x2+∞1θxπ_xlogx=x2+∞π_xlogxθx
48 47 a1i x2+∞1θxπ_xlogx=x2+∞π_xlogxθx
49 1 25 30 41 48 offval2 x2+∞xlogxπ_x×fx2+∞1θxπ_xlogx=x2+∞xπ_xlogxπ_xlogxθx
50 31 43 42 45 44 dmdcan2d x2+∞xπ_xlogxπ_xlogxθx=xθx
51 50 mpteq2ia x2+∞xπ_xlogxπ_xlogxθx=x2+∞xθx
52 49 51 eqtrdi x2+∞xlogxπ_x×fx2+∞1θxπ_xlogx=x2+∞xθx
53 chebbnd1 x2+∞xlogxπ_x𝑂1
54 ax-1cn 1
55 54 a1i x2+∞1
56 27 22 rpdivcld x2+∞θxπ_xlogx+
57 56 adantl x2+∞θxπ_xlogx+
58 57 rpcnd x2+∞θxπ_xlogx
59 6 ssriv 2+∞
60 rlimconst 2+∞1x2+∞11
61 59 54 60 mp2an x2+∞11
62 61 a1i x2+∞11
63 chtppilim x2+∞θxπ_xlogx1
64 63 a1i x2+∞θxπ_xlogx1
65 ax-1ne0 10
66 65 a1i 10
67 56 rpne0d x2+∞θxπ_xlogx0
68 67 adantl x2+∞θxπ_xlogx0
69 55 58 62 64 66 68 rlimdiv x2+∞1θxπ_xlogx11
70 rlimo1 x2+∞1θxπ_xlogx11x2+∞1θxπ_xlogx𝑂1
71 69 70 syl x2+∞1θxπ_xlogx𝑂1
72 o1mul x2+∞xlogxπ_x𝑂1x2+∞1θxπ_xlogx𝑂1x2+∞xlogxπ_x×fx2+∞1θxπ_xlogx𝑂1
73 53 71 72 sylancr x2+∞xlogxπ_x×fx2+∞1θxπ_xlogx𝑂1
74 52 73 eqeltrrd x2+∞xθx𝑂1
75 74 mptru x2+∞xθx𝑂1