Prime numbers

Symbol: PP —

\mathbb{P}

— Prime numbers

The set of prime numbers.

Definitions:

Fungrim symbol	Notation	Short description
`PP`	$\mathbb{P}$	Prime numbers

Source code for this entry:

Entry(ID("38f111"),
    SymbolDefinition(PP, PP, "Prime numbers"),
    Description("The set of prime numbers."))

0b643d

Symbol: PrimeNumber —

p_{n}

— nth prime number

Domain	Codomain
$n \in \mathbb{Z}_{\ge 1}$	$p_{n} \in \mathbb{P}$

Table data:

\left(P, Q\right)

such that

\left(P\right) \;\implies\; \left(Q\right)

Definitions:

Fungrim symbol	Notation	Short description
`PrimeNumber`	$p_{n}$	nth prime number
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n
`PP`	$\mathbb{P}$	Prime numbers

Source code for this entry:

Entry(ID("0b643d"),
    SymbolDefinition(PrimeNumber, PrimeNumber(n), "nth prime number"),
    Table(TableRelation(Tuple(P, Q), Implies(P, Q)), TableHeadings(Description("Domain"), Description("Codomain")), List(Tuple(Element(n, ZZGreaterEqual(1)), Element(PrimeNumber(n), PP)))))

6c22c8

Symbol: PrimePi —

\pi(x)

— Prime counting function

Domain	Codomain
$x \in \mathbb{R}$	$\pi(x) \in \mathbb{Z}_{\ge 0}$
$x \in \left\{\infty\right\}$	$\pi(x) \in \left\{\infty\right\}$

Table data:

\left(P, Q\right)

such that

\left(P\right) \;\implies\; \left(Q\right)

Definitions:

Fungrim symbol	Notation	Short description
`PrimePi`	$\pi(x)$	Prime counting function
`RR`	$\mathbb{R}$	Real numbers
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n
`Infinity`	$\infty$	Positive infinity

Source code for this entry:

Entry(ID("6c22c8"),
    SymbolDefinition(PrimePi, PrimePi(x), "Prime counting function"),
    Table(TableRelation(Tuple(P, Q), Implies(P, Q)), TableHeadings(Description("Domain"), Description("Codomain")), List(Tuple(Element(x, RR), Element(PrimePi(x), ZZGreaterEqual(0))), Tuple(Element(x, Set(Infinity)), Element(PrimePi(x), Set(Infinity))))))

c03de4

Symbol: RiemannHypothesis —

\operatorname{RH}

— Riemann hypothesis

Represents the truth value of the Riemann hypothesis, defined in 49704a.

Semantically,

\operatorname{RH} \in \left\{\operatorname{True}, \operatorname{False}\right\}

.

This symbol can be used in an assumption to express that a formula is valid conditionally on the truth of the Riemann hypothesis.

Definitions:

Fungrim symbol	Notation	Short description
`RiemannHypothesis`	$\operatorname{RH}$	Riemann hypothesis

Source code for this entry:

Entry(ID("c03de4"),
    SymbolDefinition(RiemannHypothesis, RiemannHypothesis, "Riemann hypothesis"),
    Description("Represents the truth value of the Riemann hypothesis, defined in ", EntryReference("49704a"), "."),
    Description("Semantically, ", Element(RiemannHypothesis, Set(True_, False_)), "."),
    Description("This symbol can be used in an assumption to express that a formula is valid conditionally on the truth of the Riemann hypothesis."))

3fc797

\mathbb{P} = \left\{ p_{n} : n \in \mathbb{Z}_{\ge 1} \right\}

TeX:

\mathbb{P} = \left\{ p_{n} : n \in \mathbb{Z}_{\ge 1} \right\}

Definitions:

Fungrim symbol	Notation	Short description
`PP`	$\mathbb{P}$	Prime numbers
`PrimeNumber`	$p_{n}$	nth prime number
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n

Source code for this entry:

Entry(ID("3fc797"),
    Formula(Equal(PP, Set(PrimeNumber(n), ForElement(n, ZZGreaterEqual(1))))))

04427b

