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\!\left(x\right)

— Prime counting function

Domain	Codomain
$x \in \mathbb{R}$	$\pi\!\left(x\right) \in \mathbb{Z}_{\ge 0}$
$x \in \left\{\infty\right\}$	$\pi\!\left(x\right) \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\!\left(x\right)$	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{RiemannHypothesis}

— Riemann hypothesis

Used as a symbol in logical formulas, represents the assertion that the Riemann hypothesis is true.

Definitions:

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

Source code for this entry:

Entry(ID("c03de4"),
    SymbolDefinition(RiemannHypothesis, RiemannHypothesis, "Riemann hypothesis"),
    Description("Used as a symbol in logical formulas, represents the assertion that the Riemann hypothesis is true."))

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
`SetBuilder`	$\left\{ f\!\left(x\right) : P\!\left(x\right) \right\}$	Set comprehension
`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, SetBuilder(PrimeNumber(n), n, Element(n, ZZGreaterEqual(1))))))

04427b

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

Assumptions:

x \in \mathbb{R}

TeX:

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

x \in \mathbb{R}

Definitions:

Fungrim symbol	Notation	Short description
`PrimePi`	$\pi\!\left(x\right)$	Prime counting function
`Cardinality`	$\left\|S\right\|$	Set cardinality
`SetBuilder`	$\left\{ f\!\left(x\right) : P\!\left(x\right) \right\}$	Set comprehension
`PP`	$\mathbb{P}$	Prime numbers
`RR`	$\mathbb{R}$	Real numbers

Source code for this entry:

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

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

Table data:

\left(n, y\right)

such that

p_{n} = y

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(TableRelation(Tuple(n, y), Equal(PrimeNumber(n), y)), TableHeadings(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))))

d1ec2d

p_{n + 1} \lt 2 p_{n}

Assumptions:

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

TeX:

p_{n + 1} \lt 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\!\left(x\right) \ge 1

Assumptions:

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

TeX:

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

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

Definitions:

Fungrim symbol	Notation	Short description
`PrimePi`	$\pi\!\left(x\right)$	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))))

8c52de

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

Assumptions:

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

TeX:

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

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

Definitions:

Fungrim symbol	Notation	Short description
`PrimeNumber`	$p_{n}$	nth prime number
`Log`	$\log\!\left(z\right)$	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))))

6f3cf7

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

Assumptions:

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

TeX:

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

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

Definitions:

Fungrim symbol	Notation	Short description
`PrimeNumber`	$p_{n}$	nth prime number
`Log`	$\log\!\left(z\right)$	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))))

d898b9

\pi\!\left(x\right) \gt \frac{x}{\log\!\left(x\right)}

Assumptions:

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

TeX:

\pi\!\left(x\right) \gt \frac{x}{\log\!\left(x\right)}

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

Definitions:

Fungrim symbol	Notation	Short description
`PrimePi`	$\pi\!\left(x\right)$	Prime counting function
`Log`	$\log\!\left(z\right)$	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))))

5258c0

\pi\!\left(x\right) \lt \frac{1.25506 x}{\log\!\left(x\right)}

Assumptions:

x \in \mathbb{R} \,\mathbin{\operatorname{and}}\, x \gt 1

TeX:

\pi\!\left(x\right) \lt \frac{1.25506 x}{\log\!\left(x\right)}

x \in \mathbb{R} \,\mathbin{\operatorname{and}}\, x \gt 1

Definitions:

Fungrim symbol	Notation	Short description
`PrimePi`	$\pi\!\left(x\right)$	Prime counting function
`Log`	$\log\!\left(z\right)$	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\!\left(x\right) - \operatorname{li}\!\left(x\right)\right| \lt \frac{\sqrt{x} \log\!\left(x\right)}{8 \pi}

Assumptions:

x \in \mathbb{R} \,\mathbin{\operatorname{and}}\, x \ge 2657 \,\mathbin{\operatorname{and}}\, \operatorname{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

TeX:

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

x \in \mathbb{R} \,\mathbin{\operatorname{and}}\, x \ge 2657 \,\mathbin{\operatorname{and}}\, \operatorname{RiemannHypothesis}

Definitions:

Fungrim symbol	Notation	Short description
`Abs`	$\left\|z\right\|$	Absolute value
`PrimePi`	$\pi\!\left(x\right)$	Prime counting function
`LogIntegral`	$\operatorname{li}\!\left(z\right)$	Logarithmic integral
`Sqrt`	$\sqrt{z}$	Principal square root
`Log`	$\log\!\left(z\right)$	Natural logarithm
`ConstPi`	$\pi$	The constant pi (3.14...)
`RR`	$\mathbb{R}$	Real numbers
`RiemannHypothesis`	$\operatorname{RiemannHypothesis}$	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, ConstPi)))),
    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"))

Basic formulas

Numerical values

Bounds and inequalities