Definition df-fppr 46691

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 46690	. 2 class FPPr
2		vn	. . 3 setvar 𝑛
3		cn 12216	. . 3 class ℕ
4		vx	. . . . . . 7 setvar 𝑥
5	4	cv 1538	. . . . . 6 class 𝑥
6		cprime 16612	. . . . . 6 class ℙ
7	5, 6	wnel 3044	. . . . 5 wff 𝑥 ∉ ℙ
8	2	cv 1538	. . . . . . . 8 class 𝑛
9		c1 11113	. . . . . . . . 9 class 1
10		cmin 11448	. . . . . . . . 9 class −
11	5, 9, 10	co 7411	. . . . . . . 8 class (𝑥 − 1)
12		cexp 14031	. . . . . . . 8 class ↑
13	8, 11, 12	co 7411	. . . . . . 7 class (𝑛↑(𝑥 − 1))
14	13, 9, 10	co 7411	. . . . . 6 class ((𝑛↑(𝑥 − 1)) − 1)
15		cdvds 16201	. . . . . 6 class ∥
16	5, 14, 15	wbr 5147	. . . . 5 wff 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1)
17	7, 16	wa 394	. . . 4 wff (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))
18		c4 12273	. . . . 5 class 4
19		cuz 12826	. . . . 5 class ℤ≥
20	18, 19	cfv 6542	. . . 4 class (ℤ≥‘4)
21	17, 4, 20	crab 3430	. . 3 class {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))}
22	2, 3, 21	cmpt 5230	. 2 class (𝑛 ∈ ℕ ↦ {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))})
23	1, 22	wceq 1539	1 wff FPPr = (𝑛 ∈ ℕ ↦ {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))})

This definition is referenced by:  fppr  46692  fpprbasnn  46695