\pi(x) = \# \left\{ p : p \in \mathbb{P} \,\mathbin{\operatorname{and}}\, p \le x \right\}

Assumptions:

x \in \mathbb{R}

TeX:

\pi(x) = \# \left\{ p : p \in \mathbb{P} \,\mathbin{\operatorname{and}}\, p \le x \right\}

x \in \mathbb{R}

Definitions:

Fungrim symbol	Notation	Short description
`PrimePi`	$\pi(x)$	Prime counting function
`Cardinality`	$\# S$	Set cardinality
`PP`	$\mathbb{P}$	Prime numbers
`RR`	$\mathbb{R}$	Real numbers

Source code for this entry:

Entry(ID("04427b"),
    Formula(Equal(PrimePi(x), Cardinality(Set(p, ForElement(p, PP), LessEqual(p, x))))),
    Variables(x),
    Assumptions(Element(x, RR)))

9d0839

p_{n} = \text{A000040}\!\left(n\right)

Assumptions:

n \in \mathbb{Z}_{\ge 1}

References:

Sequence A000040 in Sloane's On-Line Encyclopedia of Integer Sequences (OEIS)

TeX:

p_{n} = \text{A000040}\!\left(n\right)

n \in \mathbb{Z}_{\ge 1}

Definitions:

Fungrim symbol	Notation	Short description
`PrimeNumber`	$p_{n}$	nth prime number
`SloaneA`	$\text{A00000X}\!\left(n\right)$	Sequence X in Sloane's OEIS
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n

Source code for this entry:

Entry(ID("9d0839"),
    Formula(Equal(PrimeNumber(n), SloaneA("A000040", n))),
    Variables(n),
    Assumptions(Element(n, ZZGreaterEqual(1))))

4fa169

\pi(n) = \text{A000720}\!\left(n\right)

Assumptions:

n \in \mathbb{Z}_{\ge 0}

References:

Sequence A000720 in Sloane's On-Line Encyclopedia of Integer Sequences (OEIS)

TeX:

\pi(n) = \text{A000720}\!\left(n\right)

n \in \mathbb{Z}_{\ge 0}

Definitions:

Fungrim symbol	Notation	Short description
`PrimePi`	$\pi(x)$	Prime counting function
`SloaneA`	$\text{A00000X}\!\left(n\right)$	Sequence X in Sloane's OEIS
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n

Source code for this entry:

Entry(ID("4fa169"),
    Formula(Equal(PrimePi(n), SloaneA("A000720", n))),
    Variables(n),
    Assumptions(Element(n, ZZGreaterEqual(0))))

a3035f

Table of

p_{n}

for

1 \le n \le 200

$n$	$p_{n}$
1	2
2	3
3	5
4	7
5	11
6	13
7	17
8	19
9	23
10	29
11	31
12	37
13	41
14	43
15	47
16	53
17	59
18	61
19	67
20	71
21	73
22	79
23	83
24	89
25	97
26	101
27	103
28	107
29	109
30	113
31	127
32	131
33	137
34	139
35	149
36	151
37	157
38	163
39	167
40	173
41	179
42	181
43	191
44	193
45	197
46	199
47	211
48	223
49	227
50	229

$n$	$p_{n}$
51	233
52	239
53	241
54	251
55	257
56	263
57	269
58	271
59	277
60	281
61	283
62	293
63	307
64	311
65	313
66	317
67	331
68	337
69	347
70	349
71	353
72	359
73	367
74	373
75	379
76	383
77	389
78	397
79	401
80	409
81	419
82	421
83	431
84	433
85	439
86	443
87	449
88	457
89	461
90	463
91	467
92	479
93	487
94	491
95	499
96	503
97	509
98	521
99	523
100	541

$n$	$p_{n}$
101	547
102	557
103	563
104	569
105	571
106	577
107	587
108	593
109	599
110	601
111	607
112	613
113	617
114	619
115	631
116	641
117	643
118	647
119	653
120	659
121	661
122	673
123	677
124	683
125	691
126	701
127	709
128	719
129	727
130	733
131	739
132	743
133	751
134	757
135	761
136	769
137	773
138	787
139	797
140	809
141	811
142	821
143	823
144	827
145	829
146	839
147	853
148	857
149	859
150	863

