Definition df-fppr 47650

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 47649	. 2 class FPPr
2		vn	. . 3 setvar 𝑛
3		cn 12264	. . 3 class ℕ
4		vx	. . . . . . 7 setvar 𝑥
5	4	cv 1536	. . . . . 6 class 𝑥
6		cprime 16705	. . . . . 6 class ℙ
7	5, 6	wnel 3044	. . . . 5 wff 𝑥 ∉ ℙ
8	2	cv 1536	. . . . . . . 8 class 𝑛
9		c1 11154	. . . . . . . . 9 class 1
10		cmin 11490	. . . . . . . . 9 class −
11	5, 9, 10	co 7431	. . . . . . . 8 class (𝑥 − 1)
12		cexp 14099	. . . . . . . 8 class ↑
13	8, 11, 12	co 7431	. . . . . . 7 class (𝑛↑(𝑥 − 1))
14	13, 9, 10	co 7431	. . . . . 6 class ((𝑛↑(𝑥 − 1)) − 1)
15		cdvds 16287	. . . . . 6 class ∥
16	5, 14, 15	wbr 5148	. . . . 5 wff 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1)
17	7, 16	wa 395	. . . 4 wff (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))
18		c4 12321	. . . . 5 class 4
19		cuz 12876	. . . . 5 class ℤ≥
20	18, 19	cfv 6563	. . . 4 class (ℤ≥‘4)
21	17, 4, 20	crab 3433	. . 3 class {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))}
22	2, 3, 21	cmpt 5231	. 2 class (𝑛 ∈ ℕ ↦ {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))})
23	1, 22	wceq 1537	1 wff FPPr = (𝑛 ∈ ℕ ↦ {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))})

This definition is referenced by:  fppr  47651  fpprbasnn  47654