Definition df-fppr 49096

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 49095	. 2 class FPPr
2		vn	. . 3 setvar 𝑛
3		cn 12375	. . 3 class ℕ
4		vx	. . . . . . 7 setvar 𝑥
5	4	cv 1569	. . . . . 6 class 𝑥
6		cprime 16890	. . . . . 6 class ℙ
7	5, 6	wnel 3065	. . . . 5 wff 𝑥 ∉ ℙ
8	2	cv 1569	. . . . . . . 8 class 𝑛
9		c1 11240	. . . . . . . . 9 class 1
10		cmin 11580	. . . . . . . . 9 class −
11	5, 9, 10	co 7451	. . . . . . . 8 class (𝑥 − 1)
12		cexp 14244	. . . . . . . 8 class ↑
13	8, 11, 12	co 7451	. . . . . . 7 class (𝑛↑(𝑥 − 1))
14	13, 9, 10	co 7451	. . . . . 6 class ((𝑛↑(𝑥 − 1)) − 1)
15		cdvds 16466	. . . . . 6 class ∥
16	5, 14, 15	wbr 5108	. . . . 5 wff 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1)
17	7, 16	wa 401	. . . 4 wff (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))
18		c4 12439	. . . . 5 class 4
19		cuz 13005	. . . . 5 class ℤ≥
20	18, 19	cfv 6566	. . . 4 class (ℤ≥‘4)
21	17, 4, 20	crab 3416	. . 3 class {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))}
22	2, 3, 21	cmpt 5192	. 2 class (𝑛 ∈ ℕ ↦ {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))})
23	1, 22	wceq 1570	1 wff FPPr = (𝑛 ∈ ℕ ↦ {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))})

This definition is used by:  fppr  49097  fpprbasnn  49100