Database
BASIC REAL AND COMPLEX FUNCTIONS
Basic number theory
Chebyshev's Weak Prime Number Theorem, Dirichlet's Theorem
chtppilimlem2
Next ⟩
chtppilim
Metamath Proof Explorer
Ascii
Unicode
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
π
⊢
φ
→
∃
z
∈
ℝ
∀
x
∈
2
+∞
z
≤
x
→
A
2
π
_
x
log
x
<
θ
x
Proof
Step
Hyp
Ref
Expression
1
chtppilim.1
⊢
φ
→
A
∈
ℝ
+
2
chtppilim.2
⊢
φ
→
A
<
1
3
simpr
⊢
φ
∧
x
∈
2
+∞
→
x
∈
2
+∞
4
2re
⊢
2
∈
ℝ
5
elicopnf
⊢
2
∈
ℝ
→
x
∈
2
+∞
↔
x
∈
ℝ
∧
2
≤
x
6
4
5
ax-mp
⊢
x
∈
2
+∞
↔
x
∈
ℝ
∧
2
≤
x
7
3
6
sylib
⊢
φ
∧
x
∈
2
+∞
→
x
∈
ℝ
∧
2
≤
x
8
7
simpld
⊢
φ
∧
x
∈
2
+∞
→
x
∈
ℝ
9
0red
⊢
φ
∧
x
∈
2
+∞
→
0
∈
ℝ
10
4
a1i
⊢
φ
∧
x
∈
2
+∞
→
2
∈
ℝ
11
2pos
⊢
0
<
2
12
11
a1i
⊢
φ
∧
x
∈
2
+∞
→
0
<
2
13
7
simprd
⊢
φ
∧
x
∈
2
+∞
→
2
≤
x
14
9
10
8
12
13
ltletrd
⊢
φ
∧
x
∈
2
+∞
→
0
<
x
15
8
14
elrpd
⊢
φ
∧
x
∈
2
+∞
→
x
∈
ℝ
+
16
1
rpred
⊢
φ
→
A
∈
ℝ
17
16
adantr
⊢
φ
∧
x
∈
2
+∞
→
A
∈
ℝ
18
15
17
rpcxpcld
⊢
φ
∧
x
∈
2
+∞
→
x
A
∈
ℝ
+
19
ppinncl
π
⊢
x
∈
ℝ
∧
2
≤
x
→
π
_
x
∈
ℕ
20
7
19
syl
π
⊢
φ
∧
x
∈
2
+∞
→
π
_
x
∈
ℕ
21
20
nnrpd
π
⊢
φ
∧
x
∈
2
+∞
→
π
_
x
∈
ℝ
+
22
18
21
rpdivcld
π
⊢
φ
∧
x
∈
2
+∞
→
x
A
π
_
x
∈
ℝ
+
23
22
ralrimiva
π
⊢
φ
→
∀
x
∈
2
+∞
x
A
π
_
x
∈
ℝ
+
24
1re
⊢
1
∈
ℝ
25
difrp
⊢
A
∈
ℝ
∧
1
∈
ℝ
→
A
<
1
↔
1
−
A
∈
ℝ
+
26
16
24
25
sylancl
⊢
φ
→
A
<
1
↔
1
−
A
∈
ℝ
+
27
2
26
mpbid
⊢
φ
→
1
−
A
∈
ℝ
+
28
ovexd
⊢
φ
→
2
+∞
∈
V
29
24
a1i
⊢
φ
∧
x
∈
2
+∞
→
1
∈
ℝ
30
1lt2
⊢
1
<
2
31
30
a1i
⊢
φ
∧
x
∈
2
+∞
→
1
<
2
32
29
10
8
31
13
ltletrd
⊢
φ
∧
x
∈
2
+∞
→
1
<
x
33
8
32
rplogcld
⊢
φ
∧
x
∈
2
+∞
→
log
x
∈
ℝ
+
34
15
33
rpdivcld
⊢
φ
∧
x
∈
2
+∞
→
x
log
x
∈
ℝ
+
35
34
21
rpdivcld
π
⊢
φ
∧
x
∈
2
+∞
→
x
log
x
π
_
x
∈
ℝ
+
36
27
adantr
⊢
φ
∧
x
∈
2
+∞
→
1
−
A
∈
ℝ
+
37
36
rpred
⊢
φ
∧
x
∈
2
+∞
→
1
−
A
∈
ℝ
38
15
37
rpcxpcld
⊢
φ
∧
x
∈
2
+∞
→
x
1
−
A
∈
ℝ
+
39
33
38
rpdivcld
⊢
φ
∧
x
∈
2
+∞
→
log
x
x
1
−
A
∈
ℝ
+
40
eqidd
π
π
⊢
φ
→
x
∈
2
+∞
⟼
x
log
x
π
_
x
=
x
∈
2
+∞
⟼
x
log
x
π
_
x
41
eqidd
⊢
φ
→
x
∈
2
+∞
⟼
log
x
x
1
−
A
=
x
∈
2
+∞
⟼
log
x
x
1
−
A
42
28
35
39
40
41
offval2
π
π
⊢
φ
→
x
∈
2
+∞
⟼
x
log
x
π
_
x
×
f
x
∈
2
+∞
⟼
log
x
x
1
−
A
=
x
∈
2
+∞
⟼
x
log
x
π
_
x
log
x
x
1
−
A
43
34
rpcnd
⊢
φ
∧
x
∈
2
+∞
→
x
log
x
∈
ℂ
44
39
rpcnd
⊢
φ
∧
x
∈
2
+∞
→
log
x
x
1
−
A
∈
ℂ
45
21
rpcnne0d
π
π
⊢
φ
∧
x
∈
2
+∞
→
π
_
x
∈
ℂ
∧
π
_
x
≠
0
46
div23
π
π
π
π
⊢
x
log
x
∈
ℂ
∧
log
x
x
1
−
A
∈
ℂ
∧
π
_
x
∈
ℂ
∧
π
_
x
≠
0
→
x
log
x
log
x
x
1
−
A
π
_
x
=
x
log
x
π
_
x
log
x
x
1
−
A
47
43
44
45
46
syl3anc
π
π
⊢
φ
∧
x
∈
2
+∞
→
x
log
x
log
x
x
1
−
A
π
_
x
=
x
log
x
π
_
x
log
x
x
1
−
A
48
33
rpcnne0d
⊢
φ
∧
x
∈
2
+∞
→
log
x
∈
ℂ
∧
log
x
≠
0
49
38
rpcnne0d
⊢
φ
∧
x
∈
2
+∞
→
x
1
−
A
∈
ℂ
∧
x
1
−
A
≠
0
50
8
recnd
⊢
φ
∧
x
∈
2
+∞
→
x
∈
ℂ
51
dmdcan
⊢
log
x
∈
ℂ
∧
log
x
≠
0
∧
x
1
−
A
∈
ℂ
∧
x
1
−
A
≠
0
∧
x
∈
ℂ
→
log
x
x
1
−
A
x
log
x
=
x
x
1
−
A
52
48
49
50
51
syl3anc
⊢
φ
∧
x
∈
2
+∞
→
log
x
x
1
−
A
x
log
x
=
x
x
1
−
A
53
43
44
mulcomd
⊢
φ
∧
x
∈
2
+∞
→
x
log
x
log
x
x
1
−
A
=
log
x
x
1
−
A
x
log
x
54
15
rpcnne0d
⊢
φ
∧
x
∈
2
+∞
→
x
∈
ℂ
∧
x
≠
0
55
ax-1cn
⊢
1
∈
ℂ
56
55
a1i
⊢
φ
∧
x
∈
2
+∞
→
1
∈
ℂ
57
36
rpcnd
⊢
φ
∧
x
∈
2
+∞
→
1
−
A
∈
ℂ
58
cxpsub
⊢
x
∈
ℂ
∧
x
≠
0
∧
1
∈
ℂ
∧
1
−
A
∈
ℂ
→
x
1
−
1
−
A
=
x
1
x
1
−
A
59
54
56
57
58
syl3anc
⊢
φ
∧
x
∈
2
+∞
→
x
1
−
1
−
A
=
x
1
x
1
−
A
60
17
recnd
⊢
φ
∧
x
∈
2
+∞
→
A
∈
ℂ
61
nncan
⊢
1
∈
ℂ
∧
A
∈
ℂ
→
1
−
1
−
A
=
A
62
55
60
61
sylancr
⊢
φ
∧
x
∈
2
+∞
→
1
−
1
−
A
=
A
63
62
oveq2d
⊢
φ
∧
x
∈
2
+∞
→
x
1
−
1
−
A
=
x
A
64
59
63
eqtr3d
⊢
φ
∧
x
∈
2
+∞
→
x
1
x
1
−
A
=
x
A
65
50
cxp1d
⊢
φ
∧
x
∈
2
+∞
→
x
1
=
x
66
65
oveq1d
⊢
φ
∧
x
∈
2
+∞
→
x
1
x
1
−
A
=
x
x
1
−
A
67
64
66
eqtr3d
⊢
φ
∧
x
∈
2
+∞
→
x
A
=
x
x
1
−
A
68
52
53
67
3eqtr4d
⊢
φ
∧
x
∈
2
+∞
→
x
log
x
log
x
x
1
−
A
=
x
A
69
68
oveq1d
π
π
⊢
φ
∧
x
∈
2
+∞
→
x
log
x
log
x
x
1
−
A
π
_
x
=
x
A
π
_
x
70
47
69
eqtr3d
π
π
⊢
φ
∧
x
∈
2
+∞
→
x
log
x
π
_
x
log
x
x
1
−
A
=
x
A
π
_
x
71
70
mpteq2dva
π
π
⊢
φ
→
x
∈
2
+∞
⟼
x
log
x
π
_
x
log
x
x
1
−
A
=
x
∈
2
+∞
⟼
x
A
π
_
x
72
42
71
eqtrd
π
π
⊢
φ
→
x
∈
2
+∞
⟼
x
log
x
π
_
x
×
f
x
∈
2
+∞
⟼
log
x
x
1
−
A
=
x
∈
2
+∞
⟼
x
A
π
_
x
73
chebbnd1
π
⊢
x
∈
2
+∞
⟼
x
log
x
π
_
x
∈
𝑂
1
74
15
ex
⊢
φ
→
x
∈
2
+∞
→
x
∈
ℝ
+
75
74
ssrdv
⊢
φ
→
2
+∞
⊆
ℝ
+
76
cxploglim
⊢
1
−
A
∈
ℝ
+
→
x
∈
ℝ
+
⟼
log
x
x
1
−
A
⇝
ℝ
0
77
27
76
syl
⊢
φ
→
x
∈
ℝ
+
⟼
log
x
x
1
−
A
⇝
ℝ
0
78
75
77
rlimres2
⊢
φ
→
x
∈
2
+∞
⟼
log
x
x
1
−
A
⇝
ℝ
0
79
o1rlimmul
π
π
⊢
x
∈
2
+∞
⟼
x
log
x
π
_
x
∈
𝑂
1
∧
x
∈
2
+∞
⟼
log
x
x
1
−
A
⇝
ℝ
0
→
x
∈
2
+∞
⟼
x
log
x
π
_
x
×
f
x
∈
2
+∞
⟼
log
x
x
1
−
A
⇝
ℝ
0
80
73
78
79
sylancr
π
⊢
φ
→
x
∈
2
+∞
⟼
x
log
x
π
_
x
×
f
x
∈
2
+∞
⟼
log
x
x
1
−
A
⇝
ℝ
0
81
72
80
eqbrtrrd
π
⊢
φ
→
x
∈
2
+∞
⟼
x
A
π
_
x
⇝
ℝ
0
82
23
27
81
rlimi
π
⊢
φ
→
∃
z
∈
ℝ
∀
x
∈
2
+∞
z
≤
x
→
x
A
π
_
x
−
0
<
1
−
A
83
22
rpcnd
π
⊢
φ
∧
x
∈
2
+∞
→
x
A
π
_
x
∈
ℂ
84
83
subid1d
π
π
⊢
φ
∧
x
∈
2
+∞
→
x
A
π
_
x
−
0
=
x
A
π
_
x
85
84
fveq2d
π
π
⊢
φ
∧
x
∈
2
+∞
→
x
A
π
_
x
−
0
=
x
A
π
_
x
86
22
rpred
π
⊢
φ
∧
x
∈
2
+∞
→
x
A
π
_
x
∈
ℝ
87
22
rpge0d
π
⊢
φ
∧
x
∈
2
+∞
→
0
≤
x
A
π
_
x
88
86
87
absidd
π
π
⊢
φ
∧
x
∈
2
+∞
→
x
A
π
_
x
=
x
A
π
_
x
89
85
88
eqtrd
π
π
⊢
φ
∧
x
∈
2
+∞
→
x
A
π
_
x
−
0
=
x
A
π
_
x
90
89
breq1d
π
π
⊢
φ
∧
x
∈
2
+∞
→
x
A
π
_
x
−
0
<
1
−
A
↔
x
A
π
_
x
<
1
−
A
91
1
adantr
π
⊢
φ
∧
x
∈
2
+∞
∧
x
A
π
_
x
<
1
−
A
→
A
∈
ℝ
+
92
2
adantr
π
⊢
φ
∧
x
∈
2
+∞
∧
x
A
π
_
x
<
1
−
A
→
A
<
1
93
simprl
π
⊢
φ
∧
x
∈
2
+∞
∧
x
A
π
_
x
<
1
−
A
→
x
∈
2
+∞
94
simprr
π
π
⊢
φ
∧
x
∈
2
+∞
∧
x
A
π
_
x
<
1
−
A
→
x
A
π
_
x
<
1
−
A
95
91
92
93
94
chtppilimlem1
π
π
⊢
φ
∧
x
∈
2
+∞
∧
x
A
π
_
x
<
1
−
A
→
A
2
π
_
x
log
x
<
θ
x
96
95
expr
π
π
⊢
φ
∧
x
∈
2
+∞
→
x
A
π
_
x
<
1
−
A
→
A
2
π
_
x
log
x
<
θ
x
97
90
96
sylbid
π
π
⊢
φ
∧
x
∈
2
+∞
→
x
A
π
_
x
−
0
<
1
−
A
→
A
2
π
_
x
log
x
<
θ
x
98
97
imim2d
π
π
⊢
φ
∧
x
∈
2
+∞
→
z
≤
x
→
x
A
π
_
x
−
0
<
1
−
A
→
z
≤
x
→
A
2
π
_
x
log
x
<
θ
x
99
98
ralimdva
π
π
⊢
φ
→
∀
x
∈
2
+∞
z
≤
x
→
x
A
π
_
x
−
0
<
1
−
A
→
∀
x
∈
2
+∞
z
≤
x
→
A
2
π
_
x
log
x
<
θ
x
100
99
reximdv
π
π
⊢
φ
→
∃
z
∈
ℝ
∀
x
∈
2
+∞
z
≤
x
→
x
A
π
_
x
−
0
<
1
−
A
→
∃
z
∈
ℝ
∀
x
∈
2
+∞
z
≤
x
→
A
2
π
_
x
log
x
<
θ
x
101
82
100
mpd
π
⊢
φ
→
∃
z
∈
ℝ
∀
x
∈
2
+∞
z
≤
x
→
A
2
π
_
x
log
x
<
θ
x