$n$	$p_{n}$
151	877
152	881
153	883
154	887
155	907
156	911
157	919
158	929
159	937
160	941
161	947
162	953
163	967
164	971
165	977
166	983
167	991
168	997
169	1009
170	1013
171	1019
172	1021
173	1031
174	1033
175	1039
176	1049
177	1051
178	1061
179	1063
180	1069
181	1087
182	1091
183	1093
184	1097
185	1103
186	1109
187	1117
188	1123
189	1129
190	1151
191	1153
192	1163
193	1171
194	1181
195	1187
196	1193
197	1201
198	1213
199	1217
200	1223

Definitions:

Fungrim symbol	Notation	Short description
`PrimeNumber`	$p_{n}$	nth prime number

Source code for this entry:

Entry(ID("a3035f"),
    Description("Table of", PrimeNumber(n), "for", LessEqual(1, n, 200)),
    Table(Var(n), TableValueHeadings(n, PrimeNumber(n)), TableSplit(4), List(Tuple(1, 2), Tuple(2, 3), Tuple(3, 5), Tuple(4, 7), Tuple(5, 11), Tuple(6, 13), Tuple(7, 17), Tuple(8, 19), Tuple(9, 23), Tuple(10, 29), Tuple(11, 31), Tuple(12, 37), Tuple(13, 41), Tuple(14, 43), Tuple(15, 47), Tuple(16, 53), Tuple(17, 59), Tuple(18, 61), Tuple(19, 67), Tuple(20, 71), Tuple(21, 73), Tuple(22, 79), Tuple(23, 83), Tuple(24, 89), Tuple(25, 97), Tuple(26, 101), Tuple(27, 103), Tuple(28, 107), Tuple(29, 109), Tuple(30, 113), Tuple(31, 127), Tuple(32, 131), Tuple(33, 137), Tuple(34, 139), Tuple(35, 149), Tuple(36, 151), Tuple(37, 157), Tuple(38, 163), Tuple(39, 167), Tuple(40, 173), Tuple(41, 179), Tuple(42, 181), Tuple(43, 191), Tuple(44, 193), Tuple(45, 197), Tuple(46, 199), Tuple(47, 211), Tuple(48, 223), Tuple(49, 227), Tuple(50, 229), Tuple(51, 233), Tuple(52, 239), Tuple(53, 241), Tuple(54, 251), Tuple(55, 257), Tuple(56, 263), Tuple(57, 269), Tuple(58, 271), Tuple(59, 277), Tuple(60, 281), Tuple(61, 283), Tuple(62, 293), Tuple(63, 307), Tuple(64, 311), Tuple(65, 313), Tuple(66, 317), Tuple(67, 331), Tuple(68, 337), Tuple(69, 347), Tuple(70, 349), Tuple(71, 353), Tuple(72, 359), Tuple(73, 367), Tuple(74, 373), Tuple(75, 379), Tuple(76, 383), Tuple(77, 389), Tuple(78, 397), Tuple(79, 401), Tuple(80, 409), Tuple(81, 419), Tuple(82, 421), Tuple(83, 431), Tuple(84, 433), Tuple(85, 439), Tuple(86, 443), Tuple(87, 449), Tuple(88, 457), Tuple(89, 461), Tuple(90, 463), Tuple(91, 467), Tuple(92, 479), Tuple(93, 487), Tuple(94, 491), Tuple(95, 499), Tuple(96, 503), Tuple(97, 509), Tuple(98, 521), Tuple(99, 523), Tuple(100, 541), Tuple(101, 547), Tuple(102, 557), Tuple(103, 563), Tuple(104, 569), Tuple(105, 571), Tuple(106, 577), Tuple(107, 587), Tuple(108, 593), Tuple(109, 599), Tuple(110, 601), Tuple(111, 607), Tuple(112, 613), Tuple(113, 617), Tuple(114, 619), Tuple(115, 631), Tuple(116, 641), Tuple(117, 643), Tuple(118, 647), Tuple(119, 653), Tuple(120, 659), Tuple(121, 661), Tuple(122, 673), Tuple(123, 677), Tuple(124, 683), Tuple(125, 691), Tuple(126, 701), Tuple(127, 709), Tuple(128, 719), Tuple(129, 727), Tuple(130, 733), Tuple(131, 739), Tuple(132, 743), Tuple(133, 751), Tuple(134, 757), Tuple(135, 761), Tuple(136, 769), Tuple(137, 773), Tuple(138, 787), Tuple(139, 797), Tuple(140, 809), Tuple(141, 811), Tuple(142, 821), Tuple(143, 823), Tuple(144, 827), Tuple(145, 829), Tuple(146, 839), Tuple(147, 853), Tuple(148, 857), Tuple(149, 859), Tuple(150, 863), Tuple(151, 877), Tuple(152, 881), Tuple(153, 883), Tuple(154, 887), Tuple(155, 907), Tuple(156, 911), Tuple(157, 919), Tuple(158, 929), Tuple(159, 937), Tuple(160, 941), Tuple(161, 947), Tuple(162, 953), Tuple(163, 967), Tuple(164, 971), Tuple(165, 977), Tuple(166, 983), Tuple(167, 991), Tuple(168, 997), Tuple(169, 1009), Tuple(170, 1013), Tuple(171, 1019), Tuple(172, 1021), Tuple(173, 1031), Tuple(174, 1033), Tuple(175, 1039), Tuple(176, 1049), Tuple(177, 1051), Tuple(178, 1061), Tuple(179, 1063), Tuple(180, 1069), Tuple(181, 1087), Tuple(182, 1091), Tuple(183, 1093), Tuple(184, 1097), Tuple(185, 1103), Tuple(186, 1109), Tuple(187, 1117), Tuple(188, 1123), Tuple(189, 1129), Tuple(190, 1151), Tuple(191, 1153), Tuple(192, 1163), Tuple(193, 1171), Tuple(194, 1181), Tuple(195, 1187), Tuple(196, 1193), Tuple(197, 1201), Tuple(198, 1213), Tuple(199, 1217), Tuple(200, 1223))))

