Definition df-fppr 48523

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 48522	. 2 class FPPr
2		vn	. . 3 setvar 𝑛
3		cn 12244	. . 3 class ℕ
4		vx	. . . . . . 7 setvar 𝑥
5	4	cv 1569	. . . . . 6 class 𝑥
6		cprime 16747	. . . . . 6 class ℙ
7	5, 6	wnel 3066	. . . . 5 wff 𝑥 ∉ ℙ
8	2	cv 1569	. . . . . . . 8 class 𝑛
9		c1 11112	. . . . . . . . 9 class 1
10		cmin 11452	. . . . . . . . 9 class −
11	5, 9, 10	co 7416	. . . . . . . 8 class (𝑥 − 1)
12		cexp 14111	. . . . . . . 8 class ↑
13	8, 11, 12	co 7416	. . . . . . 7 class (𝑛↑(𝑥 − 1))
14	13, 9, 10	co 7416	. . . . . 6 class ((𝑛↑(𝑥 − 1)) − 1)
15		cdvds 16328	. . . . . 6 class ∥
16	5, 14, 15	wbr 5111	. . . . 5 wff 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1)
17	7, 16	wa 401	. . . 4 wff (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))
18		c4 12308	. . . . 5 class 4
19		cuz 12874	. . . . 5 class ℤ≥
20	18, 19	cfv 6540	. . . 4 class (ℤ≥‘4)
21	17, 4, 20	crab 3418	. . 3 class {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))}
22	2, 3, 21	cmpt 5194	. 2 class (𝑛 ∈ ℕ ↦ {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))})
23	1, 22	wceq 1570	1 wff FPPr = (𝑛 ∈ ℕ ↦ {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))})

This definition is used by:  fppr  48524  fpprbasnn  48527