Database
BASIC REAL AND COMPLEX FUNCTIONS
Basic number theory
Chebyshev's Weak Prime Number Theorem, Dirichlet's Theorem
chtppilimlem1
Next ⟩
chtppilimlem2
Metamath Proof Explorer
Ascii
Unicode
Theorem
chtppilimlem1
Description:
Lemma for
chtppilim
.
(Contributed by
Mario Carneiro
, 22-Sep-2014)
Ref
Expression
Hypotheses
chtppilim.1
⊢
φ
→
A
∈
ℝ
+
chtppilim.2
⊢
φ
→
A
<
1
chtppilim.3
⊢
φ
→
N
∈
2
+∞
chtppilim.4
π
⊢
φ
→
N
A
π
_
N
<
1
−
A
Assertion
chtppilimlem1
π
⊢
φ
→
A
2
π
_
N
log
N
<
θ
N
Proof
Step
Hyp
Ref
Expression
1
chtppilim.1
⊢
φ
→
A
∈
ℝ
+
2
chtppilim.2
⊢
φ
→
A
<
1
3
chtppilim.3
⊢
φ
→
N
∈
2
+∞
4
chtppilim.4
π
⊢
φ
→
N
A
π
_
N
<
1
−
A
5
1
rpred
⊢
φ
→
A
∈
ℝ
6
5
recnd
⊢
φ
→
A
∈
ℂ
7
6
sqvald
⊢
φ
→
A
2
=
A
A
8
7
oveq1d
π
π
⊢
φ
→
A
2
π
_
N
log
N
=
A
A
π
_
N
log
N
9
2re
⊢
2
∈
ℝ
10
elicopnf
⊢
2
∈
ℝ
→
N
∈
2
+∞
↔
N
∈
ℝ
∧
2
≤
N
11
9
10
ax-mp
⊢
N
∈
2
+∞
↔
N
∈
ℝ
∧
2
≤
N
12
3
11
sylib
⊢
φ
→
N
∈
ℝ
∧
2
≤
N
13
12
simpld
⊢
φ
→
N
∈
ℝ
14
ppicl
π
⊢
N
∈
ℝ
→
π
_
N
∈
ℕ
0
15
13
14
syl
π
⊢
φ
→
π
_
N
∈
ℕ
0
16
15
nn0red
π
⊢
φ
→
π
_
N
∈
ℝ
17
16
recnd
π
⊢
φ
→
π
_
N
∈
ℂ
18
0red
⊢
φ
→
0
∈
ℝ
19
9
a1i
⊢
φ
→
2
∈
ℝ
20
2pos
⊢
0
<
2
21
20
a1i
⊢
φ
→
0
<
2
22
12
simprd
⊢
φ
→
2
≤
N
23
18
19
13
21
22
ltletrd
⊢
φ
→
0
<
N
24
13
23
elrpd
⊢
φ
→
N
∈
ℝ
+
25
24
relogcld
⊢
φ
→
log
N
∈
ℝ
26
25
recnd
⊢
φ
→
log
N
∈
ℂ
27
6
6
17
26
mul4d
π
π
⊢
φ
→
A
A
π
_
N
log
N
=
A
π
_
N
A
log
N
28
8
27
eqtrd
π
π
⊢
φ
→
A
2
π
_
N
log
N
=
A
π
_
N
A
log
N
29
5
16
remulcld
π
⊢
φ
→
A
π
_
N
∈
ℝ
30
5
25
remulcld
⊢
φ
→
A
log
N
∈
ℝ
31
29
30
remulcld
π
⊢
φ
→
A
π
_
N
A
log
N
∈
ℝ
32
24
5
rpcxpcld
⊢
φ
→
N
A
∈
ℝ
+
33
32
rpred
⊢
φ
→
N
A
∈
ℝ
34
ppicl
π
⊢
N
A
∈
ℝ
→
π
_
N
A
∈
ℕ
0
35
33
34
syl
π
⊢
φ
→
π
_
N
A
∈
ℕ
0
36
35
nn0red
π
⊢
φ
→
π
_
N
A
∈
ℝ
37
16
36
resubcld
π
π
⊢
φ
→
π
_
N
−
π
_
N
A
∈
ℝ
38
37
30
remulcld
π
π
⊢
φ
→
π
_
N
−
π
_
N
A
A
log
N
∈
ℝ
39
chtcl
⊢
N
∈
ℝ
→
θ
N
∈
ℝ
40
13
39
syl
⊢
φ
→
θ
N
∈
ℝ
41
1red
⊢
φ
→
1
∈
ℝ
42
1lt2
⊢
1
<
2
43
42
a1i
⊢
φ
→
1
<
2
44
41
19
13
43
22
ltletrd
⊢
φ
→
1
<
N
45
13
44
rplogcld
⊢
φ
→
log
N
∈
ℝ
+
46
1
45
rpmulcld
⊢
φ
→
A
log
N
∈
ℝ
+
47
16
33
resubcld
π
⊢
φ
→
π
_
N
−
N
A
∈
ℝ
48
ppinncl
π
⊢
N
∈
ℝ
∧
2
≤
N
→
π
_
N
∈
ℕ
49
12
48
syl
π
⊢
φ
→
π
_
N
∈
ℕ
50
33
49
nndivred
π
⊢
φ
→
N
A
π
_
N
∈
ℝ
51
50
41
5
4
ltsub13d
π
⊢
φ
→
A
<
1
−
N
A
π
_
N
52
33
recnd
⊢
φ
→
N
A
∈
ℂ
53
49
nnrpd
π
⊢
φ
→
π
_
N
∈
ℝ
+
54
53
rpcnne0d
π
π
⊢
φ
→
π
_
N
∈
ℂ
∧
π
_
N
≠
0
55
divsubdir
π
π
π
π
π
π
π
π
⊢
π
_
N
∈
ℂ
∧
N
A
∈
ℂ
∧
π
_
N
∈
ℂ
∧
π
_
N
≠
0
→
π
_
N
−
N
A
π
_
N
=
π
_
N
π
_
N
−
N
A
π
_
N
56
17
52
54
55
syl3anc
π
π
π
π
π
⊢
φ
→
π
_
N
−
N
A
π
_
N
=
π
_
N
π
_
N
−
N
A
π
_
N
57
divid
π
π
π
π
⊢
π
_
N
∈
ℂ
∧
π
_
N
≠
0
→
π
_
N
π
_
N
=
1
58
54
57
syl
π
π
⊢
φ
→
π
_
N
π
_
N
=
1
59
58
oveq1d
π
π
π
π
⊢
φ
→
π
_
N
π
_
N
−
N
A
π
_
N
=
1
−
N
A
π
_
N
60
56
59
eqtrd
π
π
π
⊢
φ
→
π
_
N
−
N
A
π
_
N
=
1
−
N
A
π
_
N
61
51
60
breqtrrd
π
π
⊢
φ
→
A
<
π
_
N
−
N
A
π
_
N
62
5
47
53
ltmuldivd
π
π
π
π
⊢
φ
→
A
π
_
N
<
π
_
N
−
N
A
↔
A
<
π
_
N
−
N
A
π
_
N
63
61
62
mpbird
π
π
⊢
φ
→
A
π
_
N
<
π
_
N
−
N
A
64
ppiltx
π
⊢
N
A
∈
ℝ
+
→
π
_
N
A
<
N
A
65
32
64
syl
π
⊢
φ
→
π
_
N
A
<
N
A
66
36
33
16
65
ltsub2dd
π
π
π
⊢
φ
→
π
_
N
−
N
A
<
π
_
N
−
π
_
N
A
67
29
47
37
63
66
lttrd
π
π
π
⊢
φ
→
A
π
_
N
<
π
_
N
−
π
_
N
A
68
29
37
46
67
ltmul1dd
π
π
π
⊢
φ
→
A
π
_
N
A
log
N
<
π
_
N
−
π
_
N
A
A
log
N
69
fzfid
⊢
φ
→
N
A
+
1
…
N
∈
Fin
70
inss1
⊢
N
A
+
1
…
N
∩
ℙ
⊆
N
A
+
1
…
N
71
ssfi
⊢
N
A
+
1
…
N
∈
Fin
∧
N
A
+
1
…
N
∩
ℙ
⊆
N
A
+
1
…
N
→
N
A
+
1
…
N
∩
ℙ
∈
Fin
72
69
70
71
sylancl
⊢
φ
→
N
A
+
1
…
N
∩
ℙ
∈
Fin
73
simpr
⊢
φ
∧
p
∈
N
A
+
1
…
N
∩
ℙ
→
p
∈
N
A
+
1
…
N
∩
ℙ
74
73
elin2d
⊢
φ
∧
p
∈
N
A
+
1
…
N
∩
ℙ
→
p
∈
ℙ
75
prmnn
⊢
p
∈
ℙ
→
p
∈
ℕ
76
75
nnrpd
⊢
p
∈
ℙ
→
p
∈
ℝ
+
77
74
76
syl
⊢
φ
∧
p
∈
N
A
+
1
…
N
∩
ℙ
→
p
∈
ℝ
+
78
77
relogcld
⊢
φ
∧
p
∈
N
A
+
1
…
N
∩
ℙ
→
log
p
∈
ℝ
79
72
78
fsumrecl
⊢
φ
→
∑
p
∈
N
A
+
1
…
N
∩
ℙ
log
p
∈
ℝ
80
30
recnd
⊢
φ
→
A
log
N
∈
ℂ
81
fsumconst
⊢
N
A
+
1
…
N
∩
ℙ
∈
Fin
∧
A
log
N
∈
ℂ
→
∑
p
∈
N
A
+
1
…
N
∩
ℙ
A
log
N
=
N
A
+
1
…
N
∩
ℙ
A
log
N
82
72
80
81
syl2anc
⊢
φ
→
∑
p
∈
N
A
+
1
…
N
∩
ℙ
A
log
N
=
N
A
+
1
…
N
∩
ℙ
A
log
N
83
ppifl
π
π
⊢
N
∈
ℝ
→
π
_
N
=
π
_
N
84
13
83
syl
π
π
⊢
φ
→
π
_
N
=
π
_
N
85
ppifl
π
π
⊢
N
A
∈
ℝ
→
π
_
N
A
=
π
_
N
A
86
33
85
syl
π
π
⊢
φ
→
π
_
N
A
=
π
_
N
A
87
84
86
oveq12d
π
π
π
π
⊢
φ
→
π
_
N
−
π
_
N
A
=
π
_
N
−
π
_
N
A
88
41
13
44
ltled
⊢
φ
→
1
≤
N
89
1re
⊢
1
∈
ℝ
90
ltle
⊢
A
∈
ℝ
∧
1
∈
ℝ
→
A
<
1
→
A
≤
1
91
5
89
90
sylancl
⊢
φ
→
A
<
1
→
A
≤
1
92
2
91
mpd
⊢
φ
→
A
≤
1
93
13
88
5
41
92
cxplead
⊢
φ
→
N
A
≤
N
1
94
13
recnd
⊢
φ
→
N
∈
ℂ
95
94
cxp1d
⊢
φ
→
N
1
=
N
96
93
95
breqtrd
⊢
φ
→
N
A
≤
N
97
flword2
⊢
N
A
∈
ℝ
∧
N
∈
ℝ
∧
N
A
≤
N
→
N
∈
ℤ
≥
N
A
98
33
13
96
97
syl3anc
⊢
φ
→
N
∈
ℤ
≥
N
A
99
ppidif
π
π
⊢
N
∈
ℤ
≥
N
A
→
π
_
N
−
π
_
N
A
=
N
A
+
1
…
N
∩
ℙ
100
98
99
syl
π
π
⊢
φ
→
π
_
N
−
π
_
N
A
=
N
A
+
1
…
N
∩
ℙ
101
87
100
eqtr3d
π
π
⊢
φ
→
π
_
N
−
π
_
N
A
=
N
A
+
1
…
N
∩
ℙ
102
101
oveq1d
π
π
⊢
φ
→
π
_
N
−
π
_
N
A
A
log
N
=
N
A
+
1
…
N
∩
ℙ
A
log
N
103
82
102
eqtr4d
π
π
⊢
φ
→
∑
p
∈
N
A
+
1
…
N
∩
ℙ
A
log
N
=
π
_
N
−
π
_
N
A
A
log
N
104
30
adantr
⊢
φ
∧
p
∈
N
A
+
1
…
N
∩
ℙ
→
A
log
N
∈
ℝ
105
33
adantr
⊢
φ
∧
p
∈
N
A
+
1
…
N
∩
ℙ
→
N
A
∈
ℝ
106
reflcl
⊢
N
A
∈
ℝ
→
N
A
∈
ℝ
107
peano2re
⊢
N
A
∈
ℝ
→
N
A
+
1
∈
ℝ
108
33
106
107
3syl
⊢
φ
→
N
A
+
1
∈
ℝ
109
108
adantr
⊢
φ
∧
p
∈
N
A
+
1
…
N
∩
ℙ
→
N
A
+
1
∈
ℝ
110
77
rpred
⊢
φ
∧
p
∈
N
A
+
1
…
N
∩
ℙ
→
p
∈
ℝ
111
fllep1
⊢
N
A
∈
ℝ
→
N
A
≤
N
A
+
1
112
33
111
syl
⊢
φ
→
N
A
≤
N
A
+
1
113
112
adantr
⊢
φ
∧
p
∈
N
A
+
1
…
N
∩
ℙ
→
N
A
≤
N
A
+
1
114
73
elin1d
⊢
φ
∧
p
∈
N
A
+
1
…
N
∩
ℙ
→
p
∈
N
A
+
1
…
N
115
elfzle1
⊢
p
∈
N
A
+
1
…
N
→
N
A
+
1
≤
p
116
114
115
syl
⊢
φ
∧
p
∈
N
A
+
1
…
N
∩
ℙ
→
N
A
+
1
≤
p
117
105
109
110
113
116
letrd
⊢
φ
∧
p
∈
N
A
+
1
…
N
∩
ℙ
→
N
A
≤
p
118
24
rpne0d
⊢
φ
→
N
≠
0
119
94
118
6
cxpefd
⊢
φ
→
N
A
=
e
A
log
N
120
119
eqcomd
⊢
φ
→
e
A
log
N
=
N
A
121
120
adantr
⊢
φ
∧
p
∈
N
A
+
1
…
N
∩
ℙ
→
e
A
log
N
=
N
A
122
77
reeflogd
⊢
φ
∧
p
∈
N
A
+
1
…
N
∩
ℙ
→
e
log
p
=
p
123
117
121
122
3brtr4d
⊢
φ
∧
p
∈
N
A
+
1
…
N
∩
ℙ
→
e
A
log
N
≤
e
log
p
124
efle
⊢
A
log
N
∈
ℝ
∧
log
p
∈
ℝ
→
A
log
N
≤
log
p
↔
e
A
log
N
≤
e
log
p
125
104
78
124
syl2anc
⊢
φ
∧
p
∈
N
A
+
1
…
N
∩
ℙ
→
A
log
N
≤
log
p
↔
e
A
log
N
≤
e
log
p
126
123
125
mpbird
⊢
φ
∧
p
∈
N
A
+
1
…
N
∩
ℙ
→
A
log
N
≤
log
p
127
72
104
78
126
fsumle
⊢
φ
→
∑
p
∈
N
A
+
1
…
N
∩
ℙ
A
log
N
≤
∑
p
∈
N
A
+
1
…
N
∩
ℙ
log
p
128
103
127
eqbrtrrd
π
π
⊢
φ
→
π
_
N
−
π
_
N
A
A
log
N
≤
∑
p
∈
N
A
+
1
…
N
∩
ℙ
log
p
129
fzfid
⊢
φ
→
1
…
N
∈
Fin
130
inss1
⊢
1
…
N
∩
ℙ
⊆
1
…
N
131
ssfi
⊢
1
…
N
∈
Fin
∧
1
…
N
∩
ℙ
⊆
1
…
N
→
1
…
N
∩
ℙ
∈
Fin
132
129
130
131
sylancl
⊢
φ
→
1
…
N
∩
ℙ
∈
Fin
133
simpr
⊢
φ
∧
p
∈
1
…
N
∩
ℙ
→
p
∈
1
…
N
∩
ℙ
134
133
elin2d
⊢
φ
∧
p
∈
1
…
N
∩
ℙ
→
p
∈
ℙ
135
prmuz2
⊢
p
∈
ℙ
→
p
∈
ℤ
≥
2
136
134
135
syl
⊢
φ
∧
p
∈
1
…
N
∩
ℙ
→
p
∈
ℤ
≥
2
137
eluz2b2
⊢
p
∈
ℤ
≥
2
↔
p
∈
ℕ
∧
1
<
p
138
136
137
sylib
⊢
φ
∧
p
∈
1
…
N
∩
ℙ
→
p
∈
ℕ
∧
1
<
p
139
138
simpld
⊢
φ
∧
p
∈
1
…
N
∩
ℙ
→
p
∈
ℕ
140
139
nnred
⊢
φ
∧
p
∈
1
…
N
∩
ℙ
→
p
∈
ℝ
141
138
simprd
⊢
φ
∧
p
∈
1
…
N
∩
ℙ
→
1
<
p
142
140
141
rplogcld
⊢
φ
∧
p
∈
1
…
N
∩
ℙ
→
log
p
∈
ℝ
+
143
142
rpred
⊢
φ
∧
p
∈
1
…
N
∩
ℙ
→
log
p
∈
ℝ
144
142
rpge0d
⊢
φ
∧
p
∈
1
…
N
∩
ℙ
→
0
≤
log
p
145
32
rpge0d
⊢
φ
→
0
≤
N
A
146
flge0nn0
⊢
N
A
∈
ℝ
∧
0
≤
N
A
→
N
A
∈
ℕ
0
147
33
145
146
syl2anc
⊢
φ
→
N
A
∈
ℕ
0
148
nn0p1nn
⊢
N
A
∈
ℕ
0
→
N
A
+
1
∈
ℕ
149
147
148
syl
⊢
φ
→
N
A
+
1
∈
ℕ
150
nnuz
⊢
ℕ
=
ℤ
≥
1
151
149
150
eleqtrdi
⊢
φ
→
N
A
+
1
∈
ℤ
≥
1
152
fzss1
⊢
N
A
+
1
∈
ℤ
≥
1
→
N
A
+
1
…
N
⊆
1
…
N
153
ssrin
⊢
N
A
+
1
…
N
⊆
1
…
N
→
N
A
+
1
…
N
∩
ℙ
⊆
1
…
N
∩
ℙ
154
151
152
153
3syl
⊢
φ
→
N
A
+
1
…
N
∩
ℙ
⊆
1
…
N
∩
ℙ
155
132
143
144
154
fsumless
⊢
φ
→
∑
p
∈
N
A
+
1
…
N
∩
ℙ
log
p
≤
∑
p
∈
1
…
N
∩
ℙ
log
p
156
chtval
⊢
N
∈
ℝ
→
θ
N
=
∑
p
∈
0
N
∩
ℙ
log
p
157
13
156
syl
⊢
φ
→
θ
N
=
∑
p
∈
0
N
∩
ℙ
log
p
158
2eluzge1
⊢
2
∈
ℤ
≥
1
159
ppisval2
⊢
N
∈
ℝ
∧
2
∈
ℤ
≥
1
→
0
N
∩
ℙ
=
1
…
N
∩
ℙ
160
13
158
159
sylancl
⊢
φ
→
0
N
∩
ℙ
=
1
…
N
∩
ℙ
161
160
sumeq1d
⊢
φ
→
∑
p
∈
0
N
∩
ℙ
log
p
=
∑
p
∈
1
…
N
∩
ℙ
log
p
162
157
161
eqtrd
⊢
φ
→
θ
N
=
∑
p
∈
1
…
N
∩
ℙ
log
p
163
155
162
breqtrrd
⊢
φ
→
∑
p
∈
N
A
+
1
…
N
∩
ℙ
log
p
≤
θ
N
164
38
79
40
128
163
letrd
π
π
⊢
φ
→
π
_
N
−
π
_
N
A
A
log
N
≤
θ
N
165
31
38
40
68
164
ltletrd
π
⊢
φ
→
A
π
_
N
A
log
N
<
θ
N
166
28
165
eqbrtrd
π
⊢
φ
→
A
2
π
_
N
log
N
<
θ
N