1e142c

Table of

p_{{10}^{n}}

for

0 \le n \le 24

$n$	$p_{{10}^{n}}$
0	2
1	29
2	541
3	7919
4	104729
5	1299709
6	15485863
7	179424673
8	2038074743
9	22801763489
10	252097800623
11	2760727302517

$n$	$p_{{10}^{n}}$
12	29996224275833
13	323780508946331
14	3475385758524527
15	37124508045065437
16	394906913903735329
17	4185296581467695669
18	44211790234832169331
19	465675465116607065549
20	4892055594575155744537
21	51271091498016403471853
22	536193870744162118627429
23	5596564467986980643073683
24	58310039994836584070534263

Definitions:

Fungrim symbol	Notation	Short description
`PrimeNumber`	$p_{n}$	nth prime number
`Pow`	${a}^{b}$	Power

Source code for this entry:

Entry(ID("1e142c"),
    Description("Table of", PrimeNumber(Pow(10, n)), "for", LessEqual(0, n, 24)),
    Table(Var(n), TableValueHeadings(n, PrimeNumber(Pow(10, n))), TableSplit(2), List(Tuple(0, 2), Tuple(1, 29), Tuple(2, 541), Tuple(3, 7919), Tuple(4, 104729), Tuple(5, 1299709), Tuple(6, 15485863), Tuple(7, 179424673), Tuple(8, 2038074743), Tuple(9, 22801763489), Tuple(10, 252097800623), Tuple(11, 2760727302517), Tuple(12, 29996224275833), Tuple(13, 323780508946331), Tuple(14, 3475385758524527), Tuple(15, 37124508045065437), Tuple(16, 394906913903735329), Tuple(17, 4185296581467695669), Tuple(18, 44211790234832169331), Tuple(19, 465675465116607065549), Tuple(20, 4892055594575155744537), Tuple(21, 51271091498016403471853), Tuple(22, 536193870744162118627429), Tuple(23, 5596564467986980643073683), Tuple(24, 58310039994836584070534263))))

