Definition df-fppr 48822

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 48821	. 2 class FPPr
2		vn	. . 3 setvar 𝑛
3		cn 12335	. . 3 class ℕ
4		vx	. . . . . . 7 setvar 𝑥
5	4	cv 1569	. . . . . 6 class 𝑥
6		cprime 16846	. . . . . 6 class ℙ
7	5, 6	wnel 3062	. . . . 5 wff 𝑥 ∉ ℙ
8	2	cv 1569	. . . . . . . 8 class 𝑛
9		c1 11201	. . . . . . . . 9 class 1
10		cmin 11541	. . . . . . . . 9 class −
11	5, 9, 10	co 7420	. . . . . . . 8 class (𝑥 − 1)
12		cexp 14204	. . . . . . . 8 class ↑
13	8, 11, 12	co 7420	. . . . . . 7 class (𝑛↑(𝑥 − 1))
14	13, 9, 10	co 7420	. . . . . 6 class ((𝑛↑(𝑥 − 1)) − 1)
15		cdvds 16422	. . . . . 6 class ∥
16	5, 14, 15	wbr 5103	. . . . 5 wff 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1)
17	7, 16	wa 401	. . . 4 wff (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))
18		c4 12399	. . . . 5 class 4
19		cuz 12965	. . . . 5 class ℤ≥
20	18, 19	cfv 6538	. . . 4 class (ℤ≥‘4)
21	17, 4, 20	crab 3413	. . 3 class {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))}
22	2, 3, 21	cmpt 5186	. 2 class (𝑛 ∈ ℕ ↦ {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))})
23	1, 22	wceq 1570	1 wff FPPr = (𝑛 ∈ ℕ ↦ {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))})

This definition is used by:  fppr  48823  fpprbasnn  48826