Definition df-fppr 48082

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 48081	. 2 class FPPr
2		vn	. . 3 setvar 𝑛
3		cn 12157	. . 3 class ℕ
4		vx	. . . . . . 7 setvar 𝑥
5	4	cv 1541	. . . . . 6 class 𝑥
6		cprime 16610	. . . . . 6 class ℙ
7	5, 6	wnel 3037	. . . . 5 wff 𝑥 ∉ ℙ
8	2	cv 1541	. . . . . . . 8 class 𝑛
9		c1 11039	. . . . . . . . 9 class 1
10		cmin 11376	. . . . . . . . 9 class −
11	5, 9, 10	co 7368	. . . . . . . 8 class (𝑥 − 1)
12		cexp 13996	. . . . . . . 8 class ↑
13	8, 11, 12	co 7368	. . . . . . 7 class (𝑛↑(𝑥 − 1))
14	13, 9, 10	co 7368	. . . . . 6 class ((𝑛↑(𝑥 − 1)) − 1)
15		cdvds 16191	. . . . . 6 class ∥
16	5, 14, 15	wbr 5100	. . . . 5 wff 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1)
17	7, 16	wa 395	. . . 4 wff (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))
18		c4 12214	. . . . 5 class 4
19		cuz 12763	. . . . 5 class ℤ≥
20	18, 19	cfv 6500	. . . 4 class (ℤ≥‘4)
21	17, 4, 20	crab 3401	. . 3 class {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))}
22	2, 3, 21	cmpt 5181	. 2 class (𝑛 ∈ ℕ ↦ {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))})
23	1, 22	wceq 1542	1 wff FPPr = (𝑛 ∈ ℕ ↦ {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))})

This definition is referenced by:  fppr  48083  fpprbasnn  48086