5404ce

Table of

\pi\!\left({10}^{n}\right)

for

0 \le n \le 27

$n$	$\pi\!\left({10}^{n}\right)$
0	0
1	4
2	25
3	168
4	1229
5	9592
6	78498
7	664579
8	5761455
9	50847534
10	455052511
11	4118054813
12	37607912018
13	346065536839

$n$	$\pi\!\left({10}^{n}\right)$
14	3204941750802
15	29844570422669
16	279238341033925
17	2623557157654233
18	24739954287740860
19	234057667276344607
20	2220819602560918840
21	21127269486018731928
22	201467286689315906290
23	1925320391606803968923
24	18435599767349200867866
25	176846309399143769411680
26	1699246750872437141327603
27	16352460426841680446427399

Definitions:

Fungrim symbol	Notation	Short description
`PrimePi`	$\pi(x)$	Prime counting function
`Pow`	${a}^{b}$	Power

Source code for this entry:

Entry(ID("5404ce"),
    Description("Table of", PrimePi(Pow(10, n)), "for", LessEqual(0, n, 27)),
    Table(Var(n), TableValueHeadings(n, PrimePi(Pow(10, n))), TableSplit(2), List(Tuple(0, 0), Tuple(1, 4), Tuple(2, 25), Tuple(3, 168), Tuple(4, 1229), Tuple(5, 9592), Tuple(6, 78498), Tuple(7, 664579), Tuple(8, 5761455), Tuple(9, 50847534), Tuple(10, 455052511), Tuple(11, 4118054813), Tuple(12, 37607912018), Tuple(13, 346065536839), Tuple(14, 3204941750802), Tuple(15, 29844570422669), Tuple(16, 279238341033925), Tuple(17, 2623557157654233), Tuple(18, 24739954287740860), Tuple(19, 234057667276344607), Tuple(20, 2220819602560918840), Tuple(21, 21127269486018731928), Tuple(22, 201467286689315906290), Tuple(23, 1925320391606803968923), Tuple(24, 18435599767349200867866), Tuple(25, 176846309399143769411680), Tuple(26, 1699246750872437141327603), Tuple(27, 16352460426841680446427399))))

d1ec2d

p_{n + 1} < 2 p_{n}

Assumptions:

n \in \mathbb{Z}_{\ge 1}

TeX:

p_{n + 1} < 2 p_{n}

n \in \mathbb{Z}_{\ge 1}

Definitions:

Fungrim symbol	Notation	Short description
`PrimeNumber`	$p_{n}$	nth prime number
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n

Source code for this entry:

Entry(ID("d1ec2d"),
    Formula(Less(PrimeNumber(Add(n, 1)), Mul(2, PrimeNumber(n)))),
    Variables(n),
    Assumptions(Element(n, ZZGreaterEqual(1))))

69fd4b

\pi\!\left(2 x\right) - \pi(x) \ge 1

Assumptions:

x \in \mathbb{R} \;\mathbin{\operatorname{and}}\; x \ge 1

TeX:

\pi\!\left(2 x\right) - \pi(x) \ge 1

x \in \mathbb{R} \;\mathbin{\operatorname{and}}\; x \ge 1

Definitions:

Fungrim symbol	Notation	Short description
`PrimePi`	$\pi(x)$	Prime counting function
`RR`	$\mathbb{R}$	Real numbers

Source code for this entry:

Entry(ID("69fd4b"),
    Formula(GreaterEqual(Sub(PrimePi(Mul(2, x)), PrimePi(x)), 1)),
    Variables(x),
    Assumptions(And(Element(x, RR), GreaterEqual(x, 1))))

6f3cf7

p_{n} < n \log\!\left(n \log(n)\right)

Assumptions:

n \in \mathbb{Z}_{\ge 6}

TeX:

p_{n} < n \log\!\left(n \log(n)\right)

n \in \mathbb{Z}_{\ge 6}

Definitions:

Fungrim symbol	Notation	Short description
`PrimeNumber`	$p_{n}$	nth prime number
`Log`	$\log(z)$	Natural logarithm
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n

Source code for this entry:

