Metamath Proof Explorer


Theorem chtppilimlem2

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

Ref Expression
Hypotheses chtppilim.1 φA+
chtppilim.2 φA<1
Assertion chtppilimlem2 φzx2+∞zxA2π_xlogx<θx

Proof

Step Hyp Ref Expression
1 chtppilim.1 φA+
2 chtppilim.2 φA<1
3 simpr φx2+∞x2+∞
4 2re 2
5 elicopnf 2x2+∞x2x
6 4 5 ax-mp x2+∞x2x
7 3 6 sylib φx2+∞x2x
8 7 simpld φx2+∞x
9 0red φx2+∞0
10 4 a1i φx2+∞2
11 2pos 0<2
12 11 a1i φx2+∞0<2
13 7 simprd φx2+∞2x
14 9 10 8 12 13 ltletrd φx2+∞0<x
15 8 14 elrpd φx2+∞x+
16 1 rpred φA
17 16 adantr φx2+∞A
18 15 17 rpcxpcld φx2+∞xA+
19 ppinncl x2xπ_x
20 7 19 syl φx2+∞π_x
21 20 nnrpd φx2+∞π_x+
22 18 21 rpdivcld φx2+∞xAπ_x+
23 22 ralrimiva φx2+∞xAπ_x+
24 1re 1
25 difrp A1A<11A+
26 16 24 25 sylancl φA<11A+
27 2 26 mpbid φ1A+
28 ovexd φ2+∞V
29 24 a1i φx2+∞1
30 1lt2 1<2
31 30 a1i φx2+∞1<2
32 29 10 8 31 13 ltletrd φx2+∞1<x
33 8 32 rplogcld φx2+∞logx+
34 15 33 rpdivcld φx2+∞xlogx+
35 34 21 rpdivcld φx2+∞xlogxπ_x+
36 27 adantr φx2+∞1A+
37 36 rpred φx2+∞1A
38 15 37 rpcxpcld φx2+∞x1A+
39 33 38 rpdivcld φx2+∞logxx1A+
40 eqidd φx2+∞xlogxπ_x=x2+∞xlogxπ_x
41 eqidd φx2+∞logxx1A=x2+∞logxx1A
42 28 35 39 40 41 offval2 φx2+∞xlogxπ_x×fx2+∞logxx1A=x2+∞xlogxπ_xlogxx1A
43 34 rpcnd φx2+∞xlogx
44 39 rpcnd φx2+∞logxx1A
45 21 rpcnne0d φx2+∞π_xπ_x0
46 div23 xlogxlogxx1Aπ_xπ_x0xlogxlogxx1Aπ_x=xlogxπ_xlogxx1A
47 43 44 45 46 syl3anc φx2+∞xlogxlogxx1Aπ_x=xlogxπ_xlogxx1A
48 33 rpcnne0d φx2+∞logxlogx0
49 38 rpcnne0d φx2+∞x1Ax1A0
50 8 recnd φx2+∞x
51 dmdcan logxlogx0x1Ax1A0xlogxx1Axlogx=xx1A
52 48 49 50 51 syl3anc φx2+∞logxx1Axlogx=xx1A
53 43 44 mulcomd φx2+∞xlogxlogxx1A=logxx1Axlogx
54 15 rpcnne0d φx2+∞xx0
55 ax-1cn 1
56 55 a1i φx2+∞1
57 36 rpcnd φx2+∞1A
58 cxpsub xx011Ax11A=x1x1A
59 54 56 57 58 syl3anc φx2+∞x11A=x1x1A
60 17 recnd φx2+∞A
61 nncan 1A11A=A
62 55 60 61 sylancr φx2+∞11A=A
63 62 oveq2d φx2+∞x11A=xA
64 59 63 eqtr3d φx2+∞x1x1A=xA
65 50 cxp1d φx2+∞x1=x
66 65 oveq1d φx2+∞x1x1A=xx1A
67 64 66 eqtr3d φx2+∞xA=xx1A
68 52 53 67 3eqtr4d φx2+∞xlogxlogxx1A=xA
69 68 oveq1d φx2+∞xlogxlogxx1Aπ_x=xAπ_x
70 47 69 eqtr3d φx2+∞xlogxπ_xlogxx1A=xAπ_x
71 70 mpteq2dva φx2+∞xlogxπ_xlogxx1A=x2+∞xAπ_x
72 42 71 eqtrd φx2+∞xlogxπ_x×fx2+∞logxx1A=x2+∞xAπ_x
73 chebbnd1 x2+∞xlogxπ_x𝑂1
74 15 ex φx2+∞x+
75 74 ssrdv φ2+∞+
76 cxploglim 1A+x+logxx1A0
77 27 76 syl φx+logxx1A0
78 75 77 rlimres2 φx2+∞logxx1A0
79 o1rlimmul x2+∞xlogxπ_x𝑂1x2+∞logxx1A0x2+∞xlogxπ_x×fx2+∞logxx1A0
80 73 78 79 sylancr φx2+∞xlogxπ_x×fx2+∞logxx1A0
81 72 80 eqbrtrrd φx2+∞xAπ_x0
82 23 27 81 rlimi φzx2+∞zxxAπ_x0<1A
83 22 rpcnd φx2+∞xAπ_x
84 83 subid1d φx2+∞xAπ_x0=xAπ_x
85 84 fveq2d φx2+∞xAπ_x0=xAπ_x
86 22 rpred φx2+∞xAπ_x
87 22 rpge0d φx2+∞0xAπ_x
88 86 87 absidd φx2+∞xAπ_x=xAπ_x
89 85 88 eqtrd φx2+∞xAπ_x0=xAπ_x
90 89 breq1d φx2+∞xAπ_x0<1AxAπ_x<1A
91 1 adantr φx2+∞xAπ_x<1AA+
92 2 adantr φx2+∞xAπ_x<1AA<1
93 simprl φx2+∞xAπ_x<1Ax2+∞
94 simprr φx2+∞xAπ_x<1AxAπ_x<1A
95 91 92 93 94 chtppilimlem1 φx2+∞xAπ_x<1AA2π_xlogx<θx
96 95 expr φx2+∞xAπ_x<1AA2π_xlogx<θx
97 90 96 sylbid φx2+∞xAπ_x0<1AA2π_xlogx<θx
98 97 imim2d φx2+∞zxxAπ_x0<1AzxA2π_xlogx<θx
99 98 ralimdva φx2+∞zxxAπ_x0<1Ax2+∞zxA2π_xlogx<θx
100 99 reximdv φzx2+∞zxxAπ_x0<1Azx2+∞zxA2π_xlogx<θx
101 82 100 mpd φzx2+∞zxA2π_xlogx<θx