Definition df-fppr 47971

Description: Define the function that maps a positive integer to the set of Fermat pseudoprimes to the base of this positive integer. Since Fermat pseudoprimes shall be composite (positive) integers, they must be nonprime integers greater than or equal to 4 (we cannot use 𝑥 ∈ ℕ ∧ 𝑥 ∉ ℙ because 𝑥 = 1 would fulfil this requirement, but should not be regarded as "composite" integer). (Contributed by AV, 29-May-2023.)

Assertion

Ref	Expression
df-fppr	⊢ FPPr = (𝑛 ∈ ℕ ↦ {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))})

Distinct variable group:   𝑥,𝑛

Detailed syntax breakdown of Definition df-fppr

Step	Hyp	Ref	Expression
1		cfppr 47970	. 2 class FPPr
2		vn	. . 3 setvar 𝑛
3		cn 12145	. . 3 class ℕ
4		vx	. . . . . . 7 setvar 𝑥
5	4	cv 1540	. . . . . 6 class 𝑥
6		cprime 16598	. . . . . 6 class ℙ
7	5, 6	wnel 3036	. . . . 5 wff 𝑥 ∉ ℙ
8	2	cv 1540	. . . . . . . 8 class 𝑛
9		c1 11027	. . . . . . . . 9 class 1
10		cmin 11364	. . . . . . . . 9 class −
11	5, 9, 10	co 7358	. . . . . . . 8 class (𝑥 − 1)
12		cexp 13984	. . . . . . . 8 class ↑
13	8, 11, 12	co 7358	. . . . . . 7 class (𝑛↑(𝑥 − 1))
14	13, 9, 10	co 7358	. . . . . 6 class ((𝑛↑(𝑥 − 1)) − 1)
15		cdvds 16179	. . . . . 6 class ∥
16	5, 14, 15	wbr 5098	. . . . 5 wff 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1)
17	7, 16	wa 395	. . . 4 wff (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))
18		c4 12202	. . . . 5 class 4
19		cuz 12751	. . . . 5 class ℤ≥
20	18, 19	cfv 6492	. . . 4 class (ℤ≥‘4)
21	17, 4, 20	crab 3399	. . 3 class {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))}
22	2, 3, 21	cmpt 5179	. 2 class (𝑛 ∈ ℕ ↦ {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))})
23	1, 22	wceq 1541	1 wff FPPr = (𝑛 ∈ ℕ ↦ {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))})

This definition is referenced by:  fppr  47972  fpprbasnn  47975