Entry(ID("6f3cf7"),
    Formula(Less(PrimeNumber(n), Mul(n, Log(Mul(n, Log(n)))))),
    Variables(n),
    Assumptions(Element(n, ZZGreaterEqual(6))))

8c52de

p_{n} > n \left(\log\!\left(n \log(n)\right) - 1\right)

Assumptions:

n \in \mathbb{Z}_{\ge 2}

TeX:

p_{n} > n \left(\log\!\left(n \log(n)\right) - 1\right)

n \in \mathbb{Z}_{\ge 2}

Definitions:

Fungrim symbol	Notation	Short description
`PrimeNumber`	$p_{n}$	nth prime number
`Log`	$\log(z)$	Natural logarithm
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n

Source code for this entry:

Entry(ID("8c52de"),
    Formula(Greater(PrimeNumber(n), Mul(n, Sub(Log(Mul(n, Log(n))), 1)))),
    Variables(n),
    Assumptions(Element(n, ZZGreaterEqual(2))))

bfa464

p_{n} < n \left(\log(n) + \log\!\left(\log(n)\right) - 1 + \frac{\log\!\left(\log(n)\right) - 2}{\log(n)} - \frac{\log^{2}\!\left(\log(n)\right) - 6 \log\!\left(\log(n)\right) + 10.667}{2 \log^{2}\!\left(n\right)}\right)

Assumptions:

n \in \mathbb{Z}_{\ge 46254381}

References:

https://arxiv.org/abs/1706.03651

TeX:

p_{n} < n \left(\log(n) + \log\!\left(\log(n)\right) - 1 + \frac{\log\!\left(\log(n)\right) - 2}{\log(n)} - \frac{\log^{2}\!\left(\log(n)\right) - 6 \log\!\left(\log(n)\right) + 10.667}{2 \log^{2}\!\left(n\right)}\right)

n \in \mathbb{Z}_{\ge 46254381}

Definitions:

Fungrim symbol	Notation	Short description
`PrimeNumber`	$p_{n}$	nth prime number
`Log`	$\log(z)$	Natural logarithm
`Pow`	${a}^{b}$	Power
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n

Source code for this entry:

Entry(ID("bfa464"),
    Formula(Less(PrimeNumber(n), Mul(n, Sub(Add(Sub(Add(Log(n), Log(Log(n))), 1), Div(Sub(Log(Log(n)), 2), Log(n))), Div(Add(Sub(Pow(Log(Log(n)), 2), Mul(6, Log(Log(n)))), Decimal("10.667")), Mul(2, Pow(Log(n), 2))))))),
    Variables(n),
    Assumptions(Element(n, ZZGreaterEqual(46254381))),
    References("https://arxiv.org/abs/1706.03651"))

1e3388

p_{n} > n \left(\log(n) + \log\!\left(\log(n)\right) - 1 + \frac{\log\!\left(\log(n)\right) - 2}{\log(n)} - \frac{\log^{2}\!\left(\log(n)\right) - 6 \log\!\left(\log(n)\right) + 11.508}{2 \log^{2}\!\left(n\right)}\right)

Assumptions:

n \in \mathbb{Z}_{\ge 2}

References:

https://arxiv.org/abs/1706.03651

TeX:

p_{n} > n \left(\log(n) + \log\!\left(\log(n)\right) - 1 + \frac{\log\!\left(\log(n)\right) - 2}{\log(n)} - \frac{\log^{2}\!\left(\log(n)\right) - 6 \log\!\left(\log(n)\right) + 11.508}{2 \log^{2}\!\left(n\right)}\right)

n \in \mathbb{Z}_{\ge 2}

Definitions:

Fungrim symbol	Notation	Short description
`PrimeNumber`	$p_{n}$	nth prime number
`Log`	$\log(z)$	Natural logarithm
`Pow`	${a}^{b}$	Power
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n

Source code for this entry:

Entry(ID("1e3388"),
    Formula(Greater(PrimeNumber(n), Mul(n, Sub(Add(Sub(Add(Log(n), Log(Log(n))), 1), Div(Sub(Log(Log(n)), 2), Log(n))), Div(Add(Sub(Pow(Log(Log(n)), 2), Mul(6, Log(Log(n)))), Decimal("11.508")), Mul(2, Pow(Log(n), 2))))))),
    Variables(n),
    Assumptions(Element(n, ZZGreaterEqual(2))),
    References("https://arxiv.org/abs/1706.03651"))

5258c0

\pi(x) < \frac{1.25506 x}{\log(x)}

Assumptions:

x \in \mathbb{R} \;\mathbin{\operatorname{and}}\; x > 1

TeX:

\pi(x) < \frac{1.25506 x}{\log(x)}

x \in \mathbb{R} \;\mathbin{\operatorname{and}}\; x > 1

Definitions:

Fungrim symbol	Notation	Short description
`PrimePi`	$\pi(x)$	Prime counting function
`Log`	$\log(z)$	Natural logarithm
`RR`	$\mathbb{R}$	Real numbers

Source code for this entry:

Entry(ID("5258c0"),
    Formula(Less(PrimePi(x), Div(Mul(Decimal("1.25506"), x), Log(x)))),
    Variables(x),
    Assumptions(And(Element(x, RR), Greater(x, 1))))

375afe

\left|\pi(x) - \operatorname{li}(x)\right| < \frac{\sqrt{x} \log(x)}{8 \pi}

Assumptions:

x \in \mathbb{R} \;\mathbin{\operatorname{and}}\; x \ge 2657 \;\mathbin{\operatorname{and}}\; \operatorname{RH}

References:

L. Schoenfeld (1976). Sharper bounds for the Chebyshev functions θ(x) and ψ(x). II. Mathematics of Computation. 30 (134): 337-360. DOI: 10.2307/2005976

TeX:

\left|\pi(x) - \operatorname{li}(x)\right| < \frac{\sqrt{x} \log(x)}{8 \pi}

x \in \mathbb{R} \;\mathbin{\operatorname{and}}\; x \ge 2657 \;\mathbin{\operatorname{and}}\; \operatorname{RH}

Definitions:

Fungrim symbol	Notation	Short description
`Abs`	$\left\|z\right\|$	Absolute value
`PrimePi`	$\pi(x)$	Prime counting function
`LogIntegral`	$\operatorname{li}(z)$	Logarithmic integral
`Sqrt`	$\sqrt{z}$	Principal square root
`Log`	$\log(z)$	Natural logarithm
`Pi`	$\pi$	The constant pi (3.14...)
`RR`	$\mathbb{R}$	Real numbers
`RiemannHypothesis`	$\operatorname{RH}$	Riemann hypothesis

Source code for this entry:

Entry(ID("375afe"),
    Formula(Less(Abs(Sub(PrimePi(x), LogIntegral(x))), Div(Mul(Sqrt(x), Log(x)), Mul(8, Pi)))),
    Variables(x),
    Assumptions(And(Element(x, RR), GreaterEqual(x, 2657), RiemannHypothesis)),
    References("L. Schoenfeld (1976). Sharper bounds for the Chebyshev functions θ(x) and ψ(x). II. Mathematics of Computation. 30 (134): 337-360. DOI: 10.2307/2005976"))

d898b9

\pi(x) > \frac{x}{\log(x)}

Assumptions:

x \in \mathbb{R} \;\mathbin{\operatorname{and}}\; x \ge 17

TeX:

\pi(x) > \frac{x}{\log(x)}

x \in \mathbb{R} \;\mathbin{\operatorname{and}}\; x \ge 17

Definitions:

Fungrim symbol	Notation	Short description
`PrimePi`	$\pi(x)$	Prime counting function
`Log`	$\log(z)$	Natural logarithm
`RR`	$\mathbb{R}$	Real numbers

Source code for this entry:

Entry(ID("d898b9"),
    Formula(Greater(PrimePi(x), Div(x, Log(x)))),
    Variables(x),
    Assumptions(And(Element(x, RR), GreaterEqual(x, 17))))

Definitions

Connection formulas

Tables

Bounds and inequalities

Bertrand's postulate

Bounds for prime numbers

Bounds for the